From 2f643e4419e8237c63d6823720da8100da9c8b11 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Apr 2014 09:18:51 +0000 Subject: Clean-up pass on C types: - Ctypes: add useful functions on attributes; remove attrs in typeconv (because attributes are meaningless on r-values) - C2C: fixed missing or redundant Evalof - Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values); add sanity check between typeconv/classify_binarith and the C99 standard. - cparser: fixed several cases where incorrect type annotations were put on expressions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2457 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Ctypes.v | 45 +++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 41 insertions(+), 4 deletions(-) (limited to 'cfrontend/Ctypes.v') diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 5cd032d..41d0dcb 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -145,18 +145,55 @@ Definition attr_of_type (ty: type) := | Tcomp_ptr id a => a end. +(** Change the top-level attributes of a type *) + +Definition change_attributes (f: attr -> attr) (ty: type) : type := + match ty with + | Tvoid => ty + | Tint sz si a => Tint sz si (f a) + | Tlong si a => Tlong si (f a) + | Tfloat sz a => Tfloat sz (f a) + | Tpointer elt a => Tpointer elt (f a) + | Tarray elt sz a => Tarray elt sz (f a) + | Tfunction args res cc => ty + | Tstruct id fld a => Tstruct id fld (f a) + | Tunion id fld a => Tunion id fld (f a) + | Tcomp_ptr id a => Tcomp_ptr id (f a) + end. + +(** Erase the top-level attributes of a type *) + +Definition remove_attributes (ty: type) : type := + change_attributes (fun _ => noattr) ty. + +(** Add extra attributes to the top-level attributes of a type *) + +Definition attr_union (a1 a2: attr) : attr := + {| attr_volatile := a1.(attr_volatile) || a2.(attr_volatile); + attr_alignas := + match a1.(attr_alignas), a2.(attr_alignas) with + | None, al => al + | al, None => al + | Some n1, Some n2 => Some (N.max n1 n2) + end + |}. + +Definition merge_attributes (ty: type) (a: attr) : type := + change_attributes (attr_union a) ty. + Definition type_int32s := Tint I32 Signed noattr. Definition type_bool := Tint IBool Signed noattr. (** The usual unary conversion. Promotes small integer types to [signed int32] - and degrades array types and function types to pointer types. *) + and degrades array types and function types to pointer types. + Attributes are erased. *) Definition typeconv (ty: type) : type := match ty with - | Tint (I8 | I16 | IBool) _ a => Tint I32 Signed a - | Tarray t sz a => Tpointer t a + | Tint (I8 | I16 | IBool) _ _ => Tint I32 Signed noattr + | Tarray t sz a => Tpointer t noattr | Tfunction _ _ _ => Tpointer ty noattr - | _ => ty + | _ => remove_attributes ty end. (** * Operations over types *) -- cgit v1.2.3