From 891377ce1962cdb31357d6580d6546ec22df2b4f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 10:22:27 +0000 Subject: Switching to the new C parser/elaborator/simplifier git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cparser/Cutil.mli | 169 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 169 insertions(+) create mode 100644 cparser/Cutil.mli (limited to 'cparser/Cutil.mli') diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli new file mode 100644 index 00000000..de32a21c --- /dev/null +++ b/cparser/Cutil.mli @@ -0,0 +1,169 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Useful functions to manipulate C abstract syntax *) + +open C + +(* Sets and maps over identifiers *) +module IdentSet : Set.S with type elt = ident +module IdentMap : Map.S with type key = ident + +(* Typedef handling *) +val unroll : Env.t -> typ -> typ + (* Expand typedefs at head of type. Returned type is not [TNamed]. *) + +(* Attributes *) + +val add_attributes : attributes -> attributes -> attributes + (* Union of two sets of attributes *) +val remove_attributes : attributes -> attributes -> attributes + (* Difference [attr1 \ attr2] between two sets of attributes *) +val incl_attributes : attributes -> attributes -> bool + (* Check that first set of attributes is a subset of second set. *) +val attributes_of_type : Env.t -> typ -> attributes + (* Return the attributes of the given type, expanding typedefs if needed. *) +val add_attributes_type : attributes -> typ -> typ + (* Add the given set of attributes to those of the given type. *) +val remove_attributes_type : Env.t -> attributes -> typ -> typ + (* Remove the given set of attributes to those of the given type. *) +val erase_attributes_type : Env.t -> typ -> typ + (* Erase the attributes of the given type. *) + +(* Type compatibility *) +val compatible_types : ?noattrs: bool -> Env.t -> typ -> typ -> bool + (* Check that the two given types are compatible. + If [noattrs], ignore attributes (recursively). *) +val combine_types : ?noattrs: bool -> Env.t -> typ -> typ -> typ option + (* Like [compatible_types], but if the two types are compatible, + return the most precise type compatible with both. *) + +(* Size and alignment *) + +val sizeof : Env.t -> typ -> int option + (* Return the size alignment of the given type, in bytes. + Machine-dependent. [None] is returned if the type is incomplete. *) +val alignof : Env.t -> typ -> int option + (* Return the natural alignment of the given type, in bytes. + Machine-dependent. [None] is returned if the type is incomplete. *) +val sizeof_ikind: ikind -> int + (* Return the size of the given integer kind. *) +val incomplete_type : Env.t -> typ -> bool + (* Return true if the given type is incomplete, e.g. + declared but not defined struct or union, or array type without a size. *) + +(* Type classification functions *) + +val is_void_type : Env.t -> typ -> bool + (* Is type [void]? *) +val is_integer_type : Env.t -> typ -> bool + (* Is type integer? *) +val is_arith_type : Env.t -> typ -> bool + (* Is type integer or float? *) +val is_pointer_type : Env.t -> typ -> bool + (* Is type a pointer type? *) +val is_scalar_type : Env.t -> typ -> bool + (* Is type integer, float or pointer? *) +val is_composite_type : Env.t -> typ -> bool + (* Is type a struct or union? *) +val is_function_type : Env.t -> typ -> bool + (* Is type a function type? (not pointer to function) *) +val pointer_arithmetic_ok : Env.t -> typ -> bool + (* Is the type [*ty] appropriate for pointer arithmetic? + [ty] must not be void, nor a function type, nor an incomplete type. *) +val is_signed_ikind : ikind -> bool + (* Return true if the given integer kind is a signed type. *) +val unsigned_ikind_of : ikind -> ikind + (* Return the unsigned integer kind corresponding to the given + integer kind. *) +val integer_rank : ikind -> int + (* Order integer kinds from smaller to bigger *) +val float_rank : fkind -> int + (* Order float kinds from smaller to bigger *) + +(* Usual conversions over types *) + +val pointer_decay : Env.t -> typ -> typ + (* Transform (decay) array and function types to pointer types. *) +val unary_conversion : Env.t -> typ -> typ + (* The usual unary conversions: + small integer types are promoted to [int] + array and function types decay *) +val binary_conversion : Env.t -> typ -> typ -> typ + (* The usual binary conversions. Applies only to arithmetic types. + Return the arithmetic type to which both operands of the binop + are converted. *) +val argument_conversion : Env.t -> typ -> typ + (* Conversion applied to the argument of a prototyped function. + Equivalent to [pointer_decay]. *) +val default_argument_conversion : Env.t -> typ -> typ + (* Conversion applied to the argument of a nonprototyped or variadic + function. Like unary conversion, plus [float] becomes [double]. *) + +(* Special types *) +val enum_ikind : ikind + (* Integer kind for enum values. Always [IInt]. *) +val wchar_ikind : ikind + (* Integer kind for wchar_t type. Unsigned. *) +val size_t_ikind : ikind + (* Integer kind for size_t type. Unsigned. *) +val ptr_t_ikind : ikind + (* Integer kind for ptr_t type. Smallest unsigned kind large enough + to contain a pointer without information loss. *) +val ptrdiff_t_ikind : ikind + (* Integer kind for ptrdiff_t type. Smallest signed kind large enough + to contain the difference between two pointers. *) + +(* Helpers for type-checking *) + +val type_of_constant : constant -> typ + (* Return the type of the given constant. *) +val is_literal_0 : exp -> bool + (* Is the given expression the integer literal "0"? *) +val is_lvalue : Env.t -> exp -> bool + (* Is the given expression a l-value? *) +val valid_assignment : Env.t -> exp -> typ -> bool + (* Check that an assignment of the given expression to a l-value of + the given type is allowed. *) +val valid_cast : Env.t -> typ -> typ -> bool + (* Check that a cast from the first type to the second is allowed. *) +val fundef_typ: fundef -> typ + (* Return the function type for the given function definition. *) + +(* Constructors *) + +val intconst : int64 -> ikind -> exp + (* Build expression for given integer constant. *) +val floatconst : float -> fkind -> exp + (* Build expression for given float constant. *) +val nullconst : exp + (* Expression for [(void * ) 0] *) +val sskip: stmt + (* The [skip] statement. No location. *) +val sseq : location -> stmt -> stmt -> stmt + (* Return the statement [s1; s2], optimizing the cases + where [s1] or [s2] is [skip], or [s2] is a block. *) +val sassign : location -> exp -> exp -> stmt + (* Return the statement [exp1 = exp2;] *) + +(* Locations *) + +val no_loc: location + (* Denotes an unknown location. *) +val printloc: out_channel -> location -> unit + (* Printer for locations (for Printf) *) +val formatloc: Format.formatter -> location -> unit + (* Printer for locations (for Format) *) + -- cgit