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] Queries regarding WP plugin

The standard way of using WP is for proving assertions, and more generally for proving Hoare triples.
Frama-C/WP is optimized for that purpose, hence if some Hoare triple is trivial, then, we expect no proof obligation to be generated.
However, if you want to obtain the weakest precondition of what *computes* a function, you can still use Frama-C/WP, but you must use a fake Hoare Triple that exhibit your needs.
Continuing on your trivial, example you can introduce a ? model ? logic function that encapsulate your need:

```
/*@ axiomatic WeakestPrecondition {
       predicate OBSERVE(integer a,integer b);
       }
*/

/*@ ensures OBSERVE( x , \result ) ; */
int f(int x)
{
 return x + 1;
}
```

Now using `frama-c -wp -wp-gen -wp-print`, you obtain the WP of f-return:
```
Let x_0 = f_0-1.
Assume { (* Domain *) Type: (is_sint32 f_0) /\ (is_sint32 x_0). }
Prove: (P_OBSERVE x_0 f_0).
```
which implicitly defines the relation OBSERVE, hence providing you with the WP of \result in terms of x.

L.




Le 16 d?c. 2014 ? 06:00, Debasmita Lohar <dlohar2009 at gmail.com> a ?crit :

> Hello,
> I have finally installed frama-c without any configuration error.
> But I want to get initial weakest precondition of a program(simple/complicated). I did not find anything like this in frama-c (As for small programs it is not generating the proof obligations). I will look into why3. Thank you for your suggestion.
> 
> Debasmita Lohar
> MS Student
> Computer Science and Engineering
> IIT Kharagpur
> 
> 
> On Mon, Dec 15, 2014 at 2:58 PM, David MENTRE <d.mentre at fr.merce.mee.com> wrote:
> Hello,
> 
> Le 08/12/2014 10:49, Debasmita Lohar a ?crit :
> I am looking for a tool that computes weakest precondition of a program.
> 
> Another option would be to use Why3 directly, instead of Frama-C.
> 
> For example, on attached program, if you run:
>   mkdir out
>   why3 prove -o out -P alt-ergo compute.mlw
> 
> Then in directory out/ you have generated VC:
> """
> $ tail -3 out/compute-Compute-WP_parameter_f.why
> goal WP_parameter_f :
>   (forall x:int. (((0 <= x) and (x <= 10)) -> ((1 <= (x + 1)) and
>   ((x + 1) <= 11))))
> 
> """
> 
> Why3 can be found here: http://why3.lri.fr/
> 
> There is also a dedicated mailing-list if you have questions.
> 
> For sake of completness, SPARK 2014 also generates VCs in a subdirectory:
>  http://www.spark-2014.org/
> 
> Best regards,
> david
> -- 
> David MENTR? - Research engineer, Ph.D.
>   Formal Methods and tools
> MITSUBISHI ELECTRIC R&D Centre Europe (MERCE)
> Phone: +33 2 23 45 58 29 / Fax: +33 2 23 45 58 59
> http://www.fr.mitsubishielectric-rce.eu
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss