--- layout: fc_discuss_archives title: Message 4 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



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