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


  • Subject: [Frama-c-discuss] Weakest precondition calculation
  • From: gpajela at GradCenter.cuny.edu (Gilbert Pajela)
  • Date: Sun, 1 Apr 2018 14:38:32 +0000

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_formula and 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180401/a0efcf6f/attachment.html>