# 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

*Subject*: [Frama-c-discuss] Frama C path sensitiveness*From*: boris at yakobowski.org (Boris Yakobowski)*Date*: Mon, 23 May 2011 11:26:56 +0200*In-reply-to*: <4DDA1BD4.7060905@nus.edu.sg>*References*: <4DD9CDDB.9080102@nus.edu.sg> <BANLkTimq429Nsy_c9LL6aiNr2w2OGyCqow@mail.gmail.com> <4DDA1BD4.7060905@nus.edu.sg>

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

**References**:**[Frama-c-discuss] Frama C path sensitiveness***From:*m.vijay at nus.edu.sg (Vijayaraghavan Murali)

**[Frama-c-discuss] Frama C path sensitiveness***From:*dmentre at linux-france.org (David MENTRE)

**[Frama-c-discuss] Frama C path sensitiveness***From:*m.vijay at nus.edu.sg (Vijayaraghavan Murali)

- Prev by Date:
**[Frama-c-discuss] Frama C path sensitiveness** - Next by Date:
**[Frama-c-discuss] coqc: The reference frame_between_sub was not found in the current environment** - Previous by thread:
**[Frama-c-discuss] Frama C path sensitiveness** - Next by thread:
**[Frama-c-discuss] Frama C path sensitiveness** - Index(es):