Global Index

K

Q

Y

(1755 entries)

Axiom Index

A

B

G

J

K

O

Q

W

X

Y

Z

_

(228 entries)

Lemma Index

K

Q

Y

_

(436 entries)

Constructor Index

F

G

K

Q

U

Y

_

(168 entries)

Inductive Index

D

J

K

N

Q

U

X

Y

Z

(53 entries)

Definition Index

J

K

Q

Y

_

(651 entries)

Module Index

B

G

H

J

K

L

Q

X

Y

_

(180 entries)

Library Index

G

H

J

K

N

O

P

Q

U

Y

Z

_

(39 entries)

Global Index

A

Abs [module, in ProofOS.AbsInt.Reduce]
Abs [module, in ProofOS.AbsInt.Sal]
absEval_cc [definition, in ProofOS.AbsInt.SimpleCond]
ABSTRACTION [module, in ProofOS.AbsInt.Bounded]
Abstraction [module, in ProofOS.AbsInt.TypeSystem]
absValidPc [definition, in ProofOS.AbsInt.TypeSystem]
absValidPc [definition, in ProofOS.AbsInt.FixedCode]
absValidPc [definition, in ProofOS.AbsInt.FixedCode]
absValidPc' [definition, in ProofOS.AbsInt.TypeSystem]
absValidPc_dec [definition, in ProofOS.AbsInt.FixedCode]
absValidPc_imp [lemma, in ProofOS.AbsInt.TypeSystem]
Abs1 [module, in ProofOS.AbsInt.WeakDriver]
Abs1 [module, in ProofOS.Examples.Vanilla]
Abs1 [module, in ProofOS.AbsInt.SimpleDriver]
Abs2 [module, in ProofOS.AbsInt.SimpleDriver]
Abs2 [module, in ProofOS.AbsInt.WeakDriver]
Abs2 [module, in ProofOS.Examples.Vanilla]
AC [constructor, in Asm.X86.Defs]
Add [constructor, in Asm.X86.Defs]
AddCond [module, in ProofOS.AbsInt.SimpleCond]
Address [constructor, in Asm.X86.Defs]
address [inductive, in Asm.X86.Defs]
AddStackTypes [module, in ProofOS.AbsInt.StackTypes]
add_even_even [lemma, in ProofOS.Examples.EvenOdd]
add_even_odd [lemma, in ProofOS.Examples.EvenOdd]
add_odd_even [lemma, in ProofOS.Examples.EvenOdd]
add_odd_odd [lemma, in ProofOS.Examples.EvenOdd]
add_sub_four [lemma, in ProofOS.Examples.MemoryTypes]
AF [constructor, in Asm.X86.Defs]
agree_range [definition, in Asm.X86.Defs]
agree_range' [definition, in ProofOS.AbsInt.StackTypes]
agree_range'_refl [lemma, in ProofOS.AbsInt.StackTypes]
agree_range'_S [lemma, in ProofOS.AbsInt.StackTypes]
agree_range'_slot [lemma, in ProofOS.AbsInt.StackTypes]
agree_range'_trans [lemma, in ProofOS.AbsInt.StackTypes]
agree_range'_weaken [lemma, in ProofOS.AbsInt.StackTypes]
agree_range'_write [lemma, in ProofOS.AbsInt.StackTypes]
agree_range_refl [lemma, in ProofOS.AbsInt.FixedCode]
agree_range_trans [lemma, in ProofOS.AbsInt.FixedCode]
AH [constructor, in Asm.X86.Defs]
AL [constructor, in Asm.X86.Defs]
align [definition, in Asm.Util.Coqlib]
align_le [lemma, in Asm.Util.Coqlib]
AllS_dec [lemma, in Asm.Util.ListUtil]
AllS_dec_option [lemma, in Asm.Util.ListUtil]
AllS_imp [lemma, in Asm.Util.ListUtil]
AllS_In [lemma, in Asm.Util.ListUtil]
AllS_pdec [lemma, in Asm.Util.ListUtil]
AllS_pdec_option [lemma, in Asm.Util.ListUtil]
And [constructor, in Asm.X86.Defs]
and_false [lemma, in ProofOS.Examples.MemoryTypes]
and_true [lemma, in ProofOS.Examples.MemoryTypes]
Anything [constructor, in ProofOS.Examples.IntPtr]
Anything [constructor, in ProofOS.Examples.EvenOdd]
apart [inductive, in Asm.X86.Memory]
apartFromCode [definition, in ProofOS.AbsInt.FixedCode]
apartFromCode_slot [lemma, in ProofOS.AbsInt.StackTypes]
apartFromStack [definition, in ProofOS.AbsInt.StackTypes]
apartFromStack_agree_range' [lemma, in ProofOS.AbsInt.StackTypes]
apartFromStack_heap_write [lemma, in ProofOS.AbsInt.StackTypes]
apart_binc2_neq [lemma, in Asm.X86.Memory]
apart_binc3_neq [lemma, in Asm.X86.Memory]
apart_binc_neq [lemma, in Asm.X86.Memory]
apart_higher [constructor, in Asm.X86.Memory]
apart_lower [constructor, in Asm.X86.Memory]
apart_neq [lemma, in Asm.X86.Memory]
apart_or [lemma, in ProofOS.AbsInt.FixedCode]
apart_sym [lemma, in Asm.X86.Memory]
apc [inductive, in ProofOS.AbsInt.TypeSystem]
ApcConst [constructor, in ProofOS.AbsInt.TypeSystem]
ApcUnknown [constructor, in ProofOS.AbsInt.TypeSystem]
apc_eq_dec [definition, in ProofOS.AbsInt.TypeSystem]
append [definition, in Asm.Util.Maps]
append_assoc_0 [lemma, in Asm.Util.Maps]
append_assoc_1 [lemma, in Asm.Util.Maps]
append_injective [lemma, in Asm.Util.Maps]
append_neutral_l [lemma, in Asm.Util.Maps]
append_neutral_r [lemma, in Asm.Util.Maps]
Arches [library]
argsStack [definition, in ProofOS.AbsInt.StackTypes]
Arith [constructor, in Asm.X86.Defs]
Arithb [constructor, in Asm.X86.Defs]
ArithUtil [library]
arith_flags [definition, in ProofOS.AbsInt.Sal]
arith_flags [definition, in Asm.X86.Defs]
arith_flags' [definition, in Asm.X86.Defs]
arith_flags_no_CF [definition, in ProofOS.AbsInt.Sal]
arith_flags_no_CF [definition, in Asm.X86.Defs]
arith_flags_no_CF' [definition, in Asm.X86.Defs]
arith_op [inductive, in Asm.X86.Defs]
arith_op_eq_dec [definition, in ProofOS.AbsInt.WeakUpdateTypes]
arith_op_eq_dec [definition, in ProofOS.AbsInt.SimpleCond]
asafe [definition, in ProofOS.AbsInt.Bounded]

B

