Changeset 391


Ignore:
Timestamp:
Dec 8, 2010, 4:56:16 PM (9 years ago)
Author:
campbell
Message:

Comment out daemon and its uses - we don't need the properties of the memory
model at the moment.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Mem.ma

    r190 r391  
    303303  λn,p,v,m.update ? p (Datum n v) (set_cont n (p + oneZ) m).
    304304
     305(* Nonessential properties that may require arithmetic
    305306(* XXX: the daemons *)
    306307naxiom daemon : ∀A:Prop.A.
     
    555556#n;#p;//;
    556557nqed.
    557 
     558*)
    558559(* pointer_compat block_space pointer_space *)
    559560
     
    755756  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.
    756757
     758(* Nonessential properties that may require arithmetic
    757759nremark size_init_data_list_pos:
    758760  ∀i_data. OZ ≤ size_init_data_list i_data.
     
    773775##]
    774776nqed.
     777*)
    775778
    776779ndefinition block_init_data : list init_data → memory_space → block_contents ≝
     
    982985##] nqed.
    983986
     987(* Nonessential properties that may require arithmetic
    984988ntheorem load_store_similar:
    985989  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     
    35583562##]
    35593563nqed.
    3560 *)
     3564*)*)
    35613565(* ** Relation between signed and unsigned loads and stores *)
    35623566
     
    36013605  followed by a sign extension. *)
    36023606
     3607(* Nonessential properties that may require arithmetic
    36033608nlemma loadv_8_signed_unsigned:
    36043609  ∀m,a.
     
    36183623##]
    36193624nqed.
     3625*)
Note: See TracChangeset for help on using the changeset viewer.