Overall question

How can a separation logic be put to work improving static verification via trance abstraction refinement?


Ultimately, the aim is to find unsafe memory operations in c-code.  Our mechanism for doing this with Skink is to first compile via Clang to LLVM IR and to then look for problems there.  One hitch that immediately comes up is the Clang may remove any undefined behaviour in the compilation process.  It is an allowed privilege of any c compiler to do whatever it likes with undefined operations.  Of course, invalid memory dereferences are not so simple to find, so in general they won't go away but we have seen instances already where they do.  Is there a configuration we can give to Clang that prevents it from ever doing this?  Our experiments have shown that turning off optimisations will do it, and we might expect that, but I would like a stronger assurance than that.


  • No labels