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