Changeset 1143


Ignore:
Timestamp:
Aug 30, 2011, 3:39:08 PM (8 years ago)
Author:
sacerdot
Message:

Added one important observation (not implemented yet).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/CHANGES

    r1065 r1143  
    7171  arbitrary decision).
    7272
     7330/08/2011:  [annotation]
     74  There is a mismatch between the capability of external functions in the
     75  OCaml and Matita code. In OCaml they can interact with the memory. In
     76  Matita (following old? CompCert) they cannot. Hence, in the semantics
     77  of intermediate languages from ERTL on, we need to recover the arguments
     78  for the function not only from the registers, but also from the stack.
Note: See TracChangeset for help on using the changeset viewer.