--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on May 2018 ---
Hi, Le 10/05/2018 à 18:49, Gilbert Pajela a écrit : > I just now noticed a difference in the consolidated property status reported by Frama-C since the > Phosphorus version that I don't understand. Let's say I use the following as an input program to > Frama-C: > > int x; > /*@ ensures x == 3; */ > { >  x = 3; >  /*@ loop invariant x >= 0; */ >  while (x > 0) { >    x --; >  } > } > > Note that the ensures clause is false. Back in the Silicon version of Frama-C, if I try to use WP to > prove the ensures clause, the consolidated status reported by Frama-C would say, "unknown (tried by > Wp.typed)", and the circle next to the ensures clause in the GUI would turn yellow. However, from > Phosphorus (the version after Silicon) to the current version, with the same program, Frama-C > instead reports, "VALID according to Unreachable Annotations", and the circle turns green instead of > yellow. Could you give us the full program? I'm not able to reproduce the problem in the gui, nor on the command line. Using this program (assigns could be omitted): ``` int x; /*@ ensures x == 3; assigns x; */ void f() { x = 3; /*@ loop invariant x >= 0; loop assigns x; */ while (x > 0) { x --; } } ``` And this command line `frama-c test_mai.c -wp -then -report` I have this output: ``` [kernel] Parsing test.c (with preprocessing) [wp] warning: Missing RTE guards [wp] 5 goals scheduled [wp] [Alt-Ergo] Goal typed_f_post : Unknown (Qed:4ms) (51ms) [wp] Proved goals: 4 / 5 Qed: 4 Alt-Ergo: 0 (unknown: 1) [report] Computing properties status... -------------------------------------------------------------------------------- --- Properties of Function 'f' -------------------------------------------------------------------------------- [ - ] Post-condition (file test.c, line 3) tried with Wp.typed. [ Valid ] Loop assigns (file test.c, line 9) by Wp.typed. [ Valid ] Assigns (file test.c, line 4) by Wp.typed. [ Valid ] Invariant (file test.c, line 8) by Wp.typed. [ - ] Default behavior tried with Frama-C kernel. -------------------------------------------------------------------------------- --- Status Report Summary -------------------------------------------------------------------------------- 3 Completely validated 2 To be validated 5 Total -------------------------------------------------------------------------------- ```