4 ms·
Analyzing sign example doesn't work in C where signed integer overflow is undefined behavior. Example http://stackoverflow.com/questions/12729110/strange-integ
by d0mine 14y ago
Analyzing sign example doesn't work in C where signed integer overflow is undefined behavior.
Example http://stackoverflow.com/questions/12729110/strange-integer-behavior-with-gcc-o2 http://stackoverflow.com/questions/12729110/strange-integer-...
- mattmight 14y agoRight. It works for the register language with infinite precision integers. If you want it to work for C, you'll have to redefine the abstractions of addition and multiplication (and every other operation) appropriately. You'll also have to parameterize it by word size, endianness, signedness and type of arithmetic. That is, sound static analysis for C is almost certainly going to be platform-specific. But, you can still do it.
- wladimir 14y agoBut, you can still do it. Indeed. Arguably, compilers do it all the time to be able to (safely) do optimizations. Hence static analyzers are usually an extension to an compiler. Frama-C kind of being the exception, using CIL instead of the intermediate representation of a production compiler.