--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on December 2014 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141208/6d958eee/attachment.html>