--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Weakest precondition calculation



Hi
What about if you pack your formula into an ACSL requires clause, and then ask the WP for generating the associated proof-obligation(s) ?
You can access those features programmatically via the WP’s API, available online ( API Documentation <http://frama-c.com/download/frama-c-Sulfur-20171101_api.tar.gz> ).
To starts with, consider using, from module Wp.VC :

type t 
elementary proof obligation
val generate_ip : ?model:string -> Property.t -> t <file:///Users/correnson/Downloads/frama-c-api/wp/Wp.VC.html#TYPEt> Bag.t <file:///Users/correnson/doc/code/html/Bag.html#TYPEt>
val get_formula : t <file:///Users/correnson/Downloads/frama-c-api/wp/Wp.VC.html#TYPEt> -> Wp.Lang.F.pred <file:///Users/correnson/Downloads/frama-c-api/wp/Wp.Lang.F.html#TYPEpred>

Regards,
	L.


> Le 23 mars 2018 à 15:37, Niklas Rosén <nrosen at kth.se> a écrit :
> 
> Hi
> 
> I'm working on my master's thesis and I'm trying to implement an analysis as a plugin to Frama-C. As a part of this analysis I need to generate weakest precondition formulae for a given function and input formula. Could this be done using the WP plugin?
> 
> I have asked this question in greater detail at StackOverflow, https://stackoverflow.com/q/49234253/9479240 <https://stackoverflow.com/q/49234253/9479240> , without success so far.
> 
> Could anyone shed some light on this or point me in the right direction?
> 
> 
> Best regards
> Niklas
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180323/d7a95928/attachment.html>