4 ms·
Ok, which of those programs can _only_ be implemented via aliasable pointers? I don't think anyone is arguing that C's loose memory model and rampant undefined
by abeyer 4y ago
Ok, which of those programs can _only_ be implemented via aliasable pointers?
I don't think anyone is arguing that C's loose memory model and rampant undefined behavior are amenable to verification. The point is that neither of those are necessary in many of the places they've been used.
- UncleMeat 4y agoPassing an object by reference to a function creates an alias. Storing a pointer as a field creates an alias. It would be very odd to have a program with zero aliasing relationships. Do do this you would need to never assign from a pointer type. This has nothing to do with C (mostly - you havoc more frequently when analyzing C if you want to be sound). Pointer Analysis papers usually target Java and in that space it is still stunningly difficult.