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

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150330/5c12e8f6/attachment.html>