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] Weakest precondition calculation

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/20180403/b7658b9e/attachment.html>