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
|
(**************************************************************************)
(* *)
(* 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: ceffect.mli,v 1.36 2008/02/05 12:10:47 marche Exp $ i*)
open Info
type effect =
{
reads : ZoneSet.t;
assigns : ZoneSet.t;
reads_var : HeapVarSet.t;
assigns_var : HeapVarSet.t;
(* useful for generating separation invariants *)
reads_under_pointer : HeapVarSet.t;
assigns_under_pointer : HeapVarSet.t;
}
val ef_union : effect -> effect -> effect
val ef_empty : effect
val global_var : Info.var_info list ref
val intersect_only_alloc : effect -> effect -> bool
val is_alloc : Info.var_info -> bool
val assigns_alloc : effect -> bool
(* all heap vars and their associated types *)
val heap_vars : (string, Info.var_info) Hashtbl.t
val print_heap_vars : Format.formatter -> unit -> unit
val is_memory_var : var_info -> bool
val locations : Cast.nterm Clogic.location list -> effect
val predicate : Cast.npredicate -> effect
val expr : ?with_local:bool -> Cast.nexpr -> effect
val statement : ?with_local:bool -> Cast.nstatement -> effect
(* computes effects for logical symbols only *)
val file : Cast.nfile -> unit
(* Compute functions effects *)
val effect : ('a * Cast.ndecl Cast.located list) list -> fun_info list -> unit
(* table for weak invariants *)
val weak_invariants : (string, Cast.npredicate * effect) Hashtbl.t
(* table for strong invariants *)
val strong_invariants :
(string, (Cast.npredicate * effect * effect)) Hashtbl.t
val strong_invariants_2 :
(string, Cast.npredicate * effect * (string * Output.logic_type) list )
Hashtbl.t
val invariants_for_struct :
(string, (Cast.npredicate * effect * effect)) Hashtbl.t
val mem_strong_invariant_2 : string -> bool
(* table of warnings from computation of effects *)
val warnings : (Loc.position * string) Queue.t
|
