--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on May 2018 ---
Yes, here is the full program: void main(void) { int x; /*@ ensures x == 3; assigns x; */ { x = 3; /*@ loop invariant x >= 0; loop assigns x; */ while (x > 0) { x --; } } return; } Here I am using Chlorine beta. My command line is `/opt/frama-c-Chlorine-beta/bin/frama-c ~/c/wp/wp_loop_fc_clean.c -wp -then -report` Here is the output: [kernel] Parsing /data/loewenheim/a/gpajela/c/wp/wp_loop_fc_clean.c (with preprocessing) [wp] [CFG] Goal main_stmt_assign : Valid (Unreachable) [wp] [CFG] Goal main_stmt_post : Valid (Unreachable) [wp] Warning: Missing RTE guards [wp] 3 goals scheduled [wp] Proved goals: 3 / 3 Qed: 3 [report] Computing properties status... -------------------------------------------------------------------------------- --- Properties of Function 'main' -------------------------------------------------------------------------------- [ Valid ] Post-condition (file /data/loewenheim/a/gpajela/c/wp/wp_loop_fc_clean.c, line 3) at block by Unreachable Annotations. [ Valid ] Assigns (file /data/loewenheim/a/gpajela/c/wp/wp_loop_fc_clean.c, line 4) at block by Unreachable Annotations. [ Valid ] Loop assigns (file /data/loewenheim/a/gpajela/c/wp/wp_loop_fc_clean.c, line 8) by Wp.typed. [ Valid ] Invariant (file /data/loewenheim/a/gpajela/c/wp/wp_loop_fc_clean.c, line 7) by Wp.typed. [ Valid ] Default behavior at block by Frama-C kernel. -------------------------------------------------------------------------------- --- Status Report Summary -------------------------------------------------------------------------------- 5 Completely validated 5 Total -------------------------------------------------------------------------------- You can still see the "Unreachable Annotations" message above. Is it because my program is using a statement contract, while your program is using a function contract? If I use your program, I get the same results that you did. Prior to Phosphorus, it didn't matter whether it was a statement contract or a function contract. Thanks, Gilbert ---------------------------------------------------------------------- Date: Fri, 11 May 2018 11:04:37 +0200 From: François Bobot <francois.bobot at cea.fr> To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] VALID according to Unreachable        Annotations Message-ID: <38f3d947-fdfb-7e63-a864-7d367e049e8d at cea.fr> Content-Type: text/plain; charset=windows-1252; format=flowed 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 -------------------------------------------------------------------------------- ```