| 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 | _ | other | (440 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 | _ | other | (4 entries) |
| Variable 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 | _ | other | (9 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 | _ | other | (22 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 | _ | other | (170 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 | _ | other | (13 entries) |
| Projection 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 | _ | other | (7 entries) |
| Instance 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 | _ | other | (15 entries) |
| Section 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 | _ | other | (6 entries) |
| Abbreviation 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 | _ | other | (1 entry) |
| 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 | _ | other | (191 entries) |
| Record 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 | _ | other | (2 entries) |
Global Index
A
add_another [lemma, in Verif_triang]add_list_sublist_bounds [lemma, in Verif_triang]
add_list_nonneg [lemma, in Verif_triang]
add_list_app [lemma, in Verif_triang]
add_list_decreasing_eq [lemma, in Verif_triang]
add_list_decreasing_eq_alt [lemma, in Verif_triang]
add_list [definition, in Verif_triang]
append_spec [definition, in Verif_append1]
B
Bib [library]body_incr [lemma, in Verif_hash]
body_incr_field_address_lemma [lemma, in Verif_hash]
body_incr_list [lemma, in Verif_hash]
body_get [lemma, in Verif_hash]
body_new_table [lemma, in Verif_hash]
body_new_table_helper [lemma, in Verif_hash]
body_new_cell [lemma, in Verif_hash]
body_copy_string [lemma, in Verif_hash]
body_hash [lemma, in Verif_hash]
body_main [lemma, in VSU_main2]
body_append_alter2 [lemma, in Verif_append2]
body_exit [axiom, in VSU_stdlib]
body_free [axiom, in VSU_stdlib]
body_malloc [axiom, in VSU_stdlib]
body_exit [lemma, in VSU_stdlib2]
body_free [lemma, in VSU_stdlib2]
body_malloc [lemma, in VSU_stdlib2]
body_surely_malloc [lemma, in VSU_stack]
body_newstack [lemma, in VSU_stack]
body_push [lemma, in VSU_stack]
body_pop [lemma, in VSU_stack]
body_main [lemma, in Verif_triang]
body_pop_and_add [lemma, in Verif_triang]
body_pop_and_add [lemma, in Verif_triang]
body_push_increasing [lemma, in Verif_triang]
body_append_alter1 [lemma, in Verif_append1]
body_append [lemma, in Verif_append1]
body_main [lemma, in Verif_sumarray]
body_sumarray [lemma, in Verif_sumarray]
body_reverse_step [lemma, in Verif_reverse]
body_reverse [lemma, in Verif_reverse]
body_triang [lemma, in VSU_triang]
body_pop_and_add [lemma, in VSU_triang]
body_push_increasing [lemma, in VSU_triang]
body_main [lemma, in VSU_main]
body_strcmp [lemma, in Verif_strlib]
body_example_call_strcpy [lemma, in Verif_strlib]
body_strcpy [lemma, in Verif_strlib]
body_strlen [lemma, in Verif_strlib]
body_newstack [lemma, in Verif_stack]
body_push [lemma, in Verif_stack]
body_pop [lemma, in Verif_stack]
C
cancel_example [lemma, in Verif_strlib]CompSpecs [instance, in Verif_hash]
Compspecs [instance, in VSU_main2]
CompSpecs [instance, in VSU_stdlib]
CompSpecs [instance, in VSU_stdlib2]
CompSpecs [instance, in VSU_stack]
CompSpecs [instance, in Verif_triang]
CompSpecs [instance, in Verif_append1]
CompSpecs [instance, in Verif_sumarray]
CompSpecs [instance, in Verif_reverse]
CompSpecs [instance, in VSU_triang]
Compspecs [instance, in VSU_main]
CompSpecs [instance, in VSU_main]
CompSpecs [instance, in Verif_strlib]
CompSpecs [instance, in Verif_stack]
copy_string_spec [definition, in Verif_hash]
coreVSU [definition, in VSU_main2]
coreVSU [definition, in VSU_main]
COUNT_TABLE.gso [axiom, in Hashfun]
COUNT_TABLE.gss [axiom, in Hashfun]
COUNT_TABLE.gempty [axiom, in Hashfun]
COUNT_TABLE.incr [axiom, in Hashfun]
COUNT_TABLE.get [axiom, in Hashfun]
COUNT_TABLE.empty [axiom, in Hashfun]
COUNT_TABLE.key [axiom, in Hashfun]
COUNT_TABLE.table [axiom, in Hashfun]
COUNT_TABLE [module, in Hashfun]
D
data_at_thashtable_tarray [lemma, in Verif_hash]data_at_isptr_example2 [lemma, in Verif_reverse]
data_at_isptr_example1 [lemma, in Verif_reverse]
data_at_Vundef_example [lemma, in Verif_strlib]
data_at_Vundef_example [lemma, in Verif_strlib]
decreasing_Z1 [definition, in Verif_triang]
decreasing_Z1_aux [definition, in Verif_triang]
decreasing_Z [definition, in Verif_triang]
decreasing_nat [definition, in Verif_triang]
demonstrate_cstring2 [lemma, in Verif_strlib]
demonstrate_cstring1 [lemma, in Verif_strlib]
Digression [module, in VSU_stdlib2]
Digression.N [definition, in VSU_stdlib2]
Digression.N_eq [definition, in VSU_stdlib2]
Digression.N' [definition, in VSU_stdlib2]
Digression.N'' [definition, in VSU_stdlib2]
E
empty_table [definition, in Hashfun]emp_lbseg [lemma, in Verif_append2]
emp_wlseg [lemma, in Verif_append2]
emp_wand_emp_left [lemma, in Verif_append2]
emp_wand_emp_right [lemma, in Verif_append2]
EqDec_string [instance, in Hashfun]
example_field_at_data_at''' [lemma, in Verif_hash]
example_field_at_data_at'' [lemma, in Verif_hash]
example_field_at_data_at' [lemma, in Verif_hash]
example_field_at_data_at [lemma, in Verif_hash]
example_split_struct [lemma, in Verif_hash]
example_call_strcpy_spec [definition, in Verif_strlib]
exit_spec [definition, in Spec_stdlib]
F
four_contents [definition, in Verif_sumarray]freelistrep [definition, in VSU_stdlib2]
freelistrep_valid_pointer [lemma, in VSU_stdlib2]
freelistrep_local_prop [lemma, in VSU_stdlib2]
free_spec_sub [lemma, in Spec_stdlib]
free_spec [definition, in Spec_stdlib]
free_spec_sz [definition, in Spec_stdlib]
free_spec_example [definition, in Verif_stack]
FunTable [module, in Hashfun]
FunTable.empty [definition, in Hashfun]
FunTable.gempty [lemma, in Hashfun]
FunTable.get [definition, in Hashfun]
FunTable.gso [lemma, in Hashfun]
FunTable.gss [lemma, in Hashfun]
FunTable.incr [definition, in Hashfun]
FunTable.key [definition, in Hashfun]
FunTable.table [definition, in Hashfun]
G
get_spec [definition, in Verif_hash]Gprog [definition, in Verif_hash]
Gprog [definition, in Verif_triang]
Gprog [definition, in Verif_append1]
Gprog [definition, in Verif_sumarray]
Gprog [definition, in Verif_reverse]
Gprog [definition, in Verif_strlib]
Gprog [definition, in Verif_stack]
H
hashfun [definition, in Hashfun]Hashfun [library]
hashfun_snoc [lemma, in Hashfun]
hashfun_aux_snoc [lemma, in Hashfun]
hashfun_inrange [lemma, in Hashfun]
hashfun_aux [definition, in Hashfun]
hashtable_rep_valid_pointer [lemma, in Verif_hash]
hashtable_rep_local_facts [lemma, in Verif_hash]
hashtable_rep [definition, in Verif_hash]
hashtable_get_unfold [lemma, in Hashfun]
hashtable_incr [definition, in Hashfun]
hashtable_get [definition, in Hashfun]
hashtable_contents [definition, in Hashfun]
hash_spec [definition, in Verif_hash]
Hello [definition, in Verif_strlib]
Hello' [definition, in Verif_strlib]
I
implies_and_adjoint [lemma, in Verif_append2]incr_spec [definition, in Verif_hash]
incr_list_spec [definition, in Verif_hash]
initialize [lemma, in VSU_stdlib]
initialize [lemma, in VSU_stdlib2]
IntHashTable [module, in Hashfun]
IntHashTable.empty [definition, in Hashfun]
IntHashTable.empty_invariant [lemma, in Hashfun]
IntHashTable.gempty [lemma, in Hashfun]
IntHashTable.get [definition, in Hashfun]
IntHashTable.gso [lemma, in Hashfun]
IntHashTable.gss [lemma, in Hashfun]
IntHashTable.hashtable_invariant [definition, in Hashfun]
IntHashTable.incr [definition, in Hashfun]
IntHashTable.incr_invariant [lemma, in Hashfun]
IntHashTable.key [definition, in Hashfun]
IntHashTable.table [definition, in Hashfun]
Int_repr_eq_mod [lemma, in Hashfun]
iter_sepcon_split3 [lemma, in Verif_hash]
iter_sepcon_listrep_local_facts [lemma, in Verif_hash]
L
lbseg [definition, in Verif_append2]lbseg_lbseg [lemma, in Verif_append2]
listboxrep [definition, in Verif_hash]
listboxrep [definition, in Verif_append2]
listboxrep_traverse32 [lemma, in Verif_hash]
listboxrep_traverse [lemma, in Verif_hash]
listbox_lbseg [lemma, in Verif_append2]
listcell_fold [lemma, in Verif_hash]
listrep [definition, in Verif_hash]
listrep [definition, in VSU_stack]
listrep [definition, in Verif_triang]
listrep [definition, in Verif_append1]
listrep [definition, in Verif_reverse]
listrep [definition, in Verif_stack]
listrep_traverse_finish [lemma, in Verif_hash]
listrep_traverse_step_example [lemma, in Verif_hash]
listrep_traverse_step [lemma, in Verif_hash]
listrep_traverse_start [lemma, in Verif_hash]
listrep_fold [lemma, in Verif_hash]
listrep_valid_pointer [lemma, in Verif_hash]
listrep_local_prop [lemma, in Verif_hash]
listrep_valid_pointer [lemma, in VSU_stack]
listrep_local_prop [lemma, in VSU_stack]
listrep_valid_pointer [lemma, in Verif_triang]
listrep_local_prop [lemma, in Verif_triang]
listrep_nonnull [lemma, in Verif_append1]
listrep_null [lemma, in Verif_append1]
listrep_valid_pointer [lemma, in Verif_append1]
listrep_local_facts [lemma, in Verif_append1]
listrep_len_ge2_address_different [lemma, in Verif_reverse]
listrep_len_ge2_fact [lemma, in Verif_reverse]
listrep_valid_pointer [lemma, in Verif_reverse]
listrep_valid_pointer_example [lemma, in Verif_reverse]
listrep_local_facts [lemma, in Verif_reverse]
listrep_facts_example [lemma, in Verif_reverse]
listrep_facts_example [lemma, in Verif_reverse]
listrep_valid_pointer [lemma, in Verif_stack]
listrep_local_prop [lemma, in Verif_stack]
listrep2lseg [lemma, in Verif_append1]
list_cell_valid_pointer [definition, in Verif_hash]
list_cell_local_facts [definition, in Verif_hash]
list_cell [definition, in Verif_hash]
list_incr [definition, in Hashfun]
list_get [definition, in Hashfun]
loopy_lseg_no_connection [lemma, in Verif_append1]
loopy_lseg_not_bad [lemma, in Verif_append1]
lseg [definition, in Verif_append1]
lseg_lseg_inv [lemma, in Verif_append1]
lseg_listrep_equiv [lemma, in Verif_append1]
lseg_list [lemma, in Verif_append1]
lseg_lseg [lemma, in Verif_append1]
lseg_maybe_loop [lemma, in Verif_append1]
lseg2listrep [lemma, in Verif_append1]
lseg2wlseg [lemma, in Verif_append2]
M
M [definition, in VSU_main2]M [axiom, in VSU_stdlib]
M [definition, in VSU_stdlib2]
M [definition, in VSU_main]
MainComp [definition, in VSU_main2]
MainComp [definition, in VSU_main]
Main_Gprog [definition, in VSU_main2]
Main_imports [definition, in VSU_main2]
main_spec [definition, in VSU_main2]
main_spec [definition, in Verif_triang]
main_spec [definition, in Verif_sumarray]
Main_Gprog [definition, in VSU_main]
Main_imports [definition, in VSU_main]
main_spec [definition, in VSU_main]
make_mem_mgr [axiom, in VSU_stdlib]
MallocFreeAPD [record, in Spec_stdlib]
MallocFreeASI [definition, in Spec_stdlib]
MallocFreeASI [section, in Spec_stdlib]
MallocFreeASI.M [variable, in Spec_stdlib]
MallocFreeVSU [definition, in VSU_stdlib]
MallocFreeVSU [definition, in VSU_stdlib2]
malloc_spec_sub [lemma, in Spec_stdlib]
malloc_spec [definition, in Spec_stdlib]
malloc_token_local_facts [lemma, in Spec_stdlib]
malloc_token_valid_pointer [lemma, in Spec_stdlib]
malloc_token [definition, in Spec_stdlib]
malloc_spec_sz [definition, in Spec_stdlib]
malloc_token_sz_local_facts [projection, in Spec_stdlib]
malloc_token_sz_valid_pointer [projection, in Spec_stdlib]
malloc_token_sz [projection, in Spec_stdlib]
malloc_token_sz_local_facts [lemma, in VSU_stdlib2]
malloc_token_sz_valid_pointer [lemma, in VSU_stdlib2]
malloc_token_sz [definition, in VSU_stdlib2]
malloc_spec_example [definition, in Verif_stack]
mem_mgr [projection, in Spec_stdlib]
mem_mgr [definition, in VSU_stdlib2]
MFGprog [definition, in VSU_stdlib]
MFGprog [definition, in VSU_stdlib2]
MFVprog [definition, in VSU_stdlib]
MFVprog [definition, in VSU_stdlib2]
MF_E [definition, in VSU_stdlib]
MF_globals [definition, in VSU_stdlib]
MF_internal_specs [definition, in VSU_stdlib]
MF_imported_specs [definition, in VSU_stdlib]
MF_ASI [definition, in VSU_stdlib]
MF_Externs [definition, in VSU_stdlib2]
MF_globals [definition, in VSU_stdlib2]
MF_internal_specs [definition, in VSU_stdlib2]
MF_imported_specs [definition, in VSU_stdlib2]
MF_ASI [definition, in VSU_stdlib2]
modus_ponens_wand_from_adjoint [lemma, in Verif_append2]
N
N [definition, in VSU_stdlib2]N [definition, in Hashfun]
nat_sub_add_yuck [lemma, in Verif_triang]
newstack_spec [definition, in Verif_triang]
newstack_spec [definition, in Spec_stack]
newstack_spec [definition, in Verif_stack]
new_cell_spec [definition, in Verif_hash]
new_table_spec [definition, in Verif_hash]
nt_lseg_list [lemma, in Verif_append1]
nt_lseg_nt_lseg [lemma, in Verif_append1]
nt_lseg [definition, in Verif_append1]
N_eq [definition, in VSU_stdlib2]
N_eq [lemma, in Hashfun]
P
placeholder_spec [abbreviation, in VSU_stdlib]pop_and_add_spec [definition, in Verif_triang]
pop_spec [definition, in Verif_triang]
pop_spec [definition, in Spec_stack]
pop_and_add_spec [definition, in VSU_triang]
pop_spec [definition, in Verif_stack]
Postscript [library]
Preface [library]
prog_correct [lemma, in Verif_sumarray]
push_increasing_spec [definition, in Verif_triang]
push_spec [definition, in Verif_triang]
push_spec [definition, in Spec_stack]
push_increasing_spec [definition, in VSU_triang]
push_spec [definition, in Verif_stack]
R
release_needed [definition, in Preface]reverse_spec [definition, in Verif_reverse]
S
semax_func_cons_malloc_aux [lemma, in VSU_stdlib]singleton_wlseg [lemma, in Verif_append2]
singleton_nt_lseg' [lemma, in Verif_append1]
singleton_nt_lseg [lemma, in Verif_append1]
singleton_lseg [lemma, in Verif_append1]
Spec_stdlib [library]
Spec_stack [library]
Spec_triang [library]
STACK [definition, in VSU_main2]
STACK [definition, in VSU_stack]
stack [definition, in VSU_stack]
stack [definition, in Verif_triang]
STACK [definition, in VSU_main]
stack [definition, in Verif_stack]
StackAPD [record, in Spec_stack]
StackASI [definition, in Spec_stack]
StackASI [section, in Spec_stack]
StackASI.M [variable, in Spec_stack]
StackASI.STACK [variable, in Spec_stack]
stackrep [projection, in Spec_stack]
stackrep_valid_pointer [projection, in Spec_stack]
stackrep_local_facts [projection, in Spec_stack]
stacktriangVSU [lemma, in VSU_main2]
stacktriangVSU [definition, in VSU_main]
stacktriangVSU1 [definition, in VSU_main2]
stacktriangVSU1 [definition, in VSU_main]
StackVSU [lemma, in VSU_stack]
stackVSU [definition, in VSU_main]
Stack_Vprog [definition, in VSU_stack]
Stack_Gprog [definition, in VSU_stack]
Stack_internals [definition, in VSU_stack]
Stack_private [definition, in VSU_stack]
Stack_imports [definition, in VSU_stack]
stack_valid_pointer [lemma, in VSU_stack]
stack_local_prop [lemma, in VSU_stack]
Stack_VSU.M [variable, in VSU_stack]
Stack_VSU [section, in VSU_stack]
stack_valid_pointer [lemma, in Verif_triang]
stack_local_prop [lemma, in Verif_triang]
stack_valid_pointer [lemma, in Verif_stack]
stack_local_prop [lemma, in Verif_stack]
strcmp_spec [definition, in Verif_hash]
strcmp_spec [definition, in Verif_strlib]
strcpy_spec [definition, in Verif_hash]
strcpy_else_clause [lemma, in Verif_strlib]
strcpy_then_clause [lemma, in Verif_strlib]
strcpy_spec [definition, in Verif_strlib]
StringDemo [section, in Verif_strlib]
StringDemo.p [variable, in Verif_strlib]
stringlit_1_contents [definition, in Verif_strlib]
string_to_list_byte [definition, in Verif_strlib]
strlen_spec [definition, in Verif_hash]
strlen_spec [definition, in Verif_strlib]
struct_list_valid_pointer_example [lemma, in Verif_reverse]
sumarray_spec [definition, in Verif_sumarray]
sum_Z_app [lemma, in Verif_sumarray]
sum_Z [definition, in Verif_sumarray]
surely_malloc_spec [definition, in VSU_stack]
T
tcell [definition, in Verif_hash]tcell [definition, in VSU_stdlib2]
thashtable [definition, in Verif_hash]
TriangASI [definition, in Spec_triang]
TriangASI [section, in Spec_triang]
TriangASI.M [variable, in Spec_triang]
TriangVSU [definition, in VSU_triang]
triangVSU [definition, in VSU_main]
triang_spec [definition, in Spec_triang]
Triang_VSU.stackrep_nil [variable, in VSU_triang]
Triang_Vprog [definition, in VSU_triang]
Triang_Gprog [definition, in VSU_triang]
Triang_internals [definition, in VSU_triang]
Triang_imports [definition, in VSU_triang]
Triang_private [definition, in VSU_triang]
Triang_VSU.STACK [variable, in VSU_triang]
Triang_VSU.M [variable, in VSU_triang]
Triang_VSU [section, in VSU_triang]
t_list_box [definition, in Verif_append2]
t_list [definition, in Verif_append1]
t_list [definition, in Verif_reverse]
U
uncurry [definition, in Verif_hash]Unnamed_thm6 [definition, in Verif_hash]
Unnamed_thm5 [definition, in Verif_hash]
Unnamed_thm4 [definition, in Verif_hash]
Unnamed_thm3 [definition, in Verif_hash]
Unnamed_thm2 [definition, in Verif_hash]
Unnamed_thm1 [definition, in Verif_hash]
Unnamed_thm0 [definition, in Verif_hash]
Unnamed_thm [definition, in Verif_hash]
Unnamed_thm [definition, in Verif_sumarray]
Unnamed_thm0 [definition, in Verif_strlib]
Unnamed_thm [definition, in Verif_strlib]
Unnamed_thm [definition, in Preface]
Unnamed_thm [definition, in Preface]
V
Verif_append1 [library]Verif_triang [library]
Verif_sumarray [library]
Verif_stack [library]
Verif_hash [library]
Verif_append2 [library]
Verif_reverse [library]
Verif_strlib [library]
Vprog [definition, in Verif_hash]
Vprog [definition, in VSU_main2]
Vprog [definition, in Verif_triang]
Vprog [definition, in Verif_append1]
Vprog [definition, in Verif_sumarray]
Vprog [definition, in Verif_reverse]
Vprog [definition, in VSU_main]
Vprog [definition, in Verif_strlib]
Vprog [definition, in Verif_stack]
VSU_stdlib [library]
VSU_stack [library]
VSU_stdlib2 [library]
VSU_intro [library]
VSU_triang [library]
VSU_main2 [library]
VSU_main [library]
W
wandQ_frame_ver_mpred [lemma, in Verif_append2]wandQ_frame_elim_mpred [lemma, in Verif_append2]
wand_frame_ver_from_adjoint_and_modus_ponens [lemma, in Verif_append2]
wand_derives_from_adjoint_and_modus_ponens [lemma, in Verif_append2]
wand_trivial [lemma, in Verif_append2]
WholeComp [lemma, in VSU_main2]
WholeComp [lemma, in VSU_main]
WholeProgSafe [lemma, in VSU_main2]
WholeProgSafe [lemma, in VSU_main]
whole_prog [definition, in VSU_main2]
whole_prog [definition, in VSU_main]
wlseg [definition, in Verif_append2]
wlseg_weird [lemma, in Verif_append2]
wlseg_listrep_equiv [lemma, in Verif_append2]
wlseg_nullval [lemma, in Verif_append2]
wlseg_list [lemma, in Verif_append2]
wlseg_wlseg [lemma, in Verif_append2]
wlseg2lseg_nullval [lemma, in Verif_append2]
Z
Zinduction [lemma, in Verif_triang]Zlength_hashtable_incr [lemma, in Hashfun]
Z_sub_add_ok [lemma, in Verif_triang]
Module Index
C
COUNT_TABLE [in Hashfun]D
Digression [in VSU_stdlib2]F
FunTable [in Hashfun]I
IntHashTable [in Hashfun]Variable Index
M
MallocFreeASI.M [in Spec_stdlib]S
StackASI.M [in Spec_stack]StackASI.STACK [in Spec_stack]
Stack_VSU.M [in VSU_stack]
StringDemo.p [in Verif_strlib]
T
TriangASI.M [in Spec_triang]Triang_VSU.stackrep_nil [in VSU_triang]
Triang_VSU.STACK [in VSU_triang]
Triang_VSU.M [in VSU_triang]
Library Index
B
BibH
HashfunP
PostscriptPreface
S
Spec_stdlibSpec_stack
Spec_triang
V
Verif_append1Verif_triang
Verif_sumarray
Verif_stack
Verif_hash
Verif_append2
Verif_reverse
Verif_strlib
VSU_stdlib
VSU_stack
VSU_stdlib2
VSU_intro
VSU_triang
VSU_main2
VSU_main
Lemma Index
A
add_another [in Verif_triang]add_list_sublist_bounds [in Verif_triang]
add_list_nonneg [in Verif_triang]
add_list_app [in Verif_triang]
add_list_decreasing_eq [in Verif_triang]
add_list_decreasing_eq_alt [in Verif_triang]
B
body_incr [in Verif_hash]body_incr_field_address_lemma [in Verif_hash]
body_incr_list [in Verif_hash]
body_get [in Verif_hash]
body_new_table [in Verif_hash]
body_new_table_helper [in Verif_hash]
body_new_cell [in Verif_hash]
body_copy_string [in Verif_hash]
body_hash [in Verif_hash]
body_main [in VSU_main2]
body_append_alter2 [in Verif_append2]
body_exit [in VSU_stdlib2]
body_free [in VSU_stdlib2]
body_malloc [in VSU_stdlib2]
body_surely_malloc [in VSU_stack]
body_newstack [in VSU_stack]
body_push [in VSU_stack]
body_pop [in VSU_stack]
body_main [in Verif_triang]
body_pop_and_add [in Verif_triang]
body_pop_and_add [in Verif_triang]
body_push_increasing [in Verif_triang]
body_append_alter1 [in Verif_append1]
body_append [in Verif_append1]
body_main [in Verif_sumarray]
body_sumarray [in Verif_sumarray]
body_reverse_step [in Verif_reverse]
body_reverse [in Verif_reverse]
body_triang [in VSU_triang]
body_pop_and_add [in VSU_triang]
body_push_increasing [in VSU_triang]
body_main [in VSU_main]
body_strcmp [in Verif_strlib]
body_example_call_strcpy [in Verif_strlib]
body_strcpy [in Verif_strlib]
body_strlen [in Verif_strlib]
body_newstack [in Verif_stack]
body_push [in Verif_stack]
body_pop [in Verif_stack]
C
cancel_example [in Verif_strlib]D
data_at_thashtable_tarray [in Verif_hash]data_at_isptr_example2 [in Verif_reverse]
data_at_isptr_example1 [in Verif_reverse]
data_at_Vundef_example [in Verif_strlib]
data_at_Vundef_example [in Verif_strlib]
demonstrate_cstring2 [in Verif_strlib]
demonstrate_cstring1 [in Verif_strlib]
E
emp_lbseg [in Verif_append2]emp_wlseg [in Verif_append2]
emp_wand_emp_left [in Verif_append2]
emp_wand_emp_right [in Verif_append2]
example_field_at_data_at''' [in Verif_hash]
example_field_at_data_at'' [in Verif_hash]
example_field_at_data_at' [in Verif_hash]
example_field_at_data_at [in Verif_hash]
example_split_struct [in Verif_hash]
F
freelistrep_valid_pointer [in VSU_stdlib2]freelistrep_local_prop [in VSU_stdlib2]
free_spec_sub [in Spec_stdlib]
FunTable.gempty [in Hashfun]
FunTable.gso [in Hashfun]
FunTable.gss [in Hashfun]
H
hashfun_snoc [in Hashfun]hashfun_aux_snoc [in Hashfun]
hashfun_inrange [in Hashfun]
hashtable_rep_valid_pointer [in Verif_hash]
hashtable_rep_local_facts [in Verif_hash]
hashtable_get_unfold [in Hashfun]
I
implies_and_adjoint [in Verif_append2]initialize [in VSU_stdlib]
initialize [in VSU_stdlib2]
IntHashTable.empty_invariant [in Hashfun]
IntHashTable.gempty [in Hashfun]
IntHashTable.gso [in Hashfun]
IntHashTable.gss [in Hashfun]
IntHashTable.incr_invariant [in Hashfun]
Int_repr_eq_mod [in Hashfun]
iter_sepcon_split3 [in Verif_hash]
iter_sepcon_listrep_local_facts [in Verif_hash]
L
lbseg_lbseg [in Verif_append2]listboxrep_traverse32 [in Verif_hash]
listboxrep_traverse [in Verif_hash]
listbox_lbseg [in Verif_append2]
listcell_fold [in Verif_hash]
listrep_traverse_finish [in Verif_hash]
listrep_traverse_step_example [in Verif_hash]
listrep_traverse_step [in Verif_hash]
listrep_traverse_start [in Verif_hash]
listrep_fold [in Verif_hash]
listrep_valid_pointer [in Verif_hash]
listrep_local_prop [in Verif_hash]
listrep_valid_pointer [in VSU_stack]
listrep_local_prop [in VSU_stack]
listrep_valid_pointer [in Verif_triang]
listrep_local_prop [in Verif_triang]
listrep_nonnull [in Verif_append1]
listrep_null [in Verif_append1]
listrep_valid_pointer [in Verif_append1]
listrep_local_facts [in Verif_append1]
listrep_len_ge2_address_different [in Verif_reverse]
listrep_len_ge2_fact [in Verif_reverse]
listrep_valid_pointer [in Verif_reverse]
listrep_valid_pointer_example [in Verif_reverse]
listrep_local_facts [in Verif_reverse]
listrep_facts_example [in Verif_reverse]
listrep_facts_example [in Verif_reverse]
listrep_valid_pointer [in Verif_stack]
listrep_local_prop [in Verif_stack]
listrep2lseg [in Verif_append1]
loopy_lseg_no_connection [in Verif_append1]
loopy_lseg_not_bad [in Verif_append1]
lseg_lseg_inv [in Verif_append1]
lseg_listrep_equiv [in Verif_append1]
lseg_list [in Verif_append1]
lseg_lseg [in Verif_append1]
lseg_maybe_loop [in Verif_append1]
lseg2listrep [in Verif_append1]
lseg2wlseg [in Verif_append2]
M
malloc_spec_sub [in Spec_stdlib]malloc_token_local_facts [in Spec_stdlib]
malloc_token_valid_pointer [in Spec_stdlib]
malloc_token_sz_local_facts [in VSU_stdlib2]
malloc_token_sz_valid_pointer [in VSU_stdlib2]
modus_ponens_wand_from_adjoint [in Verif_append2]
N
nat_sub_add_yuck [in Verif_triang]nt_lseg_list [in Verif_append1]
nt_lseg_nt_lseg [in Verif_append1]
N_eq [in Hashfun]
P
prog_correct [in Verif_sumarray]S
semax_func_cons_malloc_aux [in VSU_stdlib]singleton_wlseg [in Verif_append2]
singleton_nt_lseg' [in Verif_append1]
singleton_nt_lseg [in Verif_append1]
singleton_lseg [in Verif_append1]
stacktriangVSU [in VSU_main2]
StackVSU [in VSU_stack]
stack_valid_pointer [in VSU_stack]
stack_local_prop [in VSU_stack]
stack_valid_pointer [in Verif_triang]
stack_local_prop [in Verif_triang]
stack_valid_pointer [in Verif_stack]
stack_local_prop [in Verif_stack]
strcpy_else_clause [in Verif_strlib]
strcpy_then_clause [in Verif_strlib]
struct_list_valid_pointer_example [in Verif_reverse]
sum_Z_app [in Verif_sumarray]
W
wandQ_frame_ver_mpred [in Verif_append2]wandQ_frame_elim_mpred [in Verif_append2]
wand_frame_ver_from_adjoint_and_modus_ponens [in Verif_append2]
wand_derives_from_adjoint_and_modus_ponens [in Verif_append2]
wand_trivial [in Verif_append2]
WholeComp [in VSU_main2]
WholeComp [in VSU_main]
WholeProgSafe [in VSU_main2]
WholeProgSafe [in VSU_main]
wlseg_weird [in Verif_append2]
wlseg_listrep_equiv [in Verif_append2]
wlseg_nullval [in Verif_append2]
wlseg_list [in Verif_append2]
wlseg_wlseg [in Verif_append2]
wlseg2lseg_nullval [in Verif_append2]
Z
Zinduction [in Verif_triang]Zlength_hashtable_incr [in Hashfun]
Z_sub_add_ok [in Verif_triang]
Axiom Index
B
body_exit [in VSU_stdlib]body_free [in VSU_stdlib]
body_malloc [in VSU_stdlib]
C
COUNT_TABLE.gso [in Hashfun]COUNT_TABLE.gss [in Hashfun]
COUNT_TABLE.gempty [in Hashfun]
COUNT_TABLE.incr [in Hashfun]
COUNT_TABLE.get [in Hashfun]
COUNT_TABLE.empty [in Hashfun]
COUNT_TABLE.key [in Hashfun]
COUNT_TABLE.table [in Hashfun]
M
M [in VSU_stdlib]make_mem_mgr [in VSU_stdlib]
Projection Index
M
malloc_token_sz_local_facts [in Spec_stdlib]malloc_token_sz_valid_pointer [in Spec_stdlib]
malloc_token_sz [in Spec_stdlib]
mem_mgr [in Spec_stdlib]
S
stackrep [in Spec_stack]stackrep_valid_pointer [in Spec_stack]
stackrep_local_facts [in Spec_stack]
Instance Index
C
CompSpecs [in Verif_hash]Compspecs [in VSU_main2]
CompSpecs [in VSU_stdlib]
CompSpecs [in VSU_stdlib2]
CompSpecs [in VSU_stack]
CompSpecs [in Verif_triang]
CompSpecs [in Verif_append1]
CompSpecs [in Verif_sumarray]
CompSpecs [in Verif_reverse]
CompSpecs [in VSU_triang]
Compspecs [in VSU_main]
CompSpecs [in VSU_main]
CompSpecs [in Verif_strlib]
CompSpecs [in Verif_stack]
E
EqDec_string [in Hashfun]Section Index
M
MallocFreeASI [in Spec_stdlib]S
StackASI [in Spec_stack]Stack_VSU [in VSU_stack]
StringDemo [in Verif_strlib]
T
TriangASI [in Spec_triang]Triang_VSU [in VSU_triang]
Abbreviation Index
P
placeholder_spec [in VSU_stdlib]Definition Index
A
add_list [in Verif_triang]append_spec [in Verif_append1]
C
copy_string_spec [in Verif_hash]coreVSU [in VSU_main2]
coreVSU [in VSU_main]
D
decreasing_Z1 [in Verif_triang]decreasing_Z1_aux [in Verif_triang]
decreasing_Z [in Verif_triang]
decreasing_nat [in Verif_triang]
Digression.N [in VSU_stdlib2]
Digression.N_eq [in VSU_stdlib2]
Digression.N' [in VSU_stdlib2]
Digression.N'' [in VSU_stdlib2]
E
empty_table [in Hashfun]example_call_strcpy_spec [in Verif_strlib]
exit_spec [in Spec_stdlib]
F
four_contents [in Verif_sumarray]freelistrep [in VSU_stdlib2]
free_spec [in Spec_stdlib]
free_spec_sz [in Spec_stdlib]
free_spec_example [in Verif_stack]
FunTable.empty [in Hashfun]
FunTable.get [in Hashfun]
FunTable.incr [in Hashfun]
FunTable.key [in Hashfun]
FunTable.table [in Hashfun]
G
get_spec [in Verif_hash]Gprog [in Verif_hash]
Gprog [in Verif_triang]
Gprog [in Verif_append1]
Gprog [in Verif_sumarray]
Gprog [in Verif_reverse]
Gprog [in Verif_strlib]
Gprog [in Verif_stack]
H
hashfun [in Hashfun]hashfun_aux [in Hashfun]
hashtable_rep [in Verif_hash]
hashtable_incr [in Hashfun]
hashtable_get [in Hashfun]
hashtable_contents [in Hashfun]
hash_spec [in Verif_hash]
Hello [in Verif_strlib]
Hello' [in Verif_strlib]
I
incr_spec [in Verif_hash]incr_list_spec [in Verif_hash]
IntHashTable.empty [in Hashfun]
IntHashTable.get [in Hashfun]
IntHashTable.hashtable_invariant [in Hashfun]
IntHashTable.incr [in Hashfun]
IntHashTable.key [in Hashfun]
IntHashTable.table [in Hashfun]
L
lbseg [in Verif_append2]listboxrep [in Verif_hash]
listboxrep [in Verif_append2]
listrep [in Verif_hash]
listrep [in VSU_stack]
listrep [in Verif_triang]
listrep [in Verif_append1]
listrep [in Verif_reverse]
listrep [in Verif_stack]
list_cell_valid_pointer [in Verif_hash]
list_cell_local_facts [in Verif_hash]
list_cell [in Verif_hash]
list_incr [in Hashfun]
list_get [in Hashfun]
lseg [in Verif_append1]
M
M [in VSU_main2]M [in VSU_stdlib2]
M [in VSU_main]
MainComp [in VSU_main2]
MainComp [in VSU_main]
Main_Gprog [in VSU_main2]
Main_imports [in VSU_main2]
main_spec [in VSU_main2]
main_spec [in Verif_triang]
main_spec [in Verif_sumarray]
Main_Gprog [in VSU_main]
Main_imports [in VSU_main]
main_spec [in VSU_main]
MallocFreeASI [in Spec_stdlib]
MallocFreeVSU [in VSU_stdlib]
MallocFreeVSU [in VSU_stdlib2]
malloc_spec [in Spec_stdlib]
malloc_token [in Spec_stdlib]
malloc_spec_sz [in Spec_stdlib]
malloc_token_sz [in VSU_stdlib2]
malloc_spec_example [in Verif_stack]
mem_mgr [in VSU_stdlib2]
MFGprog [in VSU_stdlib]
MFGprog [in VSU_stdlib2]
MFVprog [in VSU_stdlib]
MFVprog [in VSU_stdlib2]
MF_E [in VSU_stdlib]
MF_globals [in VSU_stdlib]
MF_internal_specs [in VSU_stdlib]
MF_imported_specs [in VSU_stdlib]
MF_ASI [in VSU_stdlib]
MF_Externs [in VSU_stdlib2]
MF_globals [in VSU_stdlib2]
MF_internal_specs [in VSU_stdlib2]
MF_imported_specs [in VSU_stdlib2]
MF_ASI [in VSU_stdlib2]
N
N [in VSU_stdlib2]N [in Hashfun]
newstack_spec [in Verif_triang]
newstack_spec [in Spec_stack]
newstack_spec [in Verif_stack]
new_cell_spec [in Verif_hash]
new_table_spec [in Verif_hash]
nt_lseg [in Verif_append1]
N_eq [in VSU_stdlib2]
P
pop_and_add_spec [in Verif_triang]pop_spec [in Verif_triang]
pop_spec [in Spec_stack]
pop_and_add_spec [in VSU_triang]
pop_spec [in Verif_stack]
push_increasing_spec [in Verif_triang]
push_spec [in Verif_triang]
push_spec [in Spec_stack]
push_increasing_spec [in VSU_triang]
push_spec [in Verif_stack]
R
release_needed [in Preface]reverse_spec [in Verif_reverse]
S
STACK [in VSU_main2]STACK [in VSU_stack]
stack [in VSU_stack]
stack [in Verif_triang]
STACK [in VSU_main]
stack [in Verif_stack]
StackASI [in Spec_stack]
stacktriangVSU [in VSU_main]
stacktriangVSU1 [in VSU_main2]
stacktriangVSU1 [in VSU_main]
stackVSU [in VSU_main]
Stack_Vprog [in VSU_stack]
Stack_Gprog [in VSU_stack]
Stack_internals [in VSU_stack]
Stack_private [in VSU_stack]
Stack_imports [in VSU_stack]
strcmp_spec [in Verif_hash]
strcmp_spec [in Verif_strlib]
strcpy_spec [in Verif_hash]
strcpy_spec [in Verif_strlib]
stringlit_1_contents [in Verif_strlib]
string_to_list_byte [in Verif_strlib]
strlen_spec [in Verif_hash]
strlen_spec [in Verif_strlib]
sumarray_spec [in Verif_sumarray]
sum_Z [in Verif_sumarray]
surely_malloc_spec [in VSU_stack]
T
tcell [in Verif_hash]tcell [in VSU_stdlib2]
thashtable [in Verif_hash]
TriangASI [in Spec_triang]
TriangVSU [in VSU_triang]
triangVSU [in VSU_main]
triang_spec [in Spec_triang]
Triang_Vprog [in VSU_triang]
Triang_Gprog [in VSU_triang]
Triang_internals [in VSU_triang]
Triang_imports [in VSU_triang]
Triang_private [in VSU_triang]
t_list_box [in Verif_append2]
t_list [in Verif_append1]
t_list [in Verif_reverse]
U
uncurry [in Verif_hash]Unnamed_thm6 [in Verif_hash]
Unnamed_thm5 [in Verif_hash]
Unnamed_thm4 [in Verif_hash]
Unnamed_thm3 [in Verif_hash]
Unnamed_thm2 [in Verif_hash]
Unnamed_thm1 [in Verif_hash]
Unnamed_thm0 [in Verif_hash]
Unnamed_thm [in Verif_hash]
Unnamed_thm [in Verif_sumarray]
Unnamed_thm0 [in Verif_strlib]
Unnamed_thm [in Verif_strlib]
Unnamed_thm [in Preface]
Unnamed_thm [in Preface]
V
Vprog [in Verif_hash]Vprog [in VSU_main2]
Vprog [in Verif_triang]
Vprog [in Verif_append1]
Vprog [in Verif_sumarray]
Vprog [in Verif_reverse]
Vprog [in VSU_main]
Vprog [in Verif_strlib]
Vprog [in Verif_stack]
W
whole_prog [in VSU_main2]whole_prog [in VSU_main]
wlseg [in Verif_append2]
Record Index
M
MallocFreeAPD [in Spec_stdlib]S
StackAPD [in Spec_stack]| 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 | _ | other | (440 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 | _ | other | (4 entries) |
| Variable 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 | _ | other | (9 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 | _ | other | (22 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 | _ | other | (170 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 | _ | other | (13 entries) |
| Projection 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 | _ | other | (7 entries) |
| Instance 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 | _ | other | (15 entries) |
| Section 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 | _ | other | (6 entries) |
| Abbreviation 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 | _ | other | (1 entry) |
| 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 | _ | other | (191 entries) |
| Record 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 | _ | other | (2 entries) |
This page has been generated by coqdoc