Changeset 125 for C-semantics/Csyntax.ma


Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (10 years ago)
Author:
campbell
Message:

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csyntax.ma

    r124 r125  
    4646  | F32: floatsize
    4747  | F64: floatsize.
    48 
    49 (* Pointers can point to particular memory spaces. *)
    50 ninductive mem_space : Type ≝
    51   | Generic : mem_space
    52   | Data : mem_space
    53   | IData : mem_space
    54   | XData : mem_space
    55   | Code : mem_space.
    5648
    5749(* * The syntax of type expressions.  Some points to note:
     
    9486  | Tint: intsize → signedness → type   (**r integer types *)
    9587  | Tfloat: floatsize → type            (**r floating-point types *)
    96   | Tpointer: mem_space → type → type   (**r pointer types ([*ty]) *)
    97   | Tarray: mem_space → type → Z → type (**r array types ([ty[len]]) *)
     88  | Tpointer: memory_space → type → type   (**r pointer types ([*ty]) *)
     89  | Tarray: memory_space → type → Z → type (**r array types ([ty[len]]) *)
    9890  | Tfunction: typelist → type → type   (**r function types *)
    9991  | Tstruct: ident → fieldlist → type   (**r struct types *)
Note: See TracChangeset for help on using the changeset viewer.