Abstract Interpretation for C

Discussion in 'C Programming' started by Tim Frink, Sep 19, 2007.

  1. Tim Frink

    Tim Frink Guest

    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.)

    Best regards,
    Tim
    Tim Frink, Sep 19, 2007
    #1
    1. Advertising

  2. Tim Frink

    jacob navia Guest

    Tim Frink wrote:
    > 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.)
    >
    > Best regards,
    > Tim
    >


    Interesting. Maybe you could specify for the non initiated what do you
    understand by "abstract operation" ?

    Thanks
    jacob navia, Sep 19, 2007
    #2
    1. Advertising

  3. Tim Frink

    Army1987 Guest

    On Wed, 19 Sep 2007 09:31:35 +0200, Tim Frink wrote:

    > 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.


    --
    Army1987 (Replace "NOSPAM" with "email")
    If you're sending e-mail from a Windows machine, turn off Microsoft's
    stupid “Smart Quotes†feature. This is so you'll avoid sprinkling garbage
    characters through your mail. -- Eric S. Raymond and Rick Moen
    Army1987, Sep 19, 2007
    #3
  4. Tim Frink

    Tim Frink Guest

    On Wed, 19 Sep 2007 09:54:45 +0200, jacob navia wrote:
    >
    > Interesting. Maybe you could specify for the non initiated what do you
    > understand by "abstract operation" ?


    Operations from the concrete language semantic (like C operator
    "*=") transformed into an abstract semantic.
    Tim Frink, Sep 19, 2007
    #4
  5. In article <>,
    Tim Frink <> wrote:

    >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.


    Would you say that you are looking for a Denotational Semantics
    analysis of C?
    --
    "law -- it's a commodity"
    -- Andrew Ryan (The Globe and Mail, 2005/11/26)
    Walter Roberson, Sep 19, 2007
    #5
  6. Tim Frink <> writes:
    > On Wed, 19 Sep 2007 09:54:45 +0200, jacob navia wrote:
    >>
    >> Interesting. Maybe you could specify for the non initiated what do you
    >> understand by "abstract operation" ?

    >
    > Operations from the concrete language semantic (like C operator
    > "*=") transformed into an abstract semantic.


    Okay, what is an "abstract semantic"?

    Don't expect everyone here to understand what you mean by "abstract",
    other than its ordinary English meaning. We understand C; we don't
    necessarily understand the field of study whose terminology you're
    using. If you can provide a pointer to something that explains it, we
    might be able to help.

    --
    Keith Thompson (The_Other_Keith) <http://www.ghoti.net/~kst>
    San Diego Supercomputer Center <*> <http://users.sdsc.edu/~kst>
    "We must do something. This is something. Therefore, we must do this."
    -- Antony Jay and Jonathan Lynn, "Yes Minister"
    Keith Thompson, Sep 19, 2007
    #6
    1. Advertising

Want to reply to this thread or ask your own question?

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. DaKoadMunky
    Replies:
    4
    Views:
    547
    Lee Weiner
    Apr 20, 2004
  2. Matthias Kaeppler
    Replies:
    1
    Views:
    435
    R.F. Pels
    May 22, 2005
  3. Sameer
    Replies:
    4
    Views:
    583
    Roedy Green
    Aug 31, 2005
  4. Uzytkownik
    Replies:
    3
    Views:
    589
    Uzytkownik
    Apr 3, 2005
  5. Iyer, Prasad C

    Abstract Methods & Abstract Class

    Iyer, Prasad C, Oct 20, 2005, in forum: Python
    Replies:
    0
    Views:
    530
    Iyer, Prasad C
    Oct 20, 2005
Loading...

Share This Page