| Global Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(394 entries) |
| Axiom Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(47 entries) |
| Lemma Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(191 entries) |
| Constructor Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(21 entries) |
| Inductive Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(15 entries) |
| Definition Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(92 entries) |
| Module Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(15 entries) |
| Library Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(13 entries) |
Global Index
A
AbsAllocate [constructor, in AndersenModel]
AbsCopy [constructor, in AndersenModel]
AbsRead [constructor, in AndersenModel]
abstractAllocate [lemma, in AndersenSound]
abstractAllocate' [lemma, in AndersenSound]
abstractCopy [lemma, in AndersenSound]
abstractCopy' [lemma, in AndersenSound]
abstractProgram [definition, in AndersenModel]
abstractProgram' [definition, in AndersenModel]
abstractRead [lemma, in AndersenSound]
abstractRead' [lemma, in AndersenSound]
abstractWrite [lemma, in AndersenSound]
abstractWrite' [lemma, in AndersenSound]
abstract_exec [definition, in AndersenModel]
abstract_followPath [inductive, in AndersenSound]
abstract_followPath_expand [lemma, in AndersenSound]
abstract_followPath_incl [lemma, in AndersenSound]
abstract_followPath_read [lemma, in AndersenSound]
abstract_followPath_write_preserve [lemma, in AndersenSound]
abstract_followPath_write_var [lemma, in AndersenSound]
abstract_follow_conjoin [lemma, in AndersenSound]
abstract_initState [definition, in AndersenSound]
abstract_instruction [inductive, in AndersenModel]
abstract_state [inductive, in AndersenModel]
AbsWrite [constructor, in AndersenModel]
add [axiom, in Maps]
add [definition, in Maps]
add [definition, in lib.Esets]
aexec [definition, in AndersenIter]
aexec' [lemma, in AndersenIter]
ainitState [definition, in AndersenIter]
ainstruction [definition, in AndersenIter]
ainstr_widen [lemma, in AndersenIter]
Allocate [constructor, in Pointer]
allocate_site [lemma, in AndersenIter]
allocate_var [lemma, in AndersenIter]
allocation_site [definition, in AndersenModel]
allocation_site_model_is_conservative [lemma, in AndersenSound]
allocation_site_step [lemma, in AndersenSound]
AllocMap [module, in AndersenModel]
AllocSet [module, in AndersenModel]
allPaths [definition, in AndersenSound]
allPaths_step [lemma, in AndersenSound]
allPaths_write [lemma, in AndersenSound]
AllS_dec [definition, in ListUtil]
AllS_dec_some [definition, in ListUtil]
AllS_deduce [lemma, in ListUtil]
AllS_In [lemma, in ListUtil]
AllS_not [lemma, in ListUtil]
AllS_not_dec [lemma, in ListUtil]
andersen [definition, in Andersen]
Andersen [library]
AndersenIter [library]
AndersenModel [library]
AndersenSound [library]
andersen_sound [lemma, in AndersenSound]
andersen_start [lemma, in AndersenSound]
APath_Done [constructor, in AndersenSound]
approx [definition, in AndersenIter]
approxStrict [inductive, in AndersenIter]
approxStrict_approx [lemma, in AndersenIter]
approxStrict_dec [definition, in AndersenIter]
approxStrict_trans [lemma, in AndersenIter]
approxStrict_wf [lemma, in AndersenIter]
approxStrict_wf' [lemma, in AndersenIter]
approx' [inductive, in AndersenIter]
approx_dec [definition, in AndersenIter]
approx_init [lemma, in AndersenIter]
approx_init' [lemma, in AndersenIter]
approx_refl [lemma, in AndersenIter]
approx_refl' [lemma, in AndersenIter]
approx_trans [lemma, in AndersenIter]
approx_trans' [lemma, in AndersenIter]
aprogram [definition, in AndersenIter]
aprogram' [definition, in AndersenIter]
astate [definition, in AndersenIter]
B
bound [definition, in AndersenIter]
C
card [lemma, in AndersenIter]
cardinality [definition, in AndersenIter]
cardinality_atLeast [definition, in AndersenIter]
compatible [inductive, in AndersenSound]
compatible_write_var [lemma, in AndersenSound]
Copy [constructor, in Pointer]
copy_var [lemma, in AndersenIter]
D
distinct [definition, in AndersenIter]
distinctify [definition, in AndersenIter]
dom [definition, in AndersenModel]
dom [axiom, in lib.Emaps]
dom [definition, in lib.Emaps]
dom [definition, in Maps]
dom [axiom, in Maps]
dom [axiom, in lib.Esets]
dom [definition, in Maps]
dom [definition, in AndersenIter]
dom [definition, in Pointer]
dom [definition, in AndersenModel]
dom [definition, in lib.Esets]
dom [definition, in Pointer]
dom [definition, in Maps]
dom [definition, in Maps]
dom_eq_dec [definition, in Pointer]
dom_eq_dec [axiom, in Maps]
dom_eq_dec [axiom, in lib.Emaps]
dom_eq_dec [axiom, in lib.Esets]
E
elems [definition, in lib.Esets]
elems [definition, in Maps]
elems [axiom, in Maps]
elems_ok [lemma, in lib.Esets]
elems_ok [axiom, in Maps]
elems_ok [lemma, in Maps]
elems_remove [lemma, in Maps]
elems_remove [axiom, in Maps]
elems_remove [lemma, in lib.Esets]
Emaps [library]
empty [definition, in Maps]
empty [axiom, in Maps]
empty [definition, in lib.Esets]
eO [constructor, in lib.Nonterm]
EQ [module, in lib.Esets]
EQ [module, in Maps]
EQ [module, in lib.Emaps]
Esets [library]
eSS [constructor, in lib.Nonterm]
exec [definition, in Pointer]
ext_eq [axiom, in lib.Emaps]
ext_eq [axiom, in Maps]
F
fixed_point [definition, in AndersenIter]
fixed_point [definition, in Machine]
fixed_point' [definition, in AndersenIter]
fixed_point_ok [lemma, in Machine]
flowInsensitive_is_conservative [lemma, in Machine]
fold [definition, in lib.Esets]
fold_In_union [lemma, in AndersenIter]
fold_In_unionv [lemma, in AndersenIter]
fold_left_sum [lemma, in AndersenSound]
fold_monotone_gen [lemma, in lib.Esets]
fold_monotone_1 [lemma, in lib.Esets]
fold_monotone_2 [lemma, in lib.Esets]
fold_plus_ge [lemma, in AndersenIter]
fold_plus_gt [lemma, in AndersenIter]
followPath [inductive, in AndersenSound]
followPath_case [lemma, in AndersenSound]
followPath_goto [lemma, in AndersenSound]
followPath_nothing_new [lemma, in AndersenSound]
followPath_read [lemma, in AndersenSound]
followPath_S [lemma, in AndersenSound]
followPath_SO [lemma, in AndersenSound]
followPath_SO' [lemma, in AndersenSound]
followPath_swap_var [lemma, in AndersenSound]
followPath_write_var [lemma, in AndersenSound]
follow_conjoin [lemma, in AndersenSound]
FuncMap [module, in Maps]
G
Goto [constructor, in Pointer]
I
In [definition, in Maps]
In [definition, in lib.Esets]
In [axiom, in Maps]
incl [definition, in lib.Esets]
incl [definition, in Maps]
incl [axiom, in Maps]
incl_add [lemma, in lib.Esets]
incl_add [lemma, in AndersenIter]
incl_add2 [lemma, in AndersenIter]
incl_add3 [lemma, in AndersenIter]
incl_cardinality [lemma, in AndersenIter]
incl_cardinality' [lemma, in AndersenIter]
incl_elems [lemma, in AndersenIter]
incl_empty [lemma, in Maps]
incl_empty [lemma, in lib.Esets]
incl_empty [axiom, in Maps]
incl_empty_empty [lemma, in lib.Esets]
incl_eq_dec [definition, in ListUtil]
incl_false [lemma, in Maps]
incl_false [axiom, in Maps]
incl_false [lemma, in lib.Esets]
incl_fold1 [lemma, in AndersenIter]
incl_fold2 [lemma, in AndersenIter]
incl_fold3 [lemma, in AndersenIter]
incl_fold3' [lemma, in AndersenIter]
incl_fold_read [lemma, in AndersenIter]
incl_fold_union [lemma, in AndersenSound]
incl_fold_union' [lemma, in AndersenSound]
incl_fold_union_read [lemma, in AndersenSound]
incl_fold_write [lemma, in AndersenIter]
incl_gt [lemma, in AndersenIter]
incl_In [lemma, in Maps]
incl_In [axiom, in Maps]
incl_In [lemma, in lib.Esets]
incl_intersect2 [lemma, in Andersen]
incl_length [lemma, in AndersenIter]
incl_ok [axiom, in Maps]
incl_ok [lemma, in lib.Esets]
incl_ok [lemma, in Maps]
incl_refl [axiom, in Maps]
incl_refl [lemma, in Maps]
incl_refl [lemma, in lib.Esets]
incl_S [lemma, in AndersenIter]
incl_trans [lemma, in lib.Esets]
incl_trans [lemma, in Maps]
incl_trans [axiom, in Maps]
incl_trans' [lemma, in AndersenIter]
incl_union [lemma, in AndersenIter]
incl_union2 [lemma, in AndersenIter]
incl_union_left [lemma, in lib.Esets]
incl_union_left [lemma, in Maps]
incl_union_left [axiom, in Maps]
incl_union_right [axiom, in Maps]
incl_union_right [lemma, in Maps]
incl_union_right [lemma, in lib.Esets]
incl_valid_read [lemma, in AndersenIter]
incl_valid_write [lemma, in AndersenIter]
incl_write_bonanza [lemma, in AndersenSound]
incl_write_bonanza' [lemma, in AndersenSound]
increasing [lemma, in AndersenIter]
increasing' [lemma, in AndersenIter]
init [definition, in Maps]
init [axiom, in Maps]
init [definition, in lib.Emaps]
initState [definition, in Pointer]
instruction [inductive, in Pointer]
ins_sites [definition, in AndersenIter]
ins_vars [definition, in AndersenIter]
intersect [definition, in lib.Esets]
intersect [axiom, in Maps]
intersect [definition, in Maps]
In_add [lemma, in lib.Esets]
In_add [lemma, in Maps]
In_add [axiom, in Maps]
In_add_already [lemma, in lib.Esets]
In_add_eq [lemma, in Maps]
In_add_eq [axiom, in Maps]
In_add_eq [lemma, in lib.Esets]
In_add_neq [lemma, in lib.Esets]
In_add_neq [lemma, in Maps]
In_add_neq [axiom, in Maps]
in_aprogram [lemma, in AndersenIter]
in_aprogram' [lemma, in AndersenIter]
In_dec [lemma, in lib.Esets]
In_empty [axiom, in Maps]
In_empty [lemma, in lib.Esets]
In_empty [lemma, in Maps]
In_eq [lemma, in lib.Esets]
In_eq_dec [definition, in ListUtil]
In_intersect [axiom, in Maps]
In_intersect [lemma, in lib.Esets]
In_intersect [lemma, in Maps]
In_intersect' [lemma, in lib.Esets]
In_intersect' [axiom, in Maps]
In_intersect' [lemma, in Maps]
In_list [lemma, in lib.Esets]
In_map [lemma, in AndersenIter]
In_remove [lemma, in lib.Esets]
In_remove [lemma, in Maps]
In_remove [axiom, in Maps]
In_union [axiom, in Maps]
In_union [lemma, in lib.Esets]
In_union [lemma, in Maps]
In_union' [axiom, in Maps]
In_union' [lemma, in Maps]
In_union_left [lemma, in lib.Esets]
In_union_right [lemma, in lib.Esets]
isEven [inductive, in lib.Nonterm]
iterate [definition, in Machine]
iterate_approx [lemma, in Machine]
iterate_pick [lemma, in Machine]
iterate_pick' [lemma, in Machine]
iterate_pick_cp [lemma, in Machine]
L
ListSet [module, in Maps]
ListUtil [library]
M
Machine [library]
MakeMap [module, in lib.Emaps]
MakeSet [module, in lib.Esets]
MAP [module, in Maps]
map [definition, in lib.Emaps]
map [definition, in Maps]
map [axiom, in Maps]
Maps [library]
monotonic [lemma, in AndersenIter]
monotonic' [lemma, in AndersenIter]
mult_le [lemma, in AndersenIter]
mustNotAlias [definition, in Pointer]
mustNotAlias_answer [inductive, in Pointer]
mustNotAlias_procedure [definition, in Pointer]
N
NatEq [module, in Pointer]
NatMap [module, in Pointer]
neq_nat_dec [definition, in AndersenIter]
nil [definition, in lib.Esets]
nil [definition, in lib.Esets]
nil [definition, in lib.Esets]
Nonterm [library]
NotAliased [constructor, in Pointer]
nth_spec_implies_In [lemma, in ListUtil]
O
Ok [constructor, in lib.Nonterm]
P
pathCompatible [definition, in AndersenSound]
pathCompatible_symm [lemma, in AndersenSound]
Path_Done [constructor, in AndersenSound]
pdiv2 [definition, in lib.Nonterm]
pdiv2_correct [lemma, in lib.Nonterm]
pdiv2_correct2 [lemma, in lib.Nonterm]
pdiv2_correct3 [lemma, in lib.Nonterm]
Pointer [library]
progSites [definition, in AndersenIter]
progVars [definition, in AndersenIter]
pSites [definition, in AndersenIter]
pVars [definition, in AndersenIter]
R
reachable [inductive, in Machine]
reachable_a [lemma, in AndersenIter]
reachable_flowInsensitive [inductive, in Machine]
Read [constructor, in Pointer]
read_var [lemma, in AndersenIter]
remove [axiom, in Maps]
remove [definition, in lib.Esets]
remove [definition, in Maps]
res [inductive, in lib.Nonterm]
Rfi_Done [constructor, in Machine]
Rfi_Step [constructor, in Machine]
R_Done [constructor, in Machine]
R_Step [constructor, in Machine]
S
sel [definition, in lib.Emaps]
sel [axiom, in Maps]
sel [definition, in Maps]
sel_bonanza [lemma, in AndersenSound]
sel_bonanza' [lemma, in AndersenSound]
sel_init [axiom, in Maps]
sel_init [lemma, in lib.Emaps]
sel_init [lemma, in Maps]
sel_upd [lemma, in lib.Emaps]
sel_upd [lemma, in Maps]
sel_upd [axiom, in Maps]
sel_updated [lemma, in AndersenSound]
sel_updated' [lemma, in AndersenSound]
sel_upd_eq [axiom, in Maps]
sel_upd_eq [lemma, in Maps]
sel_upd_eq [lemma, in lib.Emaps]
sel_upd_neq [lemma, in lib.Emaps]
sel_upd_neq [lemma, in Maps]
sel_upd_neq [axiom, in Maps]
sel_write_valid [lemma, in AndersenIter]
seq [definition, in lib.Esets]
seq_refl [lemma, in lib.Esets]
seq_sym [lemma, in lib.Esets]
seq_trans [lemma, in lib.Esets]
seq_union_left [lemma, in lib.Esets]
seq_union_right [lemma, in lib.Esets]
set [definition, in lib.Esets]
set [axiom, in Maps]
SET [module, in Maps]
set [definition, in Maps]
setall [definition, in lib.Esets]
setexists [definition, in lib.Esets]
set_grew [lemma, in AndersenIter]
site_bounded [definition, in AndersenIter]
size [definition, in AndersenIter]
size_approxStrict [lemma, in AndersenIter]
size_bounded [lemma, in AndersenIter]
state [inductive, in Pointer]
step_Allocate [lemma, in AndersenSound]
step_Copy [lemma, in AndersenSound]
step_Goto [lemma, in AndersenSound]
step_Read [lemma, in AndersenSound]
step_Write [lemma, in AndersenSound]
sum_plus1 [lemma, in AndersenIter]
sum_plus2 [lemma, in AndersenIter]
T
Tactics [library]
Tactics [library]
Timeout [constructor, in lib.Nonterm]
true [definition, in lib.Esets]
U
union [axiom, in Maps]
union [definition, in Maps]
union [definition, in lib.Esets]
union_ass [lemma, in lib.Esets]
union_comm [lemma, in lib.Esets]
union_congr [lemma, in lib.Esets]
union_empty_left [lemma, in lib.Esets]
union_empty_right [lemma, in lib.Esets]
union_idempotent [lemma, in Maps]
union_idempotent [axiom, in Maps]
union_idempotent [lemma, in lib.Esets]
union_idempotent' [lemma, in Maps]
union_idempotent' [lemma, in lib.Esets]
Unknown [constructor, in Pointer]
upd [definition, in Maps]
upd [axiom, in Maps]
upd [definition, in lib.Emaps]
upd_self [lemma, in lib.Emaps]
upd_self [axiom, in Maps]
upd_self [lemma, in Maps]
V
valid [inductive, in AndersenIter]
valid_irrel [axiom, in AndersenIter]
var [definition, in Pointer]
VarMap [module, in Pointer]
VarSet [module, in AndersenIter]
var_bounded [definition, in AndersenIter]
W
Write [constructor, in Pointer]
write_var [lemma, in AndersenIter]
Axiom Index
A
add [in Maps]
D
dom [in lib.Emaps]
dom [in Maps]
dom [in lib.Esets]
dom_eq_dec [in Maps]
dom_eq_dec [in lib.Emaps]
dom_eq_dec [in lib.Esets]
E
elems [in Maps]
elems_ok [in Maps]
elems_remove [in Maps]
empty [in Maps]
ext_eq [in lib.Emaps]
ext_eq [in Maps]
I
In [in Maps]
incl [in Maps]
incl_empty [in Maps]
incl_false [in Maps]
incl_In [in Maps]
incl_ok [in Maps]
incl_refl [in Maps]
incl_trans [in Maps]
incl_union_left [in Maps]
incl_union_right [in Maps]
init [in Maps]
intersect [in Maps]
In_add [in Maps]
In_add_eq [in Maps]
In_add_neq [in Maps]
In_empty [in Maps]
In_intersect [in Maps]
In_intersect' [in Maps]
In_remove [in Maps]
In_union [in Maps]
In_union' [in Maps]
M
map [in Maps]
R
remove [in Maps]
S
sel [in Maps]
sel_init [in Maps]
sel_upd [in Maps]
sel_upd_eq [in Maps]
sel_upd_neq [in Maps]
set [in Maps]
U
union [in Maps]
union_idempotent [in Maps]
upd [in Maps]
upd_self [in Maps]
V
valid_irrel [in AndersenIter]
Lemma Index
A
abstractAllocate [in AndersenSound]
abstractAllocate' [in AndersenSound]
abstractCopy [in AndersenSound]
abstractCopy' [in AndersenSound]
abstractRead [in AndersenSound]
abstractRead' [in AndersenSound]
abstractWrite [in AndersenSound]
abstractWrite' [in AndersenSound]
abstract_followPath_expand [in AndersenSound]
abstract_followPath_incl [in AndersenSound]
abstract_followPath_read [in AndersenSound]
abstract_followPath_write_preserve [in AndersenSound]
abstract_followPath_write_var [in AndersenSound]
abstract_follow_conjoin [in AndersenSound]
aexec' [in AndersenIter]
ainstr_widen [in AndersenIter]
allocate_site [in AndersenIter]
allocate_var [in AndersenIter]
allocation_site_model_is_conservative [in AndersenSound]
allocation_site_step [in AndersenSound]
allPaths_step [in AndersenSound]
allPaths_write [in AndersenSound]
AllS_deduce [in ListUtil]
AllS_In [in ListUtil]
AllS_not [in ListUtil]
AllS_not_dec [in ListUtil]
andersen_sound [in AndersenSound]
andersen_start [in AndersenSound]
approxStrict_approx [in AndersenIter]
approxStrict_trans [in AndersenIter]
approxStrict_wf [in AndersenIter]
approxStrict_wf' [in AndersenIter]
approx_init [in AndersenIter]
approx_init' [in AndersenIter]
approx_refl [in AndersenIter]
approx_refl' [in AndersenIter]
approx_trans [in AndersenIter]
approx_trans' [in AndersenIter]
C
card [in AndersenIter]
compatible_write_var [in AndersenSound]
copy_var [in AndersenIter]
E
elems_ok [in lib.Esets]
elems_ok [in Maps]
elems_remove [in Maps]
elems_remove [in lib.Esets]
F
fixed_point_ok [in Machine]
flowInsensitive_is_conservative [in Machine]
fold_In_union [in AndersenIter]
fold_In_unionv [in AndersenIter]
fold_left_sum [in AndersenSound]
fold_monotone_gen [in lib.Esets]
fold_monotone_1 [in lib.Esets]
fold_monotone_2 [in lib.Esets]
fold_plus_ge [in AndersenIter]
fold_plus_gt [in AndersenIter]
followPath_case [in AndersenSound]
followPath_goto [in AndersenSound]
followPath_nothing_new [in AndersenSound]
followPath_read [in AndersenSound]
followPath_S [in AndersenSound]
followPath_SO [in AndersenSound]
followPath_SO' [in AndersenSound]
followPath_swap_var [in AndersenSound]
followPath_write_var [in AndersenSound]
follow_conjoin [in AndersenSound]
I
incl_add [in lib.Esets]
incl_add [in AndersenIter]
incl_add2 [in AndersenIter]
incl_add3 [in AndersenIter]
incl_cardinality [in AndersenIter]
incl_cardinality' [in AndersenIter]
incl_elems [in AndersenIter]
incl_empty [in Maps]
incl_empty [in lib.Esets]
incl_empty_empty [in lib.Esets]
incl_false [in Maps]
incl_false [in lib.Esets]
incl_fold1 [in AndersenIter]
incl_fold2 [in AndersenIter]
incl_fold3 [in AndersenIter]
incl_fold3' [in AndersenIter]
incl_fold_read [in AndersenIter]
incl_fold_union [in AndersenSound]
incl_fold_union' [in AndersenSound]
incl_fold_union_read [in AndersenSound]
incl_fold_write [in AndersenIter]
incl_gt [in AndersenIter]
incl_In [in Maps]
incl_In [in lib.Esets]
incl_intersect2 [in Andersen]
incl_length [in AndersenIter]
incl_ok [in lib.Esets]
incl_ok [in Maps]
incl_refl [in Maps]
incl_refl [in lib.Esets]
incl_S [in AndersenIter]
incl_trans [in lib.Esets]
incl_trans [in Maps]
incl_trans' [in AndersenIter]
incl_union [in AndersenIter]
incl_union2 [in AndersenIter]
incl_union_left [in lib.Esets]
incl_union_left [in Maps]
incl_union_right [in Maps]
incl_union_right [in lib.Esets]
incl_valid_read [in AndersenIter]
incl_valid_write [in AndersenIter]
incl_write_bonanza [in AndersenSound]
incl_write_bonanza' [in AndersenSound]
increasing [in AndersenIter]
increasing' [in AndersenIter]
In_add [in lib.Esets]
In_add [in Maps]
In_add_already [in lib.Esets]
In_add_eq [in Maps]
In_add_eq [in lib.Esets]
In_add_neq [in lib.Esets]
In_add_neq [in Maps]
in_aprogram [in AndersenIter]
in_aprogram' [in AndersenIter]
In_dec [in lib.Esets]
In_empty [in lib.Esets]
In_empty [in Maps]
In_eq [in lib.Esets]
In_intersect [in lib.Esets]
In_intersect [in Maps]
In_intersect' [in lib.Esets]
In_intersect' [in Maps]
In_list [in lib.Esets]
In_map [in AndersenIter]
In_remove [in lib.Esets]
In_remove [in Maps]
In_union [in lib.Esets]
In_union [in Maps]
In_union' [in Maps]
In_union_left [in lib.Esets]
In_union_right [in lib.Esets]
iterate_approx [in Machine]
iterate_pick [in Machine]
iterate_pick' [in Machine]
iterate_pick_cp [in Machine]
M
monotonic [in AndersenIter]
monotonic' [in AndersenIter]
mult_le [in AndersenIter]
N
nth_spec_implies_In [in ListUtil]
P
pathCompatible_symm [in AndersenSound]
pdiv2_correct [in lib.Nonterm]
pdiv2_correct2 [in lib.Nonterm]
pdiv2_correct3 [in lib.Nonterm]
R
reachable_a [in AndersenIter]
read_var [in AndersenIter]
S
sel_bonanza [in AndersenSound]
sel_bonanza' [in AndersenSound]
sel_init [in lib.Emaps]
sel_init [in Maps]
sel_upd [in lib.Emaps]
sel_upd [in Maps]
sel_updated [in AndersenSound]
sel_updated' [in AndersenSound]
sel_upd_eq [in Maps]
sel_upd_eq [in lib.Emaps]
sel_upd_neq [in lib.Emaps]
sel_upd_neq [in Maps]
sel_write_valid [in AndersenIter]
seq_refl [in lib.Esets]
seq_sym [in lib.Esets]
seq_trans [in lib.Esets]
seq_union_left [in lib.Esets]
seq_union_right [in lib.Esets]
set_grew [in AndersenIter]
size_approxStrict [in AndersenIter]
size_bounded [in AndersenIter]
step_Allocate [in AndersenSound]
step_Copy [in AndersenSound]
step_Goto [in AndersenSound]
step_Read [in AndersenSound]
step_Write [in AndersenSound]
sum_plus1 [in AndersenIter]
sum_plus2 [in AndersenIter]
U
union_ass [in lib.Esets]
union_comm [in lib.Esets]
union_congr [in lib.Esets]
union_empty_left [in lib.Esets]
union_empty_right [in lib.Esets]
union_idempotent [in Maps]
union_idempotent [in lib.Esets]
union_idempotent' [in Maps]
union_idempotent' [in lib.Esets]
upd_self [in lib.Emaps]
upd_self [in Maps]
W
write_var [in AndersenIter]
Constructor Index
A
AbsAllocate [in AndersenModel]
AbsCopy [in AndersenModel]
AbsRead [in AndersenModel]
AbsWrite [in AndersenModel]
Allocate [in Pointer]
APath_Done [in AndersenSound]
C
Copy [in Pointer]
E
eO [in lib.Nonterm]
eSS [in lib.Nonterm]
G
Goto [in Pointer]
N
NotAliased [in Pointer]
O
Ok [in lib.Nonterm]
P
Path_Done [in AndersenSound]
R
Read [in Pointer]
Rfi_Done [in Machine]
Rfi_Step [in Machine]
R_Done [in Machine]
R_Step [in Machine]
T
Timeout [in lib.Nonterm]
U
Unknown [in Pointer]
W
Write [in Pointer]
Inductive Index
A
abstract_followPath [in AndersenSound]
abstract_instruction [in AndersenModel]
abstract_state [in AndersenModel]
approxStrict [in AndersenIter]
approx' [in AndersenIter]
C
compatible [in AndersenSound]
F
followPath [in AndersenSound]
I
instruction [in Pointer]
isEven [in lib.Nonterm]
M
mustNotAlias_answer [in Pointer]
R
reachable [in Machine]
reachable_flowInsensitive [in Machine]
res [in lib.Nonterm]
S
state [in Pointer]
V
valid [in AndersenIter]
Definition Index
A
abstractProgram [in AndersenModel]
abstractProgram' [in AndersenModel]
abstract_exec [in AndersenModel]
abstract_initState [in AndersenSound]
add [in Maps]
add [in lib.Esets]
aexec [in AndersenIter]
ainitState [in AndersenIter]
ainstruction [in AndersenIter]
allocation_site [in AndersenModel]
allPaths [in AndersenSound]
AllS_dec [in ListUtil]
AllS_dec_some [in ListUtil]
andersen [in Andersen]
approx [in AndersenIter]
approxStrict_dec [in AndersenIter]
approx_dec [in AndersenIter]
aprogram [in AndersenIter]
aprogram' [in AndersenIter]
astate [in AndersenIter]
B
bound [in AndersenIter]
C
cardinality [in AndersenIter]
cardinality_atLeast [in AndersenIter]
D
distinct [in AndersenIter]
distinctify [in AndersenIter]
dom [in AndersenModel]
dom [in lib.Emaps]
dom [in Maps]
dom [in Maps]
dom [in AndersenIter]
dom [in Pointer]
dom [in AndersenModel]
dom [in lib.Esets]
dom [in Pointer]
dom [in Maps]
dom [in Maps]
dom_eq_dec [in Pointer]
E
elems [in lib.Esets]
elems [in Maps]
empty [in Maps]
empty [in lib.Esets]
exec [in Pointer]
F
fixed_point [in AndersenIter]
fixed_point [in Machine]
fixed_point' [in AndersenIter]
fold [in lib.Esets]
I
In [in Maps]
In [in lib.Esets]
incl [in lib.Esets]
incl [in Maps]
incl_eq_dec [in ListUtil]
init [in Maps]
init [in lib.Emaps]
initState [in Pointer]
ins_sites [in AndersenIter]
ins_vars [in AndersenIter]
intersect [in lib.Esets]
intersect [in Maps]
In_eq_dec [in ListUtil]
iterate [in Machine]
M
map [in lib.Emaps]
map [in Maps]
mustNotAlias [in Pointer]
mustNotAlias_procedure [in Pointer]
N
neq_nat_dec [in AndersenIter]
nil [in lib.Esets]
nil [in lib.Esets]
nil [in lib.Esets]
P
pathCompatible [in AndersenSound]
pdiv2 [in lib.Nonterm]
progSites [in AndersenIter]
progVars [in AndersenIter]
pSites [in AndersenIter]
pVars [in AndersenIter]
R
remove [in lib.Esets]
remove [in Maps]
S
sel [in lib.Emaps]
sel [in Maps]
seq [in lib.Esets]
set [in lib.Esets]
set [in Maps]
setall [in lib.Esets]
setexists [in lib.Esets]
site_bounded [in AndersenIter]
size [in AndersenIter]
T
true [in lib.Esets]
U
union [in Maps]
union [in lib.Esets]
upd [in Maps]
upd [in lib.Emaps]
V
var [in Pointer]
var_bounded [in AndersenIter]
Module Index
A
AllocMap [in AndersenModel]
AllocSet [in AndersenModel]
E
EQ [in lib.Esets]
EQ [in Maps]
EQ [in lib.Emaps]
F
FuncMap [in Maps]
L
ListSet [in Maps]
M
MakeMap [in lib.Emaps]
MakeSet [in lib.Esets]
MAP [in Maps]
N
NatEq [in Pointer]
NatMap [in Pointer]
S
SET [in Maps]
V
VarMap [in Pointer]
VarSet [in AndersenIter]
Library Index
A
Andersen
AndersenIter
AndersenModel
AndersenSound
E
Emaps
Esets
L
ListUtil
M
Machine
Maps
N
Nonterm
P
Pointer
T
Tactics
Tactics
| Global Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(394 entries) |
| Axiom Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(47 entries) |
| Lemma Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(191 entries) |
| Constructor Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(21 entries) |
| Inductive Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(15 entries) |
| Definition Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(92 entries) |
| Module Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(15 entries) |
| Library Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(13 entries) |
This page has been generated by coqdoc