Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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