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