--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on May 2011 ---
Hi there. In the absence of any "/*undefined sequence*/" comment resulting from a successful execution of frama-c -val -print file.c can one assume one or both the following? 1) In `file.c', the order in which side effects take place is fully defined by the standard. 2) That order is faithfully reflected in the transformed program shown as output. Thanks, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara at cs.unipr.it