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*/"

  • Subject: [Frama-c-discuss] Question about (the absence of) "/*undefined sequence*/"
  • From: bagnara at cs.unipr.it (Roberto Bagnara)
  • Date: Thu, 19 May 2011 09:59:51 +0200
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