cil_datatype.mli 10.7 KB
Newer Older
1
2
3
4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
5
(*  Copyright (C) 2007-2019                                               *)
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(** Datatypes of some useful CIL types.
    @plugin development guide *)

(* This module should not be exported, but we need the alias and OCaml
   requires us to export it. *)
module UtilsFilepath = Filepath

open Cil_types
open Datatype

(** Auxiliary module for datatypes that can be pretty-printed. For those that
    do not have this signature, module {!Printer} must be used. *)
module type S_with_pretty = sig
  include S 
  (**/**)
  val pretty_ref: (Format.formatter -> t -> unit) ref
end
module type S_with_collections_pretty = sig
  include S_with_collections 
  (**/**)
  val pretty_ref: (Format.formatter -> t -> unit) ref
end


(**************************************************************************)
(** {3 Localisations} *)
(**************************************************************************)


(** Single position in a file.
    @since Nitrogen-20111001
*)
module Position: sig
  include S_with_collections_pretty with type t = UtilsFilepath.position
  val unknown : t
  val pp_with_col : Format.formatter -> t -> unit
  val of_lexing_pos : Lexing.position -> t
  val to_lexing_pos : t -> Lexing.position
end

(** Cil locations. *)
module Location: sig
  include S_with_collections_pretty with type t = location
  val unknown: t
  val pretty_long : t Pretty_utils.formatter
    (** Pretty the location under the form [file <f>, line <l>], without
        the full-path to the file. The default pretty-printer [pretty] echoes
        [<dir/f>:<l>] *)
  val pretty_line: t Pretty_utils.formatter
  (** Prints only the line of the location *)
  val of_lexing_loc : Lexing.position * Lexing.position -> t
  val to_lexing_loc : t -> Lexing.position * Lexing.position
end

module Localisation: Datatype.S with type t = localisation

module Syntactic_scope:
  Datatype.S_with_collections with type t = syntactic_scope

(**************************************************************************)
(** {3 Cabs types} *)
(**************************************************************************)

module Cabs_file: S_with_pretty with type t = Cabs.file

(**************************************************************************)
(** {3 C types}
    Sorted by alphabetic order. *)
(**************************************************************************)

module Block: S_with_pretty with type t = block
(* Blocks cannot compared or hashed, so collections are not available *)

module Compinfo: S_with_collections_pretty with type t = compinfo
module Enuminfo: S_with_collections_pretty with type t = enuminfo
module Enumitem: S_with_collections_pretty with type t = enumitem

(**
   @since Fluorine-20130401
*)
module Wide_string: S_with_collections with type t = int64 list

(**
   @since Oxygen-20120901 
*)
module Constant: S_with_collections_pretty with type t = constant

(** Note that the equality is based on eid. For structural equality, use
    {!ExpStructEq} *)
module Exp: sig
  include S_with_collections_pretty with type t = exp
  val dummy: exp (** @since Nitrogen-20111001 *)
end

module ExpStructEq: S_with_collections with type t = exp

module Fieldinfo: S_with_collections_pretty with type t = fieldinfo

module File: S with type t = file

module Global: sig
  include S_with_collections_pretty with type t = global
  val loc: t -> location
  val attr: t -> attributes
  (** @since Phosphorus-20170501-beta1 *)
end

module Initinfo: S_with_pretty with type t = initinfo

module Instr: sig
  include S_with_pretty with type t = instr
  val loc: t -> location
end

module Kinstr: sig
  include S_with_collections with type t = kinstr
  val kinstr_of_opt_stmt: stmt option -> kinstr
    (** @since Nitrogen-20111001. *)

  val loc: t -> location
end

module Label: S_with_collections_pretty with type t = label

(** Note that the equality is based on eid (for sub-expressions). 
    For structural equality, use {!LvalStructEq} *)
module Lval: S_with_collections_pretty with type t = lval

(**
   @since Oxygen-20120901 
*)
module LvalStructEq: S_with_collections with type t = lval

(** Same remark as for Lval. 
    For structural equality, use {!OffsetStructEq}. *) 
module Offset: S_with_collections_pretty with type t = offset

(** @since Oxygen-20120901 *)
module OffsetStructEq: S_with_collections with type t = offset

module Stmt_Id:  Hptmap.Id_Datatype with type t = stmt
module Stmt: sig
  include S_with_collections_pretty with type t = stmt
  module Hptset: sig
    include Hptset.S with type elt = stmt
                     and type 'a shape = 'a Hptmap.Shape(Stmt_Id).t
    val self: State.t
  end
  val loc: t -> location
  val pretty_sid: Format.formatter -> t -> unit
    (** Pretty print the sid of the statement
        @since Nitrogen-20111001 *)
