--- layout: fc_discuss_archives title: Message 11 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



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>