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