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

Hello,

The bug seems related to the CFG built by WP plug-in in presence of 
statement contracts.
A correct CFG can be restored in adding at the end of the concerned 
block a labeled skip statement or a spare assertion:

void main(void)
{
   int x;
   /*@ ensures x == 3;
       assigns x; */
   {
     x = 3;
     /*@ loop invariant x >= 0;
         loop assigns x; */
     while (x > 0) {
       x --;
     }
     Hack: ; /* or @assert \true; */
   }
   return;
}


Notice that the computation of the CFG is being rewritten in order to 
solve some known problems as that one.
The integration of these developments is still in progress and could be 
part of the successor of Frama-C Chlorine.

Best regards,

-- 
Patrick Baudin,
CEA LIST.

Le 11/05/2018 à 20:34, Gilbert Pajela a écrit :
> 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
> --------------------------------------------------------------------------------
> ```
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss