--- layout: fc_discuss_archives title: Message 74 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C: Detecting unreachable code?



Hi,

The following code has a useless if statement, which is always true, I was hoping to get some feedback on that issue, but all the behaviors are proved correct;


This code is a representative of a real error, which was manually detected during code review. I was trying to see whether WP can detect it...



[formal_verification]$ frama-c -wp -wp-rte always_true.c -lib-entry
[kernel] preprocessing with "gcc -C -E -I.  always_true.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_main_complete_Low_High : Valid
[wp] [Qed] Goal typed_main_disjoint_Low_High : Valid
[wp] [Qed] Goal typed_main_High_post : Valid (4ms)
[wp] [Qed] Goal typed_main_Low_post : Valid





int MAX_VALUE = 100;

float x = 0.0;

int status = 0;


/*@
   requires MAX_VALUE == 100;

   behavior High:
    assumes x > MAX_VALUE;
    ensures status == -1;

   behavior Low:
     assumes x <= MAX_VALUE;
     ensures status == -1;

   complete behaviors;
   disjoint behaviors;

*/
int main()
{

   if((x > MAX_VALUE) ||
      (x <= MAX_VALUE))
   {
      status = -1;
   }
}