end

module Attribute: S_with_collections_pretty with type t = attribute
module Attributes: S_with_collections with type t = attributes


(** Types, with comparison over struct done by key and unrolling of typedefs. *)
module Typ: sig
  include S_with_collections_pretty with type t = typ
  val toplevel_attr: t -> attributes
    (** returns the attributes associated to the toplevel type, without adding
        attributes from compinfo, enuminfo or typeinfo. Use {!Cil.typeAttrs}
        to retrieve the complete set of attributes. *)
end

(** Types, with comparison over struct done by name and no unrolling. *)
module TypByName: S_with_collections_pretty with type t = typ

(** Types, with comparison over struct done by key and no unrolling
    @since Fluorine-20130401 
 *)
module TypNoUnroll: S_with_collections_pretty with type t = typ


module Typeinfo: S_with_collections with type t = typeinfo

module Varinfo_Id: Hptmap.Id_Datatype

(** @plugin development guide *)
module Varinfo: sig
  include S_with_collections_pretty with type t = varinfo
  module Hptset: sig
    include Hptset.S with type elt = varinfo
                     and type 'a shape = 'a Hptmap.Shape(Varinfo_Id).t
    val self: State.t
  end
  val dummy: t
  (**/**)
  val internal_pretty_code_ref:
    (Type.precedence -> Format.formatter -> t -> unit) ref
end

module Kf: sig
  include Datatype.S_with_collections with type t = kernel_function
  val vi: t -> varinfo
  val id: t -> int

  (**/**)
  val set_formal_decls: (varinfo -> varinfo list -> unit) ref
  (**/**)
end

(**************************************************************************)
(** {3 ACSL types}
    Sorted by alphabetic order. *)
(**************************************************************************)

module Builtin_logic_info: S_with_collections_pretty with type t = builtin_logic_info

module Code_annotation: sig
  include S_with_collections_pretty with type t = code_annotation
  val loc: t -> location option
end

module Funbehavior: S with type t = funbehavior

module Funspec: S_with_pretty with type t = funspec

(** @since Fluorine-20130401 *)
module Fundec: S_with_collections_pretty with type t = fundec

module Global_annotation: sig
  include S_with_collections_pretty with type t = global_annotation
  val loc: t -> location

  val attr: t -> attributes
  (** attributes tied to the global annotation.
      @since Phosphorus-20170501-beta1 *)
end

module Identified_term: S_with_collections_pretty with type t = identified_term

module Logic_ctor_info: S_with_collections_pretty with type t = logic_ctor_info
module Logic_info: S_with_collections_pretty with type t = logic_info
module Logic_constant: S_with_collections_pretty with type t = logic_constant

module Logic_label: S_with_collections_pretty with type t = logic_label

(** Logic_type. See the various [Typ*] modules for the distinction between
    those modules *)
module Logic_type: S_with_collections_pretty with type t = logic_type
module Logic_type_ByName: S_with_collections_pretty with type t = logic_type
module Logic_type_NoUnroll: S_with_collections_pretty with type t = logic_type

module Logic_type_info: S_with_collections_pretty with type t = logic_type_info

module Logic_var: S_with_collections_pretty with type t = logic_var

(** @since Oxygen-20120901 *)
module Model_info: S_with_collections_pretty with type t = model_info

module Term: S_with_collections_pretty with type t = term

module Term_lhost: S_with_collections_pretty with type t = term_lhost
module Term_offset: S_with_collections_pretty with type t = term_offset
module Term_lval: S_with_collections_pretty with type t = term_lval

module Predicate: S_with_pretty with type t = predicate
module Identified_predicate: 
  S_with_collections_pretty with type t = identified_predicate
(** @since Neon-20140301 *)

(**************************************************************************)
(** {3 Logic_ptree}
    Sorted by alphabetic order. *)
(**************************************************************************)

module Lexpr: S with type t = Logic_ptree.lexpr
(** Beware: no pretty-printer is available. *)

(**/**)
(* ****************************************************************************)
(** {2 Internal API} *)
(* ****************************************************************************)

(* Forward declarations from Cil *)
val drop_non_logic_attributes : (attributes -> attributes) ref
val constfoldtoint : (exp -> Integer.t option) ref
val punrollType: (typ -> typ) ref

val clear_caches: unit -> unit

(**/**)

(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)