Hi,
I'm looking for any references about Abstract Interpretation
applied to the language C. More precisely, I'm interested
in the abstract domain for C, i.e. how the full set of
C operations can be modeled as abstract operations.
Do you know any publications/books or Internet resources
concerning this topic? (I did not find anything on google.)
This is from n1124.pdf, a draft for the future standard which so
far is essentially the current standard with technical corrigenda
incorporated in it. I don't understand whether this is what you're
looking for, though. HTH.
5.1.2.3 Program execution
1 The semantic descriptions in this International Standard describe the behavior of an
abstract machine in which issues of optimization are irrelevant.
2 Accessing a volatile object, modifying an object, modifying a ï¬le, or calling a function
that does any of those operations are all side effects,11) which are changes in the state of
the execution environment. Evaluation of an expression may produce side effects. At
certain speciï¬ed points in the execution sequence called sequence points, all side effects
of previous evaluations shall be complete and no side effects of subsequent evaluations
shall have taken place. (A summary of the sequence points is given in annex C.)
3 In the abstract machine, all expressions are evaluated as speciï¬ed by the semantics. An
actual implementation need not evaluate part of an expression if it can deduce that its
value is not used and that no needed side effects are produced (including any caused by
calling a function or accessing a volatile object).
4 When the processing of the abstract machine is interrupted by receipt of a signal, only the
values of objects as of the previous sequence point may be relied on. Objects that may be
modiï¬ed between the previous sequence point and the next sequence point need not have
received their correct values yet.
5 The least requirements on a conforming implementation are:
— At sequence points, volatile objects are stable in the sense that previous accesses are
complete and subsequent accesses have not yet occurred.
-----------------------------------------------------------------
11) The IEC 60559 standard for binary floating-point arithmetic
requires certain user-accessible status
flags and control modes. Floating-point operations implicitly set
the status flags; modes affect result values of floating-point
operations. Implementations that support such floating-point state
are required to regard changes to it as side effects — see annex
F for details. The floating-point environment library <fenv.h>
provides a programming facility for indicating when these side
effects matter, freeing the implementations in other cases.
§5.1.2.3 Environment
13
ISO/IEC 9899:TC2 Committee
Draft — May 6, 2005 WG14/N1124 — At program
termination, all data written into ï¬les shall be identical to the
result that
execution of the program according to the abstract semantics would
have produced.
— The input and output dynamics of interactive devices shall take
place as speciï¬ed in
7.19.3. The intent of these requirements is that unbuffered or
line-buffered output appear as soon as possible, to ensure that
prompting messages actually appear prior to a program waiting for
input.
6 What constitutes an interactive device is implementation-deï¬ned. 7
More stringent correspondences between abstract and actual semantics may
be deï¬ned by
each implementation.
