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


  • Subject: [Frama-c-discuss] VALID according to Unreachable Annotations
  • From: gpajela at GradCenter.cuny.edu (Gilbert Pajela)
  • Date: Fri, 11 May 2018 18:34:34 +0000
  • In-reply-to: <mailman.7.1526032808.10445.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.7.1526032808.10445.frama-c-discuss@lists.gforge.inria.fr>

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