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