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

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
-------------- next part --------------
module Compute

use import int.Int

 let f x
  requires { 0 <= x <= 10 }
  ensures { 1 <= result <= 11 }
  =
   x + 1

end