Ignore:
Timestamp:
Jan 25, 2011, 5:30:37 PM (9 years ago)
Author:
campbell
Message:

"memory_space" to "region" replacement to match ocaml code

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csyntax.ma

    r478 r480  
    8787  | Tint: intsize → signedness → type   (**r integer types *)
    8888  | Tfloat: floatsize → type            (**r floating-point types *)
    89   | Tpointer: memory_space → type → type   (**r pointer types ([*ty]) *)
    90   | Tarray: memory_space → type → Z → type (**r array types ([ty[len]]) *)
     89  | Tpointer: region → type → type      (**r pointer types ([*ty]) *)
     90  | Tarray: region → type → Z → type    (**r array types ([ty[len]]) *)
    9191  | Tfunction: typelist → type → type   (**r function types *)
    9292  | Tstruct: ident → fieldlist → type   (**r struct types *)
     
    447447(* * Size of a type, in bytes. *)
    448448
    449 ndefinition sizeof_pointer : memory_space → Z ≝
     449ndefinition sizeof_pointer : region → Z ≝
    450450λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    451451
Note: See TracChangeset for help on using the changeset viewer.