--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on May 2011 ---
Hi, On Mon, May 23, 2011 at 10:33 AM, Vijayaraghavan Murali <m.vijay at nus.edu.sg> wrote: > Even here a = 5 is dead code since t2 implies t1, but the value analysis > plugin is not able to catch it. Can you explain how this happens? As Pascal and David mentioned, proving that the second branches of your examples are dead is not obvious, especially in the second case. To do so in an abstract interpretation-based framework requires relational analyses such as octogons. Those may be very precise, but are also quite costly to perform. Now, here is where the 'framework' part of Frama-C comes in handy. If you really need the extra precision provided by the fact that the branches are dead, you can simply add an annotation //@ assert \false. The Value Analysis plugin will still not be able to prove it, but it will listen to the annotation, and stop evaluating the branch. Then, the WP plugin is able to prove that the annotation is true (in both examples). Calling the development version of Frama-C with "frama-c -val -wp -wp-rte ex.c" on the code below gives the following results: extern int n1, n2; main() { int a = 0, b,t1,t2; t1 = n1 > n2; t2 = n1 == n2+1; if(t1) { a = 4; } else if(t2) { /*@ assert \false; */ a = 5; } b = a+1; return b; } value] ====== VALUES COMPUTED ====== [value] Values for function main: a ? {0; 4} b ? {1; 5} t1 ? {0; 1} t2 ? {0; 1} [rte] annotating function main [wp] [Alt-Ergo] Goal store_main_assert_3_rte : Valid [wp] [Alt-Ergo] Goal store_main_assert_2_rte : Unknown [wp] [Alt-Ergo] Goal store_main_assert_1 : Valid Hence, the possible values for a and b are those you wanted, and our added assertion \assert \false is true (assert_1 : Valid). As a bonus, you get a warning on a possible int overflow on 'n2+1'. -- Boris