Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Question about (the absence of) "/*undefined sequence*/"

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