1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
7 (* Copyright Institut National de Recherche en Informatique et en *)
8 (* Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the GNU General Public License as published by *)
10 (* the Free Software Foundation, either version 2 of the License, or *)
11 (* (at your option) any later version. This file is also distributed *)
12 (* under the terms of the INRIA Non-Commercial License Agreement. *)
14 (* *********************************************************************)
16 (* Useful functions to manipulate C abstract syntax *)
20 (* Sets and maps over identifiers *)
21 module IdentSet : Set.S with type elt = ident
22 module IdentMap : Map.S with type key = ident
24 (* Typedef handling *)
25 val unroll : Env.t -> typ -> typ
26 (* Expand typedefs at head of type. Returned type is not [TNamed]. *)
30 val add_attributes : attributes -> attributes -> attributes
31 (* Union of two sets of attributes *)
32 val remove_attributes : attributes -> attributes -> attributes
33 (* Difference [attr1 \ attr2] between two sets of attributes *)
34 val incl_attributes : attributes -> attributes -> bool
35 (* Check that first set of attributes is a subset of second set. *)
36 val attributes_of_type : Env.t -> typ -> attributes
37 (* Return the attributes of the given type, expanding typedefs if needed. *)
38 val add_attributes_type : attributes -> typ -> typ
39 (* Add the given set of attributes to those of the given type. *)
40 val remove_attributes_type : Env.t -> attributes -> typ -> typ
41 (* Remove the given set of attributes to those of the given type. *)
42 val erase_attributes_type : Env.t -> typ -> typ
43 (* Erase the attributes of the given type. *)
45 (* Type compatibility *)
46 val compatible_types : ?noattrs: bool -> Env.t -> typ -> typ -> bool
47 (* Check that the two given types are compatible.
48 If [noattrs], ignore attributes (recursively). *)
49 val combine_types : ?noattrs: bool -> Env.t -> typ -> typ -> typ option
50 (* Like [compatible_types], but if the two types are compatible,
51 return the most precise type compatible with both. *)
53 (* Size and alignment *)
55 val sizeof : Env.t -> typ -> int option
56 (* Return the size alignment of the given type, in bytes.
57 Machine-dependent. [None] is returned if the type is incomplete. *)
58 val alignof : Env.t -> typ -> int option
59 (* Return the natural alignment of the given type, in bytes.
60 Machine-dependent. [None] is returned if the type is incomplete. *)
61 val sizeof_ikind: ikind -> int
62 (* Return the size of the given integer kind. *)
63 val incomplete_type : Env.t -> typ -> bool
64 (* Return true if the given type is incomplete, e.g.
65 declared but not defined struct or union, or array type without a size. *)
67 (* Computing composite_info records *)
69 val composite_info_decl: Env.t -> struct_or_union -> Env.composite_info
70 val composite_info_def: Env.t -> struct_or_union -> field list -> Env.composite_info
72 (* Type classification functions *)
74 val is_void_type : Env.t -> typ -> bool
76 val is_integer_type : Env.t -> typ -> bool
77 (* Is type integer? *)
78 val is_arith_type : Env.t -> typ -> bool
79 (* Is type integer or float? *)
80 val is_pointer_type : Env.t -> typ -> bool
81 (* Is type a pointer type? *)
82 val is_scalar_type : Env.t -> typ -> bool
83 (* Is type integer, float or pointer? *)
84 val is_composite_type : Env.t -> typ -> bool
85 (* Is type a struct or union? *)
86 val is_function_type : Env.t -> typ -> bool
87 (* Is type a function type? (not pointer to function) *)
88 val pointer_arithmetic_ok : Env.t -> typ -> bool
89 (* Is the type [*ty] appropriate for pointer arithmetic?
90 [ty] must not be void, nor a function type, nor an incomplete type. *)
91 val is_signed_ikind : ikind -> bool
92 (* Return true if the given integer kind is a signed type. *)
93 val unsigned_ikind_of : ikind -> ikind
94 (* Return the unsigned integer kind corresponding to the given
96 val integer_rank : ikind -> int
97 (* Order integer kinds from smaller to bigger *)
98 val float_rank : fkind -> int
99 (* Order float kinds from smaller to bigger *)
101 (* Usual conversions over types *)
103 val pointer_decay : Env.t -> typ -> typ
104 (* Transform (decay) array and function types to pointer types. *)
105 val unary_conversion : Env.t -> typ -> typ
106 (* The usual unary conversions:
107 small integer types are promoted to [int]
108 array and function types decay *)
109 val binary_conversion : Env.t -> typ -> typ -> typ
110 (* The usual binary conversions. Applies only to arithmetic types.
111 Return the arithmetic type to which both operands of the binop
113 val argument_conversion : Env.t -> typ -> typ
114 (* Conversion applied to the argument of a prototyped function.
115 Equivalent to [pointer_decay]. *)
116 val default_argument_conversion : Env.t -> typ -> typ
117 (* Conversion applied to the argument of a nonprototyped or variadic
118 function. Like unary conversion, plus [float] becomes [double]. *)
121 val enum_ikind : ikind
122 (* Integer kind for enum values. Always [IInt]. *)
123 val wchar_ikind : ikind
124 (* Integer kind for wchar_t type. Unsigned. *)
125 val size_t_ikind : ikind
126 (* Integer kind for size_t type. Unsigned. *)
127 val ptr_t_ikind : ikind
128 (* Integer kind for ptr_t type. Smallest unsigned kind large enough
129 to contain a pointer without information loss. *)
130 val ptrdiff_t_ikind : ikind
131 (* Integer kind for ptrdiff_t type. Smallest signed kind large enough
132 to contain the difference between two pointers. *)
134 (* Helpers for type-checking *)
136 val type_of_constant : constant -> typ
137 (* Return the type of the given constant. *)
138 val is_literal_0 : exp -> bool
139 (* Is the given expression the integer literal "0"? *)
140 val is_lvalue : Env.t -> exp -> bool
141 (* Is the given expression a l-value? *)
142 val valid_assignment : Env.t -> exp -> typ -> bool
143 (* Check that an assignment of the given expression to a l-value of
144 the given type is allowed. *)
145 val valid_cast : Env.t -> typ -> typ -> bool
146 (* Check that a cast from the first type to the second is allowed. *)
147 val fundef_typ: fundef -> typ
148 (* Return the function type for the given function definition. *)
152 val intconst : int64 -> ikind -> exp
153 (* Build expression for given integer constant. *)
154 val floatconst : float -> fkind -> exp
155 (* Build expression for given float constant. *)
157 (* Expression for [(void * ) 0] *)
159 (* The [skip] statement. No location. *)
160 val sseq : location -> stmt -> stmt -> stmt
161 (* Return the statement [s1; s2], optimizing the cases
162 where [s1] or [s2] is [skip], or [s2] is a block. *)
163 val sassign : location -> exp -> exp -> stmt
164 (* Return the statement [exp1 = exp2;] *)
169 (* Denotes an unknown location. *)
170 val printloc: out_channel -> location -> unit
171 (* Printer for locations (for Printf) *)
172 val formatloc: Format.formatter -> location -> unit
173 (* Printer for locations (for Format) *)