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,
I have finally installed frama-c without any configuration error.
But I want to get initial weakest precondition of a
program(simple/complicated). I did not find anything like this in frama-c
(As for small programs it is not generating the proof obligations). I will
look into why3. Thank you for your suggestion.

Debasmita Lohar
MS Student
Computer Science and Engineering
IIT Kharagpur


On Mon, Dec 15, 2014 at 2:58 PM, David MENTRE <d.mentre at fr.merce.mee.com>
wrote:
>
> 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
>
> _______________________________________________
> 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/20141216/f28d6613/attachment.html>