--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on March 2018 ---
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>