Frama-C-discuss mailing list archives

gpajela at GradCenter.cuny.edu (Gilbert Pajela) · Mon, 11 Jun 2018 20:36:39 +0000

Hello,

I apologize in advance for replying to an old post. Thanks for the suggestions, but unless I misunderstand something, I don't think I can actually use Conditions.iter from my own plugin to read the Mstate.state instances as suggested because the Mstate.state instances are inside Conditions.step, which is private. Also, I don't think I can make use of the pretty-printer Wp.Pcond.sequence either because it looks like it uses other data structures that are internal to Frama-C and not available to a plugin. Is there any way around these problems? I think it would be really useful to get the weakest precondition generated by the WP plugin in terms of the original variables of the input program and be able to use it from a plugin. Thanks.

Best,
Gilbert
________________________________

Date: Tue, 3 Apr 2018 10:07:56 +0200
From: LoÃ¯c Correnson <loic.correnson at cea.fr>
To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
Subject: Re: [Frama-c-discuss] Weakest precondition calculation
Message-ID: <E3145824-0C4D-431E-8C67-F4EE6AF16F4E at cea.fr>
Content-Type: text/plain; charset="utf-8"

Hi,

Two points. First, in the next release of Frama-C, aside of C/ACSL compilers Wp.CodeSemantics and Wp.LogicSemantics,
you *will* find a new complementary API `Wp.StmtSemantics` to generate proof obligations piece by piece, at the level of individual statements and instructions.
It is still experimental, but il shall be more flexible than the current one.
Second point is about renaming. Thus subject is complex because it is related to memory models. The long answer follows.

Yes there _is_ a renaming, but actually it can be much more complicated than a simple renaming.
For instance, if you have taken the address of `x`, its value is very likely to appear as something like `Mint_0[ Shift_sint32( Global(x) , 0 ) ]`â€¦

Indeed, there _is_ something like a reverse map from verification conditions to l-values.
It is located deep inside the `Conditions.sequent` type and is used inside the GUI to pretty-print expressions like the above ones into more readable ACSL l-values.

Useful entry points to go on into this direction :

module VC :
val get_sequent : t <file:///Users/correnson/Frama-C/trunk/doc/code/wp/VC.html#TYPEt> -> Conditions.sequent <file:///Users/correnson/Frama-C/trunk/doc/code/wp/Conditions.html#TYPEsequent>

module Conditions :
type sequent = sequence <file:///Users/correnson/Frama-C/trunk/doc/code/wp/Conditions.html#TYPEsequence> * Lang.F.pred <file:///Users/correnson/Frama-C/trunk/doc/code/wp/Lang.F.html#TYPEpred>

This `sequence` type is a structured collection of hypotheses and roughly corresponds to the LHS of the generated VCs.
As part of this sequence (see Conditions.iter) you will find instances of type Mstate.state, on opaque data structure that
memory models can read to reverse an expression into an l-value, and to interpret a state sequence into memory updates :

module Mstate :
type state
val lookup : state <file:///Users/correnson/Frama-C/trunk/doc/code/wp/Mstate.html#TYPEstate> -> Lang.F.term <file:///Users/correnson/Frama-C/trunk/doc/code/wp/Lang.F.html#TYPEterm> -> Memory.mval <file:///Users/correnson/Frama-C/trunk/doc/code/wp/Memory.html#TYPEmval>
val updates : state <file:///Users/correnson/Frama-C/trunk/doc/code/wp/Mstate.html#TYPEstate> Memory.sequence <file:///Users/correnson/Frama-C/trunk/doc/code/wp/Memory.html#TYPEsequence> -> Lang.F.Vars.t -> Memory.update <file:///Users/correnson/Frama-C/trunk/doc/code/wp/Memory.html#TYPEupdate> Bag.t <file:///Users/correnson/Frama-C/trunk/doc/code/html/Bag.html#TYPEt>

You may also have a look into the pretty-printer used inside the GUI : Wp.Pcond.sequence but the code is quite complex.

Hope this helpâ€¦
Regards,
        L.

> Le 1 avr. 2018 Ã  16:38, Gilbert Pajela <gpajela at GradCenter.cuny.edu> a Ã©crit :
>
> Hello,
>
> I am also trying to do something similar with the WP plugin. Specifically, I would like to use the WP plugin to generate the weakest precondition of a given statement S and postcondition Q. I have tried both Wp.VC.get_formulaand Wp.VC.generate_ip as suggested by LoÃ¯c, but I noticed that both functions return verification conditions that do not retain the original variable names that are in S. For example:
> int x, y;
> //@ ghost int u;
> //@ ensures x == u;
> {
>   if (x == y)
>     x = x + 1;
>   x = x * y;
> }
>
> With the above as the input program, here is what I get using Wp.VC.get_formula:
> forall i_0,i_1,i_2,i_3:int.
> let x_0 = (i_3*i_1) in
> (is_sint32 i_3) -> (is_sint32 i_2) -> (is_sint32 i_1) -> (is_sint32 i_0)
> -> (is_sint32 x_0) -> (if (i_3=i_2) then (i_1=(1+i_3)) else (i_2=i_1))
> -> (i_0=x_0)
>
> As you can see, variables have been renamed from x, y, and u, to x_0, i_0, i_1, i_2, and i_3. For my purposes, I'm trying to get the weakest precondition with the original variable names intact. Is there some way to get at the mapping between the variable names returned by Wp.VC.get_formula and the variable names in the input program? Thanks.
>
> Best,
> Gilbert
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180611/1ee23482/attachment.html>