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
|
(**************************************************************************)
(* *)
(* The Why platform for program certification *)
(* Copyright (C) 2002-2008 *)
(* Romain BARDOU *)
(* Jean-Franois COUCHOT *)
(* Mehdi DOGGUY *)
(* Jean-Christophe FILLITRE *)
(* Thierry HUBERT *)
(* Claude MARCH *)
(* Yannick MOY *)
(* Christine PAULIN *)
(* Yann RGIS-GIANAS *)
(* Nicolas ROUSSET *)
(* Xavier URBAIN *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU General Public *)
(* License version 2, as published by the Free Software Foundation. *)
(* *)
(* 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. *)
(* *)
(* See the GNU General Public License version 2 for more details *)
(* (enclosed in the file GPL). *)
(* *)
(**************************************************************************)
(*i $Id: info.mli,v 1.41 2008-05-23 15:24:16 marche Exp $ i*)
type why_type =
| Memory of why_type * zone
| Pointer of zone
| Addr of zone
| Int
| Real
| Unit
| Why_Logic of string
and zone =
{
zone_is_var : bool;
number : int;
mutable repr : zone option;
name : string;
(* mutable type_why_zone : why_type*)
}
val same_zone : zone -> zone -> bool
val same_why_type : why_type -> why_type -> bool
val same_why_type_no_zone : why_type -> why_type -> bool
val repr : zone -> zone
val found_repr : ?quote_var:bool -> zone -> string
val output_why_type : ?quote_var:bool -> why_type -> Output.logic_type
val output_zone_name : ?quote_var:bool -> zone -> Output.logic_type
type var_info = private
{
var_name : string;
var_uniq_tag : int;
mutable var_unique_name : string;
mutable var_is_assigned : bool;
mutable var_is_referenced : bool;
mutable var_is_static : bool;
mutable var_is_a_formal_param : bool;
mutable enum_constant_value : int64;
mutable var_type : Ctypes.ctype;
mutable var_why_type : why_type;
}
val default_var_info : string -> var_info
val set_assigned : var_info -> unit
val unset_assigned : var_info -> unit
val set_is_referenced : var_info -> unit
val without_dereference : var_info -> ('a -> 'b) -> 'a -> 'b
val set_static : var_info -> unit
val set_formal_param : var_info -> unit
val unset_formal_param : var_info -> unit
val set_const_value : var_info -> int64 -> unit
module HeapVarSet : Set.S with type elt = var_info
module HeapVarMap : Map.S with type key = var_info
module ZoneSet : Set.S with type elt = zone * string * why_type
val print_hvs : Format.formatter -> HeapVarSet.t -> unit
type label =
| Label_current
| Label_name of string
module LabelSet : Set.S with type elt = label
type logic_info =
{
logic_name : string;
mutable logic_heap_zone : ZoneSet.t;
mutable logic_heap_args : HeapVarSet.t;
(* see the .ml
mutable logic_heap_args : LabelSet.t HeapVarMap.t;
*)
mutable logic_args : var_info list;
mutable logic_why_type : why_type;
mutable logic_args_zones : zone list;
}
val default_logic_info : string -> logic_info
type fun_info =
{
fun_tag : int;
fun_name : string;
mutable fun_unique_name : string;
mutable function_reads : ZoneSet.t;
mutable function_writes : ZoneSet.t;
mutable function_reads_var : HeapVarSet.t;
mutable function_writes_var : HeapVarSet.t;
mutable has_assigns : bool;
mutable fun_type : Ctypes.ctype;
mutable args : var_info list;
mutable args_zones : zone list;
mutable graph : fun_info list;
mutable type_why_fun : why_type;
mutable has_body : bool;
}
val default_fun_info : string -> fun_info
type env_info =
| Var_info of var_info
| Fun_info of fun_info
val env_name : env_info -> string
val set_unique_name : env_info -> string -> unit
val var_type : env_info -> Ctypes.ctype
val get_why_type : env_info -> why_type
val set_var_type : env_info -> Ctypes.ctype -> why_type -> unit
val set_var_type_why : env_info -> why_type -> unit
type label_info =
{ label_info_name : string;
mutable times_used : int;
}
|
