--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on December 2014 ---
The option is `-wp-out <dir>` L. 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/18c153ba/attachment.html>