--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on May 2011 ---
On Thu, May 19, 2011 at 9:59 AM, Roberto Bagnara <bagnara at cs.unipr.it> wrote: > 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. The implication behind 1) should be true: if there are no "undefined sequence" comments, then the program should be well defined with respect to side-effects. 2) should be true too. A better criterion would be whether -unspecified-access -val emits any alarm of the form assert \separated(adr1, adr2); In your command-line, -print does not use value analysis results; it emits "undefined sequence" comments wherever it thinks there syntactically may be the possibility of such an unspecified behavior, even if the sequence is well defined for all possible executions of the program. It will even emit one for "i = j++;" But the method that involves the value analysis has known limitations: side effects caused by function calls are handled only in a separate undistributed plug-in, and some alarms are emitted for constructs that are defined. Pascal