source: Deliverables/D2.2/8051/cparser/Cutil.mli @ 486

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 7.3 KB
RevLine 
[486]1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
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.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* Useful functions to manipulate C abstract syntax *)
17
18open C
19
20(* Sets and maps over identifiers *)
21module IdentSet : Set.S with type elt = ident
22module IdentMap : Map.S with type key = ident
23
24(* Typedef handling *)
25val unroll : Env.t -> typ -> typ
26  (* Expand typedefs at head of type.  Returned type is not [TNamed]. *)
27
28(* Attributes *)
29
30val add_attributes : attributes -> attributes -> attributes
31  (* Union of two sets of attributes *)
32val remove_attributes : attributes -> attributes -> attributes
33  (* Difference [attr1 \ attr2] between two sets of attributes *)
34val incl_attributes : attributes -> attributes -> bool
35  (* Check that first set of attributes is a subset of second set. *)
36val attributes_of_type : Env.t -> typ -> attributes
37  (* Return the attributes of the given type, expanding typedefs if needed. *)
38val add_attributes_type : attributes -> typ -> typ
39  (* Add the given set of attributes to those of the given type. *)
40val remove_attributes_type : Env.t -> attributes -> typ -> typ
41  (* Remove the given set of attributes to those of the given type. *)
42val erase_attributes_type : Env.t -> typ -> typ
43  (* Erase the attributes of the given type. *)
44
45(* Type compatibility *)
46val compatible_types : ?noattrs: bool -> Env.t -> typ -> typ -> bool
47  (* Check that the two given types are compatible. 
48     If [noattrs], ignore attributes (recursively). *)
49val 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. *)
52
53(* Size and alignment *)
54
55val 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. *)
58val 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. *)
61val sizeof_ikind: ikind -> int
62  (* Return the size of the given integer kind. *)
63val 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. *)
66
67(* Computing composite_info records *)
68
69val composite_info_decl: Env.t -> struct_or_union -> Env.composite_info
70val composite_info_def: Env.t -> struct_or_union -> field list -> Env.composite_info
71
72(* Type classification functions *)
73
74val is_void_type : Env.t -> typ -> bool
75  (* Is type [void]? *)
76val is_integer_type : Env.t -> typ -> bool
77  (* Is type integer? *)
78val is_arith_type : Env.t -> typ -> bool
79  (* Is type integer or float? *)
80val is_pointer_type : Env.t -> typ -> bool
81  (* Is type a pointer type? *)
82val is_scalar_type : Env.t -> typ -> bool
83  (* Is type integer, float or pointer? *)
84val is_composite_type : Env.t -> typ -> bool
85  (* Is type a struct or union? *)
86val is_function_type : Env.t -> typ -> bool
87  (* Is type a function type? (not pointer to function) *)
88val 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. *)
91val is_signed_ikind : ikind -> bool
92  (* Return true if the given integer kind is a signed type. *)
93val unsigned_ikind_of : ikind -> ikind
94  (* Return the unsigned integer kind corresponding to the given
95     integer kind. *)
96val integer_rank : ikind -> int
97  (* Order integer kinds from smaller to bigger *)
98val float_rank : fkind -> int
99  (* Order float kinds from smaller to bigger *)
100
101(* Usual conversions over types *)
102
103val pointer_decay : Env.t -> typ -> typ
104  (* Transform (decay) array and function types to pointer types. *)
105val 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 *)
109val 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
112     are converted. *)
113val argument_conversion : Env.t -> typ -> typ
114  (* Conversion applied to the argument of a prototyped function.
115     Equivalent to [pointer_decay]. *)
116val 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]. *)
119
120(* Special types *)
121val enum_ikind : ikind
122  (* Integer kind for enum values.  Always [IInt]. *)
123val wchar_ikind : ikind
124  (* Integer kind for wchar_t type.  Unsigned. *)
125val size_t_ikind : ikind
126  (* Integer kind for size_t type.  Unsigned. *)
127val ptr_t_ikind : ikind
128  (* Integer kind for ptr_t type.  Smallest unsigned kind large enough
129     to contain a pointer without information loss. *)
130val ptrdiff_t_ikind : ikind
131  (* Integer kind for ptrdiff_t type.  Smallest signed kind large enough
132     to contain the difference between two pointers. *)
133
134(* Helpers for type-checking *)
135
136val type_of_constant : constant -> typ
137  (* Return the type of the given constant. *)
138val is_literal_0 : exp -> bool
139  (* Is the given expression the integer literal "0"?  *)
140val is_lvalue : Env.t -> exp -> bool
141  (* Is the given expression a l-value? *)
142val 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. *)
145val valid_cast : Env.t -> typ -> typ -> bool
146  (* Check that a cast from the first type to the second is allowed. *)
147val fundef_typ: fundef -> typ
148  (* Return the function type for the given function definition. *)
149
150(* Constructors *)
151
152val intconst : int64 -> ikind -> exp
153  (* Build expression for given integer constant. *)
154val floatconst : float -> fkind -> exp
155  (* Build expression for given float constant. *)
156val nullconst : exp
157  (* Expression for [(void * ) 0] *)
158val sskip: stmt
159  (* The [skip] statement.  No location. *)
160val 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. *)
163val sassign : location -> exp -> exp -> stmt
164  (* Return the statement [exp1 = exp2;] *)
165
166(* Locations *)
167
168val no_loc: location
169  (* Denotes an unknown location. *)
170val printloc: out_channel -> location -> unit
171  (* Printer for locations (for Printf) *)
172val formatloc: Format.formatter -> location -> unit
173  (* Printer for locations (for Format) *)
174
Note: See TracBrowser for help on using the repository browser.