--- layout: fc_discuss_archives title: Message 28 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



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