--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on May 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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