1
2
3
4
5
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
|
(**************************************************************************)
(* *)
(* The Why platform for program certification *)
(* *)
(* Copyright (C) 2002-2011 *)
(* *)
(* Jean-Christophe FILLIATRE, CNRS & Univ. Paris-sud 11 *)
(* Claude MARCHE, INRIA & Univ. Paris-sud 11 *)
(* Yannick MOY, Univ. Paris-sud 11 *)
(* Romain BARDOU, Univ. Paris-sud 11 *)
(* *)
(* Secondary contributors: *)
(* *)
(* Thierry HUBERT, Univ. Paris-sud 11 (former Caduceus front-end) *)
(* Nicolas ROUSSET, Univ. Paris-sud 11 (on Jessie & Krakatoa) *)
(* Ali AYAD, CNRS & CEA Saclay (floating-point support) *)
(* Sylvie BOLDO, INRIA (floating-point support) *)
(* Jean-Francois COUCHOT, INRIA (sort encodings, hyps pruning) *)
(* Mehdi DOGGUY, Univ. Paris-sud 11 (Why GUI) *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software 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. *)
(* *)
(**************************************************************************)
exception NotImplemented of string
exception Unsupported of string
val fatal : ('a,Format.formatter,unit,'b) format4 -> 'a
val notimplemented : ('a,Format.formatter,unit,'b) format4 -> 'a
val unsupported : ('a,Format.formatter,unit,'b) format4 -> 'a
val warning : ('a,Format.formatter,unit) format -> 'a
val warn_general : ('a,Format.formatter,unit) format -> 'a
(** warning for currently ignored feature which is only displayed once *)
val warn_once : string -> unit
(* Jessie specific names *)
val name_of_default_behavior : string
val name_of_valid_wstring : string
val name_of_valid_string : string
val name_of_strlen : string
val name_of_wcslen : string
val name_of_hint_assertion : string
val name_of_string_declspec : string
val name_of_padding_type : string
val name_of_integral_type : ?bitsize:int -> Cil_types.typ -> string
val name_of_assert : string
val name_of_free : string
val name_of_malloc : string
val filter_alphanumeric : string -> (char * char) list -> char -> string
val type_name: Cil_types.typ -> string
val logic_type_name: Cil_types.logic_type -> string
(* unique names generation *)
val unique_name : string -> string
val unique_logic_name : string -> string
val unique_name_if_empty : string -> string
(* ????? *)
val checking : bool
val check_types : Cil_types.file -> unit
val integral_type_size_in_bits : Cil_types.typ -> int
val max_value_of_integral_type :
?bitsize:int -> Cil_types.typ -> My_bigint.t
val min_value_of_integral_type :
?bitsize:int -> Cil_types.typ -> My_bigint.t
val all_integral_types : (string, Cil_types.typ * int) Hashtbl.t
val term_of_var : Cil_types.varinfo -> Cil_types.term
val mkterm :
Cil_types.term_node ->
Cil_types.logic_type ->
Lexing.position * Lexing.position -> Cil_types.term
val mkInfo : Cil_types.exp -> Cil_types.exp
val lift_offset : Cil_types.typ -> Cil_types.offset -> Cil_types.offset
val mkTRef : Cil_types.typ -> string -> Cil_types.typ
val mkTRefArray :
Cil_types.typ * Cil_types.exp * Cil_types.attributes ->
Cil_types.typ
val mkalloc_statement : Cil_types.varinfo ->
Cil_types.typ -> Cil_types.location -> Cil_types.stmt
val mkalloc_array_statement :
Cil_types.varinfo ->
Cil_types.typ -> int64 -> Cil_types.location -> Cil_types.stmt
val mkfree_statement :
Cil_types.varinfo ->
Cil_types.location -> Cil_types.stmt
val mkfree: Cil_types.varinfo -> Cil_types.location -> Cil_types.instr
val mkStructEmpty : string -> Cil_types.compinfo
val mkStructSingleton :
?padding:int ->
string -> string -> Cil_types.typ -> Cil_types.compinfo
val malloc_function : unit -> Cil_types.varinfo
val free_function : unit -> Cil_types.varinfo
val flatten_multi_dim_array : bool ref
val reference_of_array : Cil_types.typ -> Cil_types.typ
val get_struct_info : Cil_types.typ -> Cil_types.compinfo
val get_struct_name : Cil_types.typ -> string
val force_app_term_type : (Cil_types.typ -> 'a) -> Cil_types.logic_type -> 'a
val app_term_type : (Cil_types.typ -> 'a) -> 'a -> Cil_types.logic_type -> 'a
val is_base_addr : Cil_types.term -> bool
val is_reference_type : Cil_types.typ -> bool
val is_array_reference_type : Cil_types.typ -> bool
val is_assert_function : Cil_types.varinfo -> bool
val is_free_function : Cil_types.varinfo -> bool
val is_malloc_function : Cil_types.varinfo -> bool
val is_realloc_function : Cil_types.varinfo -> bool
val is_calloc_function : Cil_types.varinfo -> bool
val reference_size : Cil_types.typ -> int64
val bits_sizeof : Cil_types.typ -> int64
val is_unknown_location : Lexing.position * 'a -> bool
val get_unique_field : Cil_types.typ -> Cil_types.fieldinfo
val is_last_offset : Cil_types.offset -> bool
val struct_type_for_void : Cil_types.typ ref
val filter_alphanumeric : string -> (char * char) list -> char -> string
(*
val attach_globinit : Cil_types.stmt -> unit
*)
val attach_global : Cil_types.global -> unit
val attach_globaction : (unit -> unit) -> unit
val do_on_term :
(Cil_types.exp -> Cil_types.exp) option *
(Cil_types.exp -> Cil_types.exp) option ->
Cil_types.term -> Cil_types.term Cil.visitAction
val do_on_term_offset :
(Cil_types.offset -> Cil_types.offset) option *
(Cil_types.offset -> Cil_types.offset) option ->
Cil_types.term_offset -> Cil_types.term_offset Cil.visitAction
val do_on_term_lval :
(Cil_types.lval -> Cil_types.lval) option *
(Cil_types.lval -> Cil_types.lval) option ->
Cil_types.term_lval -> Cil_types.term_lval Cil.visitAction
val do_and_update_globals : (Cil_types.file -> 'a) -> Cil_types.file -> unit
val visit_and_update_globals :
Visitor.frama_c_visitor -> Cil_types.file -> unit
val signal_change : unit -> unit
val almost_integer_type : Cil_types.typ
val add_pending_statement : beginning:bool -> Cil_types.stmt -> unit
val visit_until_convergence :
Visitor.frama_c_visitor -> Cil_types.file -> unit
class proxy_frama_c_visitor: Visitor.frama_c_visitor -> Visitor.frama_c_visitor
val visit_and_push_statements_visitor :
Visitor.frama_c_visitor -> proxy_frama_c_visitor
val visit_and_push_statements :
(proxy_frama_c_visitor -> 'a -> 'b) ->
Visitor.frama_c_visitor -> 'a -> 'b
val print_to_stdout : Cil_types.file -> unit
val constant_expr : ?loc:Cil_datatype.Location.t -> My_bigint.t -> Cil_types.exp
|
