How to instruct WP not to analyze dead or unreachable code

Question

When running the command frama-c test.c -rte -eva -eva-slevel 1 then -wp on the following piece of code, I got the following results :

• Frama-c 24 : No errors
• Frama-c 25/26 : Overflows in the unreachable and dead test function

int test(int a, int b)
{
  return a+b;
}

int main(void)
{
  return 0
}

Since version 25, it looks like WP is trying to prove all annotations added by the RTE plugin, even in dead or unreachable code. I have not found any WP options to unselect unreachable properties.

Is there a way to tell WP not to select dead or unreachable properties ?

Answer 1

WP Goal Selection

The simple way from the command line is to use -wp-fct or -wp-skip-fct rather than just -wp. So in your example, run either of the following (I removed the -rte before -eva and put it with the WP call):

frama-c test.c -eva -eva-slevel 1 -then -wp-rte -wp -wp-fct main
frama-c test.c -eva -eva-slevel 1 -then -wp-rte -wp -wp-skip-fct test

Per the documentation:

• -wp generates proof obligations for all (selected) properties.
• -wp-fct <f1 ,...,fn > selects annotations of functions f1 ,...,fn (defaults to all functions).
• -wp-skip-fct <f1 ,...,fn > ignores functions f1 ,...,fn (defaults to none).