--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on December 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Queries regarding WP plugin



? as explained in the WP manual, section ? 2.3.8 ? Generated Proof Obligations ?, p. 23.

Le 8 d?c. 2014 ? 10:49, Debasmita Lohar <dlohar2009 at gmail.com> a ?crit :

> Hello,
> 
> I am looking for a tool that computes weakest precondition of a program. I have installed Frama-C and executed it. It is giving me whether the assertion is valid or not. I need to get the weakest precondition in a logical format (as an example, I may have two variables x and y and the initial precondition is x+y>=1 /\ x<=2) which is then sent to the prover for validation check. I would like to know if there is any way I can extract the input which is sent to the prover. I have tried '-wp <dir>' option but it is not showing anything in the directory.
> I look forward to hearing from you.
> Thank you.
> 
> Debasmita Lohar
> 
> _______________________________________________
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141209/8e2e76df/attachment.html>