Why is code unreachable in Frama-C Value Analysis?

Question

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?

Answer 1

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.

1. Real bugs that occur with certainty everytime a particular statement is reached. For instance the code after 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.
2. Lack of configuration of the analysis context, including not having provided an informative main() function that sets up variation ranges of the program's inputs with such built-in functions as 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, ...

Answer 2

Your code has a peculiarity which is not in Pascal's list, and which explains some parts of the dead code. Quite a few functions are declared as such

 f(int x, int y);

The return type is entirely missing. The C standard indicates that such functions should return int, and Frama-C follows this convention. When parsing those function, it indicates that they never return anything on some of their paths

Body of function f falls-through. Adding a return statement.

On top on the return statement, Frama-C also adds an /*@ assert \false; annotation, to indicate that the execution paths of the functions that return nothing should be dead code. In your code, this annotation is always false: those functions are supposed to return void, and not int. You should correct your code with the good return type.