Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama C path sensitiveness

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