B [constructor, in Asm.X86.Defs]
badd [definition, in Asm.Bitvector.Defs]
badd16 [definition, in Asm.Bitvector.Defs]
badd32 [definition, in Asm.Bitvector.Defs]
badd32_comm [lemma, in Asm.Bitvector.BArith]
badd32_swap_neg [lemma, in Asm.Bitvector.BArith]
badd8 [definition, in Asm.Bitvector.Defs]
badd_btn_neg [lemma, in Asm.Bitvector.BArith]
badd_comm [lemma, in Asm.Bitvector.BArith]
badd_zero' [lemma, in Asm.Bitvector.BArith]
band [definition, in Asm.Bitvector.Defs]
band16 [definition, in Asm.Bitvector.Defs]
band32 [definition, in Asm.Bitvector.Defs]
band8 [definition, in Asm.Bitvector.Defs]
barith [definition, in Asm.Bitvector.Defs]
BArith [library]
bdec [definition, in Asm.Bitvector.Defs]
bdec2 [definition, in Asm.Bitvector.Defs]
bdec2_btn [lemma, in Asm.Bitvector.BArith]
bdec2_btn' [lemma, in Asm.Bitvector.BArith]
bdec3 [definition, in Asm.Bitvector.Defs]
bdec3_btn [lemma, in Asm.Bitvector.BArith]
bdec3_btn' [lemma, in Asm.Bitvector.BArith]
bdec4 [definition, in Asm.Bitvector.Defs]
bdec4_btn [lemma, in Asm.Bitvector.BArith]
bdec4_btn' [lemma, in Asm.Bitvector.BArith]
bdec_binc [lemma, in Asm.Bitvector.BArith]
bdec_btn [lemma, in Asm.Bitvector.BArith]
bdec_btn' [lemma, in Asm.Bitvector.BArith]
BE [constructor, in Asm.X86.Defs]
belowMax [inductive, in Asm.Bitvector.BArith]
belowMax_binc2_dec [lemma, in Asm.Bitvector.BArith]
belowMax_binc3_dec [lemma, in Asm.Bitvector.BArith]
belowMax_binc_dec [lemma, in Asm.Bitvector.BArith]
belowMax_dec [lemma, in Asm.Bitvector.BArith]
belowMax_rule [constructor, in Asm.Bitvector.BArith]
belowMax_stackEnd [lemma, in ProofOS.AbsInt.StackTypes]
BH [constructor, in Asm.X86.Defs]
binc [definition, in Asm.Bitvector.Defs]
binc2 [definition, in Asm.Bitvector.Defs]
binc2_btn [lemma, in Asm.Bitvector.BArith]
binc2_btn_belowMax [lemma, in Asm.Bitvector.BArith]
binc2_neq [lemma, in Asm.Bitvector.BArith]
binc2_neq' [lemma, in Asm.Bitvector.BArith]
binc3 [definition, in Asm.Bitvector.Defs]
binc3_btn [lemma, in Asm.Bitvector.BArith]
binc3_btn_belowMax [lemma, in Asm.Bitvector.BArith]
binc3_neq [lemma, in Asm.Bitvector.BArith]
binc3_neq' [lemma, in Asm.Bitvector.BArith]
binc4 [definition, in Asm.Bitvector.Defs]
binc4_btn [lemma, in Asm.Bitvector.BArith]
binc4_btn_belowMax [lemma, in Asm.Bitvector.BArith]
binc_bdec [lemma, in Asm.Bitvector.BArith]
binc_btn [lemma, in Asm.Bitvector.BArith]
binc_btn_belowMax [lemma, in Asm.Bitvector.BArith]
binc_neq [lemma, in Asm.Bitvector.BArith]
binc_neq' [lemma, in Asm.Bitvector.BArith]
Bitvector [library]
Bitwise [library]
BL [constructor, in Asm.X86.Defs]
ble_dec [definition, in Asm.Bitvector.Defs]
blt_dec [definition, in Asm.Bitvector.Defs]
bmax [definition, in Asm.Bitvector.Defs]
bneg [definition, in Asm.Bitvector.Defs]
bneg16 [definition, in Asm.Bitvector.Defs]
bneg32 [definition, in Asm.Bitvector.Defs]
bneg8 [definition, in Asm.Bitvector.Defs]
bneg_btn [lemma, in Asm.Bitvector.BArith]
bneg_btn_double [lemma, in Asm.Bitvector.BArith]
bneg_btn_sub [lemma, in Asm.Bitvector.BArith]
bnot [definition, in Asm.Bitvector.Defs]
bnot16 [definition, in Asm.Bitvector.Defs]
bnot32 [definition, in Asm.Bitvector.Defs]
bnot8 [definition, in Asm.Bitvector.Defs]
bnot_btn [lemma, in Asm.Bitvector.Bitwise]
bnot_btn_double [lemma, in Asm.Bitvector.Bitwise]
bnot_bzero_mod [lemma, in Asm.Bitvector.BArith]
bone [definition, in Asm.Bitvector.Defs]
bone16 [definition, in Asm.Bitvector.Defs]
bone32 [definition, in Asm.Bitvector.Defs]
bone8 [definition, in Asm.Bitvector.Defs]
bool_eq_dec [definition, in ProofOS.AbsInt.StackTypes]
bor [definition, in Asm.Bitvector.Defs]
bor16 [definition, in Asm.Bitvector.Defs]
bor32 [definition, in Asm.Bitvector.Defs]
bor8 [definition, in Asm.Bitvector.Defs]
Bounded [library]
bounded_verify [definition, in ProofOS.AbsInt.Bounded]
bound_sptr [lemma, in ProofOS.AbsInt.StackTypes]
bshl [definition, in Asm.Bitvector.Defs]
bshl16 [definition, in Asm.Bitvector.Defs]
bshl32 [definition, in Asm.Bitvector.Defs]
bshl8 [definition, in Asm.Bitvector.Defs]
bshr [definition, in Asm.Bitvector.Defs]
bshr16 [definition, in Asm.Bitvector.Defs]
bshr32 [definition, in Asm.Bitvector.Defs]
bshr8 [definition, in Asm.Bitvector.Defs]
bsub [definition, in Asm.Bitvector.Defs]
bsub16 [definition, in Asm.Bitvector.Defs]
bsub32 [definition, in Asm.Bitvector.Defs]
bsub32_eq [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
bsub32_eq' [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
bsub8 [definition, in Asm.Bitvector.Defs]
bsub_bdec [lemma, in Asm.Bitvector.BArith]
bsub_bdec2 [lemma, in Asm.Bitvector.BArith]
bsub_bdec3 [lemma, in Asm.Bitvector.BArith]
bsub_bdec4 [lemma, in Asm.Bitvector.BArith]
bsub_btn [lemma, in Asm.Bitvector.BArith]
bsub_btn_const [lemma, in Asm.Bitvector.BArith]
bsub_btn_neg [lemma, in Asm.Bitvector.BArith]
bsub_comm [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
bsub_zero [lemma, in Asm.Bitvector.BArith]
btn_diff_pos [lemma, in Asm.Bitvector.Convert]
btn_four [lemma, in ProofOS.Examples.MemoryTypes]
btn_inj [lemma, in Asm.Bitvector.Convert]
btn_invert [lemma, in Asm.Bitvector.Convert]
btn_upper [lemma, in Asm.Bitvector.Convert]
btn_upper' [lemma, in Asm.Bitvector.Convert]
btn_upper'' [lemma, in Asm.Bitvector.Convert]
bvec_eq [definition, in Asm.Bitvector.Defs]
bvec_eq_dec [definition, in Asm.Bitvector.Defs]
bvec_to_nat [definition, in Asm.Bitvector.Defs]
byte1 [definition, in Asm.Bitvector.Split]
byte2 [definition, in Asm.Bitvector.Split]
byte3 [definition, in Asm.Bitvector.Split]
byte4 [definition, in Asm.Bitvector.Split]
bzero [definition, in Asm.Bitvector.Defs]
bzero16 [definition, in Asm.Bitvector.Defs]
bzero32 [definition, in Asm.Bitvector.Defs]
bzero8 [definition, in Asm.Bitvector.Defs]
bzero_btn [lemma, in Asm.Bitvector.BArith]
bzero_inv [lemma, in ProofOS.Examples.MemoryTypes]
bzero_neg [lemma, in Asm.Bitvector.BArith]
bzero_S_dec [lemma, in Asm.Bitvector.BArith]
bzero_S_sub [lemma, in Asm.Bitvector.BArith]

C

Call [constructor, in Asm.X86.Defs]
callStep [definition, in ProofOS.AbsInt.TypeSystem]
callStep [definition, in ProofOS.AbsInt.FixedCode]
callStep [definition, in ProofOS.AbsInt.Reduce]
callStep [definition, in ProofOS.AbsInt.Bounded]
callStep [definition, in ProofOS.AbsInt.FixedCode]
cameFrom [axiom, in ProofOS.AbsInt.Reduce]
cameFrom [definition, in ProofOS.AbsInt.Sal]
cc [definition, in Asm.X86.Defs]
CF [constructor, in Asm.X86.Defs]
Ch [module, in ProofOS.AbsInt.Sal]
Ch [module, in ProofOS.Examples.Vanilla]
Ch [module, in ProofOS.AbsInt.WeakDriver]
CH [constructor, in Asm.X86.Defs]
Ch [module, in ProofOS.AbsInt.SimpleDriver]
Ch [module, in ProofOS.AbsInt.Reduce]
checkArgs [definition, in ProofOS.AbsInt.StackTypes]
checkArgsR [definition, in ProofOS.AbsInt.StackTypes]
checkArgs' [definition, in ProofOS.AbsInt.StackTypes]
checkArgs_add [lemma, in ProofOS.AbsInt.StackTypes]
checkCmd [definition, in ProofOS.AbsInt.TypeSystem]
checkCmds [definition, in ProofOS.AbsInt.TypeSystem]
Checker [module, in ProofOS.AbsInt.Bounded]
CHECKER [module, in ProofOS.AbsInt.Bounded]
Checker [module, in ProofOS.AbsInt.Sal]
checkJump [definition, in ProofOS.AbsInt.TypeSystem]
checkStore [definition, in ProofOS.AbsInt.StackTypes]
checkStore [definition, in ProofOS.AbsInt.TopOnly]
checkStore [definition, in ProofOS.AbsInt.SimpleTypes]
checkStore [definition, in ProofOS.AbsInt.WeakUpdateTypes]
checkStore [axiom, in ProofOS.AbsInt.TypeSystem]
checkStore [definition, in ProofOS.AbsInt.WeakUpdateTypes]
checkStore [definition, in ProofOS.AbsInt.SimpleCond]
checkStore [axiom, in ProofOS.AbsInt.StackTypes]
checkStoreR [definition, in ProofOS.AbsInt.StackTypes]
check_cc [definition, in ProofOS.AbsInt.Sal]
check_cc [definition, in Asm.X86.Defs]
check_cc' [definition, in Asm.X86.Defs]
check_cc_eq [definition, in ProofOS.AbsInt.Sal]
check_cc_eq' [definition, in ProofOS.AbsInt.Sal]
check_cc_imp [definition, in ProofOS.AbsInt.Sal]
check_cc_imp' [definition, in ProofOS.AbsInt.Sal]
check_condition' [definition, in Asm.X86.Defs]
check_tripleOpt [definition, in ProofOS.AbsInt.SimpleCond]
CL [constructor, in Asm.X86.Defs]
cmdOk [definition, in ProofOS.AbsInt.FixedCode]
cmdOk_sound [lemma, in ProofOS.AbsInt.FixedCode]
cmdsOk [definition, in ProofOS.AbsInt.FixedCode]
cmdsOk_sound [lemma, in ProofOS.AbsInt.FixedCode]
Cmp [constructor, in Asm.X86.Defs]
codeBigEnough [axiom, in ProofOS.AbsInt.SimpleDriver]
codeBigEnough [axiom, in ProofOS.Examples.Vanilla]
codeBigEnough [axiom, in ProofOS.AbsInt.WeakDriver]
codeFits [axiom, in ProofOS.AbsInt.FixedCode]
codeFits [axiom, in ProofOS.AbsInt.WeakDriver]
codeFits [definition, in ProofOS.Examples.Vanilla]
codeFits [axiom, in ProofOS.AbsInt.StackTypes]
codeFits [definition, in ProofOS.AbsInt.WeakDriver]
codeFits [axiom, in ProofOS.Examples.Vanilla]
codeFits [axiom, in ProofOS.AbsInt.SimpleDriver]
codeFits [definition, in ProofOS.AbsInt.SimpleDriver]
codeFits [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
codeHigh [axiom, in ProofOS.AbsInt.SimpleDriver]
codeHigh [axiom, in ProofOS.AbsInt.FixedCode]
codeHigh [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
codeHigh [definition, in ProofOS.AbsInt.SimpleDriver]
codeHigh [axiom, in ProofOS.Examples.Vanilla]
codeHigh [axiom, in ProofOS.AbsInt.WeakDriver]
codeHigh [axiom, in ProofOS.AbsInt.StackTypes]
codeHigh [definition, in ProofOS.AbsInt.WeakDriver]
codeHigh [definition, in ProofOS.Examples.Vanilla]
codeLength [axiom, in ProofOS.AbsInt.FixedCode]
codeLength [axiom, in ProofOS.AbsInt.SimpleDriver]
codeLength [axiom, in ProofOS.AbsInt.WeakDriver]
codeLength [axiom, in ProofOS.Examples.Vanilla]
codeLength [definition, in ProofOS.Examples.Vanilla]
codeLength [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
codeLength [axiom, in ProofOS.AbsInt.StackTypes]
codeLength [definition, in ProofOS.AbsInt.SimpleDriver]
codeLength [definition, in ProofOS.AbsInt.WeakDriver]
codeStart [definition, in ProofOS.AbsInt.SimpleDriver]
codeStart [axiom, in ProofOS.AbsInt.WeakDriver]
codeStart [axiom, in ProofOS.AbsInt.FixedCode]
codeStart [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
codeStart [definition, in ProofOS.Examples.Vanilla]
codeStart [axiom, in ProofOS.Examples.Vanilla]
codeStart [definition, in ProofOS.AbsInt.WeakDriver]
codeStart [axiom, in ProofOS.AbsInt.StackTypes]
codeStart [axiom, in ProofOS.AbsInt.SimpleDriver]
codeUniform [lemma, in ProofOS.AbsInt.WeakDriver]
codeUniform [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
codeUniform [axiom, in ProofOS.AbsInt.StackTypes]
codeUniform [lemma, in ProofOS.Examples.Vanilla]
codeUniform [lemma, in ProofOS.AbsInt.SimpleDriver]
codeUniform [axiom, in ProofOS.AbsInt.FixedCode]
combine [definition, in Asm.Util.Maps]
combine_commut [lemma, in Asm.Util.Maps]
compile [definition, in ProofOS.AbsInt.Sal]
compile [axiom, in ProofOS.AbsInt.Reduce]
Conc [module, in ProofOS.AbsInt.Reduce]
Conc [module, in ProofOS.AbsInt.Sal]
concAddr [definition, in ProofOS.AbsInt.WeakUpdateTypes]
concReg [definition, in ProofOS.AbsInt.WeakUpdateTypes]
concReg_easy [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
conc_slots [definition, in ProofOS.AbsInt.StackTypes]
Cond [module, in ProofOS.AbsInt.WeakUpdateTypes]
condConc [inductive, in ProofOS.AbsInt.SimpleCond]
condition [inductive, in Asm.X86.Defs]
condState [inductive, in ProofOS.AbsInt.SimpleCond]
CondSys [module, in ProofOS.AbsInt.WeakUpdateTypes]
considerDerefEq [definition, in ProofOS.Examples.IntPtr]
considerDerefEq [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
considerDerefEq [definition, in ProofOS.Examples.MemoryTypes]
considerDerefNeq [definition, in ProofOS.Examples.IntPtr]
considerDerefNeq [definition, in ProofOS.Examples.MemoryTypes]
considerDerefNeq [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
considerNeq [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
considerNeq [definition, in ProofOS.Examples.MemoryTypes]
considerNeq [definition, in ProofOS.Examples.IntPtr]
considerTest [axiom, in ProofOS.AbsInt.SimpleCond]
considerTest [definition, in ProofOS.AbsInt.WeakUpdateTypes]
Const [constructor, in ProofOS.AbsInt.StackTypes]
Constant [constructor, in ProofOS.Examples.MemoryTypes]
Constant [constructor, in ProofOS.Examples.EvenOdd]
Constant [constructor, in ProofOS.Examples.IntPtr]
contains [definition, in ProofOS.AbsInt.WeakUpdateTypes]
Convert [library]
Coqlib [library]
Create [module, in ProofOS.AbsInt.SimpleTypes]
Create [module, in ProofOS.AbsInt.WeakUpdateTypes]
cstep [definition, in ProofOS.Trusted.Safety]
cstep [definition, in ProofOS.Trusted.Safety]
Cust [constructor, in ProofOS.AbsInt.StackTypes]

D

decode_instr [axiom, in Asm.X86.Defs]
decode_same [axiom, in Asm.X86.Defs]
Defs [library]
Defs [library]
demult [lemma, in Asm.Util.ArithUtil]
DF [constructor, in Asm.X86.Defs]
DH [constructor, in Asm.X86.Defs]
disjointRegions [definition, in ProofOS.AbsInt.StackTypes]
div2 [definition, in Asm.Util.Mod]
div2_add [lemma, in Asm.Bitvector.BArith]
div2_add_S [lemma, in Asm.Bitvector.BArith]
div2_S2 [lemma, in Asm.Util.Mod]
div2_0 [lemma, in Asm.Bitvector.BArith]
div2_1 [lemma, in Asm.Bitvector.BArith]
div2_2 [lemma, in Asm.Util.Mod]
DL [constructor, in Asm.X86.Defs]
doCastEq [definition, in ProofOS.AbsInt.WeakUpdateTypes]
doCastNeq [definition, in ProofOS.AbsInt.WeakUpdateTypes]
doStackWrite [definition, in ProofOS.AbsInt.TopOnly]
doStackWrite [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
doStackWrite [definition, in ProofOS.AbsInt.WeakUpdateTypes]
doStackWrite [definition, in ProofOS.AbsInt.SimpleCond]
doStackWrite [definition, in ProofOS.AbsInt.SimpleTypes]
doStackWrite [axiom, in ProofOS.AbsInt.StackTypes]
double_minus [lemma, in Asm.Util.ArithUtil]
double_minus' [lemma, in Asm.Util.ArithUtil]
Dr [module, in ProofOS.Examples.IntPtr]
Dr [module, in ProofOS.Examples.EvenOdd]
Dr [module, in ProofOS.Examples.MemoryTypes]
Driver [module, in ProofOS.AbsInt.WeakDriver]
Driver [module, in ProofOS.AbsInt.SimpleDriver]
DRIVER_PARAM [module, in ProofOS.AbsInt.WeakDriver]
DRIVER_PARAM [module, in ProofOS.AbsInt.SimpleDriver]
DRIVER_REGIONS [module, in ProofOS.AbsInt.SimpleDriver]
DRIVER_REGIONS [module, in ProofOS.AbsInt.WeakDriver]
dummyConc [definition, in ProofOS.AbsInt.SimpleTypes]
dummyHasTy [definition, in ProofOS.AbsInt.SimpleTypes]

E

EAX [constructor, in Asm.X86.Defs]
EBP [constructor, in Asm.X86.Defs]
EBX [constructor, in Asm.X86.Defs]
ECX [constructor, in Asm.X86.Defs]
EDI [constructor, in Asm.X86.Defs]
EDX [constructor, in Asm.X86.Defs]
effectOfCmd [definition, in ProofOS.AbsInt.WeakUpdateTypes]
effectOfCmd [axiom, in ProofOS.AbsInt.TypeSystem]
effectOfCmd [definition, in ProofOS.AbsInt.StackTypes]
effectOfCmd [definition, in ProofOS.AbsInt.WeakUpdateTypes]
effectOfCmd [axiom, in ProofOS.AbsInt.StackTypes]
effectOfCmd [definition, in ProofOS.AbsInt.SimpleTypes]
effectOfCmd [definition, in ProofOS.AbsInt.TopOnly]
effectOfCmd [definition, in ProofOS.AbsInt.SimpleCond]
effectOfCmdR [definition, in ProofOS.AbsInt.StackTypes]
effectOfConditionalJump [definition, in ProofOS.AbsInt.WeakUpdateTypes]
effectOfConditionalJump [axiom, in ProofOS.AbsInt.StackTypes]
effectOfConditionalJump [definition, in ProofOS.AbsInt.StackTypes]
effectOfConditionalJump [definition, in ProofOS.AbsInt.TopOnly]
effectOfConditionalJump [definition, in ProofOS.AbsInt.SimpleCond]
effectOfConditionalJump [definition, in ProofOS.AbsInt.WeakUpdateTypes]
effectOfConditionalJump [definition, in ProofOS.AbsInt.SimpleTypes]
effectOfConditionalJump [axiom, in ProofOS.AbsInt.TypeSystem]
effectOfJump [definition, in ProofOS.AbsInt.WeakUpdateTypes]
effectOfJump [definition, in ProofOS.AbsInt.SimpleTypes]
effectOfJump [definition, in ProofOS.AbsInt.TopOnly]
effectOfJump [axiom, in ProofOS.AbsInt.TypeSystem]
effectOfJump [definition, in ProofOS.AbsInt.WeakUpdateTypes]
effectOfJump [definition, in ProofOS.AbsInt.StackTypes]
effectOfJump [axiom, in ProofOS.AbsInt.StackTypes]
effectOfJump [definition, in ProofOS.AbsInt.SimpleCond]
effectOfJumpR [definition, in ProofOS.AbsInt.StackTypes]
elements [definition, in Asm.Util.Maps]
elements [definition, in Asm.Util.Maps]
elements_complete [lemma, in Asm.Util.Maps]
elements_correct [lemma, in Asm.Util.Maps]
elements_keys_norepet [lemma, in Asm.Util.Maps]
elt [definition, in Asm.Util.Maps]
elt [definition, in Asm.Util.Maps]
elt [definition, in Asm.Util.Maps]
elt [definition, in Asm.Util.Maps]
elt_eq [definition, in Asm.Util.Maps]
elt_eq [definition, in Asm.Util.Maps]
elt_eq [definition, in Asm.Util.Maps]
elt_eq [definition, in Asm.Util.Maps]
EMap [module, in Asm.Util.Maps]
empty [definition, in Asm.Util.Maps]
empty [axiom, in Asm.Util.Map]
eq [lemma, in Asm.Util.Maps]
eq [definition, in ProofOS.AbsInt.StackTypes]
eq [definition, in Asm.X86.Defs]
eq [definition, in ProofOS.AbsInt.Sal]
eq [definition, in Asm.X86.Defs]
eq [definition, in Asm.X86.Defs]
eq [lemma, in Asm.Util.Maps]
eq [definition, in Asm.Util.Maps]
eqMod [definition, in Asm.Util.Mod]
eqMod_add_mod [lemma, in Asm.Util.Mod]
eqMod_contra [lemma, in Asm.Util.Mod]
eqMod_div2 [lemma, in Asm.Util.Mod]
eqMod_eq [lemma, in Asm.Bitvector.BArith]
eqMod_inj [lemma, in Asm.Util.Mod]
eqMod_minus [lemma, in Asm.Util.Mod]
eqMod_mod [lemma, in Asm.Util.Mod]
eqMod_mod' [lemma, in Asm.Util.Mod]
eqMod_mod2_bool [lemma, in Asm.Util.Mod]
eqMod_mod_plus [lemma, in Asm.Util.Mod]
eqMod_mod_times [lemma, in Asm.Util.Mod]
eqMod_mult [lemma, in Asm.Util.Mod]
eqMod_mult_mod [lemma, in Asm.Util.Mod]
eqMod_nat [lemma, in Asm.Util.Mod]
eqMod_nat' [lemma, in Asm.Util.Mod]
eqMod_one [lemma, in Asm.Util.Mod]
eqMod_plus [lemma, in Asm.Util.Mod]
eqMod_plus_minus_mod [lemma, in Asm.Util.Mod]
eqMod_plus_minus_mod' [lemma, in Asm.Util.Mod]
eqMod_refl [lemma, in Asm.Util.Mod]
eqMod_refl' [lemma, in ProofOS.Examples.MemoryTypes]
eqMod_S [lemma, in Asm.Util.Mod]
eqMod_sym [lemma, in Asm.Util.Mod]
eqMod_S_contra [lemma, in Asm.Util.Mod]
eqMod_S_contra_pow2 [lemma, in Asm.Util.Mod]
eqMod_trans [lemma, in Asm.Util.Mod]
EQUALITY_TYPE [module, in Asm.Util.Maps]
eq_dec [definition, in Asm.Util.Map]
eq_dec [axiom, in Asm.Util.Map]
eq_dec [lemma, in Asm.Util.Map]
eq_dec [axiom, in Asm.Util.Map]
eq_dec_to_eq [definition, in Asm.Util.Map]
eq_dec_triple [definition, in ProofOS.AbsInt.SimpleCond]
eq_dec_tripleOpt [definition, in ProofOS.AbsInt.SimpleCond]
eq_get_mem_neq [lemma, in Asm.X86.Memory]
eq_vec_dec [lemma, in Asm.Util.Vector]
ESI [constructor, in Asm.X86.Defs]
ESP [constructor, in Asm.X86.Defs]
evalExp [definition, in ProofOS.AbsInt.Sal]
evalExp_flags [lemma, in ProofOS.AbsInt.SimpleCond]
evalExp_flags [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
evalExp_mem [lemma, in ProofOS.AbsInt.SimpleCond]
evalExp_mem [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
evalExp_pc [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
evalExp_pc [lemma, in ProofOS.AbsInt.SimpleCond]
evalExp_salAddr [lemma, in ProofOS.AbsInt.Sal]
eval_addr [definition, in Asm.X86.Defs]
eval_addr_reg [lemma, in ProofOS.AbsInt.Sal]
eval_addr_stack [lemma, in ProofOS.AbsInt.Sal]
eval_AF [axiom, in Asm.X86.Defs]
eval_arith [definition, in Asm.X86.Defs]
eval_cc [definition, in ProofOS.AbsInt.SimpleCond]
eval_CF [definition, in Asm.X86.Defs]
eval_condition' [definition, in ProofOS.AbsInt.SimpleCond]
eval_genop32 [definition, in Asm.X86.Defs]
eval_OF [definition, in Asm.X86.Defs]
eval_PF [definition, in Asm.X86.Defs]
eval_SF [definition, in Asm.X86.Defs]
eval_shift [definition, in ProofOS.AbsInt.Sal]
eval_test [definition, in ProofOS.AbsInt.SimpleCond]
eval_ZF [definition, in Asm.X86.Defs]
Even [constructor, in ProofOS.Examples.EvenOdd]
EvenOdd [library]
evenOddTy [inductive, in ProofOS.Examples.EvenOdd]
EvenOddTySys [module, in ProofOS.Examples.EvenOdd]
exec [inductive, in Asm.X86.Defs]
execCmd_pc [lemma, in ProofOS.AbsInt.TypeSystem]
expUnaffected [definition, in ProofOS.AbsInt.SimpleCond]
exten [lemma, in Asm.Util.Maps]
extensionality [axiom, in Asm.Util.Coqlib]

F

failureInstr [definition, in ProofOS.AbsInt.Sal]
FINITE [module, in Asm.Util.Map]
FiniteOrderedSet [module, in Asm.Util.Map]
Fix [module, in ProofOS.AbsInt.FixedCode]
Fixed [module, in ProofOS.AbsInt.TypeSystem]
FixedCode [library]
FIXED_CODE_ABSTRACTION [module, in ProofOS.AbsInt.FixedCode]
flag [inductive, in Asm.X86.Defs]
FlagIndexed [module, in Asm.X86.Defs]
FlagMap [module, in Asm.X86.Defs]
flags [definition, in Asm.X86.Defs]
flag_eq_dec [definition, in Asm.X86.Defs]
fold [definition, in Asm.Util.Maps]
fold_right [definition, in ProofOS.Examples.Vanilla]
fold_right [definition, in ProofOS.AbsInt.SimpleDriver]
fold_right [definition, in ProofOS.AbsInt.WeakDriver]
fold_spec [lemma, in Asm.Util.Maps]
four [definition, in Asm.X86.Defs]
four_lt_pow2 [lemma, in ProofOS.Examples.MemoryTypes]
functions [definition, in ProofOS.AbsInt.WeakDriver]
functions [definition, in ProofOS.Examples.Vanilla]
functions [definition, in ProofOS.AbsInt.SimpleDriver]
functions [axiom, in ProofOS.AbsInt.StackTypes]
function_info [inductive, in ProofOS.AbsInt.StackTypes]

G

gcombine [lemma, in Asm.Util.Maps]
gempty [lemma, in Asm.Util.Maps]
genop [inductive, in Asm.X86.Defs]
genop32 [definition, in Asm.X86.Defs]
genop8 [definition, in Asm.X86.Defs]
get [definition, in Asm.Util.Maps]
get [definition, in Asm.Util.Maps]
get [definition, in Asm.Util.Maps]
get [definition, in Asm.Util.Maps]
get_flag [definition, in Asm.X86.Defs]
get_flag [definition, in ProofOS.AbsInt.Sal]
get_instr [definition, in Asm.X86.Defs]
get_instr [definition, in ProofOS.AbsInt.FixedCode]
get_instr [definition, in ProofOS.AbsInt.Sal]
get_mem [definition, in Asm.X86.Defs]
get_mem [definition, in ProofOS.AbsInt.Sal]
get_mem32 [definition, in ProofOS.AbsInt.Sal]
get_mem32 [definition, in Asm.X86.Defs]
get_mem32' [definition, in Asm.X86.Defs]
get_mem32_flags [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
get_reg [definition, in ProofOS.AbsInt.Sal]
get_reg32 [definition, in Asm.X86.Defs]
get_sal_instr [definition, in ProofOS.AbsInt.Sal]
get_xget_h [lemma, in Asm.Util.Maps]
gi [lemma, in Asm.Util.Maps]
gi [lemma, in Asm.Util.Maps]
gi [lemma, in Asm.Util.Maps]
gleaf [lemma, in Asm.Util.Maps]
gmap [lemma, in Asm.Util.Maps]
gmap [lemma, in Asm.Util.Maps]
gmap [lemma, in Asm.Util.Maps]
gmap [lemma, in Asm.Util.Maps]
gro [lemma, in Asm.Util.Maps]
grs [lemma, in Asm.Util.Maps]
gsident [lemma, in Asm.Util.Maps]
gsident [lemma, in Asm.Util.Maps]
gsident [lemma, in Asm.Util.Maps]
gso [lemma, in Asm.Util.Maps]
gso [lemma, in Asm.Util.Maps]
gso [lemma, in Asm.Util.Maps]
gso [lemma, in Asm.Util.Maps]
gss [lemma, in Asm.Util.Maps]
gss [lemma, in Asm.Util.Maps]
gss [lemma, in Asm.Util.Maps]
gss [lemma, in Asm.Util.Maps]
gsspec [lemma, in Asm.Util.Maps]
gsspec [lemma, in Asm.Util.Maps]
gsspec [lemma, in Asm.Util.Maps]
gsspec [lemma, in Asm.Util.Maps]

H

hasEvenOddTy [inductive, in ProofOS.Examples.EvenOdd]
hasIntPtrTy [inductive, in ProofOS.Examples.IntPtr]
hasMemoryTy [inductive, in ProofOS.Examples.MemoryTypes]
hasTy [definition, in ProofOS.AbsInt.TopOnly]
hasTy [definition, in ProofOS.Examples.EvenOdd]
hasTy [definition, in ProofOS.AbsInt.StackTypes]
hasTy [definition, in ProofOS.AbsInt.WeakUpdateTypes]
hasTy [definition, in ProofOS.Examples.IntPtr]
hasTy [definition, in ProofOS.AbsInt.WeakUpdateTypes]
hasTy [definition, in ProofOS.AbsInt.SimpleCond]
hasTy [definition, in ProofOS.AbsInt.SimpleTypes]
hasTy [axiom, in ProofOS.AbsInt.TypeSystem]
hasTy [definition, in ProofOS.AbsInt.SimpleCond]
hasTy [definition, in ProofOS.AbsInt.SimpleTypes]
hasTy [axiom, in ProofOS.AbsInt.SimpleTypes]
hasTy [axiom, in ProofOS.AbsInt.StackTypes]
hasTy [definition, in ProofOS.AbsInt.WeakUpdateTypes]
hasTy [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
hasTy [definition, in ProofOS.AbsInt.StackTypes]
hasTy [definition, in ProofOS.Examples.MemoryTypes]
heapCodeSeparate [definition, in ProofOS.AbsInt.WeakDriver]
heapCodeSeparate [axiom, in ProofOS.AbsInt.WeakDriver]
heapCodeSeparate [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
heapFits [definition, in ProofOS.AbsInt.WeakDriver]
heapFits [axiom, in ProofOS.AbsInt.WeakDriver]
heapFits [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
heapHigh [axiom, in ProofOS.AbsInt.WeakDriver]
heapHigh [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
heapHigh [definition, in ProofOS.AbsInt.WeakDriver]
heapLength [definition, in ProofOS.AbsInt.WeakDriver]
heapLength [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
heapLength [axiom, in ProofOS.AbsInt.WeakDriver]
heapStackSeparate [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
heapStackSeparate [definition, in ProofOS.AbsInt.WeakDriver]
heapStackSeparate [axiom, in ProofOS.AbsInt.WeakDriver]
heapStart [definition, in ProofOS.AbsInt.WeakDriver]
heapStart [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
heapStart [axiom, in ProofOS.AbsInt.WeakDriver]
HT_Anything [constructor, in ProofOS.Examples.IntPtr]
HT_Anything [constructor, in ProofOS.Examples.EvenOdd]
HT_Const [constructor, in ProofOS.AbsInt.StackTypes]
HT_Constant [constructor, in ProofOS.Examples.EvenOdd]
HT_Constant [constructor, in ProofOS.Examples.MemoryTypes]
HT_Constant [constructor, in ProofOS.Examples.IntPtr]
HT_Const' [lemma, in ProofOS.AbsInt.StackTypes]
HT_Cust [constructor, in ProofOS.AbsInt.StackTypes]
HT_Even [constructor, in ProofOS.Examples.EvenOdd]
HT_NnPtr [constructor, in ProofOS.Examples.IntPtr]
HT_Odd [constructor, in ProofOS.Examples.EvenOdd]
HT_OldEbp [constructor, in ProofOS.AbsInt.StackTypes]
HT_Product [constructor, in ProofOS.Examples.MemoryTypes]
HT_Ptr_NonNull [constructor, in ProofOS.Examples.IntPtr]
HT_Ptr_Null [constructor, in ProofOS.Examples.IntPtr]
HT_Recursive [constructor, in ProofOS.Examples.MemoryTypes]
HT_RetPtr [constructor, in ProofOS.AbsInt.StackTypes]
HT_Stack [constructor, in ProofOS.AbsInt.StackTypes]
HT_Stack' [lemma, in ProofOS.AbsInt.StackTypes]
HT_Suml [constructor, in ProofOS.Examples.MemoryTypes]
HT_Sumr [constructor, in ProofOS.Examples.MemoryTypes]
HT_Top [constructor, in ProofOS.AbsInt.StackTypes]
HT_Unit [constructor, in ProofOS.Examples.MemoryTypes]
hypCovered [definition, in ProofOS.AbsInt.TypeSystem]

I

ID [constructor, in Asm.X86.Defs]
IF_flag [constructor, in Asm.X86.Defs]
IMap [module, in Asm.Util.Maps]
Imm [constructor, in Asm.X86.Defs]
Inc [constructor, in Asm.X86.Defs]
incl_app_inv_l [lemma, in Asm.Util.Coqlib]
incl_app_inv_r [lemma, in Asm.Util.Coqlib]
incl_cons_inv [lemma, in Asm.Util.Coqlib]
incl_same_head [lemma, in Asm.Util.Coqlib]
index [definition, in Asm.Util.Maps]
index [definition, in ProofOS.AbsInt.Sal]
index [definition, in Asm.X86.Defs]
index [definition, in Asm.Util.Maps]
index [definition, in ProofOS.AbsInt.StackTypes]
index [definition, in Asm.X86.Defs]
index [definition, in Asm.X86.Defs]
INDEXED_TYPE [module, in Asm.Util.Maps]
index_inj [lemma, in Asm.X86.Defs]
index_inj [lemma, in Asm.Util.Maps]
index_inj [lemma, in Asm.Util.Maps]
index_inj [lemma, in ProofOS.AbsInt.StackTypes]
index_inj [lemma, in ProofOS.AbsInt.Sal]
index_inj [lemma, in Asm.X86.Defs]
index_inj [lemma, in Asm.X86.Defs]
inHeap [definition, in ProofOS.AbsInt.WeakUpdateTypes]
inHeap_apartFromCode [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
inHeap_apartFromStack [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
inHeap_not_too_high [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
init [axiom, in ProofOS.AbsInt.Reduce]
init [definition, in Asm.Util.Maps]
init [definition, in Asm.Util.Maps]
init [lemma, in ProofOS.AbsInt.Sal]
init [definition, in Asm.Util.Maps]
inj [axiom, in Asm.Util.Map]
inStack [definition, in ProofOS.AbsInt.StackTypes]
instr [inductive, in Asm.X86.Defs]
instrOk [definition, in ProofOS.AbsInt.FixedCode]
instructionOk [definition, in ProofOS.AbsInt.FixedCode]
instructionsOk_sound [lemma, in ProofOS.AbsInt.FixedCode]
IntermediateTySys [module, in ProofOS.AbsInt.WeakUpdateTypes]
IntPtr [library]
intPtrTy [inductive, in ProofOS.Examples.IntPtr]
IntPtrTySys [module, in ProofOS.Examples.IntPtr]
int16 [definition, in Asm.Bitvector.Defs]
int16_eq [definition, in Asm.Bitvector.Defs]
int16_eq_dec [definition, in Asm.Bitvector.Defs]
int32 [definition, in Asm.Bitvector.Defs]
Int32Indexed [module, in Asm.X86.Defs]
Int32Map [module, in Asm.X86.Defs]
int32_eq [definition, in Asm.Bitvector.Defs]
int32_eq_dec [definition, in Asm.Bitvector.Defs]
int8 [definition, in Asm.Bitvector.Defs]
int8_eq [definition, in Asm.Bitvector.Defs]
int8_eq_dec [definition, in Asm.Bitvector.Defs]
invert [definition, in Asm.Util.Maps]
invert [definition, in Asm.X86.Defs]
invert [definition, in Asm.Util.Maps]
invert [definition, in ProofOS.AbsInt.Sal]
invert [definition, in ProofOS.AbsInt.StackTypes]
invert [definition, in Asm.X86.Defs]
invert [definition, in Asm.X86.Defs]
invert_index [lemma, in ProofOS.AbsInt.Sal]
invert_index [lemma, in Asm.Util.Maps]
invert_index [lemma, in Asm.X86.Defs]
invert_index [lemma, in ProofOS.AbsInt.StackTypes]
invert_index [lemma, in Asm.X86.Defs]
invert_index [lemma, in Asm.Util.Maps]
invert_index [lemma, in Asm.X86.Defs]
invert_set_mem' [lemma, in Asm.X86.Memory]
invert_set_mem32 [lemma, in Asm.X86.Memory]
invert_set_mem32 [lemma, in ProofOS.AbsInt.Sal]
invert_set_mem32' [lemma, in Asm.X86.Memory]
invert_set_mem32'_binc2_neq' [lemma, in Asm.X86.Memory]
invert_set_mem32'_binc3_neq' [lemma, in Asm.X86.Memory]
invert_set_mem32'_binc_neq' [lemma, in Asm.X86.Memory]
invert_set_mem32'_neq [lemma, in Asm.X86.Memory]
invert_set_mem32'_neq' [lemma, in Asm.X86.Memory]
invert_set_mem32_neq [lemma, in ProofOS.AbsInt.Sal]
invert_set_mem32_neq [lemma, in Asm.X86.Memory]
In_AllS [lemma, in Asm.Util.ListUtil]
In_dec [lemma, in Asm.Util.ListUtil]
In_map [lemma, in Asm.Util.ListUtil]
In_map' [lemma, in Asm.Util.ListUtil]
in_xelements [lemma, in Asm.Util.Maps]
in_xkeys [lemma, in Asm.Util.Maps]
IOPL [constructor, in Asm.X86.Defs]
isEven [definition, in ProofOS.Examples.EvenOdd]
isOdd [definition, in ProofOS.Examples.EvenOdd]
isTyConst [definition, in ProofOS.Examples.MemoryTypes]
isTyConst [axiom, in ProofOS.AbsInt.SimpleTypes]
isTyConst [definition, in ProofOS.AbsInt.SimpleTypes]
isTyConst [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
isTyConst [definition, in ProofOS.AbsInt.StackTypes]
isTyConst [axiom, in ProofOS.AbsInt.TypeSystem]
isTyConst [axiom, in ProofOS.AbsInt.StackTypes]
isTyConst [definition, in ProofOS.Examples.EvenOdd]
isTyConst [definition, in ProofOS.AbsInt.TopOnly]
isTyConst [definition, in ProofOS.AbsInt.WeakUpdateTypes]
isTyConst [definition, in ProofOS.AbsInt.SimpleCond]
isTyConst [definition, in ProofOS.AbsInt.WeakUpdateTypes]
isTyConst [definition, in ProofOS.Examples.IntPtr]
iter [definition, in Asm.Util.ListUtil]
iter' [definition, in Asm.Util.ListUtil]

J

Jcc [constructor, in Asm.X86.Defs]
Jmp [constructor, in Asm.X86.Defs]
jmpMem [lemma, in ProofOS.AbsInt.FixedCode]

L

L [constructor, in Asm.X86.Defs]
LE [constructor, in Asm.X86.Defs]
Lea [constructor, in Asm.X86.Defs]
Leaf [constructor, in Asm.Util.Maps]
Leave [constructor, in Asm.X86.Defs]
liftState [definition, in ProofOS.AbsInt.Sal]
ListUtil [library]
list_append_map [lemma, in Asm.Util.Coqlib]
list_disjoint [definition, in Asm.Util.Coqlib]
list_disjoint_cons_left [lemma, in Asm.Util.Coqlib]
list_disjoint_cons_right [lemma, in Asm.Util.Coqlib]
list_disjoint_notin [lemma, in Asm.Util.Coqlib]
list_disjoint_sym [lemma, in Asm.Util.Coqlib]
list_forall2 [inductive, in Asm.Util.Coqlib]
list_forall2_cons [constructor, in Asm.Util.Coqlib]
list_forall2_imply [lemma, in Asm.Util.Coqlib]
list_forall2_nil [constructor, in Asm.Util.Coqlib]
list_in_map_inv [lemma, in Asm.Util.Coqlib]
list_length_map [lemma, in Asm.Util.Coqlib]
list_map_compose [lemma, in Asm.Util.Coqlib]
list_map_exten [lemma, in Asm.Util.Coqlib]
list_map_norepet [lemma, in Asm.Util.Coqlib]
list_map_nth [lemma, in Asm.Util.Coqlib]
list_norepet [inductive, in Asm.Util.Coqlib]
list_norepet_append [lemma, in Asm.Util.Coqlib]
list_norepet_append_left [lemma, in Asm.Util.Coqlib]
list_norepet_append_right [lemma, in Asm.Util.Coqlib]
list_norepet_cons [constructor, in Asm.Util.Coqlib]
list_norepet_dec [lemma, in Asm.Util.Coqlib]
list_norepet_nil [constructor, in Asm.Util.Coqlib]
localStep [definition, in ProofOS.AbsInt.FixedCode]
localStep [definition, in ProofOS.AbsInt.Reduce]
localStep [definition, in ProofOS.AbsInt.Bounded]
localStep [definition, in ProofOS.AbsInt.FixedCode]
localStep [definition, in ProofOS.AbsInt.TypeSystem]
longestInstr [definition, in Asm.X86.Defs]
lowerTy [definition, in ProofOS.AbsInt.WeakUpdateTypes]
lowerTy [definition, in ProofOS.AbsInt.StackTypes]
lowerTy_map_sound [lemma, in ProofOS.AbsInt.StackTypes]
lowerTy_sound [lemma, in ProofOS.AbsInt.StackTypes]
lowerTy_sound [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
lower_half [definition, in Asm.Bitvector.Split]
lt [axiom, in Asm.Util.Map]
lt [definition, in Asm.Util.Map]
lt_asym [lemma, in Asm.Util.Map]
lt_asym [axiom, in Asm.Util.Map]
lt_dec [axiom, in Asm.Util.Map]
lt_dec [lemma, in Asm.Util.Map]
lt_irr [lemma, in Asm.Util.Map]
lt_irr [axiom, in Asm.Util.Map]

M

M [module, in ProofOS.AbsInt.Sal]
Mac [module, in ProofOS.AbsInt.SimpleCond]
Mac [module, in ProofOS.AbsInt.Reduce]
Mac [module, in ProofOS.AbsInt.Bounded]
Mac [module, in ProofOS.AbsInt.TopOnly]
Mac [module, in ProofOS.AbsInt.FixedCode]
Mac [module, in ProofOS.AbsInt.Reduce]
Mac [module, in ProofOS.AbsInt.TypeSystem]
Mac [module, in ProofOS.AbsInt.StackTypes]
Mac [module, in ProofOS.AbsInt.Bounded]
Mac [module, in ProofOS.AbsInt.Sal]
Mac [module, in ProofOS.AbsInt.WeakUpdateTypes]
Mac [module, in ProofOS.Examples.Vanilla]
Mac [module, in ProofOS.AbsInt.Sal]
Mac [module, in ProofOS.AbsInt.FixedCode]
Mac [module, in ProofOS.AbsInt.SimpleTypes]
Mac [module, in ProofOS.AbsInt.TypeSystem]
Mac [module, in ProofOS.AbsInt.Reduce]
Mac [module, in ProofOS.AbsInt.Sal]
Mac [module, in ProofOS.AbsInt.FixedCode]
Mac [module, in ProofOS.AbsInt.Bounded]
Mac [module, in ProofOS.AbsInt.Bounded]
Mac [module, in ProofOS.AbsInt.SimpleDriver]
Mac [module, in ProofOS.AbsInt.WeakDriver]
MACHINE [module, in ProofOS.Trusted.Machine]
MACHINE [module, in ProofOS.Trusted.Safety]
Machine [library]
maget_instr [definition, in ProofOS.AbsInt.Reduce]
maget_instr [definition, in ProofOS.AbsInt.FixedCode]
maget_instr [axiom, in ProofOS.AbsInt.Bounded]
Make [module, in ProofOS.AbsInt.SimpleTypes]
Make [module, in ProofOS.AbsInt.FixedCode]
Make [module, in ProofOS.AbsInt.WeakUpdateTypes]
Make [module, in ProofOS.AbsInt.WeakDriver]
Make [module, in ProofOS.AbsInt.TopOnly]
Make [module, in ProofOS.AbsInt.SimpleDriver]
Make [module, in ProofOS.AbsInt.SimpleCond]
Make [module, in ProofOS.AbsInt.StackTypes]
Make [module, in ProofOS.Examples.Vanilla]
Make [module, in ProofOS.AbsInt.Reduce]
Make [module, in ProofOS.AbsInt.TypeSystem]
Make [module, in ProofOS.AbsInt.Sal]
map [definition, in Asm.Util.Maps]
map [definition, in Asm.Util.Maps]
map [axiom, in Asm.Util.Map]
map [definition, in Asm.Util.Maps]
MAP [module, in Asm.Util.Maps]
map [definition, in Asm.Util.Maps]
Map [library]
maPc [axiom, in ProofOS.AbsInt.FixedCode]
maPc [definition, in ProofOS.AbsInt.TypeSystem]
maPc' [definition, in ProofOS.AbsInt.TypeSystem]
mapMap [axiom, in Asm.Util.Map]
mapMapi [axiom, in Asm.Util.Map]
Maps [library]
mastate [definition, in ProofOS.AbsInt.StackTypes]
mastate [definition, in ProofOS.AbsInt.TopOnly]
mastate [definition, in ProofOS.AbsInt.FixedCode]
mastate [definition, in ProofOS.AbsInt.StackTypes]
mastate [definition, in ProofOS.AbsInt.SimpleCond]
mastate [definition, in ProofOS.AbsInt.SimpleCond]
mastate [definition, in ProofOS.AbsInt.WeakUpdateTypes]
mastate [definition, in ProofOS.AbsInt.WeakUpdateTypes]
mastate [definition, in ProofOS.AbsInt.TypeSystem]
mastate [definition, in ProofOS.AbsInt.SimpleTypes]
mastate [axiom, in ProofOS.AbsInt.Bounded]
mastate [definition, in ProofOS.AbsInt.WeakUpdateTypes]
mastate [definition, in ProofOS.AbsInt.Reduce]
mastate [axiom, in ProofOS.AbsInt.FixedCode]
mastate [axiom, in ProofOS.AbsInt.TypeSystem]
mastate [axiom, in ProofOS.AbsInt.StackTypes]
mastate [definition, in ProofOS.AbsInt.SimpleTypes]
MC [module, in ProofOS.AbsInt.Sal]
mconc [definition, in ProofOS.AbsInt.StackTypes]
mconc [definition, in ProofOS.AbsInt.WeakUpdateTypes]
mconc [definition, in ProofOS.AbsInt.WeakUpdateTypes]
mconc [axiom, in ProofOS.AbsInt.TypeSystem]
mconc [definition, in ProofOS.AbsInt.TypeSystem]
mconc [definition, in ProofOS.AbsInt.StackTypes]
mconc [definition, in ProofOS.AbsInt.FixedCode]
mconc [axiom, in ProofOS.AbsInt.StackTypes]
mconc [axiom, in ProofOS.AbsInt.FixedCode]
mconc [definition, in ProofOS.AbsInt.SimpleCond]
mconc [definition, in ProofOS.AbsInt.Reduce]
mconc [definition, in ProofOS.AbsInt.SimpleTypes]
mconc [definition, in ProofOS.AbsInt.SimpleTypes]
mconc [definition, in ProofOS.AbsInt.SimpleCond]
mconc [definition, in ProofOS.AbsInt.WeakUpdateTypes]
mconc [definition, in ProofOS.AbsInt.TopOnly]
mconc [axiom, in ProofOS.AbsInt.Bounded]
mconc_sptr_not_too_high [lemma, in ProofOS.AbsInt.StackTypes]
mcontext [axiom, in ProofOS.AbsInt.FixedCode]
mcontext [axiom, in ProofOS.AbsInt.Bounded]
mcontext [definition, in ProofOS.AbsInt.FixedCode]
mcontext [definition, in ProofOS.AbsInt.StackTypes]
mcontext [definition, in ProofOS.AbsInt.TypeSystem]
mcontext [definition, in ProofOS.AbsInt.SimpleCond]
mcontext [definition, in ProofOS.AbsInt.StackTypes]
mcontext [definition, in ProofOS.AbsInt.SimpleTypes]
mcontext [definition, in ProofOS.AbsInt.TopOnly]
mcontext [definition, in ProofOS.AbsInt.SimpleTypes]
mcontext [axiom, in ProofOS.AbsInt.TypeSystem]
mcontext [axiom, in ProofOS.AbsInt.StackTypes]
mcontext [definition, in ProofOS.AbsInt.WeakUpdateTypes]
mcontext [definition, in ProofOS.AbsInt.WeakUpdateTypes]
mcontext [definition, in ProofOS.AbsInt.SimpleCond]
mcontext [definition, in ProofOS.AbsInt.Reduce]
mcontext [definition, in ProofOS.AbsInt.WeakUpdateTypes]
mem [definition, in Asm.X86.Defs]
Memory [library]
memoryTy [inductive, in ProofOS.Examples.MemoryTypes]
MemoryTypes [library]
MemoryTySys [module, in ProofOS.Examples.MemoryTypes]
merge_times [lemma, in ProofOS.Examples.EvenOdd]
merge_times_S [lemma, in ProofOS.Examples.EvenOdd]
merge_times_S2 [lemma, in ProofOS.Examples.EvenOdd]
merge_times_S3 [lemma, in ProofOS.Examples.EvenOdd]
mexec [definition, in ProofOS.Trusted.Arches]
mexec [axiom, in ProofOS.Trusted.Safety]
mexec [axiom, in ProofOS.Trusted.Machine]
mexec [definition, in ProofOS.AbsInt.Sal]
mget_instr [axiom, in ProofOS.Trusted.Safety]
mget_instr [definition, in ProofOS.Trusted.Arches]
mget_instr [definition, in ProofOS.AbsInt.Sal]
mget_instr [axiom, in ProofOS.Trusted.Machine]
minit [definition, in ProofOS.AbsInt.TypeSystem]
minit [axiom, in ProofOS.AbsInt.Bounded]
minit [definition, in ProofOS.Examples.Vanilla]
minit [definition, in ProofOS.AbsInt.WeakDriver]
minit [axiom, in ProofOS.AbsInt.TypeSystem]
minit [axiom, in ProofOS.AbsInt.FixedCode]
minit [definition, in ProofOS.AbsInt.SimpleDriver]
minit [definition, in ProofOS.AbsInt.Reduce]
minit [definition, in ProofOS.AbsInt.FixedCode]
minitMem [definition, in ProofOS.AbsInt.WeakDriver]
minitMem [axiom, in ProofOS.Examples.Vanilla]
minitMem [definition, in ProofOS.AbsInt.SimpleDriver]
minitMem [axiom, in ProofOS.AbsInt.WeakDriver]
minitMem [axiom, in ProofOS.AbsInt.StackTypes]
minitMem [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
minitMem [axiom, in ProofOS.AbsInt.FixedCode]
minitMem [axiom, in ProofOS.AbsInt.SimpleDriver]
minitMem [definition, in ProofOS.Examples.Vanilla]
minitState [axiom, in ProofOS.Trusted.Arches]
minitState [definition, in ProofOS.AbsInt.Sal]
minitState [axiom, in ProofOS.AbsInt.FixedCode]
minitState [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
minitState [axiom, in ProofOS.AbsInt.StackTypes]
minitState [definition, in ProofOS.Trusted.Arches]
minitState [axiom, in ProofOS.Trusted.Safety]
minitState [axiom, in ProofOS.Trusted.Machine]
minitState [definition, in ProofOS.AbsInt.SimpleDriver]
minitState [definition, in ProofOS.AbsInt.WeakDriver]
minitState [definition, in ProofOS.Examples.Vanilla]
minstr [axiom, in ProofOS.Trusted.Machine]
minstr [definition, in ProofOS.AbsInt.Sal]
minstr [definition, in ProofOS.Trusted.Arches]
minstr [axiom, in ProofOS.Trusted.Safety]
minus_lt [lemma, in ProofOS.AbsInt.StackTypes]
minus_lt2 [lemma, in ProofOS.AbsInt.StackTypes]
minus_plus' [lemma, in Asm.Util.ArithUtil]
minus_S_1 [lemma, in Asm.Util.ArithUtil]
Mod [library]
mod2 [definition, in Asm.Util.Mod]
mod2_bool [definition, in Asm.Util.Mod]
mod2_bool_add [lemma, in Asm.Bitvector.BArith]
mod2_bool_add_S [lemma, in Asm.Bitvector.BArith]
mod2_bool_S2 [lemma, in Asm.Util.Mod]
mod2_bool_0 [lemma, in Asm.Bitvector.BArith]
mod2_bool_1 [lemma, in Asm.Bitvector.BArith]
mod2_bool_2 [lemma, in Asm.Util.Mod]
mod2_div2 [lemma, in Asm.Bitvector.Convert]
mod2_inj [lemma, in Asm.Bitvector.Convert]
mod2_S2 [lemma, in Asm.Util.Mod]
mod2_2 [lemma, in Asm.Util.Mod]
Monad [library]
Mov [constructor, in Asm.X86.Defs]
Movb [constructor, in Asm.X86.Defs]
mstate [definition, in ProofOS.AbsInt.Sal]
mstate [axiom, in ProofOS.Trusted.Machine]
mstate [definition, in ProofOS.Trusted.Arches]
mstate [axiom, in ProofOS.Trusted.Safety]
mstep [definition, in ProofOS.AbsInt.Reduce]
mstep [definition, in ProofOS.AbsInt.FixedCode]
mstep [definition, in ProofOS.AbsInt.TypeSystem]
mstep [axiom, in ProofOS.AbsInt.FixedCode]
mstep [axiom, in ProofOS.AbsInt.Bounded]
mult_inc [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
MyParam [module, in ProofOS.Examples.MemoryTypes]
MyParam [module, in ProofOS.Examples.EvenOdd]
MyParam [module, in ProofOS.Examples.IntPtr]
MySal [module, in ProofOS.AbsInt.FixedCode]
MySys [module, in ProofOS.AbsInt.WeakDriver]
MySys [module, in ProofOS.AbsInt.SimpleDriver]
MyTypeSystem [module, in ProofOS.AbsInt.TopOnly]
MyTypeSystemPlus [module, in ProofOS.AbsInt.SimpleDriver]
MyTypeSystemPlus [module, in ProofOS.Examples.Vanilla]
MyTypeSystemPlus [module, in ProofOS.AbsInt.WeakDriver]
M86 [module, in ProofOS.Trusted.Arches]
M86_PARAM [module, in ProofOS.Trusted.Arches]
M86_PARAM_FIXED_CODE [module, in ProofOS.AbsInt.FixedCode]
M86_PARAM_FIXED_CODE_AND_STACK [module, in ProofOS.AbsInt.StackTypes]
M86_PARAM_FIXED_CODE_AND_STACK_AND_HEAP [module, in ProofOS.AbsInt.WeakUpdateTypes]

N

NatIndexed [module, in ProofOS.AbsInt.StackTypes]
NatMap [module, in ProofOS.AbsInt.StackTypes]
nat_to_bvec [definition, in Asm.Bitvector.Defs]
neg_four [definition, in Asm.X86.Defs]
neq_lt [lemma, in Asm.Util.Map]
neq_lt [axiom, in Asm.Util.Map]
neq_sym [lemma, in Asm.X86.Memory]
NIndexed [module, in Asm.Util.Maps]
NMap [module, in Asm.Util.Maps]
NnPtr [constructor, in ProofOS.Examples.IntPtr]
Node [constructor, in Asm.Util.Maps]
not_too_high [definition, in Asm.X86.Memory]
not_too_high_minus [lemma, in ProofOS.AbsInt.StackTypes]
not_too_high_slot [lemma, in ProofOS.AbsInt.StackTypes]
NT [constructor, in Asm.X86.Defs]
ntb_add [lemma, in Asm.Bitvector.Convert]
ntb_cong [lemma, in ProofOS.AbsInt.StackTypes]
ntb_invert [lemma, in Asm.Bitvector.Convert]
ntb_invert_eqMod [lemma, in Asm.Bitvector.Convert]
ntb_invert_mod [lemma, in Asm.Bitvector.Convert]
ntb_mod [lemma, in Asm.Bitvector.Convert]
ntb_mod' [lemma, in Asm.Bitvector.Convert]
nth_error_in [lemma, in Asm.Util.Coqlib]
nth_error_nil [lemma, in Asm.Util.Coqlib]

O

O [constructor, in Asm.X86.Defs]
Odd [constructor, in ProofOS.Examples.EvenOdd]
OF [constructor, in Asm.X86.Defs]
OldEbp [constructor, in ProofOS.AbsInt.StackTypes]
one [definition, in Asm.X86.Defs]
option_map [definition, in Asm.Util.Coqlib]
Or [constructor, in Asm.X86.Defs]
ord [inductive, in Asm.Util.Map]
OrdEq [constructor, in Asm.Util.Map]
ORDERED_SET [module, in Asm.Util.Map]
OrdGt [constructor, in Asm.Util.Map]
OrdLt [constructor, in Asm.Util.Map]
ord_dec [definition, in Asm.Util.Map]
or_true [lemma, in ProofOS.Examples.MemoryTypes]

P

P [constructor, in Asm.X86.Defs]
parity [definition, in Asm.X86.Defs]
parity_dec [definition, in ProofOS.Examples.EvenOdd]
pcInRange [axiom, in ProofOS.AbsInt.FixedCode]
pcInRange [lemma, in ProofOS.AbsInt.WeakDriver]
pcInRange [lemma, in ProofOS.Examples.Vanilla]
pcInRange [axiom, in ProofOS.AbsInt.StackTypes]
pcInRange [lemma, in ProofOS.AbsInt.SimpleDriver]
pcInRange [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
pcOk [definition, in ProofOS.AbsInt.TypeSystem]
pcToAbs [definition, in ProofOS.AbsInt.TypeSystem]
pcToAbs_map [definition, in ProofOS.AbsInt.TypeSystem]
pcToAbs_map' [definition, in ProofOS.AbsInt.TypeSystem]
pcToAbs_map'_sound [lemma, in ProofOS.AbsInt.TypeSystem]
pcToFi [definition, in ProofOS.AbsInt.StackTypes]
pcToFi_map [definition, in ProofOS.AbsInt.StackTypes]
pcToFi_map' [definition, in ProofOS.AbsInt.StackTypes]
peq [definition, in Asm.Util.Coqlib]
peq_false [lemma, in Asm.Util.Coqlib]
peq_true [lemma, in Asm.Util.Coqlib]
percolate_minus_1 [lemma, in Asm.Util.ArithUtil]
PF [constructor, in Asm.X86.Defs]
Ple [definition, in Asm.Util.Coqlib]
Ple_refl [lemma, in Asm.Util.Coqlib]
Ple_succ [lemma, in Asm.Util.Coqlib]
Ple_trans [lemma, in Asm.Util.Coqlib]
plt [definition, in Asm.Util.Coqlib]
Plt [definition, in Asm.Util.Coqlib]
Plt_ne [lemma, in Asm.Util.Coqlib]
Plt_Ple [lemma, in Asm.Util.Coqlib]
Plt_Ple_trans [lemma, in Asm.Util.Coqlib]
Plt_strict [lemma, in Asm.Util.Coqlib]
Plt_succ [lemma, in Asm.Util.Coqlib]
Plt_succ_inv [lemma, in Asm.Util.Coqlib]
Plt_trans [lemma, in Asm.Util.Coqlib]
Plt_trans_succ [lemma, in Asm.Util.Coqlib]
Plt_wf [lemma, in Asm.Util.Coqlib]
plus_minus [lemma, in Asm.Util.ArithUtil]
PMap [module, in Asm.Util.Maps]
PNone [constructor, in Asm.Util.Specif]
Pop [constructor, in Asm.X86.Defs]
popt_Prop [definition, in Asm.Util.Specif]
popt_to_bool [definition, in Asm.Util.Specif]
popt_to_bool_true [lemma, in Asm.Util.Specif]
positive_Peano_ind [lemma, in Asm.Util.Coqlib]
positive_rec [definition, in Asm.Util.Coqlib]
positive_rec_base [lemma, in Asm.Util.Coqlib]
positive_rec_succ [lemma, in Asm.Util.Coqlib]
pow2 [definition, in Asm.Util.ArithUtil]
pow2_gt_1 [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
pow2_plus [lemma, in Asm.Util.ArithUtil]
pow2_pos [lemma, in Asm.Util.ArithUtil]
pow2_times2 [lemma, in Asm.Util.ArithUtil]
Ppred_Plt [lemma, in Asm.Util.Coqlib]
pred_option [inductive, in Asm.Util.Specif]
preservation [definition, in ProofOS.AbsInt.TypeSystem]
preservation [definition, in ProofOS.AbsInt.FixedCode]
preservation [definition, in ProofOS.AbsInt.Bounded]
preservation [definition, in ProofOS.AbsInt.Reduce]
preservation [definition, in ProofOS.AbsInt.FixedCode]
preservation_call_covered [lemma, in ProofOS.AbsInt.TypeSystem]
preservation_conditional_covered [lemma, in ProofOS.AbsInt.TypeSystem]
preservation_fallthru [lemma, in ProofOS.AbsInt.TypeSystem]
preservation_fallthru_covered [lemma, in ProofOS.AbsInt.TypeSystem]
preservation_jump_covered [lemma, in ProofOS.AbsInt.TypeSystem]
preservation_ret_covered [lemma, in ProofOS.AbsInt.TypeSystem]
preserveSlots [definition, in ProofOS.AbsInt.StackTypes]
print_condState [axiom, in ProofOS.AbsInt.SimpleCond]
print_evenOddTy [axiom, in ProofOS.Examples.EvenOdd]
print_intPtrTy [axiom, in ProofOS.Examples.IntPtr]
print_int32_option [axiom, in ProofOS.AbsInt.TopOnly]
print_mastate [axiom, in ProofOS.AbsInt.StackTypes]
print_mastate [definition, in ProofOS.AbsInt.WeakUpdateTypes]
print_mastate [definition, in ProofOS.AbsInt.WeakUpdateTypes]
print_mastate [definition, in ProofOS.AbsInt.Reduce]
print_mastate [axiom, in ProofOS.AbsInt.FixedCode]
print_mastate [definition, in ProofOS.AbsInt.FixedCode]
print_mastate [definition, in ProofOS.AbsInt.SimpleTypes]
print_mastate [axiom, in ProofOS.AbsInt.Bounded]
print_mastate [definition, in ProofOS.AbsInt.StackTypes]
print_mastate [definition, in ProofOS.AbsInt.SimpleCond]
print_mastate [definition, in ProofOS.AbsInt.TypeSystem]
print_mastate [axiom, in ProofOS.AbsInt.TypeSystem]
print_mastate [definition, in ProofOS.AbsInt.TopOnly]
print_memoryTy [axiom, in ProofOS.Examples.MemoryTypes]
print_nostate [axiom, in ProofOS.AbsInt.TopOnly]
print_stackState [axiom, in ProofOS.AbsInt.StackTypes]
print_stackTy [axiom, in ProofOS.AbsInt.StackTypes]
print_stateDescription [axiom, in ProofOS.AbsInt.TypeSystem]
print_ty [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
print_ty [definition, in ProofOS.AbsInt.StackTypes]
print_ty [definition, in ProofOS.Examples.IntPtr]
print_ty [definition, in ProofOS.Examples.EvenOdd]
print_ty [axiom, in ProofOS.AbsInt.SimpleTypes]
print_ty [definition, in ProofOS.AbsInt.SimpleCond]
print_ty [definition, in ProofOS.AbsInt.WeakUpdateTypes]
print_ty [definition, in ProofOS.Examples.MemoryTypes]
print_ty [definition, in ProofOS.AbsInt.WeakUpdateTypes]
print_ty [axiom, in ProofOS.AbsInt.StackTypes]
print_ty [definition, in ProofOS.AbsInt.TopOnly]
print_ty [axiom, in ProofOS.AbsInt.TypeSystem]
print_ty [definition, in ProofOS.AbsInt.SimpleTypes]
print_weakState [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
Product [constructor, in ProofOS.Examples.MemoryTypes]
productTy [inductive, in ProofOS.Examples.MemoryTypes]
product_eq_dec' [definition, in ProofOS.Examples.MemoryTypes]
progress [definition, in ProofOS.AbsInt.FixedCode]
progress [definition, in ProofOS.AbsInt.TypeSystem]
progress [definition, in ProofOS.AbsInt.Bounded]
progress [definition, in ProofOS.AbsInt.Reduce]
progress [definition, in ProofOS.AbsInt.FixedCode]
progress_call [lemma, in ProofOS.AbsInt.TypeSystem]
progress_conditional [lemma, in ProofOS.AbsInt.TypeSystem]
progress_fallthru [lemma, in ProofOS.AbsInt.TypeSystem]
progress_jump [lemma, in ProofOS.AbsInt.TypeSystem]
progress_ret [lemma, in ProofOS.AbsInt.TypeSystem]
proof_irrelevance [axiom, in Asm.Util.Coqlib]
PSome [constructor, in Asm.Util.Specif]
Psucc_inj [lemma, in Asm.Util.ArithUtil]
Ptr [constructor, in ProofOS.Examples.IntPtr]
PTree [module, in Asm.Util.Maps]
PT_Cons [constructor, in ProofOS.Examples.MemoryTypes]
PT_Nil [constructor, in ProofOS.Examples.MemoryTypes]
Push [constructor, in Asm.X86.Defs]
P_of_succ_nat_inj [lemma, in Asm.X86.Defs]
P_of_succ_nat_inj [lemma, in Asm.Util.ArithUtil]

R

R [axiom, in ProofOS.AbsInt.Reduce]
R [inductive, in ProofOS.AbsInt.Sal]
R [definition, in ProofOS.AbsInt.Sal]
raiseTy [definition, in ProofOS.AbsInt.StackTypes]
raiseTy [definition, in ProofOS.AbsInt.WeakUpdateTypes]
raiseTy_sound [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
Recursive [constructor, in ProofOS.Examples.MemoryTypes]
Reduce [library]
ReduceAbs [module, in ProofOS.AbsInt.Reduce]
Reduction [module, in ProofOS.AbsInt.Sal]
REDUCTION [module, in ProofOS.AbsInt.Reduce]
Reg [constructor, in Asm.X86.Defs]
regFree [definition, in ProofOS.AbsInt.WeakUpdateTypes]
Regions [module, in ProofOS.AbsInt.WeakDriver]
Regions [module, in ProofOS.Examples.MemoryTypes]
Regions [module, in ProofOS.Examples.IntPtr]
Regions [module, in ProofOS.Examples.EvenOdd]
Regions [module, in ProofOS.AbsInt.SimpleDriver]
regs32 [definition, in Asm.X86.Defs]
reg32 [inductive, in Asm.X86.Defs]
Reg32Indexed [module, in Asm.X86.Defs]
Reg32Map [module, in Asm.X86.Defs]
reg32_eq_dec [definition, in Asm.X86.Defs]
reg8 [inductive, in Asm.X86.Defs]
relatively_safe [inductive, in ProofOS.AbsInt.Bounded]
relativity [lemma, in ProofOS.AbsInt.Bounded]
relaxTy [definition, in ProofOS.Examples.EvenOdd]
remove [definition, in Asm.Util.Maps]
Ret [constructor, in Asm.X86.Defs]
RetPtr [constructor, in ProofOS.AbsInt.StackTypes]
reverseRobustType [definition, in ProofOS.AbsInt.StackTypes]
rewrite_double [lemma, in ProofOS.Examples.EvenOdd]
rewrite_minus_plus [lemma, in Asm.Util.ArithUtil]
rewrite_minus_0 [lemma, in Asm.Util.ArithUtil]
rewrite_plus_four [lemma, in ProofOS.AbsInt.StackTypes]
rewrite_plus_0 [lemma, in Asm.Util.ArithUtil]
rewrite_S [lemma, in Asm.Util.ArithUtil]
rewrite_times_2 [lemma, in Asm.Util.ArithUtil]
rewrite_undistrib [lemma, in Asm.Util.ArithUtil]
rewrite_undistrib_minus [lemma, in Asm.Util.ArithUtil]
rewrite_undistrib_minus_const [lemma, in Asm.Util.ArithUtil]
RF [constructor, in Asm.X86.Defs]
rleaf [lemma, in Asm.Util.Maps]
robustType [definition, in ProofOS.AbsInt.StackTypes]
roots [axiom, in ProofOS.Examples.Vanilla]
roots [axiom, in ProofOS.AbsInt.SimpleDriver]
roots [axiom, in ProofOS.AbsInt.WeakDriver]
ROOT_STATES [module, in ProofOS.AbsInt.WeakDriver]
ROOT_STATES [module, in ProofOS.AbsInt.SimpleDriver]
ROOT_STATES [module, in ProofOS.Examples.Vanilla]
rsafe_step [constructor, in ProofOS.AbsInt.Bounded]

S

S [constructor, in Asm.X86.Defs]
S [module, in ProofOS.AbsInt.Bounded]
safe [definition, in ProofOS.Trusted.Safety]
safe [inductive, in ProofOS.Trusted.Safety]
Safety [module, in ProofOS.Trusted.Safety]
Safety [library]
safe_rule [constructor, in ProofOS.Trusted.Safety]
Sal [library]
salAddr [definition, in ProofOS.AbsInt.Sal]
salCmd [inductive, in ProofOS.AbsInt.Sal]
salCmp [inductive, in ProofOS.AbsInt.Sal]
salCompile [definition, in ProofOS.AbsInt.Sal]
salExec [definition, in ProofOS.AbsInt.Sal]
salExecCmd [definition, in ProofOS.AbsInt.Sal]
salExecJmp [definition, in ProofOS.AbsInt.Sal]
salExec' [definition, in ProofOS.AbsInt.Sal]
salExp [inductive, in ProofOS.AbsInt.Sal]
salExpOpt_ok [definition, in ProofOS.AbsInt.WeakUpdateTypes]
salExpOpt_ok_dec [definition, in ProofOS.AbsInt.WeakUpdateTypes]
salExpOpt_popt [definition, in ProofOS.AbsInt.WeakUpdateTypes]
salExp_eq_dec [definition, in ProofOS.AbsInt.SimpleCond]
salExp_eq_dec [definition, in ProofOS.AbsInt.WeakUpdateTypes]
salGenop [definition, in ProofOS.AbsInt.Sal]
salIJump [inductive, in ProofOS.AbsInt.Sal]
salInstr [definition, in ProofOS.AbsInt.Sal]
salInstruction [definition, in ProofOS.AbsInt.Sal]
salJump [inductive, in ProofOS.AbsInt.Sal]
salReg [inductive, in ProofOS.AbsInt.Sal]
SalRegIndexed [module, in ProofOS.AbsInt.Sal]
SalRegMap [module, in ProofOS.AbsInt.Sal]
salRegs [definition, in ProofOS.AbsInt.Sal]
salReg_eq_dec [definition, in ProofOS.AbsInt.Sal]
salState [inductive, in ProofOS.AbsInt.Sal]
Sal86 [module, in ProofOS.AbsInt.Sal]
SArith [constructor, in ProofOS.AbsInt.Sal]
scale [inductive, in Asm.X86.Defs]
Scale1 [constructor, in Asm.X86.Defs]
Scale2 [constructor, in Asm.X86.Defs]
Scale4 [constructor, in Asm.X86.Defs]
Scale8 [constructor, in Asm.X86.Defs]
scale_shift [definition, in Asm.X86.Defs]
SCall [constructor, in ProofOS.AbsInt.Sal]
SCompare [constructor, in ProofOS.AbsInt.Sal]
SConditionalJump [constructor, in ProofOS.AbsInt.Sal]
SConst [constructor, in ProofOS.AbsInt.Sal]
seekInProduct [definition, in ProofOS.Examples.MemoryTypes]
sel [axiom, in Asm.Util.Map]
sel_empty [axiom, in Asm.Util.Map]
sel_eq [axiom, in Asm.Util.Map]
sel_neq [axiom, in Asm.Util.Map]
set [definition, in Asm.Util.Maps]
set [definition, in Asm.Util.Maps]
set [definition, in Asm.Util.Maps]
set [definition, in Asm.Util.Maps]
set_arith_flags [definition, in ProofOS.AbsInt.Sal]
set_flag [definition, in ProofOS.AbsInt.Sal]
set_flag [definition, in Asm.X86.Defs]
set_mem [definition, in Asm.X86.Defs]
set_mem [definition, in ProofOS.AbsInt.Sal]
set_mem32 [definition, in Asm.X86.Defs]
set_mem32 [definition, in ProofOS.AbsInt.Sal]
set_mem32' [definition, in Asm.X86.Defs]
set_pc [definition, in ProofOS.AbsInt.Sal]
set_pc [definition, in Asm.X86.Defs]
set_reg [definition, in ProofOS.AbsInt.Sal]
set_reg32 [definition, in Asm.X86.Defs]
set_stack32 [definition, in ProofOS.AbsInt.StackTypes]
set_stack32_sound [lemma, in ProofOS.AbsInt.StackTypes]
SF [constructor, in Asm.X86.Defs]
SFail [constructor, in ProofOS.AbsInt.Sal]
SFallthru [constructor, in ProofOS.AbsInt.Sal]
Shift [constructor, in Asm.X86.Defs]
shiftAbs [definition, in ProofOS.AbsInt.StackTypes]
shiftAbs_lt [lemma, in ProofOS.AbsInt.StackTypes]
shiftAbs_lt' [lemma, in ProofOS.AbsInt.StackTypes]
shiftAbs_lt'' [lemma, in ProofOS.AbsInt.StackTypes]
shiftContext [definition, in ProofOS.AbsInt.StackTypes]
shift_op [inductive, in Asm.X86.Defs]
shift_op_eq_dec [definition, in ProofOS.AbsInt.WeakUpdateTypes]
shift_op_eq_dec [definition, in ProofOS.AbsInt.SimpleCond]
Shl [constructor, in Asm.X86.Defs]
Shr [constructor, in Asm.X86.Defs]
sign [definition, in Asm.X86.Defs]
sig_option [inductive, in Asm.Util.Specif]
Simple [module, in ProofOS.AbsInt.SimpleDriver]
SimpleCond [library]
SimpleDriver [library]
SimpleTypes [library]
SIMPLE_TYPE_SYSTEM [module, in ProofOS.AbsInt.SimpleTypes]
SIndirectJump [constructor, in ProofOS.AbsInt.Sal]
SJump [constructor, in ProofOS.AbsInt.Sal]
SLoad [constructor, in ProofOS.AbsInt.Sal]
SNoCF [constructor, in ProofOS.AbsInt.Sal]
SNone [constructor, in Asm.Util.Specif]
Some_get_mem32_cong [lemma, in ProofOS.AbsInt.StackTypes]
Specif [library]
Split [library]
split32_sound [lemma, in Asm.Bitvector.Split]
split_sound [lemma, in Asm.Bitvector.Split]
split_word [definition, in Asm.Bitvector.Split]
SReg [constructor, in ProofOS.AbsInt.Sal]
SRet [constructor, in ProofOS.AbsInt.Sal]
SSet [constructor, in ProofOS.AbsInt.Sal]
SShift [constructor, in ProofOS.AbsInt.Sal]
SSome [constructor, in Asm.Util.Specif]
SStore [constructor, in ProofOS.AbsInt.Sal]
Stack [module, in ProofOS.AbsInt.TopOnly]
Stack [constructor, in ProofOS.AbsInt.StackTypes]
Stack [module, in ProofOS.AbsInt.SimpleCond]
Stack [module, in ProofOS.AbsInt.SimpleTypes]
stackBig [axiom, in ProofOS.AbsInt.WeakDriver]
stackBig [axiom, in ProofOS.Examples.Vanilla]
stackBig [axiom, in ProofOS.AbsInt.SimpleDriver]
stackCodeSeparate [definition, in ProofOS.AbsInt.WeakDriver]
stackCodeSeparate [axiom, in ProofOS.AbsInt.StackTypes]
stackCodeSeparate [axiom, in ProofOS.Examples.Vanilla]
stackCodeSeparate [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
stackCodeSeparate [definition, in ProofOS.AbsInt.SimpleDriver]
stackCodeSeparate [axiom, in ProofOS.AbsInt.SimpleDriver]
stackCodeSeparate [definition, in ProofOS.Examples.Vanilla]
stackCodeSeparate [axiom, in ProofOS.AbsInt.WeakDriver]
stackConc [inductive, in ProofOS.AbsInt.StackTypes]
stackContext [inductive, in ProofOS.AbsInt.StackTypes]
stackEnd [definition, in ProofOS.AbsInt.StackTypes]
stackFits [axiom, in ProofOS.AbsInt.StackTypes]
stackFits [definition, in ProofOS.AbsInt.SimpleDriver]
stackFits [axiom, in ProofOS.Examples.Vanilla]
stackFits [definition, in ProofOS.Examples.Vanilla]
stackFits [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
stackFits [axiom, in ProofOS.AbsInt.SimpleDriver]
stackFits [axiom, in ProofOS.AbsInt.WeakDriver]
stackFits [definition, in ProofOS.AbsInt.WeakDriver]
stackHasTy [inductive, in ProofOS.AbsInt.StackTypes]
stackHigh [axiom, in ProofOS.AbsInt.WeakDriver]
stackHigh [axiom, in ProofOS.AbsInt.StackTypes]
stackHigh [axiom, in ProofOS.AbsInt.SimpleDriver]
stackHigh [axiom, in ProofOS.Examples.Vanilla]
stackHigh [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
stackHigh [definition, in ProofOS.AbsInt.SimpleDriver]
stackHigh [definition, in ProofOS.AbsInt.WeakDriver]
stackHigh [definition, in ProofOS.Examples.Vanilla]
stackLength [definition, in ProofOS.Examples.Vanilla]
stackLength [axiom, in ProofOS.AbsInt.WeakDriver]
stackLength [axiom, in ProofOS.AbsInt.StackTypes]
stackLength [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
stackLength [axiom, in ProofOS.Examples.Vanilla]
stackLength [definition, in ProofOS.AbsInt.SimpleDriver]
stackLength [definition, in ProofOS.AbsInt.WeakDriver]
stackLength [axiom, in ProofOS.AbsInt.SimpleDriver]
stackLongEnough [axiom, in ProofOS.Examples.Vanilla]
stackLongEnough [axiom, in ProofOS.AbsInt.SimpleDriver]
stackLongEnough [axiom, in ProofOS.AbsInt.WeakDriver]
StackParam [module, in ProofOS.AbsInt.SimpleDriver]
StackParam [module, in ProofOS.AbsInt.WeakDriver]
StackParam [module, in ProofOS.Examples.Vanilla]
stackSlotOf [definition, in ProofOS.AbsInt.StackTypes]
stackStart [axiom, in ProofOS.AbsInt.WeakDriver]
stackStart [definition, in ProofOS.AbsInt.SimpleDriver]
stackStart [axiom, in ProofOS.Examples.Vanilla]
stackStart [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
stackStart [definition, in ProofOS.AbsInt.WeakDriver]
stackStart [axiom, in ProofOS.AbsInt.SimpleDriver]
stackStart [axiom, in ProofOS.AbsInt.StackTypes]
stackStart [definition, in ProofOS.Examples.Vanilla]
stackState [inductive, in ProofOS.AbsInt.StackTypes]
stackTy [inductive, in ProofOS.AbsInt.StackTypes]
StackTypes [library]
STACK_READY_TYPE_SYSTEM [module, in ProofOS.AbsInt.StackTypes]
stack_slot [definition, in ProofOS.AbsInt.StackTypes]
stack_slot_rewrite [lemma, in ProofOS.AbsInt.StackTypes]
stack_slot_rewrite2 [lemma, in ProofOS.AbsInt.StackTypes]
stack_slot_rewrite3 [lemma, in ProofOS.AbsInt.StackTypes]
state [inductive, in Asm.X86.Defs]
stateDescription [inductive, in ProofOS.AbsInt.TypeSystem]
step_fp [constructor, in ProofOS.AbsInt.Bounded]
step_rel [constructor, in ProofOS.AbsInt.Bounded]
step_safe [inductive, in ProofOS.AbsInt.Bounded]
STmp1 [constructor, in ProofOS.AbsInt.Sal]
STmp2 [constructor, in ProofOS.AbsInt.Sal]
Sub [constructor, in Asm.X86.Defs]
subHyps [definition, in ProofOS.AbsInt.TypeSystem]
subMap [definition, in Asm.Util.Maps]
subMap [axiom, in Asm.Util.Map]
subMastate [definition, in ProofOS.AbsInt.TopOnly]
subMastate [axiom, in ProofOS.AbsInt.StackTypes]
subMastate [definition, in ProofOS.AbsInt.StackTypes]
subMastate [definition, in ProofOS.AbsInt.TypeSystem]
subMastate [axiom, in ProofOS.AbsInt.TypeSystem]
subMastate [definition, in ProofOS.AbsInt.WeakUpdateTypes]
subMastate [definition, in ProofOS.AbsInt.SimpleCond]
subMastate [definition, in ProofOS.AbsInt.WeakUpdateTypes]
subMastate [definition, in ProofOS.AbsInt.SimpleTypes]
subProduct' [definition, in ProofOS.Examples.MemoryTypes]
subst [definition, in ProofOS.Examples.MemoryTypes]
substProduct [definition, in ProofOS.Examples.MemoryTypes]
subsumes [definition, in ProofOS.AbsInt.Bounded]
subTy [definition, in ProofOS.Examples.MemoryTypes]
subTy [axiom, in ProofOS.AbsInt.StackTypes]
subTy [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
subTy [definition, in ProofOS.Examples.EvenOdd]
subTy [definition, in ProofOS.AbsInt.SimpleTypes]
subTy [axiom, in ProofOS.AbsInt.TypeSystem]
subTy [definition, in ProofOS.AbsInt.TopOnly]
subTy [definition, in ProofOS.AbsInt.StackTypes]
subTy [definition, in ProofOS.AbsInt.SimpleCond]
subTy [definition, in ProofOS.AbsInt.WeakUpdateTypes]
subTy [definition, in ProofOS.AbsInt.WeakUpdateTypes]
subTy [axiom, in ProofOS.AbsInt.SimpleTypes]
subTy [definition, in ProofOS.Examples.IntPtr]
subTy' [definition, in ProofOS.Examples.MemoryTypes]
subTy'_sound [lemma, in ProofOS.Examples.MemoryTypes]
subTy1 [definition, in ProofOS.Examples.MemoryTypes]
subTy2 [definition, in ProofOS.Examples.MemoryTypes]
sub_one [lemma, in Asm.Util.ArithUtil]
sub_one_pow2 [lemma, in Asm.Util.ArithUtil]
sub_one_S [lemma, in Asm.Util.ArithUtil]
Sum [constructor, in ProofOS.Examples.MemoryTypes]
sum_left_map [definition, in Asm.Util.Coqlib]
sum_to_bool [definition, in Asm.Util.Specif]
SWithCF [constructor, in ProofOS.AbsInt.Sal]
SX86 [constructor, in ProofOS.AbsInt.Sal]
Sys [module, in ProofOS.AbsInt.SimpleDriver]
Sys [module, in ProofOS.Examples.MemoryTypes]
Sys [module, in ProofOS.AbsInt.WeakDriver]
Sys [module, in ProofOS.Examples.EvenOdd]
Sys [module, in ProofOS.Examples.Vanilla]
Sys [module, in ProofOS.AbsInt.SimpleDriver]
Sys [module, in ProofOS.AbsInt.SimpleCond]
Sys [module, in ProofOS.AbsInt.SimpleDriver]
Sys [module, in ProofOS.AbsInt.StackTypes]
Sys [module, in ProofOS.AbsInt.TypeSystem]
Sys [module, in ProofOS.Examples.Vanilla]
Sys [module, in ProofOS.AbsInt.WeakUpdateTypes]
Sys [module, in ProofOS.Examples.IntPtr]
Sys [module, in ProofOS.AbsInt.WeakDriver]
Sys [module, in ProofOS.AbsInt.WeakDriver]
S_minus_1 [lemma, in Asm.Util.ArithUtil]
S_minus_1_pow2 [lemma, in Asm.Bitvector.Convert]
S_times_two [lemma, in Asm.Util.ArithUtil]

T

t [definition, in ProofOS.AbsInt.Sal]
t [definition, in ProofOS.AbsInt.StackTypes]
t [definition, in Asm.X86.Defs]
t [definition, in Asm.Util.Maps]
t [definition, in Asm.X86.Defs]
t [definition, in Asm.Util.Maps]
t [definition, in Asm.X86.Defs]
t [axiom, in Asm.Util.Map]
t [definition, in Asm.Util.Map]
t [definition, in Asm.Util.Maps]
t [definition, in Asm.Util.Maps]
t [axiom, in Asm.Util.Map]
t [definition, in Asm.Util.Maps]
t [definition, in Asm.Util.Maps]
Tactics [library]
Tactics [library]
TF [constructor, in Asm.X86.Defs]
Top [constructor, in ProofOS.AbsInt.StackTypes]
TopOnly [module, in ProofOS.Examples.Vanilla]
TopOnly [library]
TotalMap [module, in Asm.Util.Map]
to_int32 [definition, in ProofOS.Examples.EvenOdd]
to_nat [axiom, in Asm.Util.Map]
tree [inductive, in Asm.Util.Maps]
TREE [module, in Asm.Util.Maps]
tripleOpt_ok [definition, in ProofOS.AbsInt.SimpleCond]
try_pred_option_pred_option [definition, in Asm.Util.Monad]
try_pred_option_sig_option [definition, in Asm.Util.Monad]
try_sig_anything [definition, in Asm.Util.Monad]
try_sig_option_pred_option [definition, in Asm.Util.Monad]
try_sig_option_sig_option [definition, in Asm.Util.Monad]
two_gt_0 [lemma, in Asm.Util.Mod]
two_power_nat_O [lemma, in Asm.Util.Coqlib]
two_power_nat_pos [lemma, in Asm.Util.Coqlib]
ty [definition, in ProofOS.AbsInt.WeakUpdateTypes]
ty [definition, in ProofOS.AbsInt.WeakUpdateTypes]
ty [definition, in ProofOS.AbsInt.StackTypes]
ty [definition, in ProofOS.Examples.MemoryTypes]
ty [definition, in ProofOS.Examples.EvenOdd]
ty [definition, in ProofOS.AbsInt.TopOnly]
ty [axiom, in ProofOS.AbsInt.TypeSystem]
ty [axiom, in ProofOS.AbsInt.StackTypes]
ty [definition, in ProofOS.AbsInt.StackTypes]
ty [definition, in ProofOS.AbsInt.SimpleCond]
ty [axiom, in ProofOS.AbsInt.SimpleTypes]
ty [definition, in ProofOS.AbsInt.SimpleTypes]
ty [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
ty [definition, in ProofOS.AbsInt.WeakUpdateTypes]
ty [definition, in ProofOS.Examples.IntPtr]
ty [definition, in ProofOS.AbsInt.SimpleTypes]
ty [definition, in ProofOS.AbsInt.SimpleCond]
tyConst [definition, in ProofOS.AbsInt.WeakUpdateTypes]
tyConst [definition, in ProofOS.AbsInt.SimpleCond]
tyConst [definition, in ProofOS.Examples.EvenOdd]
tyConst [definition, in ProofOS.AbsInt.SimpleTypes]
tyConst [axiom, in ProofOS.AbsInt.TypeSystem]
tyConst [definition, in ProofOS.Examples.IntPtr]
tyConst [definition, in ProofOS.AbsInt.TopOnly]
tyConst [definition, in ProofOS.Examples.MemoryTypes]
tyConst [definition, in ProofOS.AbsInt.StackTypes]
tyConst [axiom, in ProofOS.AbsInt.StackTypes]
tyConst [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
tyConst [axiom, in ProofOS.AbsInt.SimpleTypes]
tyConst [definition, in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound1 [definition, in ProofOS.Examples.MemoryTypes]
tyConstSound1 [definition, in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound1 [lemma, in ProofOS.AbsInt.StackTypes]
tyConstSound1 [axiom, in ProofOS.AbsInt.TypeSystem]
tyConstSound1 [definition, in ProofOS.AbsInt.SimpleCond]
tyConstSound1 [axiom, in ProofOS.AbsInt.StackTypes]
tyConstSound1 [definition, in ProofOS.Examples.IntPtr]
tyConstSound1 [axiom, in ProofOS.AbsInt.SimpleTypes]
tyConstSound1 [definition, in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound1 [lemma, in ProofOS.AbsInt.TopOnly]
tyConstSound1 [lemma, in ProofOS.AbsInt.SimpleTypes]
tyConstSound1 [lemma, in ProofOS.Examples.EvenOdd]
tyConstSound1 [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound2 [lemma, in ProofOS.AbsInt.StackTypes]
tyConstSound2 [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound2 [definition, in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound2 [definition, in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound2 [lemma, in ProofOS.Examples.MemoryTypes]
tyConstSound2 [axiom, in ProofOS.AbsInt.TypeSystem]
tyConstSound2 [axiom, in ProofOS.AbsInt.SimpleTypes]
tyConstSound2 [lemma, in ProofOS.AbsInt.TopOnly]
tyConstSound2 [definition, in ProofOS.AbsInt.SimpleCond]
tyConstSound2 [axiom, in ProofOS.AbsInt.StackTypes]
tyConstSound2 [lemma, in ProofOS.Examples.EvenOdd]
tyConstSound2 [lemma, in ProofOS.Examples.IntPtr]
tyConstSound2 [lemma, in ProofOS.AbsInt.SimpleTypes]
typeMconc [inductive, in ProofOS.AbsInt.TypeSystem]
typeof [definition, in ProofOS.AbsInt.WeakUpdateTypes]
typeof [definition, in ProofOS.AbsInt.WeakUpdateTypes]
typeof [definition, in ProofOS.AbsInt.SimpleTypes]
typeof [definition, in ProofOS.AbsInt.TopOnly]
typeof [definition, in ProofOS.AbsInt.StackTypes]
typeof [definition, in ProofOS.AbsInt.SimpleCond]
typeof [axiom, in ProofOS.AbsInt.TypeSystem]
typeof [axiom, in ProofOS.AbsInt.StackTypes]
typeofArith [definition, in ProofOS.Examples.EvenOdd]
typeofArith [definition, in ProofOS.Examples.IntPtr]
typeofArith [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
typeofArith [definition, in ProofOS.Examples.MemoryTypes]
typeofArith [axiom, in ProofOS.AbsInt.SimpleTypes]
typeofCell [definition, in ProofOS.Examples.MemoryTypes]
typeofCell [definition, in ProofOS.Examples.IntPtr]
typeofCell [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
typeofLoad [definition, in ProofOS.AbsInt.WeakUpdateTypes]
typeofLoad [axiom, in ProofOS.AbsInt.TypeSystem]
typeofLoad [definition, in ProofOS.AbsInt.WeakUpdateTypes]
typeofLoad [axiom, in ProofOS.AbsInt.StackTypes]
typeofLoad [definition, in ProofOS.AbsInt.TopOnly]
typeofLoad [definition, in ProofOS.AbsInt.StackTypes]
typeofLoad [definition, in ProofOS.AbsInt.SimpleTypes]
typeofLoad [definition, in ProofOS.AbsInt.SimpleCond]
typeofLoadR [definition, in ProofOS.AbsInt.StackTypes]
typeofR [definition, in ProofOS.AbsInt.StackTypes]
TypeSystem [module, in ProofOS.AbsInt.SimpleDriver]
TypeSystem [module, in ProofOS.AbsInt.WeakDriver]
TypeSystem [module, in ProofOS.Examples.Vanilla]
TypeSystem [library]
TYPE_SYSTEM [module, in ProofOS.AbsInt.TypeSystem]
TYPE_SYSTEM_WITH_FUNCTIONS [module, in ProofOS.AbsInt.StackTypes]
TYPE_SYSTEM_WITH_TESTING [module, in ProofOS.AbsInt.SimpleCond]
TySys [module, in ProofOS.AbsInt.StackTypes]
tyTop [definition, in ProofOS.Examples.IntPtr]
tyTop [definition, in ProofOS.AbsInt.WeakUpdateTypes]
tyTop [definition, in ProofOS.AbsInt.WeakUpdateTypes]
tyTop [definition, in ProofOS.AbsInt.TopOnly]
tyTop [definition, in ProofOS.AbsInt.SimpleCond]
tyTop [definition, in ProofOS.Examples.MemoryTypes]
tyTop [axiom, in ProofOS.AbsInt.SimpleTypes]
tyTop [definition, in ProofOS.AbsInt.StackTypes]
tyTop [definition, in ProofOS.AbsInt.SimpleTypes]
tyTop [definition, in ProofOS.Examples.EvenOdd]
tyTop [axiom, in ProofOS.AbsInt.TypeSystem]
tyTop [axiom, in ProofOS.AbsInt.StackTypes]
tyTop [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
tyTopSound [definition, in ProofOS.Examples.MemoryTypes]
tyTopSound [lemma, in ProofOS.AbsInt.SimpleTypes]
tyTopSound [definition, in ProofOS.Examples.IntPtr]
tyTopSound [lemma, in ProofOS.Examples.EvenOdd]
tyTopSound [axiom, in ProofOS.AbsInt.WeakUpdateTypes]
tyTopSound [axiom, in ProofOS.AbsInt.TypeSystem]
tyTopSound [lemma, in ProofOS.AbsInt.StackTypes]
tyTopSound [lemma, in ProofOS.AbsInt.TopOnly]
tyTopSound [axiom, in ProofOS.AbsInt.StackTypes]
tyTopSound [definition, in ProofOS.AbsInt.WeakUpdateTypes]
tyTopSound [definition, in ProofOS.AbsInt.WeakUpdateTypes]
tyTopSound [definition, in ProofOS.AbsInt.SimpleCond]
tyTopSound [axiom, in ProofOS.AbsInt.SimpleTypes]
tyTopSound' [lemma, in ProofOS.AbsInt.TopOnly]
ty_eq_dec [definition, in ProofOS.Examples.MemoryTypes]
ty_eq_dec' [definition, in ProofOS.Examples.MemoryTypes]
ty_eq_dec'_sound1 [lemma, in ProofOS.Examples.MemoryTypes]
ty_eq_dec'_sound2 [lemma, in ProofOS.Examples.MemoryTypes]

U

undo_rewrite_fourx [lemma, in ProofOS.AbsInt.StackTypes]
undo_rewrite_fourx_plus [lemma, in ProofOS.AbsInt.StackTypes]
unroll_positive_rec [lemma, in Asm.Util.Coqlib]
upd [axiom, in Asm.Util.Map]
upper_half [definition, in Asm.Bitvector.Split]
User [module, in ProofOS.AbsInt.WeakDriver]
User [module, in ProofOS.Examples.Vanilla]
User [module, in ProofOS.AbsInt.SimpleDriver]
use_asafe [lemma, in ProofOS.AbsInt.Bounded]
USE_TYPE_SYSTEM [module, in ProofOS.AbsInt.TypeSystem]

V

validPc [definition, in ProofOS.AbsInt.FixedCode]
Vanilla [library]
VANILLA_PARAM [module, in ProofOS.Examples.Vanilla]
var [definition, in ProofOS.Examples.MemoryTypes]
Var [constructor, in ProofOS.Examples.MemoryTypes]
Vector [library]
Verifier [module, in ProofOS.Examples.IntPtr]
Verifier [module, in ProofOS.Examples.MemoryTypes]
Verifier [module, in ProofOS.Examples.EvenOdd]
Verifier [module, in ProofOS.Examples.Vanilla]
verify [definition, in ProofOS.AbsInt.WeakDriver]
verify [definition, in ProofOS.AbsInt.Sal]
verify [definition, in ProofOS.AbsInt.Reduce]
verify [definition, in ProofOS.AbsInt.Bounded]
verify [definition, in ProofOS.AbsInt.SimpleDriver]
verify [axiom, in ProofOS.AbsInt.Bounded]
verify [definition, in ProofOS.Examples.Vanilla]
verify_list [definition, in ProofOS.AbsInt.Bounded]
Vid [definition, in Asm.Util.Vector]
Vid_eq [lemma, in Asm.Util.Vector]
viewShift [inductive, in ProofOS.AbsInt.TypeSystem]
viewShiftOfJump [definition, in ProofOS.AbsInt.TopOnly]
viewShiftOfJump [definition, in ProofOS.AbsInt.WeakUpdateTypes]
viewShiftOfJump [definition, in ProofOS.AbsInt.SimpleCond]
viewShiftOfJump [definition, in ProofOS.AbsInt.SimpleTypes]
viewShiftOfJump [axiom, in ProofOS.AbsInt.TypeSystem]
viewShiftOfJump [definition, in ProofOS.AbsInt.WeakUpdateTypes]
viewShiftOfJump [definition, in ProofOS.AbsInt.StackTypes]
viewShiftOfJump [axiom, in ProofOS.AbsInt.StackTypes]
viewShift_boring [lemma, in ProofOS.AbsInt.StackTypes]
viewShift_concSlots [lemma, in ProofOS.AbsInt.StackTypes]
viewShift_eq [lemma, in ProofOS.AbsInt.StackTypes]
viewShift_ret [definition, in ProofOS.AbsInt.StackTypes]
viewShift_ret_eq [lemma, in ProofOS.AbsInt.StackTypes]
VIF [constructor, in Asm.X86.Defs]
VIP [constructor, in Asm.X86.Defs]
VM [constructor, in Asm.X86.Defs]
VO_eq [lemma, in Asm.Util.Vector]
VSn_eq [lemma, in Asm.Util.Vector]

W

Weak [module, in ProofOS.AbsInt.WeakDriver]
weakConc [inductive, in ProofOS.AbsInt.WeakUpdateTypes]
WeakDriver [library]
weakState [definition, in ProofOS.AbsInt.WeakUpdateTypes]
WeakUpdateTypes [library]
WEAK_UPDATE_TYPE_SYSTEM [module, in ProofOS.AbsInt.WeakUpdateTypes]
WithTesting [module, in ProofOS.AbsInt.WeakUpdateTypes]
wordAligned [definition, in ProofOS.AbsInt.WeakUpdateTypes]
wordAligned_neq [lemma, in ProofOS.AbsInt.WeakUpdateTypes]
WriteMem [constructor, in Asm.X86.Defs]
WriteReg [constructor, in Asm.X86.Defs]
write_genop32 [inductive, in Asm.X86.Defs]

X

XArith [constructor, in Asm.X86.Defs]
XCall [constructor, in Asm.X86.Defs]
XCmp [constructor, in Asm.X86.Defs]
xcombine_l [definition, in Asm.Util.Maps]
xcombine_lr [lemma, in Asm.Util.Maps]
xcombine_r [definition, in Asm.Util.Maps]
xelements [definition, in Asm.Util.Maps]
xelements_complete [lemma, in Asm.Util.Maps]
xelements_correct [lemma, in Asm.Util.Maps]
xelements_hi [lemma, in Asm.Util.Maps]
xelements_ho [lemma, in Asm.Util.Maps]
xelements_ih [lemma, in Asm.Util.Maps]
xelements_ii [lemma, in Asm.Util.Maps]
xelements_io [lemma, in Asm.Util.Maps]
xelements_keys_norepet [lemma, in Asm.Util.Maps]
xelements_oh [lemma, in Asm.Util.Maps]
xelements_oi [lemma, in Asm.Util.Maps]
xelements_oo [lemma, in Asm.Util.Maps]
xgcombine [lemma, in Asm.Util.Maps]
xgcombine_l [lemma, in Asm.Util.Maps]
xgcombine_r [lemma, in Asm.Util.Maps]
xget [definition, in Asm.Util.Maps]
xget_left [lemma, in Asm.Util.Maps]
xgmap [lemma, in Asm.Util.Maps]
XInc [constructor, in Asm.X86.Defs]
XJcc_false [constructor, in Asm.X86.Defs]
XJcc_true [constructor, in Asm.X86.Defs]
XJmp [constructor, in Asm.X86.Defs]
xkeys [definition, in Asm.Util.Maps]
XLea [constructor, in Asm.X86.Defs]
XLeave [constructor, in Asm.X86.Defs]
xmap [definition, in Asm.Util.Maps]
XMov [constructor, in Asm.X86.Defs]
XPop [constructor, in Asm.X86.Defs]
XPush [constructor, in Asm.X86.Defs]
XRet [constructor, in Asm.X86.Defs]
X86 [library]

Z

Z [constructor, in Asm.X86.Defs]
Zdiv_small [lemma, in Asm.Util.Coqlib]
Zdiv_unique [lemma, in Asm.Util.Coqlib]
zeq [definition, in Asm.Util.Coqlib]
zeq_false [lemma, in Asm.Util.Coqlib]
zeq_true [lemma, in Asm.Util.Coqlib]
zero_ntb [lemma, in Asm.Bitvector.BArith]
zero_one_neq [lemma, in ProofOS.Examples.MemoryTypes]
ZF [constructor, in Asm.X86.Defs]
ZIndexed [module, in Asm.Util.Maps]
zle [definition, in Asm.Util.Coqlib]
zle_false [lemma, in Asm.Util.Coqlib]
zle_true [lemma, in Asm.Util.Coqlib]
zlt [definition, in Asm.Util.Coqlib]
zlt_false [lemma, in Asm.Util.Coqlib]
zlt_true [lemma, in Asm.Util.Coqlib]
ZMap [module, in Asm.Util.Maps]
Zmax_bound_l [lemma, in Asm.Util.Coqlib]
Zmax_bound_r [lemma, in Asm.Util.Coqlib]
Zmax_spec [lemma, in Asm.Util.Coqlib]
Zmin_spec [lemma, in Asm.Util.Coqlib]
Zmod_small [lemma, in Asm.Util.Coqlib]
Zmod_unique [lemma, in Asm.Util.Coqlib]
Z_of_nat_bit [lemma, in Asm.Util.ArithUtil]
Z_of_nat_inj [lemma, in Asm.Util.ArithUtil]
Z_rewrite_plus_0 [lemma, in Asm.Util.ArithUtil]
Z_rewrite_times_0 [lemma, in Asm.Util.ArithUtil]

_

_mconc [inductive, in ProofOS.AbsInt.FixedCode]

Axiom Index

C

cameFrom [in ProofOS.AbsInt.Reduce]
checkStore [in ProofOS.AbsInt.TypeSystem]
checkStore [in ProofOS.AbsInt.StackTypes]
codeBigEnough [in ProofOS.AbsInt.SimpleDriver]
codeBigEnough [in ProofOS.Examples.Vanilla]
codeBigEnough [in ProofOS.AbsInt.WeakDriver]
codeFits [in ProofOS.AbsInt.FixedCode]
codeFits [in ProofOS.AbsInt.WeakDriver]
codeFits [in ProofOS.AbsInt.StackTypes]
codeFits [in ProofOS.Examples.Vanilla]
codeFits [in ProofOS.AbsInt.SimpleDriver]
codeFits [in ProofOS.AbsInt.WeakUpdateTypes]
codeHigh [in ProofOS.AbsInt.SimpleDriver]
codeHigh [in ProofOS.AbsInt.FixedCode]
codeHigh [in ProofOS.AbsInt.WeakUpdateTypes]
codeHigh [in ProofOS.Examples.Vanilla]
codeHigh [in ProofOS.AbsInt.WeakDriver]
codeHigh [in ProofOS.AbsInt.StackTypes]
codeLength [in ProofOS.AbsInt.FixedCode]
codeLength [in ProofOS.AbsInt.SimpleDriver]
codeLength [in ProofOS.AbsInt.WeakDriver]
codeLength [in ProofOS.Examples.Vanilla]
codeLength [in ProofOS.AbsInt.WeakUpdateTypes]
codeLength [in ProofOS.AbsInt.StackTypes]
codeStart [in ProofOS.AbsInt.WeakDriver]
codeStart [in ProofOS.AbsInt.FixedCode]
codeStart [in ProofOS.AbsInt.WeakUpdateTypes]
codeStart [in ProofOS.Examples.Vanilla]
codeStart [in ProofOS.AbsInt.StackTypes]
codeStart [in ProofOS.AbsInt.SimpleDriver]
codeUniform [in ProofOS.AbsInt.WeakUpdateTypes]
codeUniform [in ProofOS.AbsInt.StackTypes]
codeUniform [in ProofOS.AbsInt.FixedCode]
compile [in ProofOS.AbsInt.Reduce]
considerDerefEq [in ProofOS.AbsInt.WeakUpdateTypes]
considerDerefNeq [in ProofOS.AbsInt.WeakUpdateTypes]
considerNeq [in ProofOS.AbsInt.WeakUpdateTypes]
considerTest [in ProofOS.AbsInt.SimpleCond]

D

decode_instr [in Asm.X86.Defs]
decode_same [in Asm.X86.Defs]
doStackWrite [in ProofOS.AbsInt.StackTypes]

E

effectOfCmd [in ProofOS.AbsInt.TypeSystem]
effectOfCmd [in ProofOS.AbsInt.StackTypes]
effectOfConditionalJump [in ProofOS.AbsInt.StackTypes]
effectOfConditionalJump [in ProofOS.AbsInt.TypeSystem]
effectOfJump [in ProofOS.AbsInt.TypeSystem]
effectOfJump [in ProofOS.AbsInt.StackTypes]
empty [in Asm.Util.Map]
eq_dec [in Asm.Util.Map]
eq_dec [in Asm.Util.Map]
eval_AF [in Asm.X86.Defs]
extensionality [in Asm.Util.Coqlib]

F

functions [in ProofOS.AbsInt.StackTypes]

H

hasTy [in ProofOS.AbsInt.TypeSystem]
hasTy [in ProofOS.AbsInt.SimpleTypes]
hasTy [in ProofOS.AbsInt.StackTypes]
hasTy [in ProofOS.AbsInt.WeakUpdateTypes]
heapCodeSeparate [in ProofOS.AbsInt.WeakDriver]
heapCodeSeparate [in ProofOS.AbsInt.WeakUpdateTypes]
heapFits [in ProofOS.AbsInt.WeakDriver]
heapFits [in ProofOS.AbsInt.WeakUpdateTypes]
heapHigh [in ProofOS.AbsInt.WeakDriver]
heapHigh [in ProofOS.AbsInt.WeakUpdateTypes]
heapLength [in ProofOS.AbsInt.WeakUpdateTypes]
heapLength [in ProofOS.AbsInt.WeakDriver]
heapStackSeparate [in ProofOS.AbsInt.WeakUpdateTypes]
heapStackSeparate [in ProofOS.AbsInt.WeakDriver]
heapStart [in ProofOS.AbsInt.WeakUpdateTypes]
heapStart [in ProofOS.AbsInt.WeakDriver]

I

init [in ProofOS.AbsInt.Reduce]
inj [in Asm.Util.Map]
isTyConst [in ProofOS.AbsInt.SimpleTypes]
isTyConst [in ProofOS.AbsInt.WeakUpdateTypes]
isTyConst [in ProofOS.AbsInt.TypeSystem]
isTyConst [in ProofOS.AbsInt.StackTypes]

L

lt [in Asm.Util.Map]
lt_asym [in Asm.Util.Map]
lt_dec [in Asm.Util.Map]
lt_irr [in Asm.Util.Map]

M

maget_instr [in ProofOS.AbsInt.Bounded]
map [in Asm.Util.Map]
maPc [in ProofOS.AbsInt.FixedCode]
mapMap [in Asm.Util.Map]
mapMapi [in Asm.Util.Map]
mastate [in ProofOS.AbsInt.Bounded]
mastate [in ProofOS.AbsInt.FixedCode]
mastate [in ProofOS.AbsInt.TypeSystem]
mastate [in ProofOS.AbsInt.StackTypes]
mconc [in ProofOS.AbsInt.TypeSystem]
mconc [in ProofOS.AbsInt.StackTypes]
mconc [in ProofOS.AbsInt.FixedCode]
mconc [in ProofOS.AbsInt.Bounded]
mcontext [in ProofOS.AbsInt.FixedCode]
mcontext [in ProofOS.AbsInt.Bounded]
mcontext [in ProofOS.AbsInt.TypeSystem]
mcontext [in ProofOS.AbsInt.StackTypes]
mexec [in ProofOS.Trusted.Safety]
mexec [in ProofOS.Trusted.Machine]
mget_instr [in ProofOS.Trusted.Safety]
mget_instr [in ProofOS.Trusted.Machine]
minit [in ProofOS.AbsInt.Bounded]
minit [in ProofOS.AbsInt.TypeSystem]
minit [in ProofOS.AbsInt.FixedCode]
minitMem [in ProofOS.Examples.Vanilla]
minitMem [in ProofOS.AbsInt.WeakDriver]
minitMem [in ProofOS.AbsInt.StackTypes]
minitMem [in ProofOS.AbsInt.WeakUpdateTypes]
minitMem [in ProofOS.AbsInt.FixedCode]
minitMem [in ProofOS.AbsInt.SimpleDriver]
minitState [in ProofOS.Trusted.Arches]
minitState [in ProofOS.AbsInt.FixedCode]
minitState [in ProofOS.AbsInt.WeakUpdateTypes]
minitState [in ProofOS.AbsInt.StackTypes]
minitState [in ProofOS.Trusted.Safety]
minitState [in ProofOS.Trusted.Machine]
minstr [in ProofOS.Trusted.Machine]
minstr [in ProofOS.Trusted.Safety]
mstate [in ProofOS.Trusted.Machine]
mstate [in ProofOS.Trusted.Safety]
mstep [in ProofOS.AbsInt.FixedCode]
mstep [in ProofOS.AbsInt.Bounded]

N

neq_lt [in Asm.Util.Map]

P

pcInRange [in ProofOS.AbsInt.FixedCode]
pcInRange [in ProofOS.AbsInt.StackTypes]
pcInRange [in ProofOS.AbsInt.WeakUpdateTypes]
print_condState [in ProofOS.AbsInt.SimpleCond]
print_evenOddTy [in ProofOS.Examples.EvenOdd]
print_intPtrTy [in ProofOS.Examples.IntPtr]
print_int32_option [in ProofOS.AbsInt.TopOnly]
print_mastate [in ProofOS.AbsInt.StackTypes]
print_mastate [in ProofOS.AbsInt.FixedCode]
print_mastate [in ProofOS.AbsInt.Bounded]
print_mastate [in ProofOS.AbsInt.TypeSystem]
print_memoryTy [in ProofOS.Examples.MemoryTypes]
print_nostate [in ProofOS.AbsInt.TopOnly]
print_stackState [in ProofOS.AbsInt.StackTypes]
print_stackTy [in ProofOS.AbsInt.StackTypes]
print_stateDescription [in ProofOS.AbsInt.TypeSystem]
print_ty [in ProofOS.AbsInt.WeakUpdateTypes]
print_ty [in ProofOS.AbsInt.SimpleTypes]
print_ty [in ProofOS.AbsInt.StackTypes]
print_ty [in ProofOS.AbsInt.TypeSystem]
print_weakState [in ProofOS.AbsInt.WeakUpdateTypes]
proof_irrelevance [in Asm.Util.Coqlib]

R

R [in ProofOS.AbsInt.Reduce]
roots [in ProofOS.Examples.Vanilla]
roots [in ProofOS.AbsInt.SimpleDriver]
roots [in ProofOS.AbsInt.WeakDriver]

S

sel [in Asm.Util.Map]
sel_empty [in Asm.Util.Map]
sel_eq [in Asm.Util.Map]
sel_neq [in Asm.Util.Map]
stackBig [in ProofOS.AbsInt.WeakDriver]
stackBig [in ProofOS.Examples.Vanilla]
stackBig [in ProofOS.AbsInt.SimpleDriver]
stackCodeSeparate [in ProofOS.AbsInt.StackTypes]
stackCodeSeparate [in ProofOS.Examples.Vanilla]
stackCodeSeparate [in ProofOS.AbsInt.WeakUpdateTypes]
stackCodeSeparate [in ProofOS.AbsInt.SimpleDriver]
stackCodeSeparate [in ProofOS.AbsInt.WeakDriver]
stackFits [in ProofOS.AbsInt.StackTypes]
stackFits [in ProofOS.Examples.Vanilla]
stackFits [in ProofOS.AbsInt.WeakUpdateTypes]
stackFits [in ProofOS.AbsInt.SimpleDriver]
stackFits [in ProofOS.AbsInt.WeakDriver]
stackHigh [in ProofOS.AbsInt.WeakDriver]
stackHigh [in ProofOS.AbsInt.StackTypes]
stackHigh [in ProofOS.AbsInt.SimpleDriver]
stackHigh [in ProofOS.Examples.Vanilla]
stackHigh [in ProofOS.AbsInt.WeakUpdateTypes]
stackLength [in ProofOS.AbsInt.WeakDriver]
stackLength [in ProofOS.AbsInt.StackTypes]
stackLength [in ProofOS.AbsInt.WeakUpdateTypes]
stackLength [in ProofOS.Examples.Vanilla]
stackLength [in ProofOS.AbsInt.SimpleDriver]
stackLongEnough [in ProofOS.Examples.Vanilla]
stackLongEnough [in ProofOS.AbsInt.SimpleDriver]
stackLongEnough [in ProofOS.AbsInt.WeakDriver]
stackStart [in ProofOS.AbsInt.WeakDriver]
stackStart [in ProofOS.Examples.Vanilla]
stackStart [in ProofOS.AbsInt.WeakUpdateTypes]
stackStart [in ProofOS.AbsInt.SimpleDriver]
stackStart [in ProofOS.AbsInt.StackTypes]
subMap [in Asm.Util.Map]
subMastate [in ProofOS.AbsInt.StackTypes]
subMastate [in ProofOS.AbsInt.TypeSystem]
subTy [in ProofOS.AbsInt.StackTypes]
subTy [in ProofOS.AbsInt.WeakUpdateTypes]
subTy [in ProofOS.AbsInt.TypeSystem]
subTy [in ProofOS.AbsInt.SimpleTypes]

T

t [in Asm.Util.Map]
t [in Asm.Util.Map]
to_nat [in Asm.Util.Map]
ty [in ProofOS.AbsInt.TypeSystem]
ty [in ProofOS.AbsInt.StackTypes]
ty [in ProofOS.AbsInt.SimpleTypes]
ty [in ProofOS.AbsInt.WeakUpdateTypes]
tyConst [in ProofOS.AbsInt.TypeSystem]
tyConst [in ProofOS.AbsInt.StackTypes]
tyConst [in ProofOS.AbsInt.WeakUpdateTypes]
tyConst [in ProofOS.AbsInt.SimpleTypes]
tyConstSound1 [in ProofOS.AbsInt.TypeSystem]
tyConstSound1 [in ProofOS.AbsInt.StackTypes]
tyConstSound1 [in ProofOS.AbsInt.SimpleTypes]
tyConstSound1 [in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound2 [in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound2 [in ProofOS.AbsInt.TypeSystem]
tyConstSound2 [in ProofOS.AbsInt.SimpleTypes]
tyConstSound2 [in ProofOS.AbsInt.StackTypes]
typeof [in ProofOS.AbsInt.TypeSystem]
typeof [in ProofOS.AbsInt.StackTypes]
typeofArith [in ProofOS.AbsInt.WeakUpdateTypes]
typeofArith [in ProofOS.AbsInt.SimpleTypes]
typeofCell [in ProofOS.AbsInt.WeakUpdateTypes]
typeofLoad [in ProofOS.AbsInt.TypeSystem]
typeofLoad [in ProofOS.AbsInt.StackTypes]
tyTop [in ProofOS.AbsInt.SimpleTypes]
tyTop [in ProofOS.AbsInt.TypeSystem]
tyTop [in ProofOS.AbsInt.StackTypes]
tyTop [in ProofOS.AbsInt.WeakUpdateTypes]
tyTopSound [in ProofOS.AbsInt.WeakUpdateTypes]
tyTopSound [in ProofOS.AbsInt.TypeSystem]
tyTopSound [in ProofOS.AbsInt.StackTypes]
tyTopSound [in ProofOS.AbsInt.SimpleTypes]

U

upd [in Asm.Util.Map]

V

verify [in ProofOS.AbsInt.Bounded]
viewShiftOfJump [in ProofOS.AbsInt.TypeSystem]
viewShiftOfJump [in ProofOS.AbsInt.StackTypes]

Lemma Index

A

absValidPc_imp [in ProofOS.AbsInt.TypeSystem]
add_even_even [in ProofOS.Examples.EvenOdd]
add_even_odd [in ProofOS.Examples.EvenOdd]
add_odd_even [in ProofOS.Examples.EvenOdd]
add_odd_odd [in ProofOS.Examples.EvenOdd]
add_sub_four [in ProofOS.Examples.MemoryTypes]
agree_range'_refl [in ProofOS.AbsInt.StackTypes]
agree_range'_S [in ProofOS.AbsInt.StackTypes]
agree_range'_slot [in ProofOS.AbsInt.StackTypes]
agree_range'_trans [in ProofOS.AbsInt.StackTypes]
agree_range'_weaken [in ProofOS.AbsInt.StackTypes]
agree_range'_write [in ProofOS.AbsInt.StackTypes]
agree_range_refl [in ProofOS.AbsInt.FixedCode]
agree_range_trans [in ProofOS.AbsInt.FixedCode]
align_le [in Asm.Util.Coqlib]
AllS_dec [in Asm.Util.ListUtil]
AllS_dec_option [in Asm.Util.ListUtil]
AllS_imp [in Asm.Util.ListUtil]
AllS_In [in Asm.Util.ListUtil]
AllS_pdec [in Asm.Util.ListUtil]
AllS_pdec_option [in Asm.Util.ListUtil]
and_false [in ProofOS.Examples.MemoryTypes]
and_true [in ProofOS.Examples.MemoryTypes]
apartFromCode_slot [in ProofOS.AbsInt.StackTypes]
apartFromStack_agree_range' [in ProofOS.AbsInt.StackTypes]
apartFromStack_heap_write [in ProofOS.AbsInt.StackTypes]
apart_binc2_neq [in Asm.X86.Memory]
apart_binc3_neq [in Asm.X86.Memory]
apart_binc_neq [in Asm.X86.Memory]
apart_neq [in Asm.X86.Memory]
apart_or [in ProofOS.AbsInt.FixedCode]
apart_sym [in Asm.X86.Memory]
append_assoc_0 [in Asm.Util.Maps]
append_assoc_1 [in Asm.Util.Maps]
append_injective [in Asm.Util.Maps]
append_neutral_l [in Asm.Util.Maps]
append_neutral_r [in Asm.Util.Maps]

B

badd32_comm [in Asm.Bitvector.BArith]
badd32_swap_neg [in Asm.Bitvector.BArith]
badd_btn_neg [in Asm.Bitvector.BArith]
badd_comm [in Asm.Bitvector.BArith]
badd_zero' [in Asm.Bitvector.BArith]
bdec2_btn [in Asm.Bitvector.BArith]
bdec2_btn' [in Asm.Bitvector.BArith]
bdec3_btn [in Asm.Bitvector.BArith]
bdec3_btn' [in Asm.Bitvector.BArith]
bdec4_btn [in Asm.Bitvector.BArith]
bdec4_btn' [in Asm.Bitvector.BArith]
bdec_binc [in Asm.Bitvector.BArith]
bdec_btn [in Asm.Bitvector.BArith]
bdec_btn' [in Asm.Bitvector.BArith]
belowMax_binc2_dec [in Asm.Bitvector.BArith]
belowMax_binc3_dec [in Asm.Bitvector.BArith]
belowMax_binc_dec [in Asm.Bitvector.BArith]
belowMax_dec [in Asm.Bitvector.BArith]
belowMax_stackEnd [in ProofOS.AbsInt.StackTypes]
binc2_btn [in Asm.Bitvector.BArith]
binc2_btn_belowMax [in Asm.Bitvector.BArith]
binc2_neq [in Asm.Bitvector.BArith]
binc2_neq' [in Asm.Bitvector.BArith]
binc3_btn [in Asm.Bitvector.BArith]
binc3_btn_belowMax [in Asm.Bitvector.BArith]
binc3_neq [in Asm.Bitvector.BArith]
binc3_neq' [in Asm.Bitvector.BArith]
binc4_btn [in Asm.Bitvector.BArith]
binc4_btn_belowMax [in Asm.Bitvector.BArith]
binc_bdec [in Asm.Bitvector.BArith]
binc_btn [in Asm.Bitvector.BArith]
binc_btn_belowMax [in Asm.Bitvector.BArith]
binc_neq [in Asm.Bitvector.BArith]
binc_neq' [in Asm.Bitvector.BArith]
bneg_btn [in Asm.Bitvector.BArith]
bneg_btn_double [in Asm.Bitvector.BArith]
bneg_btn_sub [in Asm.Bitvector.BArith]
bnot_btn [in Asm.Bitvector.Bitwise]
bnot_btn_double [in Asm.Bitvector.Bitwise]
bnot_bzero_mod [in Asm.Bitvector.BArith]
bound_sptr [in ProofOS.AbsInt.StackTypes]
bsub32_eq [in ProofOS.AbsInt.WeakUpdateTypes]
bsub32_eq' [in ProofOS.AbsInt.WeakUpdateTypes]
bsub_bdec [in Asm.Bitvector.BArith]
bsub_bdec2 [in Asm.Bitvector.BArith]
bsub_bdec3 [in Asm.Bitvector.BArith]
bsub_bdec4 [in Asm.Bitvector.BArith]
bsub_btn [in Asm.Bitvector.BArith]
bsub_btn_const [in Asm.Bitvector.BArith]
bsub_btn_neg [in Asm.Bitvector.BArith]
bsub_comm [in ProofOS.AbsInt.WeakUpdateTypes]
bsub_zero [in Asm.Bitvector.BArith]
btn_diff_pos [in Asm.Bitvector.Convert]
btn_four [in ProofOS.Examples.MemoryTypes]
btn_inj [in Asm.Bitvector.Convert]
btn_invert [in Asm.Bitvector.Convert]
btn_upper [in Asm.Bitvector.Convert]
btn_upper' [in Asm.Bitvector.Convert]
btn_upper'' [in Asm.Bitvector.Convert]
bzero_btn [in Asm.Bitvector.BArith]
bzero_inv [in ProofOS.Examples.MemoryTypes]
bzero_neg [in Asm.Bitvector.BArith]
bzero_S_dec [in Asm.Bitvector.BArith]
bzero_S_sub [in Asm.Bitvector.BArith]

C

checkArgs_add [in ProofOS.AbsInt.StackTypes]
cmdOk_sound [in ProofOS.AbsInt.FixedCode]
cmdsOk_sound [in ProofOS.AbsInt.FixedCode]
codeUniform [in ProofOS.AbsInt.WeakDriver]
codeUniform [in ProofOS.Examples.Vanilla]
codeUniform [in ProofOS.AbsInt.SimpleDriver]
combine_commut [in Asm.Util.Maps]
concReg_easy [in ProofOS.AbsInt.WeakUpdateTypes]

D

demult [in Asm.Util.ArithUtil]
div2_add [in Asm.Bitvector.BArith]
div2_add_S [in Asm.Bitvector.BArith]
div2_S2 [in Asm.Util.Mod]
div2_0 [in Asm.Bitvector.BArith]
div2_1 [in Asm.Bitvector.BArith]
div2_2 [in Asm.Util.Mod]
doStackWrite [in ProofOS.AbsInt.WeakUpdateTypes]
double_minus [in Asm.Util.ArithUtil]
double_minus' [in Asm.Util.ArithUtil]

E

elements_complete [in Asm.Util.Maps]
elements_correct [in Asm.Util.Maps]
elements_keys_norepet [in Asm.Util.Maps]
eq [in Asm.Util.Maps]
eq [in Asm.Util.Maps]
eqMod_add_mod [in Asm.Util.Mod]
eqMod_contra [in Asm.Util.Mod]
eqMod_div2 [in Asm.Util.Mod]
eqMod_eq [in Asm.Bitvector.BArith]
eqMod_inj [in Asm.Util.Mod]
eqMod_minus [in Asm.Util.Mod]
eqMod_mod [in Asm.Util.Mod]
eqMod_mod' [in Asm.Util.Mod]
eqMod_mod2_bool [in Asm.Util.Mod]
eqMod_mod_plus [in Asm.Util.Mod]
eqMod_mod_times [in Asm.Util.Mod]
eqMod_mult [in Asm.Util.Mod]
eqMod_mult_mod [in Asm.Util.Mod]
eqMod_nat [in Asm.Util.Mod]
eqMod_nat' [in Asm.Util.Mod]
eqMod_one [in Asm.Util.Mod]
eqMod_plus [in Asm.Util.Mod]
eqMod_plus_minus_mod [in Asm.Util.Mod]
eqMod_plus_minus_mod' [in Asm.Util.Mod]
eqMod_refl [in Asm.Util.Mod]
eqMod_refl' [in ProofOS.Examples.MemoryTypes]
eqMod_S [in Asm.Util.Mod]
eqMod_sym [in Asm.Util.Mod]
eqMod_S_contra [in Asm.Util.Mod]
eqMod_S_contra_pow2 [in Asm.Util.Mod]
eqMod_trans [in Asm.Util.Mod]
eq_dec [in Asm.Util.Map]
eq_get_mem_neq [in Asm.X86.Memory]
eq_vec_dec [in Asm.Util.Vector]
evalExp_flags [in ProofOS.AbsInt.SimpleCond]
evalExp_flags [in ProofOS.AbsInt.WeakUpdateTypes]
evalExp_mem [in ProofOS.AbsInt.SimpleCond]
evalExp_mem [in ProofOS.AbsInt.WeakUpdateTypes]
evalExp_pc [in ProofOS.AbsInt.WeakUpdateTypes]
evalExp_pc [in ProofOS.AbsInt.SimpleCond]
evalExp_salAddr [in ProofOS.AbsInt.Sal]
eval_addr_reg [in ProofOS.AbsInt.Sal]
eval_addr_stack [in ProofOS.AbsInt.Sal]
execCmd_pc [in ProofOS.AbsInt.TypeSystem]
exten [in Asm.Util.Maps]

F

fold_spec [in Asm.Util.Maps]
four_lt_pow2 [in ProofOS.Examples.MemoryTypes]

G

gcombine [in Asm.Util.Maps]
gempty [in Asm.Util.Maps]
get_mem32_flags [in ProofOS.AbsInt.WeakUpdateTypes]
get_xget_h [in Asm.Util.Maps]
gi [in Asm.Util.Maps]
gi [in Asm.Util.Maps]
gi [in Asm.Util.Maps]
gleaf [in Asm.Util.Maps]
gmap [in Asm.Util.Maps]
gmap [in Asm.Util.Maps]
gmap [in Asm.Util.Maps]
gmap [in Asm.Util.Maps]
gro [in Asm.Util.Maps]
grs [in Asm.Util.Maps]
gsident [in Asm.Util.Maps]
gsident [in Asm.Util.Maps]
gsident [in Asm.Util.Maps]
gso [in Asm.Util.Maps]
gso [in Asm.Util.Maps]
gso [in Asm.Util.Maps]
gso [in Asm.Util.Maps]
gss [in Asm.Util.Maps]
gss [in Asm.Util.Maps]
gss [in Asm.Util.Maps]
gss [in Asm.Util.Maps]
gsspec [in Asm.Util.Maps]
gsspec [in Asm.Util.Maps]
gsspec [in Asm.Util.Maps]
gsspec [in Asm.Util.Maps]

H

HT_Const' [in ProofOS.AbsInt.StackTypes]
HT_Stack' [in ProofOS.AbsInt.StackTypes]

I

incl_app_inv_l [in Asm.Util.Coqlib]
incl_app_inv_r [in Asm.Util.Coqlib]
incl_cons_inv [in Asm.Util.Coqlib]
incl_same_head [in Asm.Util.Coqlib]
index_inj [in Asm.X86.Defs]
index_inj [in Asm.Util.Maps]
index_inj [in Asm.Util.Maps]
index_inj [in ProofOS.AbsInt.StackTypes]
index_inj [in ProofOS.AbsInt.Sal]
index_inj [in Asm.X86.Defs]
index_inj [in Asm.X86.Defs]
inHeap_apartFromCode [in ProofOS.AbsInt.WeakUpdateTypes]
inHeap_apartFromStack [in ProofOS.AbsInt.WeakUpdateTypes]
inHeap_not_too_high [in ProofOS.AbsInt.WeakUpdateTypes]
init [in ProofOS.AbsInt.Sal]
instructionsOk_sound [in ProofOS.AbsInt.FixedCode]
invert_index [in ProofOS.AbsInt.Sal]
invert_index [in Asm.Util.Maps]
invert_index [in Asm.X86.Defs]
invert_index [in ProofOS.AbsInt.StackTypes]
invert_index [in Asm.X86.Defs]
invert_index [in Asm.Util.Maps]
invert_index [in Asm.X86.Defs]
invert_set_mem' [in Asm.X86.Memory]
invert_set_mem32 [in Asm.X86.Memory]
invert_set_mem32 [in ProofOS.AbsInt.Sal]
invert_set_mem32' [in Asm.X86.Memory]
invert_set_mem32'_binc2_neq' [in Asm.X86.Memory]
invert_set_mem32'_binc3_neq' [in Asm.X86.Memory]
invert_set_mem32'_binc_neq' [in Asm.X86.Memory]
invert_set_mem32'_neq [in Asm.X86.Memory]
invert_set_mem32'_neq' [in Asm.X86.Memory]
invert_set_mem32_neq [in ProofOS.AbsInt.Sal]
invert_set_mem32_neq [in Asm.X86.Memory]
In_AllS [in Asm.Util.ListUtil]
In_dec [in Asm.Util.ListUtil]
In_map [in Asm.Util.ListUtil]
In_map' [in Asm.Util.ListUtil]
in_xelements [in Asm.Util.Maps]
in_xkeys [in Asm.Util.Maps]

J

jmpMem [in ProofOS.AbsInt.FixedCode]

L

list_append_map [in Asm.Util.Coqlib]
list_disjoint_cons_left [in Asm.Util.Coqlib]
list_disjoint_cons_right [in Asm.Util.Coqlib]
list_disjoint_notin [in Asm.Util.Coqlib]
list_disjoint_sym [in Asm.Util.Coqlib]
list_forall2_imply [in Asm.Util.Coqlib]
list_in_map_inv [in Asm.Util.Coqlib]
list_length_map [in Asm.Util.Coqlib]
list_map_compose [in Asm.Util.Coqlib]
list_map_exten [in Asm.Util.Coqlib]
list_map_norepet [in Asm.Util.Coqlib]
list_map_nth [in Asm.Util.Coqlib]
list_norepet_append [in Asm.Util.Coqlib]
list_norepet_append_left [in Asm.Util.Coqlib]
list_norepet_append_right [in Asm.Util.Coqlib]
list_norepet_dec [in Asm.Util.Coqlib]
lowerTy_map_sound [in ProofOS.AbsInt.StackTypes]
lowerTy_sound [in ProofOS.AbsInt.StackTypes]
lowerTy_sound [in ProofOS.AbsInt.WeakUpdateTypes]
lt_asym [in Asm.Util.Map]
lt_dec [in Asm.Util.Map]
lt_irr [in Asm.Util.Map]

M

mconc_sptr_not_too_high [in ProofOS.AbsInt.StackTypes]
merge_times [in ProofOS.Examples.EvenOdd]
merge_times_S [in ProofOS.Examples.EvenOdd]
merge_times_S2 [in ProofOS.Examples.EvenOdd]
merge_times_S3 [in ProofOS.Examples.EvenOdd]
minus_lt [in ProofOS.AbsInt.StackTypes]
minus_lt2 [in ProofOS.AbsInt.StackTypes]
minus_plus' [in Asm.Util.ArithUtil]
minus_S_1 [in Asm.Util.ArithUtil]
mod2_bool_add [in Asm.Bitvector.BArith]
mod2_bool_add_S [in Asm.Bitvector.BArith]
mod2_bool_S2 [in Asm.Util.Mod]
mod2_bool_0 [in Asm.Bitvector.BArith]
mod2_bool_1 [in Asm.Bitvector.BArith]
mod2_bool_2 [in Asm.Util.Mod]
mod2_div2 [in Asm.Bitvector.Convert]
mod2_inj [in Asm.Bitvector.Convert]
mod2_S2 [in Asm.Util.Mod]
mod2_2 [in Asm.Util.Mod]
mult_inc [in ProofOS.AbsInt.WeakUpdateTypes]

N

neq_lt [in Asm.Util.Map]
neq_sym [in Asm.X86.Memory]
not_too_high_minus [in ProofOS.AbsInt.StackTypes]
not_too_high_slot [in ProofOS.AbsInt.StackTypes]
ntb_add [in Asm.Bitvector.Convert]
ntb_cong [in ProofOS.AbsInt.StackTypes]
ntb_invert [in Asm.Bitvector.Convert]
ntb_invert_eqMod [in Asm.Bitvector.Convert]
ntb_invert_mod [in Asm.Bitvector.Convert]
ntb_mod [in Asm.Bitvector.Convert]
ntb_mod' [in Asm.Bitvector.Convert]
nth_error_in [in Asm.Util.Coqlib]
nth_error_nil [in Asm.Util.Coqlib]

O

or_true [in ProofOS.Examples.MemoryTypes]

P

pcInRange [in ProofOS.AbsInt.WeakDriver]
pcInRange [in ProofOS.Examples.Vanilla]
pcInRange [in ProofOS.AbsInt.SimpleDriver]
pcToAbs_map'_sound [in ProofOS.AbsInt.TypeSystem]
peq_false [in Asm.Util.Coqlib]
peq_true [in Asm.Util.Coqlib]
percolate_minus_1 [in Asm.Util.ArithUtil]
Ple_refl [in Asm.Util.Coqlib]
Ple_succ [in Asm.Util.Coqlib]
Ple_trans [in Asm.Util.Coqlib]
Plt_ne [in Asm.Util.Coqlib]
Plt_Ple [in Asm.Util.Coqlib]
Plt_Ple_trans [in Asm.Util.Coqlib]
Plt_strict [in Asm.Util.Coqlib]
Plt_succ [in Asm.Util.Coqlib]
Plt_succ_inv [in Asm.Util.Coqlib]
Plt_trans [in Asm.Util.Coqlib]
Plt_trans_succ [in Asm.Util.Coqlib]
Plt_wf [in Asm.Util.Coqlib]
plus_minus [in Asm.Util.ArithUtil]
popt_to_bool_true [in Asm.Util.Specif]
positive_Peano_ind [in Asm.Util.Coqlib]
positive_rec_base [in Asm.Util.Coqlib]
positive_rec_succ [in Asm.Util.Coqlib]
pow2_gt_1 [in ProofOS.AbsInt.WeakUpdateTypes]
pow2_plus [in Asm.Util.ArithUtil]
pow2_pos [in Asm.Util.ArithUtil]
pow2_times2 [in Asm.Util.ArithUtil]
Ppred_Plt [in Asm.Util.Coqlib]
preservation_call_covered [in ProofOS.AbsInt.TypeSystem]
preservation_conditional_covered [in ProofOS.AbsInt.TypeSystem]
preservation_fallthru [in ProofOS.AbsInt.TypeSystem]
preservation_fallthru_covered [in ProofOS.AbsInt.TypeSystem]
preservation_jump_covered [in ProofOS.AbsInt.TypeSystem]
preservation_ret_covered [in ProofOS.AbsInt.TypeSystem]
progress_call [in ProofOS.AbsInt.TypeSystem]
progress_conditional [in ProofOS.AbsInt.TypeSystem]
progress_fallthru [in ProofOS.AbsInt.TypeSystem]
progress_jump [in ProofOS.AbsInt.TypeSystem]
progress_ret [in ProofOS.AbsInt.TypeSystem]
Psucc_inj [in Asm.Util.ArithUtil]
P_of_succ_nat_inj [in Asm.X86.Defs]
P_of_succ_nat_inj [in Asm.Util.ArithUtil]

R

raiseTy_sound [in ProofOS.AbsInt.WeakUpdateTypes]
relativity [in ProofOS.AbsInt.Bounded]
rewrite_double [in ProofOS.Examples.EvenOdd]
rewrite_minus_plus [in Asm.Util.ArithUtil]
rewrite_minus_0 [in Asm.Util.ArithUtil]
rewrite_plus_four [in ProofOS.AbsInt.StackTypes]
rewrite_plus_0 [in Asm.Util.ArithUtil]
rewrite_S [in Asm.Util.ArithUtil]
rewrite_times_2 [in Asm.Util.ArithUtil]
rewrite_undistrib [in Asm.Util.ArithUtil]
rewrite_undistrib_minus [in Asm.Util.ArithUtil]
rewrite_undistrib_minus_const [in Asm.Util.ArithUtil]
rleaf [in Asm.Util.Maps]

S

set_stack32_sound [in ProofOS.AbsInt.StackTypes]
shiftAbs_lt [in ProofOS.AbsInt.StackTypes]
shiftAbs_lt' [in ProofOS.AbsInt.StackTypes]
shiftAbs_lt'' [in ProofOS.AbsInt.StackTypes]
Some_get_mem32_cong [in ProofOS.AbsInt.StackTypes]
split32_sound [in Asm.Bitvector.Split]
split_sound [in Asm.Bitvector.Split]
stack_slot_rewrite [in ProofOS.AbsInt.StackTypes]
stack_slot_rewrite2 [in ProofOS.AbsInt.StackTypes]
stack_slot_rewrite3 [in ProofOS.AbsInt.StackTypes]
subTy'_sound [in ProofOS.Examples.MemoryTypes]
sub_one [in Asm.Util.ArithUtil]
sub_one_pow2 [in Asm.Util.ArithUtil]
sub_one_S [in Asm.Util.ArithUtil]
S_minus_1 [in Asm.Util.ArithUtil]
S_minus_1_pow2 [in Asm.Bitvector.Convert]
S_times_two [in Asm.Util.ArithUtil]

T

two_gt_0 [in Asm.Util.Mod]
two_power_nat_O [in Asm.Util.Coqlib]
two_power_nat_pos [in Asm.Util.Coqlib]
tyConstSound1 [in ProofOS.AbsInt.StackTypes]
tyConstSound1 [in ProofOS.AbsInt.TopOnly]
tyConstSound1 [in ProofOS.AbsInt.SimpleTypes]
tyConstSound1 [in ProofOS.Examples.EvenOdd]
tyConstSound2 [in ProofOS.AbsInt.StackTypes]
tyConstSound2 [in ProofOS.Examples.MemoryTypes]
tyConstSound2 [in ProofOS.AbsInt.TopOnly]
tyConstSound2 [in ProofOS.Examples.EvenOdd]
tyConstSound2 [in ProofOS.Examples.IntPtr]
tyConstSound2 [in ProofOS.AbsInt.SimpleTypes]
tyTopSound [in ProofOS.AbsInt.SimpleTypes]
tyTopSound [in ProofOS.Examples.EvenOdd]
tyTopSound [in ProofOS.AbsInt.StackTypes]
tyTopSound [in ProofOS.AbsInt.TopOnly]
tyTopSound' [in ProofOS.AbsInt.TopOnly]
ty_eq_dec'_sound1 [in ProofOS.Examples.MemoryTypes]
ty_eq_dec'_sound2 [in ProofOS.Examples.MemoryTypes]

U

undo_rewrite_fourx [in ProofOS.AbsInt.StackTypes]
undo_rewrite_fourx_plus [in ProofOS.AbsInt.StackTypes]
unroll_positive_rec [in Asm.Util.Coqlib]
use_asafe [in ProofOS.AbsInt.Bounded]

V

Vid_eq [in Asm.Util.Vector]
viewShift_boring [in ProofOS.AbsInt.StackTypes]
viewShift_concSlots [in ProofOS.AbsInt.StackTypes]
viewShift_eq [in ProofOS.AbsInt.StackTypes]
viewShift_ret_eq [in ProofOS.AbsInt.StackTypes]
VO_eq [in Asm.Util.Vector]
VSn_eq [in Asm.Util.Vector]

W

wordAligned_neq [in ProofOS.AbsInt.WeakUpdateTypes]

X

xcombine_lr [in Asm.Util.Maps]
xelements_complete [in Asm.Util.Maps]
xelements_correct [in Asm.Util.Maps]
xelements_hi [in Asm.Util.Maps]
xelements_ho [in Asm.Util.Maps]
xelements_ih [in Asm.Util.Maps]
xelements_ii [in Asm.Util.Maps]
xelements_io [in Asm.Util.Maps]
xelements_keys_norepet [in Asm.Util.Maps]
xelements_oh [in Asm.Util.Maps]
xelements_oi [in Asm.Util.Maps]
xelements_oo [in Asm.Util.Maps]
xgcombine [in Asm.Util.Maps]
xgcombine_l [in Asm.Util.Maps]
xgcombine_r [in Asm.Util.Maps]
xget_left [in Asm.Util.Maps]
xgmap [in Asm.Util.Maps]

Z

Zdiv_small [in Asm.Util.Coqlib]
Zdiv_unique [in Asm.Util.Coqlib]
zeq_false [in Asm.Util.Coqlib]
zeq_true [in Asm.Util.Coqlib]
zero_ntb [in Asm.Bitvector.BArith]
zero_one_neq [in ProofOS.Examples.MemoryTypes]
zle_false [in Asm.Util.Coqlib]
zle_true [in Asm.Util.Coqlib]
zlt_false [in Asm.Util.Coqlib]
zlt_true [in Asm.Util.Coqlib]
Zmax_bound_l [in Asm.Util.Coqlib]
Zmax_bound_r [in Asm.Util.Coqlib]
Zmax_spec [in Asm.Util.Coqlib]
Zmin_spec [in Asm.Util.Coqlib]
Zmod_small [in Asm.Util.Coqlib]
Zmod_unique [in Asm.Util.Coqlib]
Z_of_nat_bit [in Asm.Util.ArithUtil]
Z_of_nat_inj [in Asm.Util.ArithUtil]
Z_rewrite_plus_0 [in Asm.Util.ArithUtil]
Z_rewrite_times_0 [in Asm.Util.ArithUtil]

Constructor Index

A

AC [in Asm.X86.Defs]
Add [in Asm.X86.Defs]
Address [in Asm.X86.Defs]
AF [in Asm.X86.Defs]
AH [in Asm.X86.Defs]
AL [in Asm.X86.Defs]
And [in Asm.X86.Defs]
Anything [in ProofOS.Examples.IntPtr]
Anything [in ProofOS.Examples.EvenOdd]
apart_higher [in Asm.X86.Memory]
apart_lower [in Asm.X86.Memory]
ApcConst [in ProofOS.AbsInt.TypeSystem]
ApcUnknown [in ProofOS.AbsInt.TypeSystem]
Arith [in Asm.X86.Defs]
Arithb [in Asm.X86.Defs]

B

B [in Asm.X86.Defs]
BE [in Asm.X86.Defs]
belowMax_rule [in Asm.Bitvector.BArith]
BH [in Asm.X86.Defs]
BL [in Asm.X86.Defs]

C

Call [in Asm.X86.Defs]
CF [in Asm.X86.Defs]
CH [in Asm.X86.Defs]
CL [in Asm.X86.Defs]
Cmp [in Asm.X86.Defs]
Const [in ProofOS.AbsInt.StackTypes]
Constant [in ProofOS.Examples.MemoryTypes]
Constant [in ProofOS.Examples.EvenOdd]
Constant [in ProofOS.Examples.IntPtr]
Cust [in ProofOS.AbsInt.StackTypes]

D

DF [in Asm.X86.Defs]
DH [in Asm.X86.Defs]
DL [in Asm.X86.Defs]

E

EAX [in Asm.X86.Defs]
EBP [in Asm.X86.Defs]
EBX [in Asm.X86.Defs]
ECX [in Asm.X86.Defs]
EDI [in Asm.X86.Defs]
EDX [in Asm.X86.Defs]
ESI [in Asm.X86.Defs]
ESP [in Asm.X86.Defs]
Even [in ProofOS.Examples.EvenOdd]

H

HT_Anything [in ProofOS.Examples.IntPtr]
HT_Anything [in ProofOS.Examples.EvenOdd]
HT_Const [in ProofOS.AbsInt.StackTypes]
HT_Constant [in ProofOS.Examples.EvenOdd]
HT_Constant [in ProofOS.Examples.MemoryTypes]
HT_Constant [in ProofOS.Examples.IntPtr]
HT_Cust [in ProofOS.AbsInt.StackTypes]
HT_Even [in ProofOS.Examples.EvenOdd]
HT_NnPtr [in ProofOS.Examples.IntPtr]
HT_Odd [in ProofOS.Examples.EvenOdd]
HT_OldEbp [in ProofOS.AbsInt.StackTypes]
HT_Product [in ProofOS.Examples.MemoryTypes]
HT_Ptr_NonNull [in ProofOS.Examples.IntPtr]
HT_Ptr_Null [in ProofOS.Examples.IntPtr]
HT_Recursive [in ProofOS.Examples.MemoryTypes]
HT_RetPtr [in ProofOS.AbsInt.StackTypes]
HT_Stack [in ProofOS.AbsInt.StackTypes]
HT_Suml [in ProofOS.Examples.MemoryTypes]
HT_Sumr [in ProofOS.Examples.MemoryTypes]
HT_Top [in ProofOS.AbsInt.StackTypes]
HT_Unit [in ProofOS.Examples.MemoryTypes]

I

ID [in Asm.X86.Defs]
IF_flag [in Asm.X86.Defs]
Imm [in Asm.X86.Defs]
Inc [in Asm.X86.Defs]
IOPL [in Asm.X86.Defs]

J

Jcc [in Asm.X86.Defs]
Jmp [in Asm.X86.Defs]

L

L [in Asm.X86.Defs]
LE [in Asm.X86.Defs]
Lea [in Asm.X86.Defs]
Leaf [in Asm.Util.Maps]
Leave [in Asm.X86.Defs]
list_forall2_cons [in Asm.Util.Coqlib]
list_forall2_nil [in Asm.Util.Coqlib]
list_norepet_cons [in Asm.Util.Coqlib]
list_norepet_nil [in Asm.Util.Coqlib]

M

Mov [in Asm.X86.Defs]
Movb [in Asm.X86.Defs]

N

NnPtr [in ProofOS.Examples.IntPtr]
Node [in Asm.Util.Maps]
NT [in Asm.X86.Defs]

O

O [in Asm.X86.Defs]
Odd [in ProofOS.Examples.EvenOdd]
OF [in Asm.X86.Defs]
OldEbp [in ProofOS.AbsInt.StackTypes]
Or [in Asm.X86.Defs]
OrdEq [in Asm.Util.Map]
OrdGt [in Asm.Util.Map]
OrdLt [in Asm.Util.Map]

P

P [in Asm.X86.Defs]
PF [in Asm.X86.Defs]
PNone [in Asm.Util.Specif]
Pop [in Asm.X86.Defs]
Product [in ProofOS.Examples.MemoryTypes]
PSome [in Asm.Util.Specif]
Ptr [in ProofOS.Examples.IntPtr]
PT_Cons [in ProofOS.Examples.MemoryTypes]
PT_Nil [in ProofOS.Examples.MemoryTypes]
Push [in Asm.X86.Defs]

R

Recursive [in ProofOS.Examples.MemoryTypes]
Reg [in Asm.X86.Defs]
Ret [in Asm.X86.Defs]
RetPtr [in ProofOS.AbsInt.StackTypes]
RF [in Asm.X86.Defs]
rsafe_step [in ProofOS.AbsInt.Bounded]

S

S [in Asm.X86.Defs]
safe_rule [in ProofOS.Trusted.Safety]
SArith [in ProofOS.AbsInt.Sal]
Scale1 [in Asm.X86.Defs]
Scale2 [in Asm.X86.Defs]
Scale4 [in Asm.X86.Defs]
Scale8 [in Asm.X86.Defs]
SCall [in ProofOS.AbsInt.Sal]
SCompare [in ProofOS.AbsInt.Sal]
SConditionalJump [in ProofOS.AbsInt.Sal]
SConst [in ProofOS.AbsInt.Sal]
SF [in Asm.X86.Defs]
SFail [in ProofOS.AbsInt.Sal]
SFallthru [in ProofOS.AbsInt.Sal]
Shift [in Asm.X86.Defs]
Shl [in Asm.X86.Defs]
Shr [in Asm.X86.Defs]
SIndirectJump [in ProofOS.AbsInt.Sal]
SJump [in ProofOS.AbsInt.Sal]
SLoad [in ProofOS.AbsInt.Sal]
SNoCF [in ProofOS.AbsInt.Sal]
SNone [in Asm.Util.Specif]
SReg [in ProofOS.AbsInt.Sal]
SRet [in ProofOS.AbsInt.Sal]
SSet [in ProofOS.AbsInt.Sal]
SShift [in ProofOS.AbsInt.Sal]
SSome [in Asm.Util.Specif]
SStore [in ProofOS.AbsInt.Sal]
Stack [in ProofOS.AbsInt.StackTypes]
step_fp [in ProofOS.AbsInt.Bounded]
step_rel [in ProofOS.AbsInt.Bounded]
STmp1 [in ProofOS.AbsInt.Sal]
STmp2 [in ProofOS.AbsInt.Sal]
Sub [in Asm.X86.Defs]
Sum [in ProofOS.Examples.MemoryTypes]
SWithCF [in ProofOS.AbsInt.Sal]
SX86 [in ProofOS.AbsInt.Sal]

T

TF [in Asm.X86.Defs]
Top [in ProofOS.AbsInt.StackTypes]

V

Var [in ProofOS.Examples.MemoryTypes]
VIF [in Asm.X86.Defs]
VIP [in Asm.X86.Defs]
VM [in Asm.X86.Defs]

W

WriteMem [in Asm.X86.Defs]
WriteReg [in Asm.X86.Defs]

X

XArith [in Asm.X86.Defs]
XCall [in Asm.X86.Defs]
XCmp [in Asm.X86.Defs]
XInc [in Asm.X86.Defs]
XJcc_false [in Asm.X86.Defs]
XJcc_true [in Asm.X86.Defs]
XJmp [in Asm.X86.Defs]
XLea [in Asm.X86.Defs]
XLeave [in Asm.X86.Defs]
XMov [in Asm.X86.Defs]
XPop [in Asm.X86.Defs]
XPush [in Asm.X86.Defs]
XRet [in Asm.X86.Defs]

Z

Z [in Asm.X86.Defs]
ZF [in Asm.X86.Defs]

Inductive Index

A

address [in Asm.X86.Defs]
apart [in Asm.X86.Memory]
apc [in ProofOS.AbsInt.TypeSystem]
arith_op [in Asm.X86.Defs]

B

belowMax [in Asm.Bitvector.BArith]

C

condConc [in ProofOS.AbsInt.SimpleCond]
condition [in Asm.X86.Defs]
condState [in ProofOS.AbsInt.SimpleCond]

E

evenOddTy [in ProofOS.Examples.EvenOdd]
exec [in Asm.X86.Defs]

F

flag [in Asm.X86.Defs]
function_info [in ProofOS.AbsInt.StackTypes]

G

genop [in Asm.X86.Defs]

H

hasEvenOddTy [in ProofOS.Examples.EvenOdd]
hasIntPtrTy [in ProofOS.Examples.IntPtr]
hasMemoryTy [in ProofOS.Examples.MemoryTypes]

I

instr [in Asm.X86.Defs]
intPtrTy [in ProofOS.Examples.IntPtr]

L

list_forall2 [in Asm.Util.Coqlib]
list_norepet [in Asm.Util.Coqlib]

M

memoryTy [in ProofOS.Examples.MemoryTypes]

O

ord [in Asm.Util.Map]

P

pred_option [in Asm.Util.Specif]
productTy [in ProofOS.Examples.MemoryTypes]

R

R [in ProofOS.AbsInt.Sal]
reg32 [in Asm.X86.Defs]
reg8 [in Asm.X86.Defs]
relatively_safe [in ProofOS.AbsInt.Bounded]

S

safe [in ProofOS.Trusted.Safety]
salCmd [in ProofOS.AbsInt.Sal]
salCmp [in ProofOS.AbsInt.Sal]
salExp [in ProofOS.AbsInt.Sal]
salIJump [in ProofOS.AbsInt.Sal]
salJump [in ProofOS.AbsInt.Sal]
salReg [in ProofOS.AbsInt.Sal]
salState [in ProofOS.AbsInt.Sal]
scale [in Asm.X86.Defs]
shift_op [in Asm.X86.Defs]
sig_option [in Asm.Util.Specif]
stackConc [in ProofOS.AbsInt.StackTypes]
stackContext [in ProofOS.AbsInt.StackTypes]
stackHasTy [in ProofOS.AbsInt.StackTypes]
stackState [in ProofOS.AbsInt.StackTypes]
stackTy [in ProofOS.AbsInt.StackTypes]
state [in Asm.X86.Defs]
stateDescription [in ProofOS.AbsInt.TypeSystem]
step_safe [in ProofOS.AbsInt.Bounded]

T

tree [in Asm.Util.Maps]
typeMconc [in ProofOS.AbsInt.TypeSystem]

V

viewShift [in ProofOS.AbsInt.TypeSystem]

W

weakConc [in ProofOS.AbsInt.WeakUpdateTypes]
write_genop32 [in Asm.X86.Defs]

_

_mconc [in ProofOS.AbsInt.FixedCode]

Definition Index

A

absEval_cc [in ProofOS.AbsInt.SimpleCond]
absValidPc [in ProofOS.AbsInt.TypeSystem]
absValidPc [in ProofOS.AbsInt.FixedCode]
absValidPc [in ProofOS.AbsInt.FixedCode]
absValidPc' [in ProofOS.AbsInt.TypeSystem]
absValidPc_dec [in ProofOS.AbsInt.FixedCode]
agree_range [in Asm.X86.Defs]
agree_range' [in ProofOS.AbsInt.StackTypes]
align [in Asm.Util.Coqlib]
apartFromCode [in ProofOS.AbsInt.FixedCode]
apartFromStack [in ProofOS.AbsInt.StackTypes]
apc_eq_dec [in ProofOS.AbsInt.TypeSystem]
append [in Asm.Util.Maps]
argsStack [in ProofOS.AbsInt.StackTypes]
arith_flags [in ProofOS.AbsInt.Sal]
arith_flags [in Asm.X86.Defs]
arith_flags' [in Asm.X86.Defs]
arith_flags_no_CF [in ProofOS.AbsInt.Sal]
arith_flags_no_CF [in Asm.X86.Defs]
arith_flags_no_CF' [in Asm.X86.Defs]
arith_op_eq_dec [in ProofOS.AbsInt.WeakUpdateTypes]
arith_op_eq_dec [in ProofOS.AbsInt.SimpleCond]
asafe [in ProofOS.AbsInt.Bounded]

B

badd [in Asm.Bitvector.Defs]
badd16 [in Asm.Bitvector.Defs]
badd32 [in Asm.Bitvector.Defs]
badd8 [in Asm.Bitvector.Defs]
band [in Asm.Bitvector.Defs]
band16 [in Asm.Bitvector.Defs]
band32 [in Asm.Bitvector.Defs]
band8 [in Asm.Bitvector.Defs]
barith [in Asm.Bitvector.Defs]
bdec [in Asm.Bitvector.Defs]
bdec2 [in Asm.Bitvector.Defs]
bdec3 [in Asm.Bitvector.Defs]
bdec4 [in Asm.Bitvector.Defs]
binc [in Asm.Bitvector.Defs]
binc2 [in Asm.Bitvector.Defs]
binc3 [in Asm.Bitvector.Defs]
binc4 [in Asm.Bitvector.Defs]
ble_dec [in Asm.Bitvector.Defs]
blt_dec [in Asm.Bitvector.Defs]
bmax [in Asm.Bitvector.Defs]
bneg [in Asm.Bitvector.Defs]
bneg16 [in Asm.Bitvector.Defs]
bneg32 [in Asm.Bitvector.Defs]
bneg8 [in Asm.Bitvector.Defs]
bnot [in Asm.Bitvector.Defs]
bnot16 [in Asm.Bitvector.Defs]
bnot32 [in Asm.Bitvector.Defs]
bnot8 [in Asm.Bitvector.Defs]
bone [in Asm.Bitvector.Defs]
bone16 [in Asm.Bitvector.Defs]
bone32 [in Asm.Bitvector.Defs]
bone8 [in Asm.Bitvector.Defs]
bool_eq_dec [in ProofOS.AbsInt.StackTypes]
bor [in Asm.Bitvector.Defs]
bor16 [in Asm.Bitvector.Defs]
bor32 [in Asm.Bitvector.Defs]
bor8 [in Asm.Bitvector.Defs]
bounded_verify [in ProofOS.AbsInt.Bounded]
bshl [in Asm.Bitvector.Defs]
bshl16 [in Asm.Bitvector.Defs]
bshl32 [in Asm.Bitvector.Defs]
bshl8 [in Asm.Bitvector.Defs]
bshr [in Asm.Bitvector.Defs]
bshr16 [in Asm.Bitvector.Defs]
bshr32 [in Asm.Bitvector.Defs]
bshr8 [in Asm.Bitvector.Defs]
bsub [in Asm.Bitvector.Defs]
bsub16 [in Asm.Bitvector.Defs]
bsub32 [in Asm.Bitvector.Defs]
bsub8 [in Asm.Bitvector.Defs]
bvec_eq [in Asm.Bitvector.Defs]
bvec_eq_dec [in Asm.Bitvector.Defs]
bvec_to_nat [in Asm.Bitvector.Defs]
byte1 [in Asm.Bitvector.Split]
byte2 [in Asm.Bitvector.Split]
byte3 [in Asm.Bitvector.Split]
byte4 [in Asm.Bitvector.Split]
bzero [in Asm.Bitvector.Defs]
bzero16 [in Asm.Bitvector.Defs]
bzero32 [in Asm.Bitvector.Defs]
bzero8 [in Asm.Bitvector.Defs]

C

callStep [in ProofOS.AbsInt.TypeSystem]
callStep [in ProofOS.AbsInt.FixedCode]
callStep [in ProofOS.AbsInt.Reduce]
callStep [in ProofOS.AbsInt.Bounded]
callStep [in ProofOS.AbsInt.FixedCode]
cameFrom [in ProofOS.AbsInt.Sal]
cc [in Asm.X86.Defs]
checkArgs [in ProofOS.AbsInt.StackTypes]
checkArgsR [in ProofOS.AbsInt.StackTypes]
checkArgs' [in ProofOS.AbsInt.StackTypes]
checkCmd [in ProofOS.AbsInt.TypeSystem]
checkCmds [in ProofOS.AbsInt.TypeSystem]
checkJump [in ProofOS.AbsInt.TypeSystem]
checkStore [in ProofOS.AbsInt.StackTypes]
checkStore [in ProofOS.AbsInt.TopOnly]
checkStore [in ProofOS.AbsInt.SimpleTypes]
checkStore [in ProofOS.AbsInt.WeakUpdateTypes]
checkStore [in ProofOS.AbsInt.WeakUpdateTypes]
checkStore [in ProofOS.AbsInt.SimpleCond]
checkStoreR [in ProofOS.AbsInt.StackTypes]
check_cc [in ProofOS.AbsInt.Sal]
check_cc [in Asm.X86.Defs]
check_cc' [in Asm.X86.Defs]
check_cc_eq [in ProofOS.AbsInt.Sal]
check_cc_eq' [in ProofOS.AbsInt.Sal]
check_cc_imp [in ProofOS.AbsInt.Sal]
check_cc_imp' [in ProofOS.AbsInt.Sal]
check_condition' [in Asm.X86.Defs]
check_tripleOpt [in ProofOS.AbsInt.SimpleCond]
cmdOk [in ProofOS.AbsInt.FixedCode]
cmdsOk [in ProofOS.AbsInt.FixedCode]
codeFits [in ProofOS.Examples.Vanilla]
codeFits [in ProofOS.AbsInt.WeakDriver]
codeFits [in ProofOS.AbsInt.SimpleDriver]
codeHigh [in ProofOS.AbsInt.SimpleDriver]
codeHigh [in ProofOS.AbsInt.WeakDriver]
codeHigh [in ProofOS.Examples.Vanilla]
codeLength [in ProofOS.Examples.Vanilla]
codeLength [in ProofOS.AbsInt.SimpleDriver]
codeLength [in ProofOS.AbsInt.WeakDriver]
codeStart [in ProofOS.AbsInt.SimpleDriver]
codeStart [in ProofOS.Examples.Vanilla]
codeStart [in ProofOS.AbsInt.WeakDriver]
combine [in Asm.Util.Maps]
compile [in ProofOS.AbsInt.Sal]
concAddr [in ProofOS.AbsInt.WeakUpdateTypes]
concReg [in ProofOS.AbsInt.WeakUpdateTypes]
conc_slots [in ProofOS.AbsInt.StackTypes]
considerDerefEq [in ProofOS.Examples.IntPtr]
considerDerefEq [in ProofOS.Examples.MemoryTypes]
considerDerefNeq [in ProofOS.Examples.IntPtr]
considerDerefNeq [in ProofOS.Examples.MemoryTypes]
considerNeq [in ProofOS.Examples.MemoryTypes]
considerNeq [in ProofOS.Examples.IntPtr]
considerTest [in ProofOS.AbsInt.WeakUpdateTypes]
contains [in ProofOS.AbsInt.WeakUpdateTypes]
cstep [in ProofOS.Trusted.Safety]
cstep [in ProofOS.Trusted.Safety]

D

disjointRegions [in ProofOS.AbsInt.StackTypes]
div2 [in Asm.Util.Mod]
doCastEq [in ProofOS.AbsInt.WeakUpdateTypes]
doCastNeq [in ProofOS.AbsInt.WeakUpdateTypes]
doStackWrite [in ProofOS.AbsInt.TopOnly]
doStackWrite [in ProofOS.AbsInt.WeakUpdateTypes]
doStackWrite [in ProofOS.AbsInt.SimpleCond]
doStackWrite [in ProofOS.AbsInt.SimpleTypes]
dummyConc [in ProofOS.AbsInt.SimpleTypes]
dummyHasTy [in ProofOS.AbsInt.SimpleTypes]

E

effectOfCmd [in ProofOS.AbsInt.WeakUpdateTypes]
effectOfCmd [in ProofOS.AbsInt.StackTypes]
effectOfCmd [in ProofOS.AbsInt.WeakUpdateTypes]
effectOfCmd [in ProofOS.AbsInt.SimpleTypes]
effectOfCmd [in ProofOS.AbsInt.TopOnly]
effectOfCmd [in ProofOS.AbsInt.SimpleCond]
effectOfCmdR [in ProofOS.AbsInt.StackTypes]
effectOfConditionalJump [in ProofOS.AbsInt.WeakUpdateTypes]
effectOfConditionalJump [in ProofOS.AbsInt.StackTypes]
effectOfConditionalJump [in ProofOS.AbsInt.TopOnly]
effectOfConditionalJump [in ProofOS.AbsInt.SimpleCond]
effectOfConditionalJump [in ProofOS.AbsInt.WeakUpdateTypes]
effectOfConditionalJump [in ProofOS.AbsInt.SimpleTypes]
effectOfJump [in ProofOS.AbsInt.WeakUpdateTypes]
effectOfJump [in ProofOS.AbsInt.SimpleTypes]
effectOfJump [in ProofOS.AbsInt.TopOnly]
effectOfJump [in ProofOS.AbsInt.WeakUpdateTypes]
effectOfJump [in ProofOS.AbsInt.StackTypes]
effectOfJump [in ProofOS.AbsInt.SimpleCond]
effectOfJumpR [in ProofOS.AbsInt.StackTypes]
elements [in Asm.Util.Maps]
elements [in Asm.Util.Maps]
elt [in Asm.Util.Maps]
elt [in Asm.Util.Maps]
elt [in Asm.Util.Maps]
elt [in Asm.Util.Maps]
elt_eq [in Asm.Util.Maps]
elt_eq [in Asm.Util.Maps]
elt_eq [in Asm.Util.Maps]
elt_eq [in Asm.Util.Maps]
empty [in Asm.Util.Maps]
eq [in ProofOS.AbsInt.StackTypes]
eq [in Asm.X86.Defs]
eq [in ProofOS.AbsInt.Sal]
eq [in Asm.X86.Defs]
eq [in Asm.X86.Defs]
eq [in Asm.Util.Maps]
eqMod [in Asm.Util.Mod]
eq_dec [in Asm.Util.Map]
eq_dec_to_eq [in Asm.Util.Map]
eq_dec_triple [in ProofOS.AbsInt.SimpleCond]
eq_dec_tripleOpt [in ProofOS.AbsInt.SimpleCond]
evalExp [in ProofOS.AbsInt.Sal]
eval_addr [in Asm.X86.Defs]
eval_arith [in Asm.X86.Defs]
eval_cc [in ProofOS.AbsInt.SimpleCond]
eval_CF [in Asm.X86.Defs]
eval_condition' [in ProofOS.AbsInt.SimpleCond]
eval_genop32 [in Asm.X86.Defs]
eval_OF [in Asm.X86.Defs]
eval_PF [in Asm.X86.Defs]
eval_SF [in Asm.X86.Defs]
eval_shift [in ProofOS.AbsInt.Sal]
eval_test [in ProofOS.AbsInt.SimpleCond]
eval_ZF [in Asm.X86.Defs]
expUnaffected [in ProofOS.AbsInt.SimpleCond]

F

failureInstr [in ProofOS.AbsInt.Sal]
flags [in Asm.X86.Defs]
flag_eq_dec [in Asm.X86.Defs]
fold [in Asm.Util.Maps]
fold_right [in ProofOS.Examples.Vanilla]
fold_right [in ProofOS.AbsInt.SimpleDriver]
fold_right [in ProofOS.AbsInt.WeakDriver]
four [in Asm.X86.Defs]
functions [in ProofOS.AbsInt.WeakDriver]
functions [in ProofOS.Examples.Vanilla]
functions [in ProofOS.AbsInt.SimpleDriver]

G

genop32 [in Asm.X86.Defs]
genop8 [in Asm.X86.Defs]
get [in Asm.Util.Maps]
get [in Asm.Util.Maps]
get [in Asm.Util.Maps]
get [in Asm.Util.Maps]
get_flag [in Asm.X86.Defs]
get_flag [in ProofOS.AbsInt.Sal]
get_instr [in Asm.X86.Defs]
get_instr [in ProofOS.AbsInt.FixedCode]
get_instr [in ProofOS.AbsInt.Sal]
get_mem [in Asm.X86.Defs]
get_mem [in ProofOS.AbsInt.Sal]
get_mem32 [in ProofOS.AbsInt.Sal]
get_mem32 [in Asm.X86.Defs]
get_mem32' [in Asm.X86.Defs]
get_reg [in ProofOS.AbsInt.Sal]
get_reg32 [in Asm.X86.Defs]
get_sal_instr [in ProofOS.AbsInt.Sal]

H

hasTy [in ProofOS.AbsInt.TopOnly]
hasTy [in ProofOS.Examples.EvenOdd]
hasTy [in ProofOS.AbsInt.StackTypes]
hasTy [in ProofOS.AbsInt.WeakUpdateTypes]
hasTy [in ProofOS.Examples.IntPtr]
hasTy [in ProofOS.AbsInt.WeakUpdateTypes]
hasTy [in ProofOS.AbsInt.SimpleCond]
hasTy [in ProofOS.AbsInt.SimpleTypes]
hasTy [in ProofOS.AbsInt.SimpleCond]
hasTy [in ProofOS.AbsInt.SimpleTypes]
hasTy [in ProofOS.AbsInt.WeakUpdateTypes]
hasTy [in ProofOS.AbsInt.StackTypes]
hasTy [in ProofOS.Examples.MemoryTypes]
heapCodeSeparate [in ProofOS.AbsInt.WeakDriver]
heapFits [in ProofOS.AbsInt.WeakDriver]
heapHigh [in ProofOS.AbsInt.WeakDriver]
heapLength [in ProofOS.AbsInt.WeakDriver]
heapStackSeparate [in ProofOS.AbsInt.WeakDriver]
heapStart [in ProofOS.AbsInt.WeakDriver]
hypCovered [in ProofOS.AbsInt.TypeSystem]

I

index [in Asm.Util.Maps]
index [in ProofOS.AbsInt.Sal]
index [in Asm.X86.Defs]
index [in Asm.Util.Maps]
index [in ProofOS.AbsInt.StackTypes]
index [in Asm.X86.Defs]
index [in Asm.X86.Defs]
inHeap [in ProofOS.AbsInt.WeakUpdateTypes]
init [in Asm.Util.Maps]
init [in Asm.Util.Maps]
init [in Asm.Util.Maps]
inStack [in ProofOS.AbsInt.StackTypes]
instrOk [in ProofOS.AbsInt.FixedCode]
instructionOk [in ProofOS.AbsInt.FixedCode]
int16 [in Asm.Bitvector.Defs]
int16_eq [in Asm.Bitvector.Defs]
int16_eq_dec [in Asm.Bitvector.Defs]
int32 [in Asm.Bitvector.Defs]
int32_eq [in Asm.Bitvector.Defs]
int32_eq_dec [in Asm.Bitvector.Defs]
int8 [in Asm.Bitvector.Defs]
int8_eq [in Asm.Bitvector.Defs]
int8_eq_dec [in Asm.Bitvector.Defs]
invert [in Asm.Util.Maps]
invert [in Asm.X86.Defs]
invert [in Asm.Util.Maps]
invert [in ProofOS.AbsInt.Sal]
invert [in ProofOS.AbsInt.StackTypes]
invert [in Asm.X86.Defs]
invert [in Asm.X86.Defs]
isEven [in ProofOS.Examples.EvenOdd]
isOdd [in ProofOS.Examples.EvenOdd]
isTyConst [in ProofOS.Examples.MemoryTypes]
isTyConst [in ProofOS.AbsInt.SimpleTypes]
isTyConst [in ProofOS.AbsInt.StackTypes]
isTyConst [in ProofOS.Examples.EvenOdd]
isTyConst [in ProofOS.AbsInt.TopOnly]
isTyConst [in ProofOS.AbsInt.WeakUpdateTypes]
isTyConst [in ProofOS.AbsInt.SimpleCond]
isTyConst [in ProofOS.AbsInt.WeakUpdateTypes]
isTyConst [in ProofOS.Examples.IntPtr]
iter [in Asm.Util.ListUtil]
iter' [in Asm.Util.ListUtil]

L

liftState [in ProofOS.AbsInt.Sal]
list_disjoint [in Asm.Util.Coqlib]
localStep [in ProofOS.AbsInt.FixedCode]
localStep [in ProofOS.AbsInt.Reduce]
localStep [in ProofOS.AbsInt.Bounded]
localStep [in ProofOS.AbsInt.FixedCode]
localStep [in ProofOS.AbsInt.TypeSystem]
longestInstr [in Asm.X86.Defs]
lowerTy [in ProofOS.AbsInt.WeakUpdateTypes]
lowerTy [in ProofOS.AbsInt.StackTypes]
lower_half [in Asm.Bitvector.Split]
lt [in Asm.Util.Map]

M

maget_instr [in ProofOS.AbsInt.Reduce]
maget_instr [in ProofOS.AbsInt.FixedCode]
map [in Asm.Util.Maps]
map [in Asm.Util.Maps]
map [in Asm.Util.Maps]
map [in Asm.Util.Maps]
maPc [in ProofOS.AbsInt.TypeSystem]
maPc' [in ProofOS.AbsInt.TypeSystem]
mastate [in ProofOS.AbsInt.StackTypes]
mastate [in ProofOS.AbsInt.TopOnly]
mastate [in ProofOS.AbsInt.FixedCode]
mastate [in ProofOS.AbsInt.StackTypes]
mastate [in ProofOS.AbsInt.SimpleCond]
mastate [in ProofOS.AbsInt.SimpleCond]
mastate [in ProofOS.AbsInt.WeakUpdateTypes]
mastate [in ProofOS.AbsInt.WeakUpdateTypes]
mastate [in ProofOS.AbsInt.TypeSystem]
mastate [in ProofOS.AbsInt.SimpleTypes]
mastate [in ProofOS.AbsInt.WeakUpdateTypes]
mastate [in ProofOS.AbsInt.Reduce]
mastate [in ProofOS.AbsInt.SimpleTypes]
mconc [in ProofOS.AbsInt.StackTypes]
mconc [in ProofOS.AbsInt.WeakUpdateTypes]
mconc [in ProofOS.AbsInt.WeakUpdateTypes]
mconc [in ProofOS.AbsInt.TypeSystem]
mconc [in ProofOS.AbsInt.StackTypes]
mconc [in ProofOS.AbsInt.FixedCode]
mconc [in ProofOS.AbsInt.SimpleCond]
mconc [in ProofOS.AbsInt.Reduce]
mconc [in ProofOS.AbsInt.SimpleTypes]
mconc [in ProofOS.AbsInt.SimpleTypes]
mconc [in ProofOS.AbsInt.SimpleCond]
mconc [in ProofOS.AbsInt.WeakUpdateTypes]
mconc [in ProofOS.AbsInt.TopOnly]
mcontext [in ProofOS.AbsInt.FixedCode]
mcontext [in ProofOS.AbsInt.StackTypes]
mcontext [in ProofOS.AbsInt.TypeSystem]
mcontext [in ProofOS.AbsInt.SimpleCond]
mcontext [in ProofOS.AbsInt.StackTypes]
mcontext [in ProofOS.AbsInt.SimpleTypes]
mcontext [in ProofOS.AbsInt.TopOnly]
mcontext [in ProofOS.AbsInt.SimpleTypes]
mcontext [in ProofOS.AbsInt.WeakUpdateTypes]
mcontext [in ProofOS.AbsInt.WeakUpdateTypes]
mcontext [in ProofOS.AbsInt.SimpleCond]
mcontext [in ProofOS.AbsInt.Reduce]
mcontext [in ProofOS.AbsInt.WeakUpdateTypes]
mem [in Asm.X86.Defs]
mexec [in ProofOS.Trusted.Arches]
mexec [in ProofOS.AbsInt.Sal]
mget_instr [in ProofOS.Trusted.Arches]
mget_instr [in ProofOS.AbsInt.Sal]
minit [in ProofOS.AbsInt.TypeSystem]
minit [in ProofOS.Examples.Vanilla]
minit [in ProofOS.AbsInt.WeakDriver]
minit [in ProofOS.AbsInt.SimpleDriver]
minit [in ProofOS.AbsInt.Reduce]
minit [in ProofOS.AbsInt.FixedCode]
minitMem [in ProofOS.AbsInt.WeakDriver]
minitMem [in ProofOS.AbsInt.SimpleDriver]
minitMem [in ProofOS.Examples.Vanilla]
minitState [in ProofOS.AbsInt.Sal]
minitState [in ProofOS.Trusted.Arches]
minitState [in ProofOS.AbsInt.SimpleDriver]
minitState [in ProofOS.AbsInt.WeakDriver]
minitState [in ProofOS.Examples.Vanilla]
minstr [in ProofOS.AbsInt.Sal]
minstr [in ProofOS.Trusted.Arches]
mod2 [in Asm.Util.Mod]
mod2_bool [in Asm.Util.Mod]
mstate [in ProofOS.AbsInt.Sal]
mstate [in ProofOS.Trusted.Arches]
mstep [in ProofOS.AbsInt.Reduce]
mstep [in ProofOS.AbsInt.FixedCode]
mstep [in ProofOS.AbsInt.TypeSystem]

N

nat_to_bvec [in Asm.Bitvector.Defs]
neg_four [in Asm.X86.Defs]
not_too_high [in Asm.X86.Memory]

O

one [in Asm.X86.Defs]
option_map [in Asm.Util.Coqlib]
ord_dec [in Asm.Util.Map]

P

parity [in Asm.X86.Defs]
parity_dec [in ProofOS.Examples.EvenOdd]
pcOk [in ProofOS.AbsInt.TypeSystem]
pcToAbs [in ProofOS.AbsInt.TypeSystem]
pcToAbs_map [in ProofOS.AbsInt.TypeSystem]
pcToAbs_map' [in ProofOS.AbsInt.TypeSystem]
pcToFi [in ProofOS.AbsInt.StackTypes]
pcToFi_map [in ProofOS.AbsInt.StackTypes]
pcToFi_map' [in ProofOS.AbsInt.StackTypes]
peq [in Asm.Util.Coqlib]
Ple [in Asm.Util.Coqlib]
plt [in Asm.Util.Coqlib]
Plt [in Asm.Util.Coqlib]
popt_Prop [in Asm.Util.Specif]
popt_to_bool [in Asm.Util.Specif]
positive_rec [in Asm.Util.Coqlib]
pow2 [in Asm.Util.ArithUtil]
preservation [in ProofOS.AbsInt.TypeSystem]
preservation [in ProofOS.AbsInt.FixedCode]
preservation [in ProofOS.AbsInt.Bounded]
preservation [in ProofOS.AbsInt.Reduce]
preservation [in ProofOS.AbsInt.FixedCode]
preserveSlots [in ProofOS.AbsInt.StackTypes]
print_mastate [in ProofOS.AbsInt.WeakUpdateTypes]
print_mastate [in ProofOS.AbsInt.WeakUpdateTypes]
print_mastate [in ProofOS.AbsInt.Reduce]
print_mastate [in ProofOS.AbsInt.FixedCode]
print_mastate [in ProofOS.AbsInt.SimpleTypes]
print_mastate [in ProofOS.AbsInt.StackTypes]
print_mastate [in ProofOS.AbsInt.SimpleCond]
print_mastate [in ProofOS.AbsInt.TypeSystem]
print_mastate [in ProofOS.AbsInt.TopOnly]
print_ty [in ProofOS.AbsInt.StackTypes]
print_ty [in ProofOS.Examples.IntPtr]
print_ty [in ProofOS.Examples.EvenOdd]
print_ty [in ProofOS.AbsInt.SimpleCond]
print_ty [in ProofOS.AbsInt.WeakUpdateTypes]
print_ty [in ProofOS.Examples.MemoryTypes]
print_ty [in ProofOS.AbsInt.WeakUpdateTypes]
print_ty [in ProofOS.AbsInt.TopOnly]
print_ty [in ProofOS.AbsInt.SimpleTypes]
product_eq_dec' [in ProofOS.Examples.MemoryTypes]
progress [in ProofOS.AbsInt.FixedCode]
progress [in ProofOS.AbsInt.TypeSystem]
progress [in ProofOS.AbsInt.Bounded]
progress [in ProofOS.AbsInt.Reduce]
progress [in ProofOS.AbsInt.FixedCode]

R

R [in ProofOS.AbsInt.Sal]
raiseTy [in ProofOS.AbsInt.StackTypes]
raiseTy [in ProofOS.AbsInt.WeakUpdateTypes]
regFree [in ProofOS.AbsInt.WeakUpdateTypes]
regs32 [in Asm.X86.Defs]
reg32_eq_dec [in Asm.X86.Defs]
relaxTy [in ProofOS.Examples.EvenOdd]
remove [in Asm.Util.Maps]
reverseRobustType [in ProofOS.AbsInt.StackTypes]
robustType [in ProofOS.AbsInt.StackTypes]

S

safe [in ProofOS.Trusted.Safety]
salAddr [in ProofOS.AbsInt.Sal]
salCompile [in ProofOS.AbsInt.Sal]
salExec [in ProofOS.AbsInt.Sal]
salExecCmd [in ProofOS.AbsInt.Sal]
salExecJmp [in ProofOS.AbsInt.Sal]
salExec' [in ProofOS.AbsInt.Sal]
salExpOpt_ok [in ProofOS.AbsInt.WeakUpdateTypes]
salExpOpt_ok_dec [in ProofOS.AbsInt.WeakUpdateTypes]
salExpOpt_popt [in ProofOS.AbsInt.WeakUpdateTypes]
salExp_eq_dec [in ProofOS.AbsInt.SimpleCond]
salExp_eq_dec [in ProofOS.AbsInt.WeakUpdateTypes]
salGenop [in ProofOS.AbsInt.Sal]
salInstr [in ProofOS.AbsInt.Sal]
salInstruction [in ProofOS.AbsInt.Sal]
salRegs [in ProofOS.AbsInt.Sal]
salReg_eq_dec [in ProofOS.AbsInt.Sal]
scale_shift [in Asm.X86.Defs]
seekInProduct [in ProofOS.Examples.MemoryTypes]
set [in Asm.Util.Maps]
set [in Asm.Util.Maps]
set [in Asm.Util.Maps]
set [in Asm.Util.Maps]
set_arith_flags [in ProofOS.AbsInt.Sal]
set_flag [in ProofOS.AbsInt.Sal]
set_flag [in Asm.X86.Defs]
set_mem [in Asm.X86.Defs]
set_mem [in ProofOS.AbsInt.Sal]
set_mem32 [in Asm.X86.Defs]
set_mem32 [in ProofOS.AbsInt.Sal]
set_mem32' [in Asm.X86.Defs]
set_pc [in ProofOS.AbsInt.Sal]
set_pc [in Asm.X86.Defs]
set_reg [in ProofOS.AbsInt.Sal]
set_reg32 [in Asm.X86.Defs]
set_stack32 [in ProofOS.AbsInt.StackTypes]
shiftAbs [in ProofOS.AbsInt.StackTypes]
shiftContext [in ProofOS.AbsInt.StackTypes]
shift_op_eq_dec [in ProofOS.AbsInt.WeakUpdateTypes]
shift_op_eq_dec [in ProofOS.AbsInt.SimpleCond]
sign [in Asm.X86.Defs]
split_word [in Asm.Bitvector.Split]
stackCodeSeparate [in ProofOS.AbsInt.WeakDriver]
stackCodeSeparate [in ProofOS.AbsInt.SimpleDriver]
stackCodeSeparate [in ProofOS.Examples.Vanilla]
stackEnd [in ProofOS.AbsInt.StackTypes]
stackFits [in ProofOS.AbsInt.SimpleDriver]
stackFits [in ProofOS.Examples.Vanilla]
stackFits [in ProofOS.AbsInt.WeakDriver]
stackHigh [in ProofOS.AbsInt.SimpleDriver]
stackHigh [in ProofOS.AbsInt.WeakDriver]
stackHigh [in ProofOS.Examples.Vanilla]
stackLength [in ProofOS.Examples.Vanilla]
stackLength [in ProofOS.AbsInt.SimpleDriver]
stackLength [in ProofOS.AbsInt.WeakDriver]
stackSlotOf [in ProofOS.AbsInt.StackTypes]
stackStart [in ProofOS.AbsInt.SimpleDriver]
stackStart [in ProofOS.AbsInt.WeakDriver]
stackStart [in ProofOS.Examples.Vanilla]
stack_slot [in ProofOS.AbsInt.StackTypes]
subHyps [in ProofOS.AbsInt.TypeSystem]
subMap [in Asm.Util.Maps]
subMastate [in ProofOS.AbsInt.TopOnly]
subMastate [in ProofOS.AbsInt.StackTypes]
subMastate [in ProofOS.AbsInt.TypeSystem]
subMastate [in ProofOS.AbsInt.WeakUpdateTypes]
subMastate [in ProofOS.AbsInt.SimpleCond]
subMastate [in ProofOS.AbsInt.WeakUpdateTypes]
subMastate [in ProofOS.AbsInt.SimpleTypes]
subProduct' [in ProofOS.Examples.MemoryTypes]
subst [in ProofOS.Examples.MemoryTypes]
substProduct [in ProofOS.Examples.MemoryTypes]
subsumes [in ProofOS.AbsInt.Bounded]
subTy [in ProofOS.Examples.MemoryTypes]
subTy [in ProofOS.Examples.EvenOdd]
subTy [in ProofOS.AbsInt.SimpleTypes]
subTy [in ProofOS.AbsInt.TopOnly]
subTy [in ProofOS.AbsInt.StackTypes]
subTy [in ProofOS.AbsInt.SimpleCond]
subTy [in ProofOS.AbsInt.WeakUpdateTypes]
subTy [in ProofOS.AbsInt.WeakUpdateTypes]
subTy [in ProofOS.Examples.IntPtr]
subTy' [in ProofOS.Examples.MemoryTypes]
subTy1 [in ProofOS.Examples.MemoryTypes]
subTy2 [in ProofOS.Examples.MemoryTypes]
sum_left_map [in Asm.Util.Coqlib]
sum_to_bool [in Asm.Util.Specif]

T

t [in ProofOS.AbsInt.Sal]
t [in ProofOS.AbsInt.StackTypes]
t [in Asm.X86.Defs]
t [in Asm.Util.Maps]
t [in Asm.X86.Defs]
t [in Asm.Util.Maps]
t [in Asm.X86.Defs]
t [in Asm.Util.Map]
t [in Asm.Util.Maps]
t [in Asm.Util.Maps]
t [in Asm.Util.Maps]
t [in Asm.Util.Maps]
to_int32 [in ProofOS.Examples.EvenOdd]
tripleOpt_ok [in ProofOS.AbsInt.SimpleCond]
try_pred_option_pred_option [in Asm.Util.Monad]
try_pred_option_sig_option [in Asm.Util.Monad]
try_sig_anything [in Asm.Util.Monad]
try_sig_option_pred_option [in Asm.Util.Monad]
try_sig_option_sig_option [in Asm.Util.Monad]
ty [in ProofOS.AbsInt.WeakUpdateTypes]
ty [in ProofOS.AbsInt.WeakUpdateTypes]
ty [in ProofOS.AbsInt.StackTypes]
ty [in ProofOS.Examples.MemoryTypes]
ty [in ProofOS.Examples.EvenOdd]
ty [in ProofOS.AbsInt.TopOnly]
ty [in ProofOS.AbsInt.StackTypes]
ty [in ProofOS.AbsInt.SimpleCond]
ty [in ProofOS.AbsInt.SimpleTypes]
ty [in ProofOS.AbsInt.WeakUpdateTypes]
ty [in ProofOS.Examples.IntPtr]
ty [in ProofOS.AbsInt.SimpleTypes]
ty [in ProofOS.AbsInt.SimpleCond]
tyConst [in ProofOS.AbsInt.WeakUpdateTypes]
tyConst [in ProofOS.AbsInt.SimpleCond]
tyConst [in ProofOS.Examples.EvenOdd]
tyConst [in ProofOS.AbsInt.SimpleTypes]
tyConst [in ProofOS.Examples.IntPtr]
tyConst [in ProofOS.AbsInt.TopOnly]
tyConst [in ProofOS.Examples.MemoryTypes]
tyConst [in ProofOS.AbsInt.StackTypes]
tyConst [in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound1 [in ProofOS.Examples.MemoryTypes]
tyConstSound1 [in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound1 [in ProofOS.AbsInt.SimpleCond]
tyConstSound1 [in ProofOS.Examples.IntPtr]
tyConstSound1 [in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound2 [in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound2 [in ProofOS.AbsInt.WeakUpdateTypes]
tyConstSound2 [in ProofOS.AbsInt.SimpleCond]
typeof [in ProofOS.AbsInt.WeakUpdateTypes]
typeof [in ProofOS.AbsInt.WeakUpdateTypes]
typeof [in ProofOS.AbsInt.SimpleTypes]
typeof [in ProofOS.AbsInt.TopOnly]
typeof [in ProofOS.AbsInt.StackTypes]
typeof [in ProofOS.AbsInt.SimpleCond]
typeofArith [in ProofOS.Examples.EvenOdd]
typeofArith [in ProofOS.Examples.IntPtr]
typeofArith [in ProofOS.Examples.MemoryTypes]
typeofCell [in ProofOS.Examples.MemoryTypes]
typeofCell [in ProofOS.Examples.IntPtr]
typeofLoad [in ProofOS.AbsInt.WeakUpdateTypes]
typeofLoad [in ProofOS.AbsInt.WeakUpdateTypes]
typeofLoad [in ProofOS.AbsInt.TopOnly]
typeofLoad [in ProofOS.AbsInt.StackTypes]
typeofLoad [in ProofOS.AbsInt.SimpleTypes]
typeofLoad [in ProofOS.AbsInt.SimpleCond]
typeofLoadR [in ProofOS.AbsInt.StackTypes]
typeofR [in ProofOS.AbsInt.StackTypes]
tyTop [in ProofOS.Examples.IntPtr]
tyTop [in ProofOS.AbsInt.WeakUpdateTypes]
tyTop [in ProofOS.AbsInt.WeakUpdateTypes]
tyTop [in ProofOS.AbsInt.TopOnly]
tyTop [in ProofOS.AbsInt.SimpleCond]
tyTop [in ProofOS.Examples.MemoryTypes]
tyTop [in ProofOS.AbsInt.StackTypes]
tyTop [in ProofOS.AbsInt.SimpleTypes]
tyTop [in ProofOS.Examples.EvenOdd]
tyTopSound [in ProofOS.Examples.MemoryTypes]
tyTopSound [in ProofOS.Examples.IntPtr]
tyTopSound [in ProofOS.AbsInt.WeakUpdateTypes]
tyTopSound [in ProofOS.AbsInt.WeakUpdateTypes]
tyTopSound [in ProofOS.AbsInt.SimpleCond]
ty_eq_dec [in ProofOS.Examples.MemoryTypes]
ty_eq_dec' [in ProofOS.Examples.MemoryTypes]

U

upper_half [in Asm.Bitvector.Split]

V

validPc [in ProofOS.AbsInt.FixedCode]
var [in ProofOS.Examples.MemoryTypes]
verify [in ProofOS.AbsInt.WeakDriver]
verify [in ProofOS.AbsInt.Sal]
verify [in ProofOS.AbsInt.Reduce]
verify [in ProofOS.AbsInt.Bounded]
verify [in ProofOS.AbsInt.SimpleDriver]
verify [in ProofOS.Examples.Vanilla]
verify_list [in ProofOS.AbsInt.Bounded]
Vid [in Asm.Util.Vector]
viewShiftOfJump [in ProofOS.AbsInt.TopOnly]
viewShiftOfJump [in ProofOS.AbsInt.WeakUpdateTypes]
viewShiftOfJump [in ProofOS.AbsInt.SimpleCond]
viewShiftOfJump [in ProofOS.AbsInt.SimpleTypes]
viewShiftOfJump [in ProofOS.AbsInt.WeakUpdateTypes]
viewShiftOfJump [in ProofOS.AbsInt.StackTypes]
viewShift_ret [in ProofOS.AbsInt.StackTypes]

W

weakState [in ProofOS.AbsInt.WeakUpdateTypes]
wordAligned [in ProofOS.AbsInt.WeakUpdateTypes]

X

xcombine_l [in Asm.Util.Maps]
xcombine_r [in Asm.Util.Maps]
xelements [in Asm.Util.Maps]
xget [in Asm.Util.Maps]
xkeys [in Asm.Util.Maps]
xmap [in Asm.Util.Maps]

Z

zeq [in Asm.Util.Coqlib]
zle [in Asm.Util.Coqlib]
zlt [in Asm.Util.Coqlib]

Module Index

A

Abs [in ProofOS.AbsInt.Reduce]
Abs [in ProofOS.AbsInt.Sal]
ABSTRACTION [in ProofOS.AbsInt.Bounded]
Abstraction [in ProofOS.AbsInt.TypeSystem]
Abs1 [in ProofOS.AbsInt.WeakDriver]
Abs1 [in ProofOS.Examples.Vanilla]
Abs1 [in ProofOS.AbsInt.SimpleDriver]
Abs2 [in ProofOS.AbsInt.SimpleDriver]
Abs2 [in ProofOS.AbsInt.WeakDriver]
Abs2 [in ProofOS.Examples.Vanilla]
AddCond [in ProofOS.AbsInt.SimpleCond]
AddStackTypes [in ProofOS.AbsInt.StackTypes]

C

Ch [in ProofOS.AbsInt.Sal]
Ch [in ProofOS.Examples.Vanilla]
Ch [in ProofOS.AbsInt.WeakDriver]
Ch [in ProofOS.AbsInt.SimpleDriver]
Ch [in ProofOS.AbsInt.Reduce]
Checker [in ProofOS.AbsInt.Bounded]
CHECKER [in ProofOS.AbsInt.Bounded]
Checker [in ProofOS.AbsInt.Sal]
Conc [in ProofOS.AbsInt.Reduce]
Conc [in ProofOS.AbsInt.Sal]
Cond [in ProofOS.AbsInt.WeakUpdateTypes]
CondSys [in ProofOS.AbsInt.WeakUpdateTypes]
Create [in ProofOS.AbsInt.SimpleTypes]
Create [in ProofOS.AbsInt.WeakUpdateTypes]

D

Dr [in ProofOS.Examples.IntPtr]
Dr [in ProofOS.Examples.EvenOdd]
Dr [in ProofOS.Examples.MemoryTypes]
Driver [in ProofOS.AbsInt.WeakDriver]
Driver [in ProofOS.AbsInt.SimpleDriver]
DRIVER_PARAM [in ProofOS.AbsInt.WeakDriver]
DRIVER_PARAM [in ProofOS.AbsInt.SimpleDriver]
DRIVER_REGIONS [in ProofOS.AbsInt.SimpleDriver]
DRIVER_REGIONS [in ProofOS.AbsInt.WeakDriver]

E

EMap [in Asm.Util.Maps]
EQUALITY_TYPE [in Asm.Util.Maps]
EvenOddTySys [in ProofOS.Examples.EvenOdd]

F

FINITE [in Asm.Util.Map]
FiniteOrderedSet [in Asm.Util.Map]
Fix [in ProofOS.AbsInt.FixedCode]
Fixed [in ProofOS.AbsInt.TypeSystem]
FIXED_CODE_ABSTRACTION [in ProofOS.AbsInt.FixedCode]
FlagIndexed [in Asm.X86.Defs]
FlagMap [in Asm.X86.Defs]

I

IMap [in Asm.Util.Maps]
INDEXED_TYPE [in Asm.Util.Maps]
IntermediateTySys [in ProofOS.AbsInt.WeakUpdateTypes]
IntPtrTySys [in ProofOS.Examples.IntPtr]
Int32Indexed [in Asm.X86.Defs]
Int32Map [in Asm.X86.Defs]

M

M [in ProofOS.AbsInt.Sal]
Mac [in ProofOS.AbsInt.SimpleCond]
Mac [in ProofOS.AbsInt.Reduce]
Mac [in ProofOS.AbsInt.Bounded]
Mac [in ProofOS.AbsInt.TopOnly]
Mac [in ProofOS.AbsInt.FixedCode]
Mac [in ProofOS.AbsInt.Reduce]
Mac [in ProofOS.AbsInt.TypeSystem]
Mac [in ProofOS.AbsInt.StackTypes]
Mac [in ProofOS.AbsInt.Bounded]
Mac [in ProofOS.AbsInt.Sal]
Mac [in ProofOS.AbsInt.WeakUpdateTypes]
Mac [in ProofOS.Examples.Vanilla]
Mac [in ProofOS.AbsInt.Sal]
Mac [in ProofOS.AbsInt.FixedCode]
Mac [in ProofOS.AbsInt.SimpleTypes]
Mac [in ProofOS.AbsInt.TypeSystem]
Mac [in ProofOS.AbsInt.Reduce]
Mac [in ProofOS.AbsInt.Sal]
Mac [in ProofOS.AbsInt.FixedCode]
Mac [in ProofOS.AbsInt.Bounded]
Mac [in ProofOS.AbsInt.Bounded]
Mac [in ProofOS.AbsInt.SimpleDriver]
Mac [in ProofOS.AbsInt.WeakDriver]
MACHINE [in ProofOS.Trusted.Machine]
MACHINE [in ProofOS.Trusted.Safety]
Make [in ProofOS.AbsInt.SimpleTypes]
Make [in ProofOS.AbsInt.FixedCode]
Make [in ProofOS.AbsInt.WeakUpdateTypes]
Make [in ProofOS.AbsInt.WeakDriver]
Make [in ProofOS.AbsInt.TopOnly]
Make [in ProofOS.AbsInt.SimpleDriver]
Make [in ProofOS.AbsInt.SimpleCond]
Make [in ProofOS.AbsInt.StackTypes]
Make [in ProofOS.Examples.Vanilla]
Make [in ProofOS.AbsInt.Reduce]
Make [in ProofOS.AbsInt.TypeSystem]
Make [in ProofOS.AbsInt.Sal]
MAP [in Asm.Util.Maps]
MC [in ProofOS.AbsInt.Sal]
MemoryTySys [in ProofOS.Examples.MemoryTypes]
MyParam [in ProofOS.Examples.MemoryTypes]
MyParam [in ProofOS.Examples.EvenOdd]
MyParam [in ProofOS.Examples.IntPtr]
MySal [in ProofOS.AbsInt.FixedCode]
MySys [in ProofOS.AbsInt.WeakDriver]
MySys [in ProofOS.AbsInt.SimpleDriver]
MyTypeSystem [in ProofOS.AbsInt.TopOnly]
MyTypeSystemPlus [in ProofOS.AbsInt.SimpleDriver]
MyTypeSystemPlus [in ProofOS.Examples.Vanilla]
MyTypeSystemPlus [in ProofOS.AbsInt.WeakDriver]
M86 [in ProofOS.Trusted.Arches]
M86_PARAM [in ProofOS.Trusted.Arches]
M86_PARAM_FIXED_CODE [in ProofOS.AbsInt.FixedCode]
M86_PARAM_FIXED_CODE_AND_STACK [in ProofOS.AbsInt.StackTypes]
M86_PARAM_FIXED_CODE_AND_STACK_AND_HEAP [in ProofOS.AbsInt.WeakUpdateTypes]

N

NatIndexed [in ProofOS.AbsInt.StackTypes]
NatMap [in ProofOS.AbsInt.StackTypes]
NIndexed [in Asm.Util.Maps]
NMap [in Asm.Util.Maps]

O

ORDERED_SET [in Asm.Util.Map]

P

PMap [in Asm.Util.Maps]
PTree [in Asm.Util.Maps]

R

ReduceAbs [in ProofOS.AbsInt.Reduce]
Reduction [in ProofOS.AbsInt.Sal]
REDUCTION [in ProofOS.AbsInt.Reduce]
Regions [in ProofOS.AbsInt.WeakDriver]
Regions [in ProofOS.Examples.MemoryTypes]
Regions [in ProofOS.Examples.IntPtr]
Regions [in ProofOS.Examples.EvenOdd]
Regions [in ProofOS.AbsInt.SimpleDriver]
Reg32Indexed [in Asm.X86.Defs]
Reg32Map [in Asm.X86.Defs]
ROOT_STATES [in ProofOS.AbsInt.WeakDriver]
ROOT_STATES [in ProofOS.AbsInt.SimpleDriver]
ROOT_STATES [in ProofOS.Examples.Vanilla]

S

S [in ProofOS.AbsInt.Bounded]
Safety [in ProofOS.Trusted.Safety]
SalRegIndexed [in ProofOS.AbsInt.Sal]
SalRegMap [in ProofOS.AbsInt.Sal]
Sal86 [in ProofOS.AbsInt.Sal]
Simple [in ProofOS.AbsInt.SimpleDriver]
SIMPLE_TYPE_SYSTEM [in ProofOS.AbsInt.SimpleTypes]
Stack [in ProofOS.AbsInt.TopOnly]
Stack [in ProofOS.AbsInt.SimpleCond]
Stack [in ProofOS.AbsInt.SimpleTypes]
StackParam [in ProofOS.AbsInt.SimpleDriver]
StackParam [in ProofOS.AbsInt.WeakDriver]
StackParam [in ProofOS.Examples.Vanilla]
STACK_READY_TYPE_SYSTEM [in ProofOS.AbsInt.StackTypes]
Sys [in ProofOS.AbsInt.SimpleDriver]
Sys [in ProofOS.Examples.MemoryTypes]
Sys [in ProofOS.AbsInt.WeakDriver]
Sys [in ProofOS.Examples.EvenOdd]
Sys [in ProofOS.Examples.Vanilla]
Sys [in ProofOS.AbsInt.SimpleDriver]
Sys [in ProofOS.AbsInt.SimpleCond]
Sys [in ProofOS.AbsInt.SimpleDriver]
Sys [in ProofOS.AbsInt.StackTypes]
Sys [in ProofOS.AbsInt.TypeSystem]
Sys [in ProofOS.Examples.Vanilla]
Sys [in ProofOS.AbsInt.WeakUpdateTypes]
Sys [in ProofOS.Examples.IntPtr]
Sys [in ProofOS.AbsInt.WeakDriver]
Sys [in ProofOS.AbsInt.WeakDriver]

T

TopOnly [in ProofOS.Examples.Vanilla]
TotalMap [in Asm.Util.Map]
TREE [in Asm.Util.Maps]
TypeSystem [in ProofOS.AbsInt.SimpleDriver]
TypeSystem [in ProofOS.AbsInt.WeakDriver]
TypeSystem [in ProofOS.Examples.Vanilla]
TYPE_SYSTEM [in ProofOS.AbsInt.TypeSystem]
TYPE_SYSTEM_WITH_FUNCTIONS [in ProofOS.AbsInt.StackTypes]
TYPE_SYSTEM_WITH_TESTING [in ProofOS.AbsInt.SimpleCond]
TySys [in ProofOS.AbsInt.StackTypes]

U

User [in ProofOS.AbsInt.WeakDriver]
User [in ProofOS.Examples.Vanilla]
User [in ProofOS.AbsInt.SimpleDriver]
USE_TYPE_SYSTEM [in ProofOS.AbsInt.TypeSystem]

V

VANILLA_PARAM [in ProofOS.Examples.Vanilla]
Verifier [in ProofOS.Examples.IntPtr]
Verifier [in ProofOS.Examples.MemoryTypes]
Verifier [in ProofOS.Examples.EvenOdd]
Verifier [in ProofOS.Examples.Vanilla]

W

Weak [in ProofOS.AbsInt.WeakDriver]
WEAK_UPDATE_TYPE_SYSTEM [in ProofOS.AbsInt.WeakUpdateTypes]
WithTesting [in ProofOS.AbsInt.WeakUpdateTypes]

Z

ZIndexed [in Asm.Util.Maps]
ZMap [in Asm.Util.Maps]

Library Index

A

Arches
ArithUtil

B

BArith
Bitvector
Bitwise
Bounded

C

D

Defs
Defs

E

F

I

IntPtr

L

M

Machine
Map
Maps
Memory
MemoryTypes
Mod
Monad

R

Reduce

S

Safety
Sal
SimpleCond
SimpleDriver
SimpleTypes
Specif
Split
StackTypes

T

Tactics
Tactics
TopOnly
TypeSystem

V

W

WeakDriver
WeakUpdateTypes

X

X86

Global Index

K

Q

Y

(1755 entries)

Axiom Index

A

B

G

J

K

O

Q

W

X

Y

Z

_

(228 entries)

Lemma Index

K

Q

Y

_

(436 entries)

Constructor Index

F

G

K

Q

U

Y

_

(168 entries)

Inductive Index

D

J

K

N

Q

U

X

Y

Z

(53 entries)

Definition Index

J

K

Q

Y

_

(651 entries)

Module Index

B

G

H

J

K

L

Q

X

Y

_

(180 entries)

Library Index

G

H

J

K

N

O

P

Q

U

Y

Z

_

(39 entries)

This page has been generated by coqdoc