Changeset 9 for C-semantics/Mem.ma


Ignore:
Timestamp:
Jun 21, 2010, 4:22:09 PM (10 years ago)
Author:
campbell
Message:

Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Mem.ma

    r3 r9  
    23652365    ##]
    23662366##] nqed.
    2367 
     2367(*  XXX: reenable once I've sorted out Integers.ma a bit
    23682368nlemma valid_pointer_inject_no_overflow:
    23692369  ∀f,m1,m2,b,ofs,b',x.
     
    34333433##]
    34343434nqed.
    3435 
     3435*)
    34363436(* ** Relation between signed and unsigned loads and stores *)
    34373437
Note: See TracChangeset for help on using the changeset viewer.