--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on May 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] VALID according to Unreachable Annotations



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
--------------------------------------------------------------------------------
```