Changeset 718 for src/Clight/Csyntax.ma


Ignore:
Timestamp:
Mar 29, 2011, 5:54:37 PM (9 years ago)
Author:
campbell
Message:

Add an AST type (i.e., intermediate language type) for pointers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r700 r718  
    447447(* * Size of a type, in bytes. *)
    448448
    449 definition sizeof_pointer : region → Z ≝
    450 λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
    451 
    452449let rec sizeof (t: type) : Z ≝
    453450  match t return λ_.Z with
     
    455452  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    456453  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    457   | Tpointer r _ ⇒ sizeof_pointer r
     454  | Tpointer r _ ⇒ size_pointer r
    458455  | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
    459456  | Tfunction _ _ ⇒ 1
    460457  | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
    461458  | Tunion _ fld ⇒ align (Zmax 1 (sizeof_union fld)) (alignof t)
    462   | Tcomp_ptr r _ ⇒ sizeof_pointer r
     459  | Tcomp_ptr r _ ⇒ size_pointer r
    463460  ]
    464461
Note: See TracChangeset for help on using the changeset viewer.