When running Frama-C value analysis with some benchmarks, e.g. susan
in http://www.eecs.umich.edu/mibench/automotive.tar.gz
, we noticed that a lot of blocks are considered dead code or unreachable. However, in practice, these code is executed as we printed out some debug information from these blocks. Is there anybody noticed this issue? How can we solve this?
Occurrences of dead code in the results of Frama-C's value analysis boil down to two aspects, and even these two aspects are only a question of human intentions and are indistinguishable from the point of view of the analyzer.
y = 0; x = 100 / y;
is unreachable because the program stops at the division everytime. Some bugs that should be run-time errors do not always stop execution, for instance, writing to an invalid address. Consider yourself lucky that they do in Frama-C's value analysis, not the other way round.Frama_C_interval()
, missing library functions for which neither specifications nor replacement code are provided, assembly code inside the C program, missing option -absolute-valid-range
when one would be appropriate, ...