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
|
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
val print_qualified_ident : Format.formatter -> Java_ast.qualified_ident -> unit
val print_type_name : Format.formatter -> Java_env.java_type_info -> unit
val print_type : Format.formatter -> Java_env.java_type -> unit
val type_table : (int, Java_env.java_type_info) Hashtbl.t
type method_table_info =
{ mt_method_info : Java_env.method_info;
mt_requires : Java_tast.assertion option;
mt_decreases : Java_tast.term option;
mt_behaviors : (Java_ast.identifier *
Java_tast.assertion option *
Java_env.java_class_info option *
(Loc.position * Java_tast.term list) option *
Java_tast.assertion) list ;
mt_body : Java_tast.block option;
}
val methods_table :
(int, method_table_info) Hashtbl.t
type constructor_table_info =
{ ct_constr_info : Java_env.constructor_info;
ct_requires : Java_tast.assertion option;
ct_decreases : Java_tast.term option;
ct_behaviors : (Java_ast.identifier *
Java_tast.assertion option *
Java_env.java_class_info option *
(Loc.position * Java_tast.term list) option *
Java_tast.assertion) list ;
ct_body : Java_tast.block;
}
val constructors_table :
(int, constructor_table_info) Hashtbl.t
val invariants_table :
(int, Java_env.java_class_info * Java_env.java_var_info *
(Java_ast.identifier * Java_tast.assertion) list) Hashtbl.t
val static_invariants_table :
(int, (string * Java_tast.assertion) list) Hashtbl.t
val field_initializer_table :
(int, Java_tast.initialiser option) Hashtbl.t
val final_field_values_table :
(int, Num.num list) Hashtbl.t
val axioms_table : (string,(bool * Java_env.logic_label list * Java_tast.assertion)) Hashtbl.t
type logic_body =
| JAssertion of Java_tast.assertion
| JTerm of Java_tast.term
| JReads of Java_tast.term list
val logic_types_table : (string, Java_env.logic_type_info) Hashtbl.t
val logics_table :
(int,Java_env.java_logic_info * logic_body) Hashtbl.t
exception Typing_error of Loc.position * string
val catch_typing_errors : ('a -> 'b) -> 'a -> 'b
(*
val get_types :
Java_ast.compilation_unit ->
Java_env.package_info list *
(string * Java_env.java_type_info) list
*)
val get_types :
Java_env.package_info list ->
Java_ast.compilation_unit list ->
Java_env.package_info list *
(string * Java_env.java_type_info) list
val get_bodies :
Java_env.package_info list ->
(string * Java_env.java_type_info) list ->
Java_ast.compilation_unit -> unit
val type_specs :
Java_env.package_info list ->
(string * Java_env.java_type_info) list ->
unit
(*
Local Variables:
compile-command: "make -j -C .. bin/krakatoa.byte"
End:
*)
|
