--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on March 2015 ---
No, there is no function inlining for WP yet. An opportunity for internship indeed ;-) L. > Le 30 mars 2015 ? 19:06, Junkil (David) Park <junkil.park at cis.upenn.edu> a ?crit : > > Hi Benjamin, > > Thank you for your quick response. Can the WP plugin also do that? It is because I'd like to get proof obligations and discharge them with other provers. > > Thanks, > Junkil > > On Mon, Mar 30, 2015 at 1:01 PM, Benjamin Monate <benjamin.monate at trust-in-soft.com <mailto:benjamin.monate at trust-in-soft.com>> wrote: > Hi, > > frama-c -val -main verif > > proves your assertion automatically. > > HTH, > Benjamin Monate > CTO -- TrustInSoft > > > Le 30 mars 2015 ? 18:58, Junkil (David) Park <junkil.park at cis.upenn.edu <mailto:junkil.park at cis.upenn.edu>> a ?crit : > > > > Hi, > > > > Is there a way to verify the assertion in the example below without specifying the function contract of the step function as "//@ ensures x == 1;". I'd like to expand the function body in the place where it is invoked in the function verif(), and let it be simulated there. Is there any Frama-C option to do this job for me? > > > > int x; > > > > inline void step() > > { > > x = 1; > > } > > > > void verif() > > { > > step(); > > //@ assert x == 1; > > } > > > > Thanks, > > Junkil > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr> > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss <http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss> > > _______________________________________________ > 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/20150331/5acb57ae/attachment.html>