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

[Frama-c-discuss] inline expansion of inline function



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>