Global Index

Q

U

W

X

Y

Z

_

other

(2041 entries)

Module Index

B

E

G

J

K

O

Q

T

U

W

X

Y

Z

_

other

(161 entries)

Variable Index

G

I

J

P

Q

T

U

W

X

Y

Z

_

other

(81 entries)

Library Index

B

D

E

G

J

K

M

O

Q

T

U

W

X

Y

Z

_

other

(28 entries)

Lemma Index

E

K

L

O

Q

U

W

X

Y

Z

_

other

(302 entries)

Axiom Index

B

D

E

G

I

J

K

L

O

Q

U

W

X

Y

Z

_

other

(375 entries)

Constructor Index

B

C

E

G

J

K

M

N

Q

U

W

X

Y

Z

_

other

(527 entries)

Inductive Index

B

C

E

G

J

K

M

N

O

Q

U

W

X

Y

Z

_

other

(133 entries)

Projection Index

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(34 entries)

Section Index

A

B

C

G

I

J

K

N

O

P

Q

T

U

W

X

Y

Z

_

other

(16 entries)

Definition Index

G

K

O

Q

U

W

X

Y

Z

_

other

(373 entries)

Record Index

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(11 entries)

Global Index

A

ADDR_ARITHMETIC.arithmetic [definition, in Arithmetic]
ADDR_ARITHMETIC.castArithmetic [definition, in Arithmetic]
ADDR_ARITHMETIC.castInd [inductive, in Arithmetic]
ADDR_ARITHMETIC.cmpiArithmetic [definition, in Arithmetic]
ADDR_ARITHMETIC.cmpiInd [inductive, in Arithmetic]
ADDR_ARITHMETIC.cmpValuesArithmetic [definition, in Arithmetic]
ADDR_ARITHMETIC.cmpValuesInd [inductive, in Arithmetic]
ADDR_ARITHMETIC.cmpZeroArithmetic [definition, in Arithmetic]
ADDR_ARITHMETIC.cmpZeroInd [inductive, in Arithmetic]
ADDR_ARITHMETIC.binOpArithmetic [definition, in Arithmetic]
ADDR_ARITHMETIC.binOpInd [inductive, in Arithmetic]
ADDR_ARITHMETIC.unOpArithmetic [definition, in Arithmetic]
ADDR_ARITHMETIC.unOpInd [inductive, in Arithmetic]
ADDR_ARITHMETIC.M_ArithmeticTypes [module, in Arithmetic]
ADDR_ARITHMETIC [module, in Arithmetic]
add_add [lemma, in Loop_Assertions]
add_i2_i_small [lemma, in Loop_Assertions]
add_add [lemma, in Loop]
add_i2_i_small [lemma, in Loop]
add1_small [lemma, in Loop_Assertions]
add1_small [lemma, in Loop]
add2_small [lemma, in Loop_Assertions]
add2_small [lemma, in Loop]
ak [variable, in Instructions]
AllStr [module, in Loop_Assertions]
AllStr [module, in Loop]
AllStr [module, in IAdd]
AllStructures [library]
ALL_STRUCTURES.M_HeapFacts [module, in AllStructures]
ALL_STRUCTURES.M_RuntimeStructuresFacts [module, in AllStructures]
ALL_STRUCTURES.M_ProgramStructuresFacts [module, in AllStructures]
ALL_STRUCTURES.M_Arithmetics [module, in AllStructures]
ALL_STRUCTURES.M_Program [module, in AllStructures]
ALL_STRUCTURES.M_RuntimeStructures [module, in AllStructures]
ALL_STRUCTURES [module, in AllStructures]
ARITHMETIC [module, in Arithmetic]
Arithmetic [library]
ArithmeticOperators [module, in ArithOps]
ArithmeticOperators.BinOp_ushr [constructor, in ArithOps]
ArithmeticOperators.BinOp_shr [constructor, in ArithOps]
ArithmeticOperators.BinOp_shl [constructor, in ArithOps]
ArithmeticOperators.BinOp_or [constructor, in ArithOps]
ArithmeticOperators.BinOp_and [constructor, in ArithOps]
ArithmeticOperators.BinOp_xor [constructor, in ArithOps]
ArithmeticOperators.BinOp_rem [constructor, in ArithOps]
ArithmeticOperators.BinOp_div [constructor, in ArithOps]
ArithmeticOperators.BinOp_mul [constructor, in ArithOps]
ArithmeticOperators.BinOp_sub [constructor, in ArithOps]
ArithmeticOperators.BinOp_add [constructor, in ArithOps]
ArithmeticOperators.CastOp_d [constructor, in ArithOps]
ArithmeticOperators.CastOp_f [constructor, in ArithOps]
ArithmeticOperators.CastOp_l [constructor, in ArithOps]
ArithmeticOperators.CastOp_i [constructor, in ArithOps]
ArithmeticOperators.CastOp_s [constructor, in ArithOps]
ArithmeticOperators.CastOp_c [constructor, in ArithOps]
ArithmeticOperators.CastOp_b [constructor, in ArithOps]
ArithmeticOperators.CmpiOp_cmpg [constructor, in ArithOps]
ArithmeticOperators.CmpiOp_cmpl [constructor, in ArithOps]
ArithmeticOperators.CmpOp_gt [constructor, in ArithOps]
ArithmeticOperators.CmpOp_ge [constructor, in ArithOps]
ArithmeticOperators.CmpOp_lt [constructor, in ArithOps]
ArithmeticOperators.CmpOp_le [constructor, in ArithOps]
ArithmeticOperators.CmpOp_ne [constructor, in ArithOps]
ArithmeticOperators.CmpOp_eq [constructor, in ArithOps]
ArithmeticOperators.FCmpOp_fcmpl [constructor, in ArithOps]
ArithmeticOperators.FCmpOp_fcmpg [constructor, in ArithOps]
ArithmeticOperators.TBinOp [inductive, in ArithOps]
ArithmeticOperators.TCastOp [inductive, in ArithOps]
ArithmeticOperators.TCmpAOp [inductive, in ArithOps]
ArithmeticOperators.TCmpiOp [inductive, in ArithOps]
ArithmeticOperators.TCmpOp [inductive, in ArithOps]
ArithmeticOperators.TUnOp [inductive, in ArithOps]
ArithmeticOperators.UnOp_neg [constructor, in ArithOps]
ARITHMETICS [module, in Arithmetic]
ARITHMETICS.arithmeticForKind [definition, in Arithmetic]
ARITHMETICS.kindOfCastOp [definition, in Arithmetic]
ARITHMETICS.M_DoubleArithmetic [module, in Arithmetic]
ARITHMETICS.M_LongArithmetic [module, in Arithmetic]
ARITHMETICS.M_FloatArithmetic [module, in Arithmetic]
ARITHMETICS.M_IntArithmetic [module, in Arithmetic]
ARITHMETICS.M_AddrArithmetic [module, in Arithmetic]
ARITHMETICS.M_RefArithmetic [module, in Arithmetic]
ARITHMETICS.M_ArithmeticTypes [module, in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindBinOp [lemma, in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindCastOp [lemma, in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindCmpi [lemma, in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindCmpValues [lemma, in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindCmpZero [lemma, in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindUnOp [lemma, in Arithmetic]
ArithmeticTypes [module, in Arithmetic]
ArithmeticTypes.arithBinOp [projection, in Arithmetic]
ArithmeticTypes.arithCast [projection, in Arithmetic]
ArithmeticTypes.arithCmpi [projection, in Arithmetic]
ArithmeticTypes.arithCmpValues [projection, in Arithmetic]
ArithmeticTypes.arithCmpZero [projection, in Arithmetic]
ArithmeticTypes.arithMake [constructor, in Arithmetic]
ArithmeticTypes.arithUnOp [projection, in Arithmetic]
ArithmeticTypes.TArithmetic [record, in Arithmetic]
ArithmeticTypes.TBinOpArithmetic [definition, in Arithmetic]
ArithmeticTypes.TCastArithmetic [definition, in Arithmetic]
ArithmeticTypes.TCmpiArithmetic [definition, in Arithmetic]
ArithmeticTypes.TCmpValuesArithmetic [definition, in Arithmetic]
ArithmeticTypes.TCmpZeroArithmetic [definition, in Arithmetic]
ArithmeticTypes.TUnOpArithmetic [definition, in Arithmetic]
ARITHMETIC.arithmetic [definition, in Arithmetic]
ARITHMETIC.binOpArithmetic [axiom, in Arithmetic]
ARITHMETIC.castArithmetic [axiom, in Arithmetic]
ARITHMETIC.cmpiArithmetic [axiom, in Arithmetic]
ARITHMETIC.cmpValuesArithmetic [axiom, in Arithmetic]
ARITHMETIC.cmpZeroArithmetic [axiom, in Arithmetic]
ARITHMETIC.kind [axiom, in Arithmetic]
ARITHMETIC.M_ArithmeticTypes [module, in Arithmetic]
ARITHMETIC.unOpArithmetic [axiom, in Arithmetic]
ArithOps [library]
ARS [module, in Loop_Assertions]
ARS [module, in Loop]
ARS [module, in IAdd]
A_m_code [definition, in Program_A]

B

base_max [lemma, in Loop_Assertions]
base_max [lemma, in Loop]
bijection [definition, in Common]
bijection_id [lemma, in Common]
binop_224_impl_toZ [lemma, in IAdd]
binop_224 [lemma, in IAdd]
bt [variable, in Instructions]

C

c [variable, in Instructions]
c [axiom, in IAdd]
caller_loc_class_loc [axiom, in IAdd]
caller_loc [axiom, in IAdd]
CHAR [module, in Char]
Char [library]
CHARSIZE [module, in Char]
CHARSIZE.power [axiom, in Char]
CHARSIZE.power_positive [axiom, in Char]
CHAR.base [definition, in Char]
CHAR.power [axiom, in Char]
CHAR.power_positive [axiom, in Char]
CHAR.PzeroToZ [axiom, in Char]
CHAR.range [definition, in Char]
CHAR.range_prop [axiom, in Char]
CHAR.t [axiom, in Char]
CHAR.toZ [axiom, in Char]
CHAR.truncate_on_zero [axiom, in Char]
CHAR.truncate_to_char [axiom, in Char]
CHAR.zero [axiom, in Char]
closed_states [lemma, in Loop]
cm [definition, in IAdd]
cn [variable, in Instructions]
code [definition, in Loop_Assertions]
code [definition, in Loop]
code [definition, in IAdd]
Code_to_test_instructions [definition, in Instructions]
Common [library]
constLemma [lemma, in Loop_Assertions]
constn [lemma, in Loop_Assertions]
constn [lemma, in Loop]
const0 [lemma, in Loop]
const1 [lemma, in Loop_Assertions]
const1 [lemma, in Loop]

D

Dec [section, in Common]
Dec.P [variable, in Common]
described [inductive, in Loop]
described_0 [lemma, in Loop_Assertions]
described_20 [constructor, in Loop]
described_19 [constructor, in Loop]
described_18 [constructor, in Loop]
described_17 [constructor, in Loop]
described_16 [constructor, in Loop]
described_15 [constructor, in Loop]
described_14 [constructor, in Loop]
described_13 [constructor, in Loop]
described_12 [constructor, in Loop]
described_11 [constructor, in Loop]
described_10 [constructor, in Loop]
described_9 [constructor, in Loop]
described_8 [constructor, in Loop]
described_7 [constructor, in Loop]
described_6 [constructor, in Loop]
described_5 [constructor, in Loop]
described_4 [constructor, in Loop]
described_3 [constructor, in Loop]
described_2 [constructor, in Loop]
described_1 [constructor, in Loop]
described_0 [constructor, in Loop]
DNum [module, in Instructions]
DOUBLE_ARITHMETIC.arithmetic [definition, in Arithmetic]
DOUBLE_ARITHMETIC.castArithmetic [definition, in Arithmetic]
DOUBLE_ARITHMETIC.CastInd_d2l [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.CastInd_d2i [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.CastInd_d2f [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.castInd [inductive, in Arithmetic]
DOUBLE_ARITHMETIC.cmpiArithmetic [definition, in Arithmetic]
DOUBLE_ARITHMETIC.CmpiInd_cmpl [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.CmpiInd_cmpg [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.cmpiInd [inductive, in Arithmetic]
DOUBLE_ARITHMETIC.cmpValuesArithmetic [definition, in Arithmetic]
DOUBLE_ARITHMETIC.cmpValuesInd [inductive, in Arithmetic]
DOUBLE_ARITHMETIC.cmpZeroArithmetic [definition, in Arithmetic]
DOUBLE_ARITHMETIC.cmpZeroInd [inductive, in Arithmetic]
DOUBLE_ARITHMETIC.binOpArithmetic [definition, in Arithmetic]
DOUBLE_ARITHMETIC.CmpIInd_fcmpl [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.CmpIInd_fcmpg [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.CmpIInd [inductive, in Arithmetic]
DOUBLE_ARITHMETIC.BinOpInd_rem [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.BinOpInd_div [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.BinOpInd_mul [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.BinOpInd_sub [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.BinOpInd_add [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.binOpInd [inductive, in Arithmetic]
DOUBLE_ARITHMETIC.unOpArithmetic [definition, in Arithmetic]
DOUBLE_ARITHMETIC.UnOpInd_neg [constructor, in Arithmetic]
DOUBLE_ARITHMETIC.unOpInd [inductive, in Arithmetic]
DOUBLE_ARITHMETIC.kind [definition, in Arithmetic]
DOUBLE_ARITHMETIC.M_ArithmeticTypes [module, in Arithmetic]
DOUBLE_ARITHMETIC [module, in Arithmetic]

E

eqDec [definition, in Common]
EqDec [section, in Common]
eqDecS [definition, in Common]
EqDec.A [variable, in Common]

F

final_20 [lemma, in Loop_Assertions]
final_20 [lemma, in Loop]
findInListOfPairs [definition, in Common]
flip3 [definition, in Common]
FLOAT_ARITHMETIC.arithmetic [definition, in Arithmetic]
FLOAT_ARITHMETIC.castArithmetic [definition, in Arithmetic]
FLOAT_ARITHMETIC.CastInd_f2l [constructor, in Arithmetic]
FLOAT_ARITHMETIC.CastInd_f2i [constructor, in Arithmetic]
FLOAT_ARITHMETIC.CastInd_f2d [constructor, in Arithmetic]
FLOAT_ARITHMETIC.castInd [inductive, in Arithmetic]
FLOAT_ARITHMETIC.cmpiArithmetic [definition, in Arithmetic]
FLOAT_ARITHMETIC.CmpiInd_cmpl [constructor, in Arithmetic]
FLOAT_ARITHMETIC.CmpiInd_cmpg [constructor, in Arithmetic]
FLOAT_ARITHMETIC.cmpiInd [inductive, in Arithmetic]
FLOAT_ARITHMETIC.cmpValuesArithmetic [definition, in Arithmetic]
FLOAT_ARITHMETIC.cmpValuesInd [inductive, in Arithmetic]
FLOAT_ARITHMETIC.cmpZeroArithmetic [definition, in Arithmetic]
FLOAT_ARITHMETIC.cmpZeroInd [inductive, in Arithmetic]
FLOAT_ARITHMETIC.binOpArithmetic [definition, in Arithmetic]
FLOAT_ARITHMETIC.BinOpInd_rem [constructor, in Arithmetic]
FLOAT_ARITHMETIC.BinOpInd_div [constructor, in Arithmetic]
FLOAT_ARITHMETIC.BinOpInd_mul [constructor, in Arithmetic]
FLOAT_ARITHMETIC.BinOpInd_sub [constructor, in Arithmetic]
FLOAT_ARITHMETIC.BinOpInd_add [constructor, in Arithmetic]
FLOAT_ARITHMETIC.binOpInd [inductive, in Arithmetic]
FLOAT_ARITHMETIC.unOpArithmetic [definition, in Arithmetic]
FLOAT_ARITHMETIC.UnOpInd_neg [constructor, in Arithmetic]
FLOAT_ARITHMETIC.unOpInd [inductive, in Arithmetic]
FLOAT_ARITHMETIC.kind [definition, in Arithmetic]
FLOAT_ARITHMETIC.M_ArithmeticTypes [module, in Arithmetic]
FLOAT_ARITHMETIC [module, in Arithmetic]
FMake [module, in FNumeric]
FMake.abstract_rem [definition, in FNumeric]
FMake.add [definition, in FNumeric]
FMake.add_prop [lemma, in FNumeric]
FMake.cmpg_nan [lemma, in FNumeric]
FMake.cmpg_lt [lemma, in FNumeric]
FMake.cmpg_eq [lemma, in FNumeric]
FMake.cmpg_gt [lemma, in FNumeric]
FMake.cmpl_nan [lemma, in FNumeric]
FMake.cmpl_lt [lemma, in FNumeric]
FMake.cmpl_eq [lemma, in FNumeric]
FMake.cmpl_gt [lemma, in FNumeric]
FMake.const [definition, in FNumeric]
FMake.div [definition, in FNumeric]
FMake.div_prop [lemma, in FNumeric]
FMake.fit_into [definition, in FNumeric]
FMake.fromDiadic [definition, in FNumeric]
FMake.GeIEEE [definition, in FNumeric]
FMake.GtIEEE [definition, in FNumeric]
FMake.iconst [definition, in FNumeric]
FMake.isNaN [inductive, in FNumeric]
FMake.IsNaNIs [constructor, in FNumeric]
FMake.mul [definition, in FNumeric]
FMake.mul_prop [lemma, in FNumeric]
FMake.neg [definition, in FNumeric]
FMake.neg_prop [lemma, in FNumeric]
FMake.one [definition, in FNumeric]
FMake.one_prop [lemma, in FNumeric]
FMake.precision [definition, in FNumeric]
FMake.rem [definition, in FNumeric]
FMake.rem_prop [lemma, in FNumeric]
FMake.rmode [definition, in FNumeric]
FMake.round_mag_down_int [definition, in FNumeric]
FMake.sign_of [definition, in FNumeric]
FMake.sub [definition, in FNumeric]
FMake.sub_prop [lemma, in FNumeric]
FMake.t [definition, in FNumeric]
FMake.toDiadic [definition, in FNumeric]
FMake.toIEEE [definition, in FNumeric]
FMake.truncate [definition, in FNumeric]
FMake.truncate_too_large [lemma, in FNumeric]
FMake.truncate_too_small [lemma, in FNumeric]
FMake.truncate_range_negative [lemma, in FNumeric]
FMake.truncate_range_positive [lemma, in FNumeric]
FMake.truncate_nan [lemma, in FNumeric]
FMake.two [definition, in FNumeric]
FMake.two_prop [lemma, in FNumeric]
FMake.zero [definition, in FNumeric]
FMake.zero_prop [lemma, in FNumeric]
fname [variable, in Instructions]
FNum [module, in Instructions]
FNUMERIC [module, in FNumeric]
FNumeric [library]
FNUMERIC.abstract_rem [axiom, in FNumeric]
FNUMERIC.add [axiom, in FNumeric]
FNUMERIC.add_prop [axiom, in FNumeric]
FNUMERIC.cmpg [axiom, in FNumeric]
FNUMERIC.cmpg_nan [axiom, in FNumeric]
FNUMERIC.cmpg_lt [axiom, in FNumeric]
FNUMERIC.cmpg_eq [axiom, in FNumeric]
FNUMERIC.cmpg_gt [axiom, in FNumeric]
FNUMERIC.cmpl [axiom, in FNumeric]
FNUMERIC.cmpl_nan [axiom, in FNumeric]
FNUMERIC.cmpl_lt [axiom, in FNumeric]
FNUMERIC.cmpl_eq [axiom, in FNumeric]
FNUMERIC.cmpl_gt [axiom, in FNumeric]
FNUMERIC.const [axiom, in FNumeric]
FNUMERIC.div [axiom, in FNumeric]
FNUMERIC.div_prop [axiom, in FNumeric]
FNUMERIC.fromDiadic [axiom, in FNumeric]
FNUMERIC.GeIEEE [definition, in FNumeric]
FNUMERIC.GtIEEE [definition, in FNumeric]
FNUMERIC.iconst [axiom, in FNumeric]
FNUMERIC.isNaN [inductive, in FNumeric]
FNUMERIC.IsNaNIs [constructor, in FNumeric]
FNUMERIC.mul [axiom, in FNumeric]
FNUMERIC.mul_prop [axiom, in FNumeric]
FNUMERIC.neg [axiom, in FNumeric]
FNUMERIC.neg_prop [axiom, in FNumeric]
FNUMERIC.one [axiom, in FNumeric]
FNUMERIC.one_prop [axiom, in FNumeric]
FNUMERIC.precision [axiom, in FNumeric]
FNUMERIC.rem [axiom, in FNumeric]
FNUMERIC.rem_prop [axiom, in FNumeric]
FNUMERIC.rmode [definition, in FNumeric]
FNUMERIC.sub [axiom, in FNumeric]
FNUMERIC.sub_prop [axiom, in FNumeric]
FNUMERIC.t [axiom, in FNumeric]
FNUMERIC.toDiadic [axiom, in FNumeric]
FNUMERIC.toIEEE [axiom, in FNumeric]
FNUMERIC.truncate [axiom, in FNumeric]
FNUMERIC.truncate_too_large [axiom, in FNumeric]
FNUMERIC.truncate_too_small [axiom, in FNumeric]
FNUMERIC.truncate_range_negative [axiom, in FNumeric]
FNUMERIC.truncate_range_positive [axiom, in FNumeric]
FNUMERIC.truncate_nan [axiom, in FNumeric]
FNUMERIC.two [axiom, in FNumeric]
FNUMERIC.two_prop [axiom, in FNumeric]
FNUMERIC.zero [axiom, in FNumeric]
FNUMERIC.zero_prop [axiom, in FNumeric]
FPRECISION [module, in FNumeric]
FPRECISION.precision [axiom, in FNumeric]
frame_2_3_impl [lemma, in IAdd]
frame_1_2_impl [lemma, in IAdd]
frame_0_1_impl [lemma, in IAdd]
frame_2_3 [lemma, in IAdd]
frame_1_2 [lemma, in IAdd]
frame_0_1 [lemma, in IAdd]
frame0 [definition, in Loop_Assertions]
frame0 [definition, in Loop]
frame0 [definition, in IAdd]
frame0_ok [lemma, in IAdd]
frame0_props [definition, in IAdd]
frame1 [definition, in IAdd]
frame1_ok [lemma, in IAdd]
frame1_props [definition, in IAdd]
frame2 [definition, in IAdd]
frame2_ok [lemma, in IAdd]
frame2_props [definition, in IAdd]
frame3 [definition, in IAdd]
frame3_ok [lemma, in IAdd]
frame3_props [definition, in IAdd]
Functions [section, in Common]
Functions.A [variable, in Common]
Functions.B [variable, in Common]

G

getPC_isPC3 [lemma, in IAdd]
getPC_isPC2 [lemma, in IAdd]
getPC_isPC1 [lemma, in IAdd]
getPC_isPC0 [lemma, in IAdd]

H

H [module, in Loop_Assertions]
H [module, in Loop]
H [module, in IAdd]
half_base_max [lemma, in Loop_Assertions]
half_base_max [lemma, in Loop]
heap [axiom, in IAdd]
HEAP [module, in Heap]
Heap [library]
HeapFacts [module, in Heap]
HeapFacts.PRefType_NotNull [lemma, in Heap]
HEAP.arraySizeFromNat [definition, in Heap]
HEAP.emptyHeap [axiom, in Heap]
HEAP.freshLocation [axiom, in Heap]
HEAP.get [axiom, in Heap]
HEAP.getArrayCell [axiom, in Heap]
HEAP.getArrayComponentType [axiom, in Heap]
HEAP.getArraySize [axiom, in Heap]
HEAP.getArrayValue [axiom, in Heap]
HEAP.getClassObjectLoc [axiom, in Heap]
HEAP.getLocClass [definition, in Heap]
HEAP.getMonitorLockCount [axiom, in Heap]
HEAP.getMonitorThreadId [axiom, in Heap]
HEAP.getObjectClass [axiom, in Heap]
HEAP.getObjectField [axiom, in Heap]
HEAP.getObjectMonitor [axiom, in Heap]
HEAP.getReferenceType [definition, in Heap]
HEAP.getsetMonitorLockCount [axiom, in Heap]
HEAP.getsetMonitorThreadId [axiom, in Heap]
HEAP.getStaticField [axiom, in Heap]
HEAP.HeapSpec [section, in Heap]
HEAP.HeapSpec.arr [variable, in Heap]
HEAP.HeapSpec.arr1 [variable, in Heap]
HEAP.HeapSpec.arr2 [variable, in Heap]
HEAP.HeapSpec.cn [variable, in Heap]
HEAP.HeapSpec.cn1 [variable, in Heap]
HEAP.HeapSpec.cn2 [variable, in Heap]
HEAP.HeapSpec.fn [variable, in Heap]
HEAP.HeapSpec.fn1 [variable, in Heap]
HEAP.HeapSpec.fn2 [variable, in Heap]
HEAP.HeapSpec.h [variable, in Heap]
HEAP.HeapSpec.hval [variable, in Heap]
HEAP.HeapSpec.hval1 [variable, in Heap]
HEAP.HeapSpec.hval2 [variable, in Heap]
HEAP.HeapSpec.h1 [variable, in Heap]
HEAP.HeapSpec.h2 [variable, in Heap]
HEAP.HeapSpec.idx [variable, in Heap]
HEAP.HeapSpec.idx1 [variable, in Heap]
HEAP.HeapSpec.idx2 [variable, in Heap]
HEAP.HeapSpec.init_values [variable, in Heap]
HEAP.HeapSpec.loc [variable, in Heap]
HEAP.HeapSpec.loc1 [variable, in Heap]
HEAP.HeapSpec.loc2 [variable, in Heap]
HEAP.HeapSpec.obj [variable, in Heap]
HEAP.HeapSpec.obj1 [variable, in Heap]
HEAP.HeapSpec.obj2 [variable, in Heap]
HEAP.HeapSpec.th [variable, in Heap]
HEAP.HeapSpec.th1 [variable, in Heap]
HEAP.HeapSpec.th2 [variable, in Heap]
HEAP.HeapSpec.v [variable, in Heap]
HEAP.HeapSpec.va [variable, in Heap]
HEAP.HeapSpec.va1 [variable, in Heap]
HEAP.HeapSpec.va2 [variable, in Heap]
HEAP.HeapSpec.v1 [variable, in Heap]
HEAP.HeapSpec.v2 [variable, in Heap]
HEAP.HV_Array [constructor, in Heap]
HEAP.HV_Object [constructor, in Heap]
HEAP.HV_Empty [constructor, in Heap]
HEAP.initArray [axiom, in Heap]
HEAP.initObject [axiom, in Heap]
HEAP.MonitorInvariant [axiom, in Heap]
HEAP.MonitorInvariant1 [lemma, in Heap]
HEAP.MonitorLock [inductive, in Heap]
HEAP.MonitorLock_owner [constructor, in Heap]
HEAP.MonitorLock_free [constructor, in Heap]
HEAP.MonitorUnlock [inductive, in Heap]
HEAP.MonitorUnlock_owner [constructor, in Heap]
HEAP.MonitorUnlock_zero [constructor, in Heap]
HEAP.M_ProgramStructures [module, in Heap]
HEAP.newMonitor [axiom, in Heap]
HEAP.newMonitorLockCount [lemma, in Heap]
HEAP.newMonitorThreadId [axiom, in Heap]
HEAP.Pempty_empty_static [axiom, in Heap]
HEAP.Pempty_empty [axiom, in Heap]
HEAP.PfreshLocation_fresh [axiom, in Heap]
HEAP.PinitArray_otherCells [axiom, in Heap]
HEAP.PinitArray_initialised [axiom, in Heap]
HEAP.PinitObject_otherFields [axiom, in Heap]
HEAP.PinitObject_initialised [axiom, in Heap]
HEAP.Pnull_empty [axiom, in Heap]
HEAP.PsetArrayCell_size [axiom, in Heap]
HEAP.PsetArrayCell_other [axiom, in Heap]
HEAP.PsetArrayCell_same [axiom, in Heap]
HEAP.PsetObjectField_Class [axiom, in Heap]
HEAP.PsetObjectField_otherField [axiom, in Heap]
HEAP.PsetObjectField_sameField [axiom, in Heap]
HEAP.PsetStaticField_otherClass [axiom, in Heap]
HEAP.PsetStaticField_otherField [axiom, in Heap]
HEAP.PsetStaticField_change [axiom, in Heap]
HEAP.Pset_otherLocation [axiom, in Heap]
HEAP.Pset_get [axiom, in Heap]
HEAP.PsystemException_otherLocations [axiom, in Heap]
HEAP.PsystemException_locationAfter [axiom, in Heap]
HEAP.PThreadId_eqDec [axiom, in Heap]
HEAP.set [axiom, in Heap]
HEAP.setArrayCell [axiom, in Heap]
HEAP.setMonitorState [axiom, in Heap]
HEAP.setObjectField [axiom, in Heap]
HEAP.setObjectMonitor [axiom, in Heap]
HEAP.setStaticField [axiom, in Heap]
HEAP.systemException [axiom, in Heap]
HEAP.TArray [axiom, in Heap]
HEAP.TArrayIndex [definition, in Heap]
HEAP.TArraySize [definition, in Heap]
HEAP.THeap [axiom, in Heap]
HEAP.THeapValue [inductive, in Heap]
HEAP.TMonitor [axiom, in Heap]
HEAP.TObject [axiom, in Heap]
HEAP.TThreadId [axiom, in Heap]
HEAP.validIndex [definition, in Heap]
HEAP.validIndexNat [definition, in Heap]
HF [module, in Loop_Assertions]
HF [module, in Loop]
HF [module, in IAdd]

I

IAdd [library]
Instructions [library]
Instruction0 [lemma, in IAdd]
Instruction1 [lemma, in IAdd]
Instruction2 [lemma, in IAdd]
Instruction3 [lemma, in IAdd]
intArith [definition, in Loop_Assertions]
intArith [definition, in Loop]
intArith [definition, in IAdd]
INT_ARITHMETIC.arithmetic [definition, in Arithmetic]
INT_ARITHMETIC.castArithmetic [definition, in Arithmetic]
INT_ARITHMETIC.CastInd_i2d [constructor, in Arithmetic]
INT_ARITHMETIC.CastInd_i2f [constructor, in Arithmetic]
INT_ARITHMETIC.CastInd_i2l [constructor, in Arithmetic]
INT_ARITHMETIC.CastInd_i2s [constructor, in Arithmetic]
INT_ARITHMETIC.CastInd_i2c [constructor, in Arithmetic]
INT_ARITHMETIC.CastInd_i2b [constructor, in Arithmetic]
INT_ARITHMETIC.castInd [inductive, in Arithmetic]
INT_ARITHMETIC.cmpiArithmetic [definition, in Arithmetic]
INT_ARITHMETIC.cmpiInd [inductive, in Arithmetic]
INT_ARITHMETIC.cmpValuesArithmetic [definition, in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_gt [constructor, in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_ge [constructor, in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_lt [constructor, in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_le [constructor, in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_ne [constructor, in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_eq [constructor, in Arithmetic]
INT_ARITHMETIC.cmpValuesInd [inductive, in Arithmetic]
INT_ARITHMETIC.cmpZeroArithmetic [definition, in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_gt [constructor, in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_ge [constructor, in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_lt [constructor, in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_le [constructor, in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_ne [constructor, in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_eq [constructor, in Arithmetic]
INT_ARITHMETIC.cmpZeroInd [inductive, in Arithmetic]
INT_ARITHMETIC.binOpArithmetic [definition, in Arithmetic]
INT_ARITHMETIC.BinOpInd_ushr [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_shr [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_shl [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_or [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_and [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_xor [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_rem0 [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_rem [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_div0 [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_div [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_mul [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_sub [constructor, in Arithmetic]
INT_ARITHMETIC.BinOpInd_add [constructor, in Arithmetic]
INT_ARITHMETIC.binOpInd [inductive, in Arithmetic]
INT_ARITHMETIC.unOpArithmetic [definition, in Arithmetic]
INT_ARITHMETIC.UnOpInd_neg [constructor, in Arithmetic]
INT_ARITHMETIC.unOpInd [inductive, in Arithmetic]
INT_ARITHMETIC.kind [definition, in Arithmetic]
INT_ARITHMETIC.M_ArithmeticTypes [module, in Arithmetic]
INT_ARITHMETIC [module, in Arithmetic]
INum [module, in Instructions]
INum [module, in Loop_Assertions]
INum [module, in Program_A]
INum [module, in Loop]
inverse [definition, in Common]
inverse_id [lemma, in Common]

J

jvm0 [definition, in IAdd]
jvm0_ok [lemma, in IAdd]
jvm0_props [definition, in IAdd]
jvm1 [definition, in IAdd]
jvm1_ok [lemma, in IAdd]
jvm1_props [definition, in IAdd]
jvm2 [definition, in IAdd]
jvm2_ok [lemma, in IAdd]
jvm2_props [definition, in IAdd]
jvm3 [definition, in IAdd]
jvm3_ok [lemma, in IAdd]
jvm3_props [definition, in IAdd]

K

k [variable, in Instructions]

L

lassertions [definition, in Loop_Assertions]
ListPrefix [inductive, in Common]
ListPrefix_Rec [constructor, in Common]
ListPrefix_Nil [constructor, in Common]
Lists [section, in Common]
Lists.A [variable, in Common]
Lists.K [variable, in Common]
Lists.keyEqDec [variable, in Common]
LNum [module, in Instructions]
LONG_ARITHMETIC.arithmetic [definition, in Arithmetic]
LONG_ARITHMETIC.castArithmetic [definition, in Arithmetic]
LONG_ARITHMETIC.CastInd_l2f [constructor, in Arithmetic]
LONG_ARITHMETIC.CastInd_l2d [constructor, in Arithmetic]
LONG_ARITHMETIC.CastInd_l2i [constructor, in Arithmetic]
LONG_ARITHMETIC.castInd [inductive, in Arithmetic]
LONG_ARITHMETIC.cmpiArithmetic [definition, in Arithmetic]
LONG_ARITHMETIC.CmpiInd_cmpl [constructor, in Arithmetic]
LONG_ARITHMETIC.cmpiInd [inductive, in Arithmetic]
LONG_ARITHMETIC.cmpValuesArithmetic [definition, in Arithmetic]
LONG_ARITHMETIC.cmpValuesInd [inductive, in Arithmetic]
LONG_ARITHMETIC.cmpZeroArithmetic [definition, in Arithmetic]
LONG_ARITHMETIC.cmpZeroInd [inductive, in Arithmetic]
LONG_ARITHMETIC.binOpArithmetic [definition, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_ushr [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_shr [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_shl [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_or [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_and [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_xor [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_rem0 [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_rem [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_div0 [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_div [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_mul [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_sub [constructor, in Arithmetic]
LONG_ARITHMETIC.BinOpInd_add [constructor, in Arithmetic]
LONG_ARITHMETIC.binOpInd [inductive, in Arithmetic]
LONG_ARITHMETIC.unOpArithmetic [definition, in Arithmetic]
LONG_ARITHMETIC.UnOpInd_neg [constructor, in Arithmetic]
LONG_ARITHMETIC.unOpInd [inductive, in Arithmetic]
LONG_ARITHMETIC.kind [definition, in Arithmetic]
LONG_ARITHMETIC.M_ArithmeticTypes [module, in Arithmetic]
LONG_ARITHMETIC [module, in Arithmetic]
Loop [library]
LoopExample [section, in Loop_Assertions]
LoopExample [section, in Loop]
LoopExample.n_small [variable, in Loop_Assertions]
LoopExample.n_positive [variable, in Loop_Assertions]
LoopExample.n_small [variable, in Loop]
LoopExample.n_positive [variable, in Loop]
LoopExample.n2_small [variable, in Loop_Assertions]
LoopExample.n2_small [variable, in Loop]
Loop_Assertions [library]

M

Make [module, in Char]
Make [module, in Numeric]
Make.add [axiom, in Numeric]
Make.add_prop [axiom, in Numeric]
Make.and [axiom, in Numeric]
Make.base [definition, in Char]
Make.base [definition, in Numeric]
Make.base_ge_2 [lemma, in Char]
Make.clear_false [definition, in Char]
Make.clear_false [definition, in Numeric]
Make.compare [definition, in Numeric]
Make.const [axiom, in Char]
Make.const [axiom, in Numeric]
Make.const_prop [axiom, in Char]
Make.const_prop [axiom, in Numeric]
Make.digits_of_Z [definition, in Char]
Make.digits_of_pos [definition, in Char]
Make.digits_of_Z [definition, in Numeric]
Make.digits_of_pos [definition, in Numeric]
Make.div [axiom, in Numeric]
Make.div_prop [axiom, in Numeric]
Make.half_base_ge_2 [lemma, in Numeric]
Make.half_base [definition, in Numeric]
Make.isNotZero [definition, in Numeric]
Make.is_gt [definition, in Numeric]
Make.is_ge [definition, in Numeric]
Make.is_lt [definition, in Numeric]
Make.is_le [definition, in Numeric]
Make.is_ne [definition, in Numeric]
Make.is_eq [definition, in Numeric]
Make.minus_one [definition, in Numeric]
Make.mul [axiom, in Numeric]
Make.mul_prop [axiom, in Numeric]
Make.neg [axiom, in Numeric]
Make.neg_prop [axiom, in Numeric]
Make.one [definition, in Numeric]
Make.or [axiom, in Numeric]
Make.Pcompare_toZ [lemma, in Numeric]
Make.PisNotZero [lemma, in Numeric]
Make.PminusOneToZ [lemma, in Numeric]
Make.PNumericEqDec [axiom, in Numeric]
Make.PoneIsNotZero [lemma, in Numeric]
Make.PoneToZ [lemma, in Numeric]
Make.pos_Z_of_digits [definition, in Char]
Make.pos_of_digits [definition, in Char]
Make.pos_of_digits [definition, in Numeric]
Make.power [definition, in Char]
Make.power [definition, in Numeric]
Make.power_positive [lemma, in Char]
Make.power_positive [lemma, in Numeric]
Make.PToZDistinct [axiom, in Numeric]
Make.PzeroToZ [lemma, in Char]
Make.PzeroToZ [lemma, in Numeric]
Make.range [definition, in Char]
Make.range [definition, in Numeric]
Make.range_prop [axiom, in Char]
Make.range_prop [axiom, in Numeric]
Make.rem [axiom, in Numeric]
Make.rem_prop [axiom, in Numeric]
Make.shl [axiom, in Numeric]
Make.shl_prop [axiom, in Numeric]
Make.shr [axiom, in Numeric]
Make.shr_prop [axiom, in Numeric]
Make.smod [definition, in Numeric]
Make.sub [axiom, in Numeric]
Make.sub_prop [axiom, in Numeric]
Make.t [axiom, in Char]
Make.t [axiom, in Numeric]
Make.testdop45 [lemma, in Char]
Make.testdop45 [lemma, in Numeric]
Make.testm42 [lemma, in Numeric]
Make.testm43 [lemma, in Char]
Make.testm43 [lemma, in Numeric]
Make.testm44 [lemma, in Char]
Make.testm44 [lemma, in Numeric]
Make.testm45 [lemma, in Char]
Make.testm45 [lemma, in Numeric]
Make.testm73 [lemma, in Char]
Make.testm73 [lemma, in Numeric]
Make.testm74 [lemma, in Char]
Make.testm74 [lemma, in Numeric]
Make.testm75 [lemma, in Char]
Make.testm75 [lemma, in Numeric]
Make.toZ [axiom, in Char]
Make.toZ [axiom, in Numeric]
Make.truncate [definition, in Numeric]
Make.truncateZ [definition, in Char]
Make.truncateZ [definition, in Numeric]
Make.truncate_on_zero [axiom, in Char]
Make.truncate_to_char [definition, in Char]
Make.ushr [axiom, in Numeric]
Make.ushr_prop2 [axiom, in Numeric]
Make.ushr_prop1 [axiom, in Numeric]
Make.xor [axiom, in Numeric]
Make.zero [definition, in Char]
Make.zero [definition, in Numeric]
Make.Z_of_digits [definition, in Numeric]
map_oneOrTwo [definition, in Common]
max [definition, in Loop_Assertions]
max [definition, in Loop]
method_name [axiom, in IAdd]
MONOLITIC_HEAP.PsetStaticField_mono [axiom, in Heap]
MONOLITIC_HEAP.Pset_mono [axiom, in Heap]
MONOLITIC_HEAP.PgetStaticField_mono [axiom, in Heap]
MONOLITIC_HEAP.Pget_mono [axiom, in Heap]
MONOLITIC_HEAP.MonoHeapSpec.init_values [variable, in Heap]
MONOLITIC_HEAP.MonoHeapSpec.v [variable, in Heap]
MONOLITIC_HEAP.MonoHeapSpec.hv [variable, in Heap]
MONOLITIC_HEAP.MonoHeapSpec.fn [variable, in Heap]
MONOLITIC_HEAP.MonoHeapSpec.cn [variable, in Heap]
MONOLITIC_HEAP.MonoHeapSpec.th2 [variable, in Heap]
MONOLITIC_HEAP.MonoHeapSpec.th1 [variable, in Heap]
MONOLITIC_HEAP.MonoHeapSpec.loc [variable, in Heap]
MONOLITIC_HEAP.MonoHeapSpec.h [variable, in Heap]
MONOLITIC_HEAP.MonoHeapSpec [section, in Heap]
MONOLITIC_HEAP [module, in Heap]
msig [variable, in Instructions]
M_IntNumProperties [module, in Loop_Assertions]
M_IntNumProperties [module, in Loop]

N

n [variable, in Instructions]
n [axiom, in Loop_Assertions]
n [axiom, in Program_A]
n [axiom, in Loop]
nfour [definition, in IAdd]
ntwo [definition, in IAdd]
NUMERIC [module, in Numeric]
Numeric [library]
NumericProperties [module, in Numeric]
NumericProperties.example_is_gt_f [axiom, in Numeric]
NumericProperties.example_is_gt_t [axiom, in Numeric]
NumericProperties.example_is_ge_f [axiom, in Numeric]
NumericProperties.example_is_ge_t [axiom, in Numeric]
NumericProperties.example_is_lt_f [axiom, in Numeric]
NumericProperties.example_is_lt_t [axiom, in Numeric]
NumericProperties.example_is_le_f [axiom, in Numeric]
NumericProperties.example_is_le_t [axiom, in Numeric]
NumericProperties.example_is_ne_f [axiom, in Numeric]
NumericProperties.example_is_ne_t [axiom, in Numeric]
NumericProperties.example_is_eq_f [axiom, in Numeric]
NumericProperties.example_is_eq_t [axiom, in Numeric]
NumericProperties.is_gt_f_toZ_prop [axiom, in Numeric]
NumericProperties.is_gt_t_toZ_prop [axiom, in Numeric]
NumericProperties.is_ge_f_toZ_prop [axiom, in Numeric]
NumericProperties.is_ge_t_toZ_prop [axiom, in Numeric]
NumericProperties.is_lt_f_toZ_prop [axiom, in Numeric]
NumericProperties.is_lt_t_toZ_prop [axiom, in Numeric]
NumericProperties.is_le_f_toZ_prop [axiom, in Numeric]
NumericProperties.is_le_t_toZ_prop [axiom, in Numeric]
NumericProperties.is_ne_f_toZ_prop [axiom, in Numeric]
NumericProperties.is_ne_t_toZ_prop [axiom, in Numeric]
NumericProperties.is_eq_f_toZ_prop [axiom, in Numeric]
NumericProperties.is_eq_t_toZ_prop [axiom, in Numeric]
NumericProperties.Pcompare_const [lemma, in Numeric]
NUMERIC.add [axiom, in Numeric]
NUMERIC.add_prop [axiom, in Numeric]
NUMERIC.and [axiom, in Numeric]
NUMERIC.base [definition, in Numeric]
NUMERIC.compare [axiom, in Numeric]
NUMERIC.const [axiom, in Numeric]
NUMERIC.const_prop [axiom, in Numeric]
NUMERIC.div [axiom, in Numeric]
NUMERIC.div_prop [axiom, in Numeric]
NUMERIC.half_base [definition, in Numeric]
NUMERIC.isNotZero [axiom, in Numeric]
NUMERIC.is_gt [axiom, in Numeric]
NUMERIC.is_ge [axiom, in Numeric]
NUMERIC.is_lt [axiom, in Numeric]
NUMERIC.is_le [axiom, in Numeric]
NUMERIC.is_ne [axiom, in Numeric]
NUMERIC.is_eq [axiom, in Numeric]
NUMERIC.minus_one [axiom, in Numeric]
NUMERIC.mul [axiom, in Numeric]
NUMERIC.mul_prop [axiom, in Numeric]
NUMERIC.neg [axiom, in Numeric]
NUMERIC.neg_prop [axiom, in Numeric]
NUMERIC.one [axiom, in Numeric]
NUMERIC.or [axiom, in Numeric]
NUMERIC.Pcompare_toZ [axiom, in Numeric]
NUMERIC.PisNotZero [axiom, in Numeric]
NUMERIC.PminusOneToZ [axiom, in Numeric]
NUMERIC.PNumericEqDec [axiom, in Numeric]
NUMERIC.PoneIsNotZero [axiom, in Numeric]
NUMERIC.PoneToZ [axiom, in Numeric]
NUMERIC.power [axiom, in Numeric]
NUMERIC.power_positive [axiom, in Numeric]
NUMERIC.PToZDistinct [axiom, in Numeric]
NUMERIC.PzeroToZ [axiom, in Numeric]
NUMERIC.range [definition, in Numeric]
NUMERIC.range_prop [axiom, in Numeric]
NUMERIC.rem [axiom, in Numeric]
NUMERIC.rem_prop [axiom, in Numeric]
NUMERIC.shl [axiom, in Numeric]
NUMERIC.shl_prop [axiom, in Numeric]
NUMERIC.shr [axiom, in Numeric]
NUMERIC.shr_prop [axiom, in Numeric]
NUMERIC.smod [definition, in Numeric]
NUMERIC.sub [axiom, in Numeric]
NUMERIC.sub_prop [axiom, in Numeric]
NUMERIC.t [axiom, in Numeric]
NUMERIC.toZ [axiom, in Numeric]
NUMERIC.truncate [axiom, in Numeric]
NUMERIC.ushr [axiom, in Numeric]
NUMERIC.ushr_prop2 [axiom, in Numeric]
NUMERIC.ushr_prop1 [axiom, in Numeric]
NUMERIC.xor [axiom, in Numeric]
NUMERIC.zero [axiom, in Numeric]
NUMSIZE [module, in Numeric]
NUMSIZE.power [axiom, in Numeric]
NUMSIZE.power_positive [axiom, in Numeric]
num_224_const [lemma, in IAdd]
num_224_toZ [lemma, in IAdd]
num_224_impl_toZ [lemma, in IAdd]

O

off [variable, in Instructions]
One [constructor, in Common]

P

P [module, in Instructions]
P [module, in Loop_Assertions]
P [module, in Program_A]
P [module, in Loop]
p [axiom, in IAdd]
P [module, in IAdd]
partial_correctness [lemma, in Loop_Assertions]
partial_correctness [lemma, in Loop]
PASSERT [module, in Loop_Assertions]
pc0 [definition, in Loop_Assertions]
pc0 [definition, in Loop]
pc0 [definition, in IAdd]
pc0_neq_pc3 [lemma, in IAdd]
pc0_next [lemma, in IAdd]
pc1 [definition, in IAdd]
pc1_neq_pc3 [lemma, in IAdd]
pc1_next [lemma, in IAdd]
pc2 [definition, in IAdd]
pc2_neq_pc3 [lemma, in IAdd]
pc2_next [lemma, in IAdd]
pc3 [definition, in IAdd]
PeqDecS_eqDec [lemma, in Common]
Pnth_error_in [lemma, in Common]
Pnth_error_length [lemma, in Common]
post5_impl_pre6 [lemma, in Loop_Assertions]
post5_impl_pre6 [lemma, in Loop]
post8_impl_9_or_19 [lemma, in Loop_Assertions]
post8_impl_9_or_19 [lemma, in Loop]
PpropDecS_propDec [lemma, in Common]
PROGRAM [module, in Program]
Program [library]
ProgramAssertions [library]
ProgramStructures [library]
ProgramStructuresFacts [module, in ProgramStructures]
ProgramStructuresFacts.distinct_vars_next [lemma, in ProgramStructures]
ProgramStructuresFacts.distinct_vars_2_3 [lemma, in ProgramStructures]
ProgramStructuresFacts.distinct_vars_1_3 [lemma, in ProgramStructures]
ProgramStructuresFacts.distinct_vars_1_2 [lemma, in ProgramStructures]
ProgramStructuresFacts.distinct_vars_0_3 [lemma, in ProgramStructures]
ProgramStructuresFacts.distinct_vars_0_2 [lemma, in ProgramStructures]
ProgramStructuresFacts.distinct_vars_0_1 [lemma, in ProgramStructures]
ProgramStructuresFacts.distinct_varFromNat [lemma, in ProgramStructures]
ProgramStructuresFacts.StandardNames [module, in ProgramStructures]
ProgramStructuresFacts.StandardNames.AbstractMethodError [axiom, in ProgramStructures]
ProgramStructuresFacts.StandardNames.ArithmeticException [axiom, in ProgramStructures]
ProgramStructuresFacts.StandardNames.ArrayIndexOutOfBoundsException [axiom, in ProgramStructures]
ProgramStructuresFacts.StandardNames.arrayInterfaces [definition, in ProgramStructures]
ProgramStructuresFacts.StandardNames.ArrayStoreException [axiom, in ProgramStructures]
ProgramStructuresFacts.StandardNames.ClassCastException [axiom, in ProgramStructures]
ProgramStructuresFacts.StandardNames.IllegalMonitorStateException [axiom, in ProgramStructures]
ProgramStructuresFacts.StandardNames.NegativeArraySizeException [axiom, in ProgramStructures]
ProgramStructuresFacts.StandardNames.NullPointerException [axiom, in ProgramStructures]
ProgramStructuresFacts.StandardNames.Object [axiom, in ProgramStructures]
ProgramStructuresFacts.StandardNames.Throwable [axiom, in ProgramStructures]
ProgramStructuresFacts.var0 [definition, in ProgramStructures]
ProgramStructuresFacts.var1 [definition, in ProgramStructures]
ProgramStructuresFacts.var2 [definition, in ProgramStructures]
ProgramStructuresFacts.var3 [definition, in ProgramStructures]
ProgramStructuresImpl [module, in ProgramStructuresImpl]
ProgramStructuresImpl [library]
ProgramStructuresImpl.M_VarMap [module, in ProgramStructuresImpl]
ProgramStructuresImpl.M_Var_as_OT [module, in ProgramStructuresImpl]
ProgramStructuresImpl.M_ValuesAndTypes [module, in ProgramStructuresImpl]
ProgramStructuresImpl.nextVar [definition, in ProgramStructuresImpl]
ProgramStructuresImpl.N_eqDec [lemma, in ProgramStructuresImpl]
ProgramStructuresImpl.PnatVar [definition, in ProgramStructuresImpl]
ProgramStructuresImpl.PnextVarSucc [lemma, in ProgramStructuresImpl]
ProgramStructuresImpl.PvarNat [definition, in ProgramStructuresImpl]
ProgramStructuresImpl.PVar_eqDec [definition, in ProgramStructuresImpl]
ProgramStructuresImpl.TQualifiedMethodName [definition, in ProgramStructuresImpl]
ProgramStructuresImpl.TSignature [definition, in ProgramStructuresImpl]
ProgramStructuresImpl.TVar [definition, in ProgramStructuresImpl]
ProgramStructuresImpl.varFromNat [definition, in ProgramStructuresImpl]
ProgramStructuresImpl.varToNat [definition, in ProgramStructuresImpl]
PROGRAM_ASSERTIONS_W_CONSTRUCTORS.frameDescribed_inRange [lemma, in ProgramAssertions]
PROGRAM_ASSERTIONS_W_CONSTRUCTORS.PgetInstructionIffNth [axiom, in ProgramAssertions]
PROGRAM_ASSERTIONS_W_CONSTRUCTORS.assertionsFromList [axiom, in ProgramAssertions]
PROGRAM_ASSERTIONS_W_CONSTRUCTORS [module, in ProgramAssertions]
PROGRAM_ASSERTIONS.multiTransitions [lemma, in ProgramAssertions]
PROGRAM_ASSERTIONS.singleTransitions [definition, in ProgramAssertions]
PROGRAM_ASSERTIONS.frameDescribed_equiv [lemma, in ProgramAssertions]
PROGRAM_ASSERTIONS.frameDescribed2 [definition, in ProgramAssertions]
PROGRAM_ASSERTIONS.frameDescribed [definition, in ProgramAssertions]
PROGRAM_ASSERTIONS.positionedAssertionPc [lemma, in ProgramAssertions]
PROGRAM_ASSERTIONS.codeDescribed [definition, in ProgramAssertions]
PROGRAM_ASSERTIONS.getPositionedAssertion [definition, in ProgramAssertions]
PROGRAM_ASSERTIONS.getCodeAssertion [axiom, in ProgramAssertions]
PROGRAM_ASSERTIONS.TCodeAssertions [axiom, in ProgramAssertions]
PROGRAM_ASSERTIONS.TCodeAssertion [definition, in ProgramAssertions]
PROGRAM_ASSERTIONS.M_Sem_Frame [module, in ProgramAssertions]
PROGRAM_ASSERTIONS [module, in ProgramAssertions]
PROGRAM_W_CONSTRUCTORS.PgetClassIffIn [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.makeProgram [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PgetMethodIffIn [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PmakeClass_getClassName [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.makeClass [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PcodeFromList_next_pc [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PcodeFromList_next [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PmakeMethod_methodBeginning [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PmakeMethod_getCode [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PmakeMethod_getSignature [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.makeMethod [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PgetInstructionIffNth [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.codeFromList [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PmakeOffset_pc [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PmakeOffset [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.offsetFromPosition [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PpositionPc [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.PpcPosition [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.pcToPosition [axiom, in Program]
PROGRAM_W_CONSTRUCTORS.pcFromPosition [axiom, in Program]
PROGRAM_W_CONSTRUCTORS [module, in Program]
PROGRAM_STRUCTURES_WITH_MAP.M_VarMap [module, in ProgramStructures]
PROGRAM_STRUCTURES_WITH_MAP.M_Var_as_OT [module, in ProgramStructures]
PROGRAM_STRUCTURES_WITH_MAP [module, in ProgramStructures]
PROGRAM_STRUCTURES.PnextVarSucc [axiom, in ProgramStructures]
PROGRAM_STRUCTURES.nextVar [axiom, in ProgramStructures]
PROGRAM_STRUCTURES.PnatVar [axiom, in ProgramStructures]
PROGRAM_STRUCTURES.PvarNat [axiom, in ProgramStructures]
PROGRAM_STRUCTURES.varToNat [axiom, in ProgramStructures]
PROGRAM_STRUCTURES.varFromNat [axiom, in ProgramStructures]
PROGRAM_STRUCTURES.PVar_eqDec [axiom, in ProgramStructures]
PROGRAM_STRUCTURES.TVar [axiom, in ProgramStructures]
PROGRAM_STRUCTURES.TQualifiedMethodName [definition, in ProgramStructures]
PROGRAM_STRUCTURES.TSignature [definition, in ProgramStructures]
PROGRAM_STRUCTURES.M_ValuesAndTypes [module, in ProgramStructures]
PROGRAM_STRUCTURES [module, in ProgramStructures]
Program_A [library]
PROGRAM.CI_Lookupswitch [constructor, in Program]
PROGRAM.CI_Tableswitch [constructor, in Program]
PROGRAM.CI_Cmp [constructor, in Program]
PROGRAM.CI_If [constructor, in Program]
PROGRAM.CI_Goto [constructor, in Program]
PROGRAM.class_Throwable [axiom, in Program]
PROGRAM.class_Object [axiom, in Program]
PROGRAM.currentInstruction [definition, in Program]
PROGRAM.FI_Ret [constructor, in Program]
PROGRAM.FI_Jsr [constructor, in Program]
PROGRAM.FI_Cond [constructor, in Program]
PROGRAM.FI_Var [constructor, in Program]
PROGRAM.FI_Stackop [constructor, in Program]
PROGRAM.getClass [axiom, in Program]
PROGRAM.getClassInterfaces [axiom, in Program]
PROGRAM.getClassName [axiom, in Program]
PROGRAM.getDynamicFields [axiom, in Program]
PROGRAM.getEmptyObject [axiom, in Program]
PROGRAM.getField [axiom, in Program]
PROGRAM.getFieldName [axiom, in Program]
PROGRAM.getFieldType [axiom, in Program]
PROGRAM.getFieldVisibility [axiom, in Program]
PROGRAM.getInstruction [axiom, in Program]
PROGRAM.getMethod [axiom, in Program]
PROGRAM.getMethodBeginning [axiom, in Program]
PROGRAM.getMethodBodyFromProgram [axiom, in Program]
PROGRAM.getMethodCode [axiom, in Program]
PROGRAM.getMethodFromProgram [definition, in Program]
PROGRAM.getMethodSignature [axiom, in Program]
PROGRAM.getMethodVisibility [axiom, in Program]
PROGRAM.handlerInScope [axiom, in Program]
PROGRAM.handlerTarget [axiom, in Program]
PROGRAM.handlerType [axiom, in Program]
PROGRAM.hasSuperFlag [axiom, in Program]
PROGRAM.HI_Monitor [constructor, in Program]
PROGRAM.HI_New [constructor, in Program]
PROGRAM.HI_Put [constructor, in Program]
PROGRAM.HI_Get [constructor, in Program]
PROGRAM.InvokeInterface [constructor, in Program]
PROGRAM.InvokeSpecial [constructor, in Program]
PROGRAM.InvokeStatic [constructor, in Program]
PROGRAM.InvokeVirtual [constructor, in Program]
PROGRAM.isAbstractClass [axiom, in Program]
PROGRAM.isAncestorClass [definition, in Program]
PROGRAM.isAncestorClassOrSelf [definition, in Program]
PROGRAM.isClassInit [axiom, in Program]
PROGRAM.isConstructor [axiom, in Program]
PROGRAM.isDirectSuperTypeClass [definition, in Program]
PROGRAM.isFieldFinal [axiom, in Program]
PROGRAM.isFieldStatic [axiom, in Program]
PROGRAM.isInterfaceClass [axiom, in Program]
PROGRAM.isMethodAbstract [axiom, in Program]
PROGRAM.isMethodStatic [axiom, in Program]
PROGRAM.isMethodSynchronized [axiom, in Program]
PROGRAM.isParentClass [definition, in Program]
PROGRAM.isSuperTypeClass [definition, in Program]
PROGRAM.isSuperTypeClassOrSelf [definition, in Program]
PROGRAM.I_Throw [constructor, in Program]
PROGRAM.I_Return [constructor, in Program]
PROGRAM.I_Invoke [constructor, in Program]
PROGRAM.I_Heap [constructor, in Program]
PROGRAM.I_Frame [constructor, in Program]
PROGRAM.methodExnHandlers [axiom, in Program]
PROGRAM.M_ProgramStructuresFacts [module, in Program]
PROGRAM.M_ProgramStructures [module, in Program]
PROGRAM.next [axiom, in Program]
PROGRAM.Op_Lock [constructor, in Program]
PROGRAM.Op_Unlock [constructor, in Program]
PROGRAM.Op_newmultiarray [constructor, in Program]
PROGRAM.Op_newarray_ref [constructor, in Program]
PROGRAM.Op_newarray [constructor, in Program]
PROGRAM.Op_newobject [constructor, in Program]
PROGRAM.Op_putarray [constructor, in Program]
PROGRAM.Op_putstatic [constructor, in Program]
PROGRAM.Op_putfield [constructor, in Program]
PROGRAM.Op_instanceof [constructor, in Program]
PROGRAM.Op_checkcast [constructor, in Program]
PROGRAM.Op_array_length [constructor, in Program]
PROGRAM.Op_getarray [constructor, in Program]
PROGRAM.Op_getstatic [constructor, in Program]
PROGRAM.Op_getfield [constructor, in Program]
PROGRAM.Op_swap [constructor, in Program]
PROGRAM.Op_pop2 [constructor, in Program]
PROGRAM.Op_pop [constructor, in Program]
PROGRAM.Op_dup2_x2 [constructor, in Program]
PROGRAM.Op_dup2_x1 [constructor, in Program]
PROGRAM.Op_dup2 [constructor, in Program]
PROGRAM.Op_dup_x2 [constructor, in Program]
PROGRAM.Op_dup_x1 [constructor, in Program]
PROGRAM.Op_dup [constructor, in Program]
PROGRAM.Op_nop [constructor, in Program]
PROGRAM.PabstractMethodNoBody [axiom, in Program]
PROGRAM.Package [constructor, in Program]
PROGRAM.parentClass [axiom, in Program]
PROGRAM.PgetMethodBodyFromProgram [axiom, in Program]
PROGRAM.PObjectRoot [axiom, in Program]
PROGRAM.PparentClass [axiom, in Program]
PROGRAM.PparentClassDifferent [axiom, in Program]
PROGRAM.PparentClassWf [axiom, in Program]
PROGRAM.Private [constructor, in Program]
PROGRAM.Protected [constructor, in Program]
PROGRAM.Public [constructor, in Program]
PROGRAM.SI_Cmpi [constructor, in Program]
PROGRAM.SI_Cast [constructor, in Program]
PROGRAM.SI_Binop [constructor, in Program]
PROGRAM.SI_Unop [constructor, in Program]
PROGRAM.SI_Const [constructor, in Program]
PROGRAM.SI_Generic [constructor, in Program]
PROGRAM.subtypeRef [definition, in Program]
PROGRAM.TClass [axiom, in Program]
PROGRAM.TCode [axiom, in Program]
PROGRAM.TCondInstr [inductive, in Program]
PROGRAM.TField [axiom, in Program]
PROGRAM.TFrameInstr [inductive, in Program]
PROGRAM.TGenericOp [inductive, in Program]
PROGRAM.TGetOp [inductive, in Program]
PROGRAM.THandler [axiom, in Program]
PROGRAM.THeapInstr [inductive, in Program]
PROGRAM.TInstruction [inductive, in Program]
PROGRAM.TInvocationMode [inductive, in Program]
PROGRAM.TMethod [axiom, in Program]
PROGRAM.TMonitorOp [inductive, in Program]
PROGRAM.TNewOp [inductive, in Program]
PROGRAM.TProgram [axiom, in Program]
PROGRAM.TPutOp [inductive, in Program]
PROGRAM.TStackInstr [inductive, in Program]
PROGRAM.TVarInstr [inductive, in Program]
PROGRAM.TVisibility [inductive, in Program]
PROGRAM.validExceptionHandler [definition, in Program]
PROGRAM.validHandlerInd [inductive, in Program]
PROGRAM.ValidHandler_Cons [constructor, in Program]
PROGRAM.ValidHandler_Found [constructor, in Program]
PROGRAM.ValidHandler_Nil [constructor, in Program]
PROGRAM.VI_Inc [constructor, in Program]
PROGRAM.VI_Store [constructor, in Program]
PROGRAM.VI_Load [constructor, in Program]
propDec [definition, in Common]
propDecS [definition, in Common]
PS [module, in Instructions]
PS [module, in Loop_Assertions]
PS [module, in Program_A]
PS [module, in Loop]
PS [module, in IAdd]
PSF [module, in Loop_Assertions]
PSF [module, in Loop]
PSFacts [module, in Instructions]
PSFacts [module, in Program_A]

R

range_pos [lemma, in Loop_Assertions]
range_pos [lemma, in Loop]
reachable [definition, in Loop]
REF_ARITHMETIC.arithmetic [definition, in Arithmetic]
REF_ARITHMETIC.castArithmetic [definition, in Arithmetic]
REF_ARITHMETIC.castInd [inductive, in Arithmetic]
REF_ARITHMETIC.cmpiArithmetic [definition, in Arithmetic]
REF_ARITHMETIC.cmpiInd [inductive, in Arithmetic]
REF_ARITHMETIC.cmpValuesArithmetic [definition, in Arithmetic]
REF_ARITHMETIC.CmpValuesInd_nef [constructor, in Arithmetic]
REF_ARITHMETIC.CmpValuesInd_net [constructor, in Arithmetic]
REF_ARITHMETIC.CmpValuesInd_eqf [constructor, in Arithmetic]
REF_ARITHMETIC.CmpValuesInd_eqt [constructor, in Arithmetic]
REF_ARITHMETIC.cmpValuesInd [inductive, in Arithmetic]
REF_ARITHMETIC.cmpZeroArithmetic [definition, in Arithmetic]
REF_ARITHMETIC.CmpZeroInd_notnullf [constructor, in Arithmetic]
REF_ARITHMETIC.CmpZeroInd_notnullt [constructor, in Arithmetic]
REF_ARITHMETIC.CmpZeroInd_nullf [constructor, in Arithmetic]
REF_ARITHMETIC.CmpZeroInd_nullt [constructor, in Arithmetic]
REF_ARITHMETIC.cmpZeroInd [inductive, in Arithmetic]
REF_ARITHMETIC.binOpArithmetic [definition, in Arithmetic]
REF_ARITHMETIC.binOpInd [inductive, in Arithmetic]
REF_ARITHMETIC.unOpArithmetic [definition, in Arithmetic]
REF_ARITHMETIC.unOpInd [inductive, in Arithmetic]
REF_ARITHMETIC.kind [definition, in Arithmetic]
REF_ARITHMETIC.M_ArithmeticTypes [module, in Arithmetic]
REF_ARITHMETIC [module, in Arithmetic]
RS [module, in Loop_Assertions]
RS [module, in Loop]
RS [module, in IAdd]
RSF [module, in Loop_Assertions]
RSF [module, in Loop]
RSF [module, in IAdd]
rt [variable, in Instructions]
RuntimeStructures [library]
RuntimeStructuresFacts [module, in RuntimeStructures]
RuntimeStructuresFacts.initVarsInd [inductive, in RuntimeStructures]
RuntimeStructuresFacts.initVars_two [constructor, in RuntimeStructures]
RuntimeStructuresFacts.initVars_one [constructor, in RuntimeStructures]
RuntimeStructuresFacts.InitVars_nil [constructor, in RuntimeStructures]
RuntimeStructuresFacts.mapROX [definition, in RuntimeStructures]
RuntimeStructuresFacts.PlocalStackKAbstractionApp [lemma, in RuntimeStructures]
RuntimeStructuresFacts.PprefixMap [lemma, in RuntimeStructures]
RuntimeStructuresFacts.PprefixNilImpliesNil [lemma, in RuntimeStructures]
RuntimeStructuresFacts.PprefixTrivial [lemma, in RuntimeStructures]
RuntimeStructuresFacts.prefix [definition, in RuntimeStructures]
RuntimeStructuresFacts.prefixInd [inductive, in RuntimeStructures]
RuntimeStructuresFacts.Prefix_cons [constructor, in RuntimeStructures]
RuntimeStructuresFacts.Prefix_nil [constructor, in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValuesMap [lemma, in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValuesNilCons [lemma, in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValuesSame [lemma, in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValuesTrivial [lemma, in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValues_implies_prefix_r [lemma, in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValues_implies_prefix_l [lemma, in RuntimeStructures]
RuntimeStructuresFacts.stackTopValues [definition, in RuntimeStructures]
RuntimeStructuresImpl [module, in RuntimeStructuresImpl]
RuntimeStructuresImpl [library]
RuntimeStructuresImpl.cmCtxObjectLoc [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.cmCurrentClass [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.cmDeclClass [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.cmMake [constructor, in RuntimeStructuresImpl]
RuntimeStructuresImpl.cmQName [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.cmSignature [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.Exception [constructor, in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameGetLocalStack [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameGetPC [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameGetVars [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKAbstraction [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKConcretisation [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKShadowGetLocalStack [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKShadowGetPC [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKShadowGetVars [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKShadowMake [constructor, in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameMake [constructor, in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericStackDefinition [section, in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericStackDefinition.t [variable, in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition [section, in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.t [variable, in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.VarsProperties [section, in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.VarsProperties.v [variable, in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.VarsProperties.vars [variable, in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.VarsProperties.x [variable, in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.VarsProperties.y [variable, in RuntimeStructuresImpl]
RuntimeStructuresImpl.jvmGetHeap [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.jvmGetThreads [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.jvmMake [constructor, in RuntimeStructuresImpl]
RuntimeStructuresImpl.localStackKAbstraction [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.localStackKConcretisation [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.M_Heap [module, in RuntimeStructuresImpl]
RuntimeStructuresImpl.noneNotMapsTo [lemma, in RuntimeStructuresImpl]
RuntimeStructuresImpl.notMapsToNone [lemma, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PframeKConcretisationAbstraction [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PlocalStackKConcretisationAbstraction [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsEmptyGet [lemma, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsEqEquiv [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKAbstractionConsistent [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKAbstractionConsistentSet [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKAbstractionConsistentSome [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKConcretisationAbstraction [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKConcretisationConsistent [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKConcretisationConsistentSome [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsSetGet [lemma, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsSetGetOther [lemma, in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsSetSameEquiv [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.Result [constructor, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TCurrentMethod [record, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TEvalState [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TFrame [record, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TFrameKShadow [record, in RuntimeStructuresImpl]
RuntimeStructuresImpl.threadGetCallStack [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.threadGetEvalState [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.threadGetId [projection, in RuntimeStructuresImpl]
RuntimeStructuresImpl.threadMake [constructor, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TJVM [record, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TLocalStack [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TLocalStackGeneric [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TLocalStackKShadow [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TLocalStackTShadow [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TResultOrException [inductive, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TRichFrame [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TThread [record, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TVars [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TVarsGeneric [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TVarsKShadow [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.TVarsTShadow [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsEmpty [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsEquiv [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsGet [definition, in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsKAbstraction [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsKConcretisation [axiom, in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsSet [definition, in RuntimeStructuresImpl]
RUNTIME_STRUCTURES.Exception [constructor, in RuntimeStructures]
RUNTIME_STRUCTURES.Result [constructor, in RuntimeStructures]
RUNTIME_STRUCTURES.TResultOrException [inductive, in RuntimeStructures]
RUNTIME_STRUCTURES.jvmGetThreads [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.jvmGetHeap [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.TJVM [record, in RuntimeStructures]
RUNTIME_STRUCTURES.jvmMake [constructor, in RuntimeStructures]
RUNTIME_STRUCTURES.threadGetCallStack [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.threadGetEvalState [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.threadGetId [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.TThread [record, in RuntimeStructures]
RUNTIME_STRUCTURES.threadMake [constructor, in RuntimeStructures]
RUNTIME_STRUCTURES.TEvalState [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.TRichFrame [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.cmSignature [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.cmDeclClass [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.cmCtxObjectLoc [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.cmCurrentClass [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.cmQName [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.TCurrentMethod [record, in RuntimeStructures]
RUNTIME_STRUCTURES.cmMake [constructor, in RuntimeStructures]
RUNTIME_STRUCTURES.PframeKConcretisationAbstraction [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.frameKConcretisation [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.frameKAbstraction [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.frameKShadowGetPC [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.frameKShadowGetLocalStack [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.frameKShadowGetVars [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.TFrameKShadow [record, in RuntimeStructures]
RUNTIME_STRUCTURES.frameKShadowMake [constructor, in RuntimeStructures]
RUNTIME_STRUCTURES.frameGetPC [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.frameGetLocalStack [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.frameGetVars [projection, in RuntimeStructures]
RUNTIME_STRUCTURES.TFrame [record, in RuntimeStructures]
RUNTIME_STRUCTURES.frameMake [constructor, in RuntimeStructures]
RUNTIME_STRUCTURES.PlocalStackKConcretisationAbstraction [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.localStackKConcretisation [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.localStackKAbstraction [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKConcretisationAbstraction [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKConcretisationConsistentSome [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKConcretisationConsistent [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKAbstractionConsistentSet [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKAbstractionConsistentSome [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKAbstractionConsistent [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.varsKConcretisation [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.varsKAbstraction [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.TLocalStackTShadow [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.TVarsTShadow [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.TLocalStackKShadow [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.TVarsKShadow [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.TLocalStack [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.TVars [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.TLocalStackGeneric [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.GenericStackDefinition.t [variable, in RuntimeStructures]
RUNTIME_STRUCTURES.GenericStackDefinition [section, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsSetSameEquiv [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsEqEquiv [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsSetGetOther [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsSetGet [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsEmptyGet [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.VarsProperties.v [variable, in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.VarsProperties.y [variable, in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.VarsProperties.x [variable, in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.VarsProperties.vars [variable, in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.VarsProperties [section, in RuntimeStructures]
RUNTIME_STRUCTURES.varsEquiv [definition, in RuntimeStructures]
RUNTIME_STRUCTURES.varsSet [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.varsGet [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.varsEmpty [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.t [variable, in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition [section, in RuntimeStructures]
RUNTIME_STRUCTURES.TVarsGeneric [axiom, in RuntimeStructures]
RUNTIME_STRUCTURES.M_Heap [module, in RuntimeStructures]
RUNTIME_STRUCTURES [module, in RuntimeStructures]

S

SCOND [module, in Loop_Assertions]
SCOND [module, in Loop]
SEM [module, in IAdd]
SEMANTICS [module, in Semantics]
Semantics [library]
SEMANTICS.M_Sem_Call [module, in Semantics]
SEMANTICS.M_Sem_Heap [module, in Semantics]
SEMANTICS.M_Sem_Monitor [module, in Semantics]
SEMANTICS.M_Sem_Frame [module, in Semantics]
SEMANTICS.M_AllStructures [module, in Semantics]
SEMANTICS.oneThreadAndHeapChanged [inductive, in Semantics]
SEMANTICS.OneThreadAndHeapChanged_onlyone [constructor, in Semantics]
SEMANTICS.OneThreadAndHeapChanged_other [constructor, in Semantics]
SEMANTICS.OneThreadAndHeapChanged_this [constructor, in Semantics]
SEMANTICS.oneThreadAndHeapChanged1 [inductive, in Semantics]
SEMANTICS.oneThreadChanged [inductive, in Semantics]
SEMANTICS.OneThreadChanged_other [constructor, in Semantics]
SEMANTICS.OneThreadChanged_this [constructor, in Semantics]
SEMANTICS.oneThreadChanged1 [inductive, in Semantics]
SEMANTICS.OneThreadChanged1_onlyone [constructor, in Semantics]
SEMANTICS.oneThreadSelected [lemma, in Semantics]
SEMANTICS.oneThreadSelectedAlways [lemma, in Semantics]
SEMANTICS.PoneThreadAndHeapChanged_1thread_inv [lemma, in Semantics]
SEMANTICS.PoneThreadAndHeapChanged_1thread [lemma, in Semantics]
SEMANTICS.PoneThreadChanged_1thread_inv [lemma, in Semantics]
SEMANTICS.PoneThreadChanged_1thread [lemma, in Semantics]
SEMANTICS.selectedThread [inductive, in Semantics]
SEMANTICS.selectedThread_onlyone [constructor, in Semantics]
SEMANTICS.SelectedThread_other [constructor, in Semantics]
SEMANTICS.SelectedThread_this [constructor, in Semantics]
SEMANTICS.selectedThread1 [inductive, in Semantics]
SEMANTICS.semInstr [inductive, in Semantics]
SEMANTICS.SemInstr_athrow_null [constructor, in Semantics]
SEMANTICS.SemInstr_athrow [constructor, in Semantics]
SEMANTICS.SemInstr_return_exn [constructor, in Semantics]
SEMANTICS.SemInstr_return [constructor, in Semantics]
SEMANTICS.SemInstr_invoke_exn [constructor, in Semantics]
SEMANTICS.SemInstr_invoke [constructor, in Semantics]
SEMANTICS.SemInstr_heap_exn [constructor, in Semantics]
SEMANTICS.SemInstr_heap [constructor, in Semantics]
SEMANTICS.SemInstr_frame_exn [constructor, in Semantics]
SEMANTICS.SemInstr_frame [constructor, in Semantics]
SEMANTICS.semThrow [inductive, in Semantics]
SEMANTICS.SemThrow_null [constructor, in Semantics]
SEMANTICS.SemThrow_ok [constructor, in Semantics]
SEMANTICS.step [inductive, in Semantics]
SEMANTICS.stepInThread [inductive, in Semantics]
SEMANTICS.StepInThread_uncaught_exn [constructor, in Semantics]
SEMANTICS.StepInThread_uncaught [constructor, in Semantics]
SEMANTICS.StepInThread_caught [constructor, in Semantics]
SEMANTICS.StepInThread_instruction_exn [constructor, in Semantics]
SEMANTICS.StepInThread_instruction_ok [constructor, in Semantics]
SEMANTICS.steps [definition, in Semantics]
SEMANTICS.Step_thread [constructor, in Semantics]
semInstr_2_3_impl [lemma, in IAdd]
semInstr_1_2_impl [lemma, in IAdd]
semInstr_0_1_impl [lemma, in IAdd]
semInstr_2_3 [lemma, in IAdd]
semInstr_1_2 [lemma, in IAdd]
semInstr_0_1 [lemma, in IAdd]
SEM_VAR.PSemVarInversion_store_1 [lemma, in Sem_Var]
SEM_VAR.PSemVarInversion_load_1 [lemma, in Sem_Var]
SEM_VAR.staticSemVarComplete [lemma, in Sem_Var]
SEM_VAR.staticSemVarConsistent [lemma, in Sem_Var]
SEM_VAR.PvarsKAbstractionSetSame [lemma, in Sem_Var]
SEM_VAR.PVarsSetSame [axiom, in Sem_Var]
SEM_VAR.StaticSemVar_iinc [constructor, in Sem_Var]
SEM_VAR.StaticSemVar_store_2 [constructor, in Sem_Var]
SEM_VAR.StaticSemVar_store_1 [constructor, in Sem_Var]
SEM_VAR.StaticSemVar_load_2 [constructor, in Sem_Var]
SEM_VAR.StaticSemVar_load_1 [constructor, in Sem_Var]
SEM_VAR.staticSemVar [inductive, in Sem_Var]
SEM_VAR.SemVar_iinc [constructor, in Sem_Var]
SEM_VAR.SemVar_store_2 [constructor, in Sem_Var]
SEM_VAR.SemVar_store_1 [constructor, in Sem_Var]
SEM_VAR.SemVar_load_2 [constructor, in Sem_Var]
SEM_VAR.SemVar_load_1 [constructor, in Sem_Var]
SEM_VAR.semVar [inductive, in Sem_Var]
SEM_VAR.IsStorable_Double [constructor, in Sem_Var]
SEM_VAR.IsStorable_Long [constructor, in Sem_Var]
SEM_VAR.IsStorable_Float [constructor, in Sem_Var]
SEM_VAR.IsStorable_Int [constructor, in Sem_Var]
SEM_VAR.IsStorable_Addr [constructor, in Sem_Var]
SEM_VAR.IsStorable_Ref [constructor, in Sem_Var]
SEM_VAR.isStorable [inductive, in Sem_Var]
SEM_VAR.IsLoadable_Double [constructor, in Sem_Var]
SEM_VAR.IsLoadable_Long [constructor, in Sem_Var]
SEM_VAR.IsLoadable_Float [constructor, in Sem_Var]
SEM_VAR.IsLoadable_Int [constructor, in Sem_Var]
SEM_VAR.IsLoadable_Ref [constructor, in Sem_Var]
SEM_VAR.isLoadable [inductive, in Sem_Var]
SEM_VAR.M_AllStructures [module, in Sem_Var]
SEM_VAR [module, in Sem_Var]
SEM_HEAP.SemHeap_monitor [constructor, in Sem_Heap]
SEM_HEAP.SemHeap_new [constructor, in Sem_Heap]
SEM_HEAP.SemHeap_put [constructor, in Sem_Heap]
SEM_HEAP.SemHeap_get [constructor, in Sem_Heap]
SEM_HEAP.semHeap [inductive, in Sem_Heap]
SEM_HEAP.SemNew_multiarray_negativeSize [constructor, in Sem_Heap]
SEM_HEAP.SemNew_multiarray [constructor, in Sem_Heap]
SEM_HEAP.SemNew_refarray_neg [constructor, in Sem_Heap]
SEM_HEAP.SemNew_refarray [constructor, in Sem_Heap]
SEM_HEAP.SemNew_array_neg [constructor, in Sem_Heap]
SEM_HEAP.SemNew_array [constructor, in Sem_Heap]
SEM_HEAP.SemNew_object [constructor, in Sem_Heap]
SEM_HEAP.semNew [inductive, in Sem_Heap]
SEM_HEAP.PmakeMultiArray [axiom, in Sem_Heap]
SEM_HEAP.MadeMultiArray_end [constructor, in Sem_Heap]
SEM_HEAP.MadeMultiArray_step [constructor, in Sem_Heap]
SEM_HEAP.madeMultiArrayInd [inductive, in Sem_Heap]
SEM_HEAP.makeMultiArray [axiom, in Sem_Heap]
SEM_HEAP.SemPut_array_indexOutOfBounds [constructor, in Sem_Heap]
SEM_HEAP.SemPut_array_null [constructor, in Sem_Heap]
SEM_HEAP.SemPut_array [constructor, in Sem_Heap]
SEM_HEAP.SemPut_putfield_null [constructor, in Sem_Heap]
SEM_HEAP.SemPut_putfield [constructor, in Sem_Heap]
SEM_HEAP.SemPut_putstatic [constructor, in Sem_Heap]
SEM_HEAP.semPut [inductive, in Sem_Heap]
SEM_HEAP.SemGet_checkCast_null [constructor, in Sem_Heap]
SEM_HEAP.SemGet_checkCast_false [constructor, in Sem_Heap]
SEM_HEAP.SemGet_checkCast_true [constructor, in Sem_Heap]
SEM_HEAP.SemGet_instanceOf_null [constructor, in Sem_Heap]
SEM_HEAP.SemGet_instanceOf_false [constructor, in Sem_Heap]
SEM_HEAP.SemGet_instanceOf_true [constructor, in Sem_Heap]
SEM_HEAP.SemGet_arrayLength_null [constructor, in Sem_Heap]
SEM_HEAP.SemGet_arrayLength [constructor, in Sem_Heap]
SEM_HEAP.SemGet_array_out [constructor, in Sem_Heap]
SEM_HEAP.SemGet_array_null [constructor, in Sem_Heap]
SEM_HEAP.SemGet_array [constructor, in Sem_Heap]
SEM_HEAP.SemGet_getfield_null [constructor, in Sem_Heap]
SEM_HEAP.SemGet_getfield [constructor, in Sem_Heap]
SEM_HEAP.SemGet_getstatic [constructor, in Sem_Heap]
SEM_HEAP.semGet [inductive, in Sem_Heap]
SEM_HEAP.M_Sem_Monitor [module, in Sem_Heap]
SEM_HEAP.M_AllStructures [module, in Sem_Heap]
SEM_HEAP [module, in Sem_Heap]
SEM_STACKOP.staticSemStackComplete [lemma, in Sem_Stackop]
SEM_STACKOP.PmapPattern [lemma, in Sem_Stackop]
SEM_STACKOP.staticSemStackConsistent [lemma, in Sem_Stackop]
SEM_STACKOP.StaticSemStack_CastOp [constructor, in Sem_Stackop]
SEM_STACKOP.StaticSemStack_Cmpi [constructor, in Sem_Stackop]
SEM_STACKOP.StaticSemStack_BinOp_Exn [constructor, in Sem_Stackop]
SEM_STACKOP.StaticSemStack_BinOp [constructor, in Sem_Stackop]
SEM_STACKOP.StaticSemStack_UnOp [constructor, in Sem_Stackop]
SEM_STACKOP.StaticSemStack_Const [constructor, in Sem_Stackop]
SEM_STACKOP.StaticSemStack_Generic [constructor, in Sem_Stackop]
SEM_STACKOP.staticSemStack [inductive, in Sem_Stackop]
SEM_STACKOP.PstaticSemStackCastOp [lemma, in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_d [constructor, in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_f [constructor, in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_l [constructor, in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_i [constructor, in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_s [constructor, in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_c [constructor, in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_b [constructor, in Sem_Stackop]
SEM_STACKOP.staticSemStackCastOp [inductive, in Sem_Stackop]
SEM_STACKOP.PstaticSemStackCmpi [lemma, in Sem_Stackop]
SEM_STACKOP.CmpiStaticSem_cmpg [constructor, in Sem_Stackop]
SEM_STACKOP.CmpiStaticSem_cmpl [constructor, in Sem_Stackop]
SEM_STACKOP.staticSemStackCmpi [inductive, in Sem_Stackop]
SEM_STACKOP.PstaticSemStackBinOp_NoResult [lemma, in Sem_Stackop]
SEM_STACKOP.PstaticSemStackBinOp [lemma, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSemNoResult_rem [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSemNoResult_div [constructor, in Sem_Stackop]
SEM_STACKOP.staticSemStackBinOp_NoResult [inductive, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_ushr [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_shr [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_shl [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_or [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_and [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_xor [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_rem [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_div [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_mul [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_sub [constructor, in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_add [constructor, in Sem_Stackop]
SEM_STACKOP.staticSemStackBinOp [inductive, in Sem_Stackop]
SEM_STACKOP.PstaticSemStackUnOp [lemma, in Sem_Stackop]
SEM_STACKOP.UnOpStaticSem_add [constructor, in Sem_Stackop]
SEM_STACKOP.staticSemStackUnOp [inductive, in Sem_Stackop]
SEM_STACKOP.SemStack_Cast [constructor, in Sem_Stackop]
SEM_STACKOP.SemStack_Cmpi [constructor, in Sem_Stackop]
SEM_STACKOP.SemStack_BinOp_ArithmeticException [constructor, in Sem_Stackop]
SEM_STACKOP.SemStack_BinOp [constructor, in Sem_Stackop]
SEM_STACKOP.SemStack_UnOp [constructor, in Sem_Stackop]
SEM_STACKOP.SemStack_Const [constructor, in Sem_Stackop]
SEM_STACKOP.SemStack_Generic [constructor, in Sem_Stackop]
SEM_STACKOP.semStack [inductive, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_swap [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_pop2_form2 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_pop2_form1 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_pop [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x2_form4 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x2_form3 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x2_form2 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x2_form1 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x1_form2 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x1_form1 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_form2 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_form1 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup_x2_form2 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup_x2_form1 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup_x1 [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup [constructor, in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_nop [constructor, in Sem_Stackop]
SEM_STACKOP.semStackGeneric [inductive, in Sem_Stackop]
SEM_STACKOP.GenericOps [section, in Sem_Stackop]
SEM_STACKOP.M_AllStructures [module, in Sem_Stackop]
SEM_STACKOP [module, in Sem_Stackop]
SEM_CALL.SemReturnValue [constructor, in Sem_Call]
SEM_CALL.SemReturnVoid [constructor, in Sem_Call]
SEM_CALL.semReturn [inductive, in Sem_Call]
SEM_CALL.MU_NotSychnronized [constructor, in Sem_Call]
SEM_CALL.MU_Synchronized [constructor, in Sem_Call]
SEM_CALL.maybeUnlock [inductive, in Sem_Call]
SEM_CALL.SemInvokeSpecial [constructor, in Sem_Call]
SEM_CALL.SemInvokeInterface [constructor, in Sem_Call]
SEM_CALL.SemInvokeVirtual [constructor, in Sem_Call]
SEM_CALL.SemInvokeStatic [constructor, in Sem_Call]
SEM_CALL.semInvoke [inductive, in Sem_Call]
SEM_CALL.CallInstance_notFound [constructor, in Sem_Call]
SEM_CALL.CallInstance_null [constructor, in Sem_Call]
SEM_CALL.CallInstance_ok [constructor, in Sem_Call]
SEM_CALL.callInstanceMethod [inductive, in Sem_Call]
SEM_CALL.CallStatic_ok [constructor, in Sem_Call]
SEM_CALL.callStaticMethod [inductive, in Sem_Call]
SEM_CALL.ML_NotSychnronized [constructor, in Sem_Call]
SEM_CALL.ML_Synchronized [constructor, in Sem_Call]
SEM_CALL.maybeLock [inductive, in Sem_Call]
SEM_CALL.InvokeSpecial_Virtual [constructor, in Sem_Call]
SEM_CALL.InvokeSpecial_Direct [constructor, in Sem_Call]
SEM_CALL.invokeSpecialMode [inductive, in Sem_Call]
SEM_CALL.GetMethod_virtual [constructor, in Sem_Call]
SEM_CALL.GetMethod_direct [constructor, in Sem_Call]
SEM_CALL.getMethodToCall [inductive, in Sem_Call]
SEM_CALL.MLM_Virtual [constructor, in Sem_Call]
SEM_CALL.MLM_Direct [constructor, in Sem_Call]
SEM_CALL.TMethodLookupMode [inductive, in Sem_Call]
SEM_CALL.PlookupMethod_eqv_lookupMethodInd [lemma, in Sem_Call]
SEM_CALL.LookupMethod_fail [constructor, in Sem_Call]
SEM_CALL.LookupMethod_step [constructor, in Sem_Call]
SEM_CALL.LookupMethod_found [constructor, in Sem_Call]
SEM_CALL.lookupMethodInd [inductive, in Sem_Call]
SEM_CALL.initFrame [definition, in Sem_Call]
SEM_CALL.M_Sem_Monitor [module, in Sem_Call]
SEM_CALL.M_AllStructures [module, in Sem_Call]
SEM_CALL [module, in Sem_Call]
SEM_MONITOR.SemMonitor_null [constructor, in Sem_Monitor]
SEM_MONITOR.SemMonitor_unlock_badThd [constructor, in Sem_Monitor]
SEM_MONITOR.SemMonitor_unlock [constructor, in Sem_Monitor]
SEM_MONITOR.SemMonitor_lock [constructor, in Sem_Monitor]
SEM_MONITOR.semMonitor [inductive, in Sem_Monitor]
SEM_MONITOR.M_AllStructures [module, in Sem_Monitor]
SEM_MONITOR [module, in Sem_Monitor]
SEM_FRAME.stepsFrame [definition, in Sem_Frame]
SEM_FRAME.StepFrame_one [constructor, in Sem_Frame]
SEM_FRAME.stepFrame [inductive, in Sem_Frame]
SEM_FRAME.staticSemFrameComplete [lemma, in Sem_Frame]
SEM_FRAME.staticSemFrameConsistent [lemma, in Sem_Frame]
SEM_FRAME.StaticSemFrame_ret [constructor, in Sem_Frame]
SEM_FRAME.StaticSemFrame_jsr [constructor, in Sem_Frame]
SEM_FRAME.StaticSemFrame_cond [constructor, in Sem_Frame]
SEM_FRAME.StaticSemFrame_var [constructor, in Sem_Frame]
SEM_FRAME.StaticSemFrame_stackop_exn [constructor, in Sem_Frame]
SEM_FRAME.StaticSemFrame_stackop [constructor, in Sem_Frame]
SEM_FRAME.staticSemFrame [inductive, in Sem_Frame]
SEM_FRAME.SemFrame_ret [constructor, in Sem_Frame]
SEM_FRAME.SemFrame_jsr [constructor, in Sem_Frame]
SEM_FRAME.SemFrame_cond [constructor, in Sem_Frame]
SEM_FRAME.SemFrame_var [constructor, in Sem_Frame]
SEM_FRAME.SemFrame_stackop_exn [constructor, in Sem_Frame]
SEM_FRAME.SemFrame_stackop [constructor, in Sem_Frame]
SEM_FRAME.semFrame [inductive, in Sem_Frame]
SEM_FRAME.calculatePC [definition, in Sem_Frame]
SEM_FRAME.M_Sem_Cond [module, in Sem_Frame]
SEM_FRAME.M_Sem_Var [module, in Sem_Frame]
SEM_FRAME.M_Sem_Stackop [module, in Sem_Frame]
SEM_FRAME.M_AllStructures [module, in Sem_Frame]
SEM_FRAME [module, in Sem_Frame]
SEM_COND.staticSemCondComplete [lemma, in Sem_Cond]
SEM_COND.staticSemCondConsistent [lemma, in Sem_Cond]
SEM_COND.StaticSemCond_lookupswitch_default [constructor, in Sem_Cond]
SEM_COND.StaticSemCond_lookupswitch_found [constructor, in Sem_Cond]
SEM_COND.StaticSemCond_tableswitch_default [constructor, in Sem_Cond]
SEM_COND.StaticSemCond_tableswitch_found [constructor, in Sem_Cond]
SEM_COND.StaticSemCond_cmp_false [constructor, in Sem_Cond]
SEM_COND.StaticSemCond_cmp_true [constructor, in Sem_Cond]
SEM_COND.StaticSemCond_if_false [constructor, in Sem_Cond]
SEM_COND.StaticSemCond_if_true [constructor, in Sem_Cond]
SEM_COND.StaticSemCond_goto [constructor, in Sem_Cond]
SEM_COND.staticSemCond [inductive, in Sem_Cond]
SEM_COND.PstaticSemCondCmp [lemma, in Sem_Cond]
SEM_COND.CmpStaticSem_Gt [constructor, in Sem_Cond]
SEM_COND.CmpStaticSem_Ge [constructor, in Sem_Cond]
SEM_COND.CmpStaticSem_Lt [constructor, in Sem_Cond]
SEM_COND.CmpStaticSem_Le [constructor, in Sem_Cond]
SEM_COND.CmpStaticSem_Ne [constructor, in Sem_Cond]
SEM_COND.CmpStaticSem_Eq [constructor, in Sem_Cond]
SEM_COND.staticSemCondCmp [inductive, in Sem_Cond]
SEM_COND.PstaticSemCondIf [lemma, in Sem_Cond]
SEM_COND.IfStaticSem_Gt [constructor, in Sem_Cond]
SEM_COND.IfStaticSem_Ge [constructor, in Sem_Cond]
SEM_COND.IfStaticSem_Lt [constructor, in Sem_Cond]
SEM_COND.IfStaticSem_Le [constructor, in Sem_Cond]
SEM_COND.IfStaticSem_Ne [constructor, in Sem_Cond]
SEM_COND.IfStaticSem_Eq [constructor, in Sem_Cond]
SEM_COND.staticSemCondIf [inductive, in Sem_Cond]
SEM_COND.SemCond_lookupswitch_default [constructor, in Sem_Cond]
SEM_COND.SemCond_lookupswitch_found [constructor, in Sem_Cond]
SEM_COND.SemCond_tableswitch_default [constructor, in Sem_Cond]
SEM_COND.SemCond_tableswitch_found [constructor, in Sem_Cond]
SEM_COND.SemCond_cmp_false [constructor, in Sem_Cond]
SEM_COND.SemCond_cmp_true [constructor, in Sem_Cond]
SEM_COND.SemCond_if_false [constructor, in Sem_Cond]
SEM_COND.SemCond_if_true [constructor, in Sem_Cond]
SEM_COND.SemCond_goto [constructor, in Sem_Cond]
SEM_COND.semCond [inductive, in Sem_Cond]
SEM_COND.intArith [variable, in Sem_Cond]
SEM_COND.M_IntNumProperties [module, in Sem_Cond]
SEM_COND.M_AllStructures [module, in Sem_Cond]
SEM_COND [module, in Sem_Cond]
Sem_Monitor [library]
Sem_Call [library]
Sem_Frame [library]
Sem_Heap [library]
Sem_Cond [library]
Sem_Stackop [library]
Sem_Var [library]
SF [module, in Loop_Assertions]
SF [module, in Loop]
SF [module, in IAdd]
singles [lemma, in Loop_Assertions]
sk0 [definition, in Loop_Assertions]
sk0 [definition, in Loop]
small_4 [lemma, in IAdd]
small_2 [lemma, in IAdd]
specification [definition, in Loop_Assertions]
SSOP [module, in Loop_Assertions]
SSOP [module, in Loop]
SSOP [module, in IAdd]
stackop_dup_inversion [lemma, in IAdd]
stackop_binop_inversion [lemma, in IAdd]
stackop_2_3_impl_gen [lemma, in IAdd]
stackop_2_3_impl [lemma, in IAdd]
stackop_1_2_impl [lemma, in IAdd]
stackop_0_1_impl [lemma, in IAdd]
stackop_2_3 [lemma, in IAdd]
stackop_1_2 [lemma, in IAdd]
stackop_0_1 [lemma, in IAdd]
stack_value_from_var [lemma, in Loop_Assertions]
stack_values_other_fields [lemma, in Loop_Assertions]
stack_values [definition, in Loop_Assertions]
stack_values_cons [constructor, in Loop_Assertions]
stack_values_nil [constructor, in Loop_Assertions]
stack_values_ind [inductive, in Loop_Assertions]
stack_value_from_var [lemma, in Loop]
stack_values_other_fields [lemma, in Loop]
stack_values [definition, in Loop]
stack_values_cons [constructor, in Loop]
stack_values_nil [constructor, in Loop]
stack_values_ind [inductive, in Loop]
start_0 [lemma, in Loop_Assertions]
start_0 [lemma, in Loop]
stepFrame_3_impossible [lemma, in IAdd]
stepFrame_2_3_impl [lemma, in IAdd]
stepFrame_1_2_impl [lemma, in IAdd]
stepFrame_0_1_impl [lemma, in IAdd]
stepFrame_2_3 [lemma, in IAdd]
stepFrame_1_2 [lemma, in IAdd]
stepFrame_0_1 [lemma, in IAdd]
StepsConcrete [lemma, in IAdd]
StepsFrameConcrete [lemma, in IAdd]
StepsFrameImpl [lemma, in IAdd]
stepThread_3_impossible [lemma, in IAdd]
stepThread_2_3_impl [lemma, in IAdd]
stepThread_1_2_impl [lemma, in IAdd]
stepThread_0_1_impl [lemma, in IAdd]
stepThread_2_3 [lemma, in IAdd]
stepThread_1_2 [lemma, in IAdd]
stepThread_0_1 [lemma, in IAdd]
step_3_impossible [lemma, in IAdd]
step_2_3_impl [lemma, in IAdd]
step_1_2_impl [lemma, in IAdd]
step_0_1_impl [lemma, in IAdd]
step_2_3 [lemma, in IAdd]
step_1_2 [lemma, in IAdd]
step_0_1 [lemma, in IAdd]
SVAR [module, in Loop_Assertions]
SVAR [module, in Loop]
s0_prop [definition, in Loop_Assertions]
s0_prop [definition, in Loop]
s1_prop [definition, in Loop_Assertions]
s1_prop [definition, in Loop]
s10_prop [definition, in Loop_Assertions]
s10_prop [definition, in Loop]
s11_prop [definition, in Loop_Assertions]
s11_prop [definition, in Loop]
s12_prop [definition, in Loop_Assertions]
s12_prop [definition, in Loop]
s13_prop [definition, in Loop_Assertions]
s13_prop [definition, in Loop]
s14_prop [definition, in Loop_Assertions]
s14_prop [definition, in Loop]
s15_prop [definition, in Loop_Assertions]
s15_prop [definition, in Loop]
s16_prop [definition, in Loop_Assertions]
s16_prop [definition, in Loop]
s17_prop [definition, in Loop_Assertions]
s17_prop [definition, in Loop]
s18_post_prop [definition, in Loop_Assertions]
s18_prop [definition, in Loop_Assertions]
s18_post_prop [definition, in Loop]
s18_prop [definition, in Loop]
s19_prop [definition, in Loop_Assertions]
s19_prop [definition, in Loop]
s2_prop [definition, in Loop_Assertions]
s2_prop [definition, in Loop]
s20 [lemma, in Loop_Assertions]
s20 [lemma, in Loop]
s20_prop [definition, in Loop_Assertions]
s20_prop [definition, in Loop]
s3_prop [definition, in Loop_Assertions]
s3_prop [definition, in Loop]
s4_prop [definition, in Loop_Assertions]
s4_prop [definition, in Loop]
s5_post_prop [definition, in Loop_Assertions]
s5_prop [definition, in Loop_Assertions]
s5_post_prop [definition, in Loop]
s5_prop [definition, in Loop]
s6_prop [definition, in Loop_Assertions]
s6_prop [definition, in Loop]
s7_prop [definition, in Loop_Assertions]
s7_prop [definition, in Loop]
s8_post_prop [definition, in Loop_Assertions]
s8_prop [definition, in Loop_Assertions]
s8_post_prop [definition, in Loop]
s8_prop [definition, in Loop]
s9_prop [definition, in Loop_Assertions]
s9_prop [definition, in Loop]

T

thid0 [axiom, in IAdd]
ThisMethod [axiom, in IAdd]
ThisMethodCM [lemma, in IAdd]
thread0_ok [lemma, in IAdd]
thread1_ok [lemma, in IAdd]
thread2_ok [lemma, in IAdd]
thread3_ok [lemma, in IAdd]
thstate0 [definition, in IAdd]
thstate0_props [definition, in IAdd]
thstate1 [definition, in IAdd]
thstate1_props [definition, in IAdd]
thstate2 [definition, in IAdd]
thstate2_props [definition, in IAdd]
thstate3 [definition, in IAdd]
thstate3_props [definition, in IAdd]
TOneOrTwo [inductive, in Common]
toZ2 [lemma, in IAdd]
toZ4 [lemma, in IAdd]
trans_19_20 [lemma, in Loop_Assertions]
trans_18_6 [lemma, in Loop_Assertions]
trans_17_18 [lemma, in Loop_Assertions]
trans_16_17 [lemma, in Loop_Assertions]
trans_15_16 [lemma, in Loop_Assertions]
trans_14_15 [lemma, in Loop_Assertions]
trans_13_14 [lemma, in Loop_Assertions]
trans_12_13 [lemma, in Loop_Assertions]
trans_11_12 [lemma, in Loop_Assertions]
trans_10_11 [lemma, in Loop_Assertions]
trans_9_10 [lemma, in Loop_Assertions]
trans_8_post8 [lemma, in Loop_Assertions]
trans_7_8 [lemma, in Loop_Assertions]
trans_6_7 [lemma, in Loop_Assertions]
trans_5_post [lemma, in Loop_Assertions]
trans_4_5 [lemma, in Loop_Assertions]
trans_3_4 [lemma, in Loop_Assertions]
trans_2_3 [lemma, in Loop_Assertions]
trans_1_2 [lemma, in Loop_Assertions]
trans_0_1 [lemma, in Loop_Assertions]
trans_19_20 [lemma, in Loop]
trans_18_6 [lemma, in Loop]
trans_17_18 [lemma, in Loop]
trans_16_17 [lemma, in Loop]
trans_15_16 [lemma, in Loop]
trans_14_15 [lemma, in Loop]
trans_13_14 [lemma, in Loop]
trans_12_13 [lemma, in Loop]
trans_11_12 [lemma, in Loop]
trans_10_11 [lemma, in Loop]
trans_9_10 [lemma, in Loop]
trans_8_post8 [lemma, in Loop]
trans_7_8 [lemma, in Loop]
trans_6_7 [lemma, in Loop]
trans_5_post [lemma, in Loop]
trans_4_5 [lemma, in Loop]
trans_3_4 [lemma, in Loop]
trans_2_3 [lemma, in Loop]
trans_1_2 [lemma, in Loop]
trans_0_1 [lemma, in Loop]
Two [constructor, in Common]

V

v [variable, in Instructions]
ValuesNTypes [library]
VALUES_AND_TYPES.sizeOfTypes [definition, in ValuesNTypes]
VALUES_AND_TYPES.sizeOfType [definition, in ValuesNTypes]
VALUES_AND_TYPES.sizeOfValues [definition, in ValuesNTypes]
VALUES_AND_TYPES.sizeOfValue [definition, in ValuesNTypes]
VALUES_AND_TYPES.PsizeOfKindCat2 [lemma, in ValuesNTypes]
VALUES_AND_TYPES.PsizeOfKindCat1 [lemma, in ValuesNTypes]
VALUES_AND_TYPES.sizeOfKind [definition, in ValuesNTypes]
VALUES_AND_TYPES.IsCatVIK_Double [constructor, in ValuesNTypes]
VALUES_AND_TYPES.IsCatVIK_Long [constructor, in ValuesNTypes]
VALUES_AND_TYPES.IsCatVIK_Float [constructor, in ValuesNTypes]
VALUES_AND_TYPES.IsCatVIK_Int [constructor, in ValuesNTypes]
VALUES_AND_TYPES.IsCatVIK_Ref [constructor, in ValuesNTypes]
VALUES_AND_TYPES.isCatVIK [inductive, in ValuesNTypes]
VALUES_AND_TYPES.PisCatOK [lemma, in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Double [constructor, in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Long [constructor, in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Float [constructor, in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Int [constructor, in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Addr [constructor, in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Ref [constructor, in ValuesNTypes]
VALUES_AND_TYPES.isCat [inductive, in ValuesNTypes]
VALUES_AND_TYPES.catOfKind [definition, in ValuesNTypes]
VALUES_AND_TYPES.sizeOfCat [definition, in ValuesNTypes]
VALUES_AND_TYPES.cat2 [constructor, in ValuesNTypes]
VALUES_AND_TYPES.cat1 [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TValueCategory [inductive, in ValuesNTypes]
VALUES_AND_TYPES.PtransformAFromValueKindConsistent [lemma, in ValuesNTypes]
VALUES_AND_TYPES.PtransformAToValueKindConsistent [lemma, in ValuesNTypes]
VALUES_AND_TYPES.kindOfArrayKind [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformAFromValue [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformVADouble [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformVALong [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformVAFloat [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformVAInt [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformVAShort [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformVABool [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformVAByte [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformVAChar [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformVARef [definition, in ValuesNTypes]
VALUES_AND_TYPES.transformAToValue [definition, in ValuesNTypes]
VALUES_AND_TYPES.PValVarMappingConsistentInv_EVal_EVar [lemma, in ValuesNTypes]
VALUES_AND_TYPES.PValVarMappingConsistentInv_AVar_EVal [lemma, in ValuesNTypes]
VALUES_AND_TYPES.PValVarMappingConsistentInv_AVal_EVar [lemma, in ValuesNTypes]
VALUES_AND_TYPES.PValVarMappingConsistent [lemma, in ValuesNTypes]
VALUES_AND_TYPES.PtransformValToVarValConsistent [lemma, in ValuesNTypes]
VALUES_AND_TYPES.PvalVarKindMapping_transform_equiv [lemma, in ValuesNTypes]
VALUES_AND_TYPES.transformKToVarK [definition, in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Double [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Long [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Float [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Int [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Addr [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Ref [constructor, in ValuesNTypes]
VALUES_AND_TYPES.ValVarKindMapping [inductive, in ValuesNTypes]
VALUES_AND_TYPES.PvalVarMapping_transform_equiv [lemma, in ValuesNTypes]
VALUES_AND_TYPES.transformValToVar [definition, in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Double [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Long [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Float [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Int [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Addr [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Ref [constructor, in ValuesNTypes]
VALUES_AND_TYPES.ValVarMapping [inductive, in ValuesNTypes]
VALUES_AND_TYPES.int2double [definition, in ValuesNTypes]
VALUES_AND_TYPES.int2float [definition, in ValuesNTypes]
VALUES_AND_TYPES.long2float [definition, in ValuesNTypes]
VALUES_AND_TYPES.long2double [definition, in ValuesNTypes]
VALUES_AND_TYPES.double2int [definition, in ValuesNTypes]
VALUES_AND_TYPES.double2long [definition, in ValuesNTypes]
VALUES_AND_TYPES.double2float [definition, in ValuesNTypes]
VALUES_AND_TYPES.float2long [definition, in ValuesNTypes]
VALUES_AND_TYPES.float2int [definition, in ValuesNTypes]
VALUES_AND_TYPES.float2double [definition, in ValuesNTypes]
VALUES_AND_TYPES.long2int [definition, in ValuesNTypes]
VALUES_AND_TYPES.int2long [definition, in ValuesNTypes]
VALUES_AND_TYPES.int2ichar [definition, in ValuesNTypes]
VALUES_AND_TYPES.int2char [definition, in ValuesNTypes]
VALUES_AND_TYPES.char2int [definition, in ValuesNTypes]
VALUES_AND_TYPES.int2ishort [definition, in ValuesNTypes]
VALUES_AND_TYPES.int2short [definition, in ValuesNTypes]
VALUES_AND_TYPES.short2int [definition, in ValuesNTypes]
VALUES_AND_TYPES.int2bool [definition, in ValuesNTypes]
VALUES_AND_TYPES.bool2int [definition, in ValuesNTypes]
VALUES_AND_TYPES.int2ibyte [definition, in ValuesNTypes]
VALUES_AND_TYPES.int2byte [definition, in ValuesNTypes]
VALUES_AND_TYPES.byte2int [definition, in ValuesNTypes]
VALUES_AND_TYPES.NumericConversions [section, in ValuesNTypes]
VALUES_AND_TYPES.defaultArrayValueForType [definition, in ValuesNTypes]
VALUES_AND_TYPES.PdefaultValueForType_ForKind_Consistent [lemma, in ValuesNTypes]
VALUES_AND_TYPES.defaultValueForType [definition, in ValuesNTypes]
VALUES_AND_TYPES.PForEachKindListExistsValueList [lemma, in ValuesNTypes]
VALUES_AND_TYPES.PForEachKindExistsAValue [lemma, in ValuesNTypes]
VALUES_AND_TYPES.PdefaultForKindConsistent [lemma, in ValuesNTypes]
VALUES_AND_TYPES.PexampleForKindConsistent [lemma, in ValuesNTypes]
VALUES_AND_TYPES.defaultForKind [definition, in ValuesNTypes]
VALUES_AND_TYPES.exampleForKind [definition, in ValuesNTypes]
VALUES_AND_TYPES.arrayKindOfType [definition, in ValuesNTypes]
VALUES_AND_TYPES.kindOfTypes [definition, in ValuesNTypes]
VALUES_AND_TYPES.kindOfType [definition, in ValuesNTypes]
VALUES_AND_TYPES.kindOfAValue [definition, in ValuesNTypes]
VALUES_AND_TYPES.kindOfVarValue [definition, in ValuesNTypes]
VALUES_AND_TYPES.kindOfValues [definition, in ValuesNTypes]
VALUES_AND_TYPES.kindOfValue [definition, in ValuesNTypes]
VALUES_AND_TYPES.AIKDouble [constructor, in ValuesNTypes]
VALUES_AND_TYPES.AIKLong [constructor, in ValuesNTypes]
VALUES_AND_TYPES.AIKFloat [constructor, in ValuesNTypes]
VALUES_AND_TYPES.AIKInt [constructor, in ValuesNTypes]
VALUES_AND_TYPES.AIKShort [constructor, in ValuesNTypes]
VALUES_AND_TYPES.AIKByteBool [constructor, in ValuesNTypes]
VALUES_AND_TYPES.AIKChar [constructor, in ValuesNTypes]
VALUES_AND_TYPES.AIKRef [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TArrayIKind [inductive, in ValuesNTypes]
VALUES_AND_TYPES.VIKDouble [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VIKLong [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VIKFloat [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VIKInt [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VIKRef [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TVarIKind [inductive, in ValuesNTypes]
VALUES_AND_TYPES.VKDouble2 [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VKDouble1 [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VKLong2 [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VKLong1 [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VKFloat [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VKInt [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VKAddr [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VKRef [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TVarKind [inductive, in ValuesNTypes]
VALUES_AND_TYPES.KDouble [constructor, in ValuesNTypes]
VALUES_AND_TYPES.KLong [constructor, in ValuesNTypes]
VALUES_AND_TYPES.KFloat [constructor, in ValuesNTypes]
VALUES_AND_TYPES.KInt [constructor, in ValuesNTypes]
VALUES_AND_TYPES.KAddr [constructor, in ValuesNTypes]
VALUES_AND_TYPES.KRef [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TKind [inductive, in ValuesNTypes]
VALUES_AND_TYPES.BTDouble [constructor, in ValuesNTypes]
VALUES_AND_TYPES.BTLong [constructor, in ValuesNTypes]
VALUES_AND_TYPES.BTFloat [constructor, in ValuesNTypes]
VALUES_AND_TYPES.BTChar [constructor, in ValuesNTypes]
VALUES_AND_TYPES.BTInt [constructor, in ValuesNTypes]
VALUES_AND_TYPES.BTShort [constructor, in ValuesNTypes]
VALUES_AND_TYPES.BTBool [constructor, in ValuesNTypes]
VALUES_AND_TYPES.BTByte [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TBaseType [inductive, in ValuesNTypes]
VALUES_AND_TYPES.RTArray [constructor, in ValuesNTypes]
VALUES_AND_TYPES.RTObject [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TReferenceType [inductive, in ValuesNTypes]
VALUES_AND_TYPES.BaseType [constructor, in ValuesNTypes]
VALUES_AND_TYPES.ReferenceType [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TType [inductive, in ValuesNTypes]
VALUES_AND_TYPES.VADouble [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VALong [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VAFloat [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VAInt [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VAShort [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VAByte [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VABool [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VAChar [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VARef [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TAValue [inductive, in ValuesNTypes]
VALUES_AND_TYPES.VVDouble2 [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVDouble1 [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVLong2 [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVLong1 [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVFloat [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVInt [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVAddr [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VVRef [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TVarValue [inductive, in ValuesNTypes]
VALUES_AND_TYPES.VDouble [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VLong [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VFloat [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VInt [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VAddr [constructor, in ValuesNTypes]
VALUES_AND_TYPES.VRef [constructor, in ValuesNTypes]
VALUES_AND_TYPES.TValue [inductive, in ValuesNTypes]
VALUES_AND_TYPES.PNotNullExists [axiom, in ValuesNTypes]
VALUES_AND_TYPES.null [axiom, in ValuesNTypes]
VALUES_AND_TYPES.PLoc_eqDec [axiom, in ValuesNTypes]
VALUES_AND_TYPES.TLoc [axiom, in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Double [module, in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Float [module, in ValuesNTypes]
VALUES_AND_TYPES.M_Char [module, in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Long [module, in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Int [module, in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Short [module, in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Byte [module, in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Bool [module, in ValuesNTypes]
VALUES_AND_TYPES.jump [axiom, in ValuesNTypes]
VALUES_AND_TYPES.TOffset [axiom, in ValuesNTypes]
VALUES_AND_TYPES.PPC_eqDec [axiom, in ValuesNTypes]
VALUES_AND_TYPES.TPC [axiom, in ValuesNTypes]
VALUES_AND_TYPES.PShortName_eqDec [axiom, in ValuesNTypes]
VALUES_AND_TYPES.TShortName [axiom, in ValuesNTypes]
VALUES_AND_TYPES.PClassName_eqDec [axiom, in ValuesNTypes]
VALUES_AND_TYPES.TClassName [axiom, in ValuesNTypes]
VALUES_AND_TYPES [module, in ValuesNTypes]
var [variable, in Instructions]
vars0 [definition, in Loop_Assertions]
vars0 [definition, in Loop]
var_set_other [lemma, in Loop_Assertions]
var_set_this [lemma, in Loop_Assertions]
var_value_other_fields [lemma, in Loop_Assertions]
var_value_def [constructor, in Loop_Assertions]
var_value [inductive, in Loop_Assertions]
var_set_other [lemma, in Loop]
var_set_this [lemma, in Loop]
var_value_other_fields [lemma, in Loop]
var_value_def [constructor, in Loop]
var_value [inductive, in Loop]
VAT [module, in Instructions]
VAT [module, in Loop_Assertions]
VAT [module, in Program_A]
VAT [module, in Loop]
VAT [module, in IAdd]
vfour [definition, in IAdd]
vtwo [definition, in IAdd]

Module Index

A

ADDR_ARITHMETIC.M_ArithmeticTypes [in Arithmetic]
ADDR_ARITHMETIC [in Arithmetic]
AllStr [in Loop_Assertions]
AllStr [in Loop]
AllStr [in IAdd]
ALL_STRUCTURES.M_HeapFacts [in AllStructures]
ALL_STRUCTURES.M_RuntimeStructuresFacts [in AllStructures]
ALL_STRUCTURES.M_ProgramStructuresFacts [in AllStructures]
ALL_STRUCTURES.M_Arithmetics [in AllStructures]
ALL_STRUCTURES.M_Program [in AllStructures]
ALL_STRUCTURES.M_RuntimeStructures [in AllStructures]
ALL_STRUCTURES [in AllStructures]
ARITHMETIC [in Arithmetic]
ArithmeticOperators [in ArithOps]
ARITHMETICS [in Arithmetic]
ARITHMETICS.M_DoubleArithmetic [in Arithmetic]
ARITHMETICS.M_LongArithmetic [in Arithmetic]
ARITHMETICS.M_FloatArithmetic [in Arithmetic]
ARITHMETICS.M_IntArithmetic [in Arithmetic]
ARITHMETICS.M_AddrArithmetic [in Arithmetic]
ARITHMETICS.M_RefArithmetic [in Arithmetic]
ARITHMETICS.M_ArithmeticTypes [in Arithmetic]
ArithmeticTypes [in Arithmetic]
ARITHMETIC.M_ArithmeticTypes [in Arithmetic]
ARS [in Loop_Assertions]
ARS [in Loop]
ARS [in IAdd]

C

CHAR [in Char]
CHARSIZE [in Char]

D

DNum [in Instructions]
DOUBLE_ARITHMETIC.M_ArithmeticTypes [in Arithmetic]
DOUBLE_ARITHMETIC [in Arithmetic]

F

FLOAT_ARITHMETIC.M_ArithmeticTypes [in Arithmetic]
FLOAT_ARITHMETIC [in Arithmetic]
FMake [in FNumeric]
FNum [in Instructions]
FNUMERIC [in FNumeric]
FPRECISION [in FNumeric]

H

H [in Loop_Assertions]
H [in Loop]
H [in IAdd]
HEAP [in Heap]
HeapFacts [in Heap]
HEAP.M_ProgramStructures [in Heap]
HF [in Loop_Assertions]
HF [in Loop]
HF [in IAdd]

I

INT_ARITHMETIC.M_ArithmeticTypes [in Arithmetic]
INT_ARITHMETIC [in Arithmetic]
INum [in Instructions]
INum [in Loop_Assertions]
INum [in Program_A]
INum [in Loop]

L

LNum [in Instructions]
LONG_ARITHMETIC.M_ArithmeticTypes [in Arithmetic]
LONG_ARITHMETIC [in Arithmetic]

M

Make [in Char]
Make [in Numeric]
MONOLITIC_HEAP [in Heap]
M_IntNumProperties [in Loop_Assertions]
M_IntNumProperties [in Loop]

N

NUMERIC [in Numeric]
NumericProperties [in Numeric]
NUMSIZE [in Numeric]

P

P [in Instructions]
P [in Loop_Assertions]
P [in Program_A]
P [in Loop]
P [in IAdd]
PASSERT [in Loop_Assertions]
PROGRAM [in Program]
ProgramStructuresFacts [in ProgramStructures]
ProgramStructuresFacts.StandardNames [in ProgramStructures]
ProgramStructuresImpl [in ProgramStructuresImpl]
ProgramStructuresImpl.M_VarMap [in ProgramStructuresImpl]
ProgramStructuresImpl.M_Var_as_OT [in ProgramStructuresImpl]
ProgramStructuresImpl.M_ValuesAndTypes [in ProgramStructuresImpl]
PROGRAM_ASSERTIONS_W_CONSTRUCTORS [in ProgramAssertions]
PROGRAM_ASSERTIONS.M_Sem_Frame [in ProgramAssertions]
PROGRAM_ASSERTIONS [in ProgramAssertions]
PROGRAM_W_CONSTRUCTORS [in Program]
PROGRAM_STRUCTURES_WITH_MAP.M_VarMap [in ProgramStructures]
PROGRAM_STRUCTURES_WITH_MAP.M_Var_as_OT [in ProgramStructures]
PROGRAM_STRUCTURES_WITH_MAP [in ProgramStructures]
PROGRAM_STRUCTURES.M_ValuesAndTypes [in ProgramStructures]
PROGRAM_STRUCTURES [in ProgramStructures]
PROGRAM.M_ProgramStructuresFacts [in Program]
PROGRAM.M_ProgramStructures [in Program]
PS [in Instructions]
PS [in Loop_Assertions]
PS [in Program_A]
PS [in Loop]
PS [in IAdd]
PSF [in Loop_Assertions]
PSF [in Loop]
PSFacts [in Instructions]
PSFacts [in Program_A]

R

REF_ARITHMETIC.M_ArithmeticTypes [in Arithmetic]
REF_ARITHMETIC [in Arithmetic]
RS [in Loop_Assertions]
RS [in Loop]
RS [in IAdd]
RSF [in Loop_Assertions]
RSF [in Loop]
RSF [in IAdd]
RuntimeStructuresFacts [in RuntimeStructures]
RuntimeStructuresImpl [in RuntimeStructuresImpl]
RuntimeStructuresImpl.M_Heap [in RuntimeStructuresImpl]
RUNTIME_STRUCTURES.M_Heap [in RuntimeStructures]
RUNTIME_STRUCTURES [in RuntimeStructures]

S

SCOND [in Loop_Assertions]
SCOND [in Loop]
SEM [in IAdd]
SEMANTICS [in Semantics]
SEMANTICS.M_Sem_Call [in Semantics]
SEMANTICS.M_Sem_Heap [in Semantics]
SEMANTICS.M_Sem_Monitor [in Semantics]
SEMANTICS.M_Sem_Frame [in Semantics]
SEMANTICS.M_AllStructures [in Semantics]
SEM_VAR.M_AllStructures [in Sem_Var]
SEM_VAR [in Sem_Var]
SEM_HEAP.M_Sem_Monitor [in Sem_Heap]
SEM_HEAP.M_AllStructures [in Sem_Heap]
SEM_HEAP [in Sem_Heap]
SEM_STACKOP.M_AllStructures [in Sem_Stackop]
SEM_STACKOP [in Sem_Stackop]
SEM_CALL.M_Sem_Monitor [in Sem_Call]
SEM_CALL.M_AllStructures [in Sem_Call]
SEM_CALL [in Sem_Call]
SEM_MONITOR.M_AllStructures [in Sem_Monitor]
SEM_MONITOR [in Sem_Monitor]
SEM_FRAME.M_Sem_Cond [in Sem_Frame]
SEM_FRAME.M_Sem_Var [in Sem_Frame]
SEM_FRAME.M_Sem_Stackop [in Sem_Frame]
SEM_FRAME.M_AllStructures [in Sem_Frame]
SEM_FRAME [in Sem_Frame]
SEM_COND.M_IntNumProperties [in Sem_Cond]
SEM_COND.M_AllStructures [in Sem_Cond]
SEM_COND [in Sem_Cond]
SF [in Loop_Assertions]
SF [in Loop]
SF [in IAdd]
SSOP [in Loop_Assertions]
SSOP [in Loop]
SSOP [in IAdd]
SVAR [in Loop_Assertions]
SVAR [in Loop]

V

VALUES_AND_TYPES.M_Numeric_Double [in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Float [in ValuesNTypes]
VALUES_AND_TYPES.M_Char [in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Long [in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Int [in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Short [in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Byte [in ValuesNTypes]
VALUES_AND_TYPES.M_Numeric_Bool [in ValuesNTypes]
VALUES_AND_TYPES [in ValuesNTypes]
VAT [in Instructions]
VAT [in Loop_Assertions]
VAT [in Program_A]
VAT [in Loop]
VAT [in IAdd]

Variable Index

A

ak [in Instructions]

B

bt [in Instructions]

C

c [in Instructions]
cn [in Instructions]

D

Dec.P [in Common]

E

EqDec.A [in Common]

F

fname [in Instructions]
Functions.A [in Common]
Functions.B [in Common]

H

HEAP.HeapSpec.arr [in Heap]
HEAP.HeapSpec.arr1 [in Heap]
HEAP.HeapSpec.arr2 [in Heap]
HEAP.HeapSpec.cn [in Heap]
HEAP.HeapSpec.cn1 [in Heap]
HEAP.HeapSpec.cn2 [in Heap]
HEAP.HeapSpec.fn [in Heap]
HEAP.HeapSpec.fn1 [in Heap]
HEAP.HeapSpec.fn2 [in Heap]
HEAP.HeapSpec.h [in Heap]
HEAP.HeapSpec.hval [in Heap]
HEAP.HeapSpec.hval1 [in Heap]
HEAP.HeapSpec.hval2 [in Heap]
HEAP.HeapSpec.h1 [in Heap]
HEAP.HeapSpec.h2 [in Heap]
HEAP.HeapSpec.idx [in Heap]
HEAP.HeapSpec.idx1 [in Heap]
HEAP.HeapSpec.idx2 [in Heap]
HEAP.HeapSpec.init_values [in Heap]
HEAP.HeapSpec.loc [in Heap]
HEAP.HeapSpec.loc1 [in Heap]
HEAP.HeapSpec.loc2 [in Heap]
HEAP.HeapSpec.obj [in Heap]
HEAP.HeapSpec.obj1 [in Heap]
HEAP.HeapSpec.obj2 [in Heap]
HEAP.HeapSpec.th [in Heap]
HEAP.HeapSpec.th1 [in Heap]
HEAP.HeapSpec.th2 [in Heap]
HEAP.HeapSpec.v [in Heap]
HEAP.HeapSpec.va [in Heap]
HEAP.HeapSpec.va1 [in Heap]
HEAP.HeapSpec.va2 [in Heap]
HEAP.HeapSpec.v1 [in Heap]
HEAP.HeapSpec.v2 [in Heap]

K

k [in Instructions]

L

Lists.A [in Common]
Lists.K [in Common]
Lists.keyEqDec [in Common]
LoopExample.n_small [in Loop_Assertions]
LoopExample.n_positive [in Loop_Assertions]
LoopExample.n_small [in Loop]
LoopExample.n_positive [in Loop]
LoopExample.n2_small [in Loop_Assertions]
LoopExample.n2_small [in Loop]

M

MONOLITIC_HEAP.MonoHeapSpec.init_values [in Heap]
MONOLITIC_HEAP.MonoHeapSpec.v [in Heap]
MONOLITIC_HEAP.MonoHeapSpec.hv [in Heap]
MONOLITIC_HEAP.MonoHeapSpec.fn [in Heap]
MONOLITIC_HEAP.MonoHeapSpec.cn [in Heap]
MONOLITIC_HEAP.MonoHeapSpec.th2 [in Heap]
MONOLITIC_HEAP.MonoHeapSpec.th1 [in Heap]
MONOLITIC_HEAP.MonoHeapSpec.loc [in Heap]
MONOLITIC_HEAP.MonoHeapSpec.h [in Heap]
msig [in Instructions]

N

n [in Instructions]

O

off [in Instructions]

R

rt [in Instructions]
RuntimeStructuresImpl.GenericStackDefinition.t [in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.t [in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.VarsProperties.v [in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.VarsProperties.vars [in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.VarsProperties.x [in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.VarsProperties.y [in RuntimeStructuresImpl]
RUNTIME_STRUCTURES.GenericStackDefinition.t [in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.VarsProperties.v [in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.VarsProperties.y [in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.VarsProperties.x [in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.VarsProperties.vars [in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.t [in RuntimeStructures]

S

SEM_COND.intArith [in Sem_Cond]

V

v [in Instructions]
var [in Instructions]

Library Index

A

AllStructures
Arithmetic
ArithOps

C

F

H

Heap

I

IAdd
Instructions

L

Loop
Loop_Assertions

N

P

Program
ProgramAssertions
ProgramStructures
ProgramStructuresImpl
Program_A

R

RuntimeStructures
RuntimeStructuresImpl

S

Semantics
Sem_Monitor
Sem_Call
Sem_Frame
Sem_Heap
Sem_Cond
Sem_Stackop
Sem_Var

V

Lemma Index

A

add_add [in Loop_Assertions]
add_i2_i_small [in Loop_Assertions]
add_add [in Loop]
add_i2_i_small [in Loop]
add1_small [in Loop_Assertions]
add1_small [in Loop]
add2_small [in Loop_Assertions]
add2_small [in Loop]
ARITHMETICS.PArithmeticConsistentKindBinOp [in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindCastOp [in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindCmpi [in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindCmpValues [in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindCmpZero [in Arithmetic]
ARITHMETICS.PArithmeticConsistentKindUnOp [in Arithmetic]

B

base_max [in Loop_Assertions]
base_max [in Loop]
bijection_id [in Common]
binop_224_impl_toZ [in IAdd]
binop_224 [in IAdd]

C

closed_states [in Loop]
constLemma [in Loop_Assertions]
constn [in Loop_Assertions]
constn [in Loop]
const0 [in Loop]
const1 [in Loop_Assertions]
const1 [in Loop]

D

described_0 [in Loop_Assertions]

F

final_20 [in Loop_Assertions]
final_20 [in Loop]
FMake.add_prop [in FNumeric]
FMake.cmpg_nan [in FNumeric]
FMake.cmpg_lt [in FNumeric]
FMake.cmpg_eq [in FNumeric]
FMake.cmpg_gt [in FNumeric]
FMake.cmpl_nan [in FNumeric]
FMake.cmpl_lt [in FNumeric]
FMake.cmpl_eq [in FNumeric]
FMake.cmpl_gt [in FNumeric]
FMake.div_prop [in FNumeric]
FMake.mul_prop [in FNumeric]
FMake.neg_prop [in FNumeric]
FMake.one_prop [in FNumeric]
FMake.rem_prop [in FNumeric]
FMake.sub_prop [in FNumeric]
FMake.truncate_too_large [in FNumeric]
FMake.truncate_too_small [in FNumeric]
FMake.truncate_range_negative [in FNumeric]
FMake.truncate_range_positive [in FNumeric]
FMake.truncate_nan [in FNumeric]
FMake.two_prop [in FNumeric]
FMake.zero_prop [in FNumeric]
frame_2_3_impl [in IAdd]
frame_1_2_impl [in IAdd]
frame_0_1_impl [in IAdd]
frame_2_3 [in IAdd]
frame_1_2 [in IAdd]
frame_0_1 [in IAdd]
frame0_ok [in IAdd]
frame1_ok [in IAdd]
frame2_ok [in IAdd]
frame3_ok [in IAdd]

G

getPC_isPC3 [in IAdd]
getPC_isPC2 [in IAdd]
getPC_isPC1 [in IAdd]
getPC_isPC0 [in IAdd]

H

half_base_max [in Loop_Assertions]
half_base_max [in Loop]
HeapFacts.PRefType_NotNull [in Heap]
HEAP.MonitorInvariant1 [in Heap]
HEAP.newMonitorLockCount [in Heap]

I

Instruction0 [in IAdd]
Instruction1 [in IAdd]
Instruction2 [in IAdd]
Instruction3 [in IAdd]
inverse_id [in Common]

J

jvm0_ok [in IAdd]
jvm1_ok [in IAdd]
jvm2_ok [in IAdd]
jvm3_ok [in IAdd]

M

Make.base_ge_2 [in Char]
Make.half_base_ge_2 [in Numeric]
Make.Pcompare_toZ [in Numeric]
Make.PisNotZero [in Numeric]
Make.PminusOneToZ [in Numeric]
Make.PoneIsNotZero [in Numeric]
Make.PoneToZ [in Numeric]
Make.power_positive [in Char]
Make.power_positive [in Numeric]
Make.PzeroToZ [in Char]
Make.PzeroToZ [in Numeric]
Make.testdop45 [in Char]
Make.testdop45 [in Numeric]
Make.testm42 [in Numeric]
Make.testm43 [in Char]
Make.testm43 [in Numeric]
Make.testm44 [in Char]
Make.testm44 [in Numeric]
Make.testm45 [in Char]
Make.testm45 [in Numeric]
Make.testm73 [in Char]
Make.testm73 [in Numeric]
Make.testm74 [in Char]
Make.testm74 [in Numeric]
Make.testm75 [in Char]
Make.testm75 [in Numeric]

N

NumericProperties.Pcompare_const [in Numeric]
num_224_const [in IAdd]
num_224_toZ [in IAdd]
num_224_impl_toZ [in IAdd]

P

partial_correctness [in Loop_Assertions]
partial_correctness [in Loop]
pc0_neq_pc3 [in IAdd]
pc0_next [in IAdd]
pc1_neq_pc3 [in IAdd]
pc1_next [in IAdd]
pc2_neq_pc3 [in IAdd]
pc2_next [in IAdd]
PeqDecS_eqDec [in Common]
Pnth_error_in [in Common]
Pnth_error_length [in Common]
post5_impl_pre6 [in Loop_Assertions]
post5_impl_pre6 [in Loop]
post8_impl_9_or_19 [in Loop_Assertions]
post8_impl_9_or_19 [in Loop]
PpropDecS_propDec [in Common]
ProgramStructuresFacts.distinct_vars_next [in ProgramStructures]
ProgramStructuresFacts.distinct_vars_2_3 [in ProgramStructures]
ProgramStructuresFacts.distinct_vars_1_3 [in ProgramStructures]
ProgramStructuresFacts.distinct_vars_1_2 [in ProgramStructures]
ProgramStructuresFacts.distinct_vars_0_3 [in ProgramStructures]
ProgramStructuresFacts.distinct_vars_0_2 [in ProgramStructures]
ProgramStructuresFacts.distinct_vars_0_1 [in ProgramStructures]
ProgramStructuresFacts.distinct_varFromNat [in ProgramStructures]
ProgramStructuresImpl.N_eqDec [in ProgramStructuresImpl]
ProgramStructuresImpl.PnextVarSucc [in ProgramStructuresImpl]
PROGRAM_ASSERTIONS_W_CONSTRUCTORS.frameDescribed_inRange [in ProgramAssertions]
PROGRAM_ASSERTIONS.multiTransitions [in ProgramAssertions]
PROGRAM_ASSERTIONS.frameDescribed_equiv [in ProgramAssertions]
PROGRAM_ASSERTIONS.positionedAssertionPc [in ProgramAssertions]

R

range_pos [in Loop_Assertions]
range_pos [in Loop]
RuntimeStructuresFacts.PlocalStackKAbstractionApp [in RuntimeStructures]
RuntimeStructuresFacts.PprefixMap [in RuntimeStructures]
RuntimeStructuresFacts.PprefixNilImpliesNil [in RuntimeStructures]
RuntimeStructuresFacts.PprefixTrivial [in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValuesMap [in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValuesNilCons [in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValuesSame [in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValuesTrivial [in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValues_implies_prefix_r [in RuntimeStructures]
RuntimeStructuresFacts.PstackTopValues_implies_prefix_l [in RuntimeStructures]
RuntimeStructuresImpl.noneNotMapsTo [in RuntimeStructuresImpl]
RuntimeStructuresImpl.notMapsToNone [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsEmptyGet [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsSetGet [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsSetGetOther [in RuntimeStructuresImpl]

S

SEMANTICS.oneThreadSelected [in Semantics]
SEMANTICS.oneThreadSelectedAlways [in Semantics]
SEMANTICS.PoneThreadAndHeapChanged_1thread_inv [in Semantics]
SEMANTICS.PoneThreadAndHeapChanged_1thread [in Semantics]
SEMANTICS.PoneThreadChanged_1thread_inv [in Semantics]
SEMANTICS.PoneThreadChanged_1thread [in Semantics]
semInstr_2_3_impl [in IAdd]
semInstr_1_2_impl [in IAdd]
semInstr_0_1_impl [in IAdd]
semInstr_2_3 [in IAdd]
semInstr_1_2 [in IAdd]
semInstr_0_1 [in IAdd]
SEM_VAR.PSemVarInversion_store_1 [in Sem_Var]
SEM_VAR.PSemVarInversion_load_1 [in Sem_Var]
SEM_VAR.staticSemVarComplete [in Sem_Var]
SEM_VAR.staticSemVarConsistent [in Sem_Var]
SEM_VAR.PvarsKAbstractionSetSame [in Sem_Var]
SEM_STACKOP.staticSemStackComplete [in Sem_Stackop]
SEM_STACKOP.PmapPattern [in Sem_Stackop]
SEM_STACKOP.staticSemStackConsistent [in Sem_Stackop]
SEM_STACKOP.PstaticSemStackCastOp [in Sem_Stackop]
SEM_STACKOP.PstaticSemStackCmpi [in Sem_Stackop]
SEM_STACKOP.PstaticSemStackBinOp_NoResult [in Sem_Stackop]
SEM_STACKOP.PstaticSemStackBinOp [in Sem_Stackop]
SEM_STACKOP.PstaticSemStackUnOp [in Sem_Stackop]
SEM_CALL.PlookupMethod_eqv_lookupMethodInd [in Sem_Call]
SEM_FRAME.staticSemFrameComplete [in Sem_Frame]
SEM_FRAME.staticSemFrameConsistent [in Sem_Frame]
SEM_COND.staticSemCondComplete [in Sem_Cond]
SEM_COND.staticSemCondConsistent [in Sem_Cond]
SEM_COND.PstaticSemCondCmp [in Sem_Cond]
SEM_COND.PstaticSemCondIf [in Sem_Cond]
singles [in Loop_Assertions]
small_4 [in IAdd]
small_2 [in IAdd]
stackop_dup_inversion [in IAdd]
stackop_binop_inversion [in IAdd]
stackop_2_3_impl_gen [in IAdd]
stackop_2_3_impl [in IAdd]
stackop_1_2_impl [in IAdd]
stackop_0_1_impl [in IAdd]
stackop_2_3 [in IAdd]
stackop_1_2 [in IAdd]
stackop_0_1 [in IAdd]
stack_value_from_var [in Loop_Assertions]
stack_values_other_fields [in Loop_Assertions]
stack_value_from_var [in Loop]
stack_values_other_fields [in Loop]
start_0 [in Loop_Assertions]
start_0 [in Loop]
stepFrame_3_impossible [in IAdd]
stepFrame_2_3_impl [in IAdd]
stepFrame_1_2_impl [in IAdd]
stepFrame_0_1_impl [in IAdd]
stepFrame_2_3 [in IAdd]
stepFrame_1_2 [in IAdd]
stepFrame_0_1 [in IAdd]
StepsConcrete [in IAdd]
StepsFrameConcrete [in IAdd]
StepsFrameImpl [in IAdd]
stepThread_3_impossible [in IAdd]
stepThread_2_3_impl [in IAdd]
stepThread_1_2_impl [in IAdd]
stepThread_0_1_impl [in IAdd]
stepThread_2_3 [in IAdd]
stepThread_1_2 [in IAdd]
stepThread_0_1 [in IAdd]
step_3_impossible [in IAdd]
step_2_3_impl [in IAdd]
step_1_2_impl [in IAdd]
step_0_1_impl [in IAdd]
step_2_3 [in IAdd]
step_1_2 [in IAdd]
step_0_1 [in IAdd]
s20 [in Loop_Assertions]
s20 [in Loop]

T

ThisMethodCM [in IAdd]
thread0_ok [in IAdd]
thread1_ok [in IAdd]
thread2_ok [in IAdd]
thread3_ok [in IAdd]
toZ2 [in IAdd]
toZ4 [in IAdd]
trans_19_20 [in Loop_Assertions]
trans_18_6 [in Loop_Assertions]
trans_17_18 [in Loop_Assertions]
trans_16_17 [in Loop_Assertions]
trans_15_16 [in Loop_Assertions]
trans_14_15 [in Loop_Assertions]
trans_13_14 [in Loop_Assertions]
trans_12_13 [in Loop_Assertions]
trans_11_12 [in Loop_Assertions]
trans_10_11 [in Loop_Assertions]
trans_9_10 [in Loop_Assertions]
trans_8_post8 [in Loop_Assertions]
trans_7_8 [in Loop_Assertions]
trans_6_7 [in Loop_Assertions]
trans_5_post [in Loop_Assertions]
trans_4_5 [in Loop_Assertions]
trans_3_4 [in Loop_Assertions]
trans_2_3 [in Loop_Assertions]
trans_1_2 [in Loop_Assertions]
trans_0_1 [in Loop_Assertions]
trans_19_20 [in Loop]
trans_18_6 [in Loop]
trans_17_18 [in Loop]
trans_16_17 [in Loop]
trans_15_16 [in Loop]
trans_14_15 [in Loop]
trans_13_14 [in Loop]
trans_12_13 [in Loop]
trans_11_12 [in Loop]
trans_10_11 [in Loop]
trans_9_10 [in Loop]
trans_8_post8 [in Loop]
trans_7_8 [in Loop]
trans_6_7 [in Loop]
trans_5_post [in Loop]
trans_4_5 [in Loop]
trans_3_4 [in Loop]
trans_2_3 [in Loop]
trans_1_2 [in Loop]
trans_0_1 [in Loop]

V

VALUES_AND_TYPES.PsizeOfKindCat2 [in ValuesNTypes]
VALUES_AND_TYPES.PsizeOfKindCat1 [in ValuesNTypes]
VALUES_AND_TYPES.PisCatOK [in ValuesNTypes]
VALUES_AND_TYPES.PtransformAFromValueKindConsistent [in ValuesNTypes]
VALUES_AND_TYPES.PtransformAToValueKindConsistent [in ValuesNTypes]
VALUES_AND_TYPES.PValVarMappingConsistentInv_EVal_EVar [in ValuesNTypes]
VALUES_AND_TYPES.PValVarMappingConsistentInv_AVar_EVal [in ValuesNTypes]
VALUES_AND_TYPES.PValVarMappingConsistentInv_AVal_EVar [in ValuesNTypes]
VALUES_AND_TYPES.PValVarMappingConsistent [in ValuesNTypes]
VALUES_AND_TYPES.PtransformValToVarValConsistent [in ValuesNTypes]
VALUES_AND_TYPES.PvalVarKindMapping_transform_equiv [in ValuesNTypes]
VALUES_AND_TYPES.PvalVarMapping_transform_equiv [in ValuesNTypes]
VALUES_AND_TYPES.PdefaultValueForType_ForKind_Consistent [in ValuesNTypes]
VALUES_AND_TYPES.PForEachKindListExistsValueList [in ValuesNTypes]
VALUES_AND_TYPES.PForEachKindExistsAValue [in ValuesNTypes]
VALUES_AND_TYPES.PdefaultForKindConsistent [in ValuesNTypes]
VALUES_AND_TYPES.PexampleForKindConsistent [in ValuesNTypes]
var_set_other [in Loop_Assertions]
var_set_this [in Loop_Assertions]
var_value_other_fields [in Loop_Assertions]
var_set_other [in Loop]
var_set_this [in Loop]
var_value_other_fields [in Loop]

Axiom Index

A

ARITHMETIC.binOpArithmetic [in Arithmetic]
ARITHMETIC.castArithmetic [in Arithmetic]
ARITHMETIC.cmpiArithmetic [in Arithmetic]
ARITHMETIC.cmpValuesArithmetic [in Arithmetic]
ARITHMETIC.cmpZeroArithmetic [in Arithmetic]
ARITHMETIC.kind [in Arithmetic]
ARITHMETIC.unOpArithmetic [in Arithmetic]

C

c [in IAdd]
caller_loc_class_loc [in IAdd]
caller_loc [in IAdd]
CHARSIZE.power [in Char]
CHARSIZE.power_positive [in Char]
CHAR.power [in Char]
CHAR.power_positive [in Char]
CHAR.PzeroToZ [in Char]
CHAR.range_prop [in Char]
CHAR.t [in Char]
CHAR.toZ [in Char]
CHAR.truncate_on_zero [in Char]
CHAR.truncate_to_char [in Char]
CHAR.zero [in Char]

F

FNUMERIC.abstract_rem [in FNumeric]
FNUMERIC.add [in FNumeric]
FNUMERIC.add_prop [in FNumeric]
FNUMERIC.cmpg [in FNumeric]
FNUMERIC.cmpg_nan [in FNumeric]
FNUMERIC.cmpg_lt [in FNumeric]
FNUMERIC.cmpg_eq [in FNumeric]
FNUMERIC.cmpg_gt [in FNumeric]
FNUMERIC.cmpl [in FNumeric]
FNUMERIC.cmpl_nan [in FNumeric]
FNUMERIC.cmpl_lt [in FNumeric]
FNUMERIC.cmpl_eq [in FNumeric]
FNUMERIC.cmpl_gt [in FNumeric]
FNUMERIC.const [in FNumeric]
FNUMERIC.div [in FNumeric]
FNUMERIC.div_prop [in FNumeric]
FNUMERIC.fromDiadic [in FNumeric]
FNUMERIC.iconst [in FNumeric]
FNUMERIC.mul [in FNumeric]
FNUMERIC.mul_prop [in FNumeric]
FNUMERIC.neg [in FNumeric]
FNUMERIC.neg_prop [in FNumeric]
FNUMERIC.one [in FNumeric]
FNUMERIC.one_prop [in FNumeric]
FNUMERIC.precision [in FNumeric]
FNUMERIC.rem [in FNumeric]
FNUMERIC.rem_prop [in FNumeric]
FNUMERIC.sub [in FNumeric]
FNUMERIC.sub_prop [in FNumeric]
FNUMERIC.t [in FNumeric]
FNUMERIC.toDiadic [in FNumeric]
FNUMERIC.toIEEE [in FNumeric]
FNUMERIC.truncate [in FNumeric]
FNUMERIC.truncate_too_large [in FNumeric]
FNUMERIC.truncate_too_small [in FNumeric]
FNUMERIC.truncate_range_negative [in FNumeric]
FNUMERIC.truncate_range_positive [in FNumeric]
FNUMERIC.truncate_nan [in FNumeric]
FNUMERIC.two [in FNumeric]
FNUMERIC.two_prop [in FNumeric]
FNUMERIC.zero [in FNumeric]
FNUMERIC.zero_prop [in FNumeric]
FPRECISION.precision [in FNumeric]

H

heap [in IAdd]
HEAP.emptyHeap [in Heap]
HEAP.freshLocation [in Heap]
HEAP.get [in Heap]
HEAP.getArrayCell [in Heap]
HEAP.getArrayComponentType [in Heap]
HEAP.getArraySize [in Heap]
HEAP.getArrayValue [in Heap]
HEAP.getClassObjectLoc [in Heap]
HEAP.getMonitorLockCount [in Heap]
HEAP.getMonitorThreadId [in Heap]
HEAP.getObjectClass [in Heap]
HEAP.getObjectField [in Heap]
HEAP.getObjectMonitor [in Heap]
HEAP.getsetMonitorLockCount [in Heap]
HEAP.getsetMonitorThreadId [in Heap]
HEAP.getStaticField [in Heap]
HEAP.initArray [in Heap]
HEAP.initObject [in Heap]
HEAP.MonitorInvariant [in Heap]
HEAP.newMonitor [in Heap]
HEAP.newMonitorThreadId [in Heap]
HEAP.Pempty_empty_static [in Heap]
HEAP.Pempty_empty [in Heap]
HEAP.PfreshLocation_fresh [in Heap]
HEAP.PinitArray_otherCells [in Heap]
HEAP.PinitArray_initialised [in Heap]
HEAP.PinitObject_otherFields [in Heap]
HEAP.PinitObject_initialised [in Heap]
HEAP.Pnull_empty [in Heap]
HEAP.PsetArrayCell_size [in Heap]
HEAP.PsetArrayCell_other [in Heap]
HEAP.PsetArrayCell_same [in Heap]
HEAP.PsetObjectField_Class [in Heap]
HEAP.PsetObjectField_otherField [in Heap]
HEAP.PsetObjectField_sameField [in Heap]
HEAP.PsetStaticField_otherClass [in Heap]
HEAP.PsetStaticField_otherField [in Heap]
HEAP.PsetStaticField_change [in Heap]
HEAP.Pset_otherLocation [in Heap]
HEAP.Pset_get [in Heap]
HEAP.PsystemException_otherLocations [in Heap]
HEAP.PsystemException_locationAfter [in Heap]
HEAP.PThreadId_eqDec [in Heap]
HEAP.set [in Heap]
HEAP.setArrayCell [in Heap]
HEAP.setMonitorState [in Heap]
HEAP.setObjectField [in Heap]
HEAP.setObjectMonitor [in Heap]
HEAP.setStaticField [in Heap]
HEAP.systemException [in Heap]
HEAP.TArray [in Heap]
HEAP.THeap [in Heap]
HEAP.TMonitor [in Heap]
HEAP.TObject [in Heap]
HEAP.TThreadId [in Heap]

M

Make.add [in Numeric]
Make.add_prop [in Numeric]
Make.and [in Numeric]
Make.const [in Char]
Make.const [in Numeric]
Make.const_prop [in Char]
Make.const_prop [in Numeric]
Make.div [in Numeric]
Make.div_prop [in Numeric]
Make.mul [in Numeric]
Make.mul_prop [in Numeric]
Make.neg [in Numeric]
Make.neg_prop [in Numeric]
Make.or [in Numeric]
Make.PNumericEqDec [in Numeric]
Make.PToZDistinct [in Numeric]
Make.range_prop [in Char]
Make.range_prop [in Numeric]
Make.rem [in Numeric]
Make.rem_prop [in Numeric]
Make.shl [in Numeric]
Make.shl_prop [in Numeric]
Make.shr [in Numeric]
Make.shr_prop [in Numeric]
Make.sub [in Numeric]
Make.sub_prop [in Numeric]
Make.t [in Char]
Make.t [in Numeric]
Make.toZ [in Char]
Make.toZ [in Numeric]
Make.truncate_on_zero [in Char]
Make.ushr [in Numeric]
Make.ushr_prop2 [in Numeric]
Make.ushr_prop1 [in Numeric]
Make.xor [in Numeric]
method_name [in IAdd]
MONOLITIC_HEAP.PsetStaticField_mono [in Heap]
MONOLITIC_HEAP.Pset_mono [in Heap]
MONOLITIC_HEAP.PgetStaticField_mono [in Heap]
MONOLITIC_HEAP.Pget_mono [in Heap]

N

n [in Loop_Assertions]
n [in Program_A]
n [in Loop]
NumericProperties.example_is_gt_f [in Numeric]
NumericProperties.example_is_gt_t [in Numeric]
NumericProperties.example_is_ge_f [in Numeric]
NumericProperties.example_is_ge_t [in Numeric]
NumericProperties.example_is_lt_f [in Numeric]
NumericProperties.example_is_lt_t [in Numeric]
NumericProperties.example_is_le_f [in Numeric]
NumericProperties.example_is_le_t [in Numeric]
NumericProperties.example_is_ne_f [in Numeric]
NumericProperties.example_is_ne_t [in Numeric]
NumericProperties.example_is_eq_f [in Numeric]
NumericProperties.example_is_eq_t [in Numeric]
NumericProperties.is_gt_f_toZ_prop [in Numeric]
NumericProperties.is_gt_t_toZ_prop [in Numeric]
NumericProperties.is_ge_f_toZ_prop [in Numeric]
NumericProperties.is_ge_t_toZ_prop [in Numeric]
NumericProperties.is_lt_f_toZ_prop [in Numeric]
NumericProperties.is_lt_t_toZ_prop [in Numeric]
NumericProperties.is_le_f_toZ_prop [in Numeric]
NumericProperties.is_le_t_toZ_prop [in Numeric]
NumericProperties.is_ne_f_toZ_prop [in Numeric]
NumericProperties.is_ne_t_toZ_prop [in Numeric]
NumericProperties.is_eq_f_toZ_prop [in Numeric]
NumericProperties.is_eq_t_toZ_prop [in Numeric]
NUMERIC.add [in Numeric]
NUMERIC.add_prop [in Numeric]
NUMERIC.and [in Numeric]
NUMERIC.compare [in Numeric]
NUMERIC.const [in Numeric]
NUMERIC.const_prop [in Numeric]
NUMERIC.div [in Numeric]
NUMERIC.div_prop [in Numeric]
NUMERIC.isNotZero [in Numeric]
NUMERIC.is_gt [in Numeric]
NUMERIC.is_ge [in Numeric]
NUMERIC.is_lt [in Numeric]
NUMERIC.is_le [in Numeric]
NUMERIC.is_ne [in Numeric]
NUMERIC.is_eq [in Numeric]
NUMERIC.minus_one [in Numeric]
NUMERIC.mul [in Numeric]
NUMERIC.mul_prop [in Numeric]
NUMERIC.neg [in Numeric]
NUMERIC.neg_prop [in Numeric]
NUMERIC.one [in Numeric]
NUMERIC.or [in Numeric]
NUMERIC.Pcompare_toZ [in Numeric]
NUMERIC.PisNotZero [in Numeric]
NUMERIC.PminusOneToZ [in Numeric]
NUMERIC.PNumericEqDec [in Numeric]
NUMERIC.PoneIsNotZero [in Numeric]
NUMERIC.PoneToZ [in Numeric]
NUMERIC.power [in Numeric]
NUMERIC.power_positive [in Numeric]
NUMERIC.PToZDistinct [in Numeric]
NUMERIC.PzeroToZ [in Numeric]
NUMERIC.range_prop [in Numeric]
NUMERIC.rem [in Numeric]
NUMERIC.rem_prop [in Numeric]
NUMERIC.shl [in Numeric]
NUMERIC.shl_prop [in Numeric]
NUMERIC.shr [in Numeric]
NUMERIC.shr_prop [in Numeric]
NUMERIC.sub [in Numeric]
NUMERIC.sub_prop [in Numeric]
NUMERIC.t [in Numeric]
NUMERIC.toZ [in Numeric]
NUMERIC.truncate [in Numeric]
NUMERIC.ushr [in Numeric]
NUMERIC.ushr_prop2 [in Numeric]
NUMERIC.ushr_prop1 [in Numeric]
NUMERIC.xor [in Numeric]
NUMERIC.zero [in Numeric]
NUMSIZE.power [in Numeric]
NUMSIZE.power_positive [in Numeric]

P

p [in IAdd]
ProgramStructuresFacts.StandardNames.AbstractMethodError [in ProgramStructures]
ProgramStructuresFacts.StandardNames.ArithmeticException [in ProgramStructures]
ProgramStructuresFacts.StandardNames.ArrayIndexOutOfBoundsException [in ProgramStructures]
ProgramStructuresFacts.StandardNames.ArrayStoreException [in ProgramStructures]
ProgramStructuresFacts.StandardNames.ClassCastException [in ProgramStructures]
ProgramStructuresFacts.StandardNames.IllegalMonitorStateException [in ProgramStructures]
ProgramStructuresFacts.StandardNames.NegativeArraySizeException [in ProgramStructures]
ProgramStructuresFacts.StandardNames.NullPointerException [in ProgramStructures]
ProgramStructuresFacts.StandardNames.Object [in ProgramStructures]
ProgramStructuresFacts.StandardNames.Throwable [in ProgramStructures]
PROGRAM_ASSERTIONS_W_CONSTRUCTORS.PgetInstructionIffNth [in ProgramAssertions]
PROGRAM_ASSERTIONS_W_CONSTRUCTORS.assertionsFromList [in ProgramAssertions]
PROGRAM_ASSERTIONS.getCodeAssertion [in ProgramAssertions]
PROGRAM_ASSERTIONS.TCodeAssertions [in ProgramAssertions]
PROGRAM_W_CONSTRUCTORS.PgetClassIffIn [in Program]
PROGRAM_W_CONSTRUCTORS.makeProgram [in Program]
PROGRAM_W_CONSTRUCTORS.PgetMethodIffIn [in Program]
PROGRAM_W_CONSTRUCTORS.PmakeClass_getClassName [in Program]
PROGRAM_W_CONSTRUCTORS.makeClass [in Program]
PROGRAM_W_CONSTRUCTORS.PcodeFromList_next_pc [in Program]
PROGRAM_W_CONSTRUCTORS.PcodeFromList_next [in Program]
PROGRAM_W_CONSTRUCTORS.PmakeMethod_methodBeginning [in Program]
PROGRAM_W_CONSTRUCTORS.PmakeMethod_getCode [in Program]
PROGRAM_W_CONSTRUCTORS.PmakeMethod_getSignature [in Program]
PROGRAM_W_CONSTRUCTORS.makeMethod [in Program]
PROGRAM_W_CONSTRUCTORS.PgetInstructionIffNth [in Program]
PROGRAM_W_CONSTRUCTORS.codeFromList [in Program]
PROGRAM_W_CONSTRUCTORS.PmakeOffset_pc [in Program]
PROGRAM_W_CONSTRUCTORS.PmakeOffset [in Program]
PROGRAM_W_CONSTRUCTORS.offsetFromPosition [in Program]
PROGRAM_W_CONSTRUCTORS.PpositionPc [in Program]
PROGRAM_W_CONSTRUCTORS.PpcPosition [in Program]
PROGRAM_W_CONSTRUCTORS.pcToPosition [in Program]
PROGRAM_W_CONSTRUCTORS.pcFromPosition [in Program]
PROGRAM_STRUCTURES.PnextVarSucc [in ProgramStructures]
PROGRAM_STRUCTURES.nextVar [in ProgramStructures]
PROGRAM_STRUCTURES.PnatVar [in ProgramStructures]
PROGRAM_STRUCTURES.PvarNat [in ProgramStructures]
PROGRAM_STRUCTURES.varToNat [in ProgramStructures]
PROGRAM_STRUCTURES.varFromNat [in ProgramStructures]
PROGRAM_STRUCTURES.PVar_eqDec [in ProgramStructures]
PROGRAM_STRUCTURES.TVar [in ProgramStructures]
PROGRAM.class_Throwable [in Program]
PROGRAM.class_Object [in Program]
PROGRAM.getClass [in Program]
PROGRAM.getClassInterfaces [in Program]
PROGRAM.getClassName [in Program]
PROGRAM.getDynamicFields [in Program]
PROGRAM.getEmptyObject [in Program]
PROGRAM.getField [in Program]
PROGRAM.getFieldName [in Program]
PROGRAM.getFieldType [in Program]
PROGRAM.getFieldVisibility [in Program]
PROGRAM.getInstruction [in Program]
PROGRAM.getMethod [in Program]
PROGRAM.getMethodBeginning [in Program]
PROGRAM.getMethodBodyFromProgram [in Program]
PROGRAM.getMethodCode [in Program]
PROGRAM.getMethodSignature [in Program]
PROGRAM.getMethodVisibility [in Program]
PROGRAM.handlerInScope [in Program]
PROGRAM.handlerTarget [in Program]
PROGRAM.handlerType [in Program]
PROGRAM.hasSuperFlag [in Program]
PROGRAM.isAbstractClass [in Program]
PROGRAM.isClassInit [in Program]
PROGRAM.isConstructor [in Program]
PROGRAM.isFieldFinal [in Program]
PROGRAM.isFieldStatic [in Program]
PROGRAM.isInterfaceClass [in Program]
PROGRAM.isMethodAbstract [in Program]
PROGRAM.isMethodStatic [in Program]
PROGRAM.isMethodSynchronized [in Program]
PROGRAM.methodExnHandlers [in Program]
PROGRAM.next [in Program]
PROGRAM.PabstractMethodNoBody [in Program]
PROGRAM.parentClass [in Program]
PROGRAM.PgetMethodBodyFromProgram [in Program]
PROGRAM.PObjectRoot [in Program]
PROGRAM.PparentClass [in Program]
PROGRAM.PparentClassDifferent [in Program]
PROGRAM.PparentClassWf [in Program]
PROGRAM.TClass [in Program]
PROGRAM.TCode [in Program]
PROGRAM.TField [in Program]
PROGRAM.THandler [in Program]
PROGRAM.TMethod [in Program]
PROGRAM.TProgram [in Program]

R

RuntimeStructuresImpl.PframeKConcretisationAbstraction [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PlocalStackKConcretisationAbstraction [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsEqEquiv [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKAbstractionConsistent [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKAbstractionConsistentSet [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKAbstractionConsistentSome [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKConcretisationAbstraction [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKConcretisationConsistent [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsKConcretisationConsistentSome [in RuntimeStructuresImpl]
RuntimeStructuresImpl.PvarsSetSameEquiv [in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsKAbstraction [in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsKConcretisation [in RuntimeStructuresImpl]
RUNTIME_STRUCTURES.PframeKConcretisationAbstraction [in RuntimeStructures]
RUNTIME_STRUCTURES.PlocalStackKConcretisationAbstraction [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKConcretisationAbstraction [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKConcretisationConsistentSome [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKConcretisationConsistent [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKAbstractionConsistentSet [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKAbstractionConsistentSome [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsKAbstractionConsistent [in RuntimeStructures]
RUNTIME_STRUCTURES.varsKConcretisation [in RuntimeStructures]
RUNTIME_STRUCTURES.varsKAbstraction [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsSetSameEquiv [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsEqEquiv [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsSetGetOther [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsSetGet [in RuntimeStructures]
RUNTIME_STRUCTURES.PvarsEmptyGet [in RuntimeStructures]
RUNTIME_STRUCTURES.varsSet [in RuntimeStructures]
RUNTIME_STRUCTURES.varsGet [in RuntimeStructures]
RUNTIME_STRUCTURES.varsEmpty [in RuntimeStructures]
RUNTIME_STRUCTURES.TVarsGeneric [in RuntimeStructures]

S

SEM_VAR.PVarsSetSame [in Sem_Var]
SEM_HEAP.PmakeMultiArray [in Sem_Heap]
SEM_HEAP.makeMultiArray [in Sem_Heap]

T

thid0 [in IAdd]
ThisMethod [in IAdd]

V

VALUES_AND_TYPES.PNotNullExists [in ValuesNTypes]
VALUES_AND_TYPES.null [in ValuesNTypes]
VALUES_AND_TYPES.PLoc_eqDec [in ValuesNTypes]
VALUES_AND_TYPES.TLoc [in ValuesNTypes]
VALUES_AND_TYPES.jump [in ValuesNTypes]
VALUES_AND_TYPES.TOffset [in ValuesNTypes]
VALUES_AND_TYPES.PPC_eqDec [in ValuesNTypes]
VALUES_AND_TYPES.TPC [in ValuesNTypes]
VALUES_AND_TYPES.PShortName_eqDec [in ValuesNTypes]
VALUES_AND_TYPES.TShortName [in ValuesNTypes]
VALUES_AND_TYPES.PClassName_eqDec [in ValuesNTypes]
VALUES_AND_TYPES.TClassName [in ValuesNTypes]

Constructor Index

A

ArithmeticOperators.BinOp_ushr [in ArithOps]
ArithmeticOperators.BinOp_shr [in ArithOps]
ArithmeticOperators.BinOp_shl [in ArithOps]
ArithmeticOperators.BinOp_or [in ArithOps]
ArithmeticOperators.BinOp_and [in ArithOps]
ArithmeticOperators.BinOp_xor [in ArithOps]
ArithmeticOperators.BinOp_rem [in ArithOps]
ArithmeticOperators.BinOp_div [in ArithOps]
ArithmeticOperators.BinOp_mul [in ArithOps]
ArithmeticOperators.BinOp_sub [in ArithOps]
ArithmeticOperators.BinOp_add [in ArithOps]
ArithmeticOperators.CastOp_d [in ArithOps]
ArithmeticOperators.CastOp_f [in ArithOps]
ArithmeticOperators.CastOp_l [in ArithOps]
ArithmeticOperators.CastOp_i [in ArithOps]
ArithmeticOperators.CastOp_s [in ArithOps]
ArithmeticOperators.CastOp_c [in ArithOps]
ArithmeticOperators.CastOp_b [in ArithOps]
ArithmeticOperators.CmpiOp_cmpg [in ArithOps]
ArithmeticOperators.CmpiOp_cmpl [in ArithOps]
ArithmeticOperators.CmpOp_gt [in ArithOps]
ArithmeticOperators.CmpOp_ge [in ArithOps]
ArithmeticOperators.CmpOp_lt [in ArithOps]
ArithmeticOperators.CmpOp_le [in ArithOps]
ArithmeticOperators.CmpOp_ne [in ArithOps]
ArithmeticOperators.CmpOp_eq [in ArithOps]
ArithmeticOperators.FCmpOp_fcmpl [in ArithOps]
ArithmeticOperators.FCmpOp_fcmpg [in ArithOps]
ArithmeticOperators.UnOp_neg [in ArithOps]
ArithmeticTypes.arithMake [in Arithmetic]

D

described_20 [in Loop]
described_19 [in Loop]
described_18 [in Loop]
described_17 [in Loop]
described_16 [in Loop]
described_15 [in Loop]
described_14 [in Loop]
described_13 [in Loop]
described_12 [in Loop]
described_11 [in Loop]
described_10 [in Loop]
described_9 [in Loop]
described_8 [in Loop]
described_7 [in Loop]
described_6 [in Loop]
described_5 [in Loop]
described_4 [in Loop]
described_3 [in Loop]
described_2 [in Loop]
described_1 [in Loop]
described_0 [in Loop]
DOUBLE_ARITHMETIC.CastInd_d2l [in Arithmetic]
DOUBLE_ARITHMETIC.CastInd_d2i [in Arithmetic]
DOUBLE_ARITHMETIC.CastInd_d2f [in Arithmetic]
DOUBLE_ARITHMETIC.CmpiInd_cmpl [in Arithmetic]
DOUBLE_ARITHMETIC.CmpiInd_cmpg [in Arithmetic]
DOUBLE_ARITHMETIC.CmpIInd_fcmpl [in Arithmetic]
DOUBLE_ARITHMETIC.CmpIInd_fcmpg [in Arithmetic]
DOUBLE_ARITHMETIC.BinOpInd_rem [in Arithmetic]
DOUBLE_ARITHMETIC.BinOpInd_div [in Arithmetic]
DOUBLE_ARITHMETIC.BinOpInd_mul [in Arithmetic]
DOUBLE_ARITHMETIC.BinOpInd_sub [in Arithmetic]
DOUBLE_ARITHMETIC.BinOpInd_add [in Arithmetic]
DOUBLE_ARITHMETIC.UnOpInd_neg [in Arithmetic]

F

FLOAT_ARITHMETIC.CastInd_f2l [in Arithmetic]
FLOAT_ARITHMETIC.CastInd_f2i [in Arithmetic]
FLOAT_ARITHMETIC.CastInd_f2d [in Arithmetic]
FLOAT_ARITHMETIC.CmpiInd_cmpl [in Arithmetic]
FLOAT_ARITHMETIC.CmpiInd_cmpg [in Arithmetic]
FLOAT_ARITHMETIC.BinOpInd_rem [in Arithmetic]
FLOAT_ARITHMETIC.BinOpInd_div [in Arithmetic]
FLOAT_ARITHMETIC.BinOpInd_mul [in Arithmetic]
FLOAT_ARITHMETIC.BinOpInd_sub [in Arithmetic]
FLOAT_ARITHMETIC.BinOpInd_add [in Arithmetic]
FLOAT_ARITHMETIC.UnOpInd_neg [in Arithmetic]
FMake.IsNaNIs [in FNumeric]
FNUMERIC.IsNaNIs [in FNumeric]

H

HEAP.HV_Array [in Heap]
HEAP.HV_Object [in Heap]
HEAP.HV_Empty [in Heap]
HEAP.MonitorLock_owner [in Heap]
HEAP.MonitorLock_free [in Heap]
HEAP.MonitorUnlock_owner [in Heap]
HEAP.MonitorUnlock_zero [in Heap]

I

INT_ARITHMETIC.CastInd_i2d [in Arithmetic]
INT_ARITHMETIC.CastInd_i2f [in Arithmetic]
INT_ARITHMETIC.CastInd_i2l [in Arithmetic]
INT_ARITHMETIC.CastInd_i2s [in Arithmetic]
INT_ARITHMETIC.CastInd_i2c [in Arithmetic]
INT_ARITHMETIC.CastInd_i2b [in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_gt [in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_ge [in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_lt [in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_le [in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_ne [in Arithmetic]
INT_ARITHMETIC.CmpValuesInd_eq [in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_gt [in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_ge [in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_lt [in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_le [in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_ne [in Arithmetic]
INT_ARITHMETIC.CmpZeroInd_eq [in Arithmetic]
INT_ARITHMETIC.BinOpInd_ushr [in Arithmetic]
INT_ARITHMETIC.BinOpInd_shr [in Arithmetic]
INT_ARITHMETIC.BinOpInd_shl [in Arithmetic]
INT_ARITHMETIC.BinOpInd_or [in Arithmetic]
INT_ARITHMETIC.BinOpInd_and [in Arithmetic]
INT_ARITHMETIC.BinOpInd_xor [in Arithmetic]
INT_ARITHMETIC.BinOpInd_rem0 [in Arithmetic]
INT_ARITHMETIC.BinOpInd_rem [in Arithmetic]
INT_ARITHMETIC.BinOpInd_div0 [in Arithmetic]
INT_ARITHMETIC.BinOpInd_div [in Arithmetic]
INT_ARITHMETIC.BinOpInd_mul [in Arithmetic]
INT_ARITHMETIC.BinOpInd_sub [in Arithmetic]
INT_ARITHMETIC.BinOpInd_add [in Arithmetic]
INT_ARITHMETIC.UnOpInd_neg [in Arithmetic]

L

ListPrefix_Rec [in Common]
ListPrefix_Nil [in Common]
LONG_ARITHMETIC.CastInd_l2f [in Arithmetic]
LONG_ARITHMETIC.CastInd_l2d [in Arithmetic]
LONG_ARITHMETIC.CastInd_l2i [in Arithmetic]
LONG_ARITHMETIC.CmpiInd_cmpl [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_ushr [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_shr [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_shl [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_or [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_and [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_xor [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_rem0 [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_rem [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_div0 [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_div [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_mul [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_sub [in Arithmetic]
LONG_ARITHMETIC.BinOpInd_add [in Arithmetic]
LONG_ARITHMETIC.UnOpInd_neg [in Arithmetic]

O

One [in Common]

P

PROGRAM.CI_Lookupswitch [in Program]
PROGRAM.CI_Tableswitch [in Program]
PROGRAM.CI_Cmp [in Program]
PROGRAM.CI_If [in Program]
PROGRAM.CI_Goto [in Program]
PROGRAM.FI_Ret [in Program]
PROGRAM.FI_Jsr [in Program]
PROGRAM.FI_Cond [in Program]
PROGRAM.FI_Var [in Program]
PROGRAM.FI_Stackop [in Program]
PROGRAM.HI_Monitor [in Program]
PROGRAM.HI_New [in Program]
PROGRAM.HI_Put [in Program]
PROGRAM.HI_Get [in Program]
PROGRAM.InvokeInterface [in Program]
PROGRAM.InvokeSpecial [in Program]
PROGRAM.InvokeStatic [in Program]
PROGRAM.InvokeVirtual [in Program]
PROGRAM.I_Throw [in Program]
PROGRAM.I_Return [in Program]
PROGRAM.I_Invoke [in Program]
PROGRAM.I_Heap [in Program]
PROGRAM.I_Frame [in Program]
PROGRAM.Op_Lock [in Program]
PROGRAM.Op_Unlock [in Program]
PROGRAM.Op_newmultiarray [in Program]
PROGRAM.Op_newarray_ref [in Program]
PROGRAM.Op_newarray [in Program]
PROGRAM.Op_newobject [in Program]
PROGRAM.Op_putarray [in Program]
PROGRAM.Op_putstatic [in Program]
PROGRAM.Op_putfield [in Program]
PROGRAM.Op_instanceof [in Program]
PROGRAM.Op_checkcast [in Program]
PROGRAM.Op_array_length [in Program]
PROGRAM.Op_getarray [in Program]
PROGRAM.Op_getstatic [in Program]
PROGRAM.Op_getfield [in Program]
PROGRAM.Op_swap [in Program]
PROGRAM.Op_pop2 [in Program]
PROGRAM.Op_pop [in Program]
PROGRAM.Op_dup2_x2 [in Program]
PROGRAM.Op_dup2_x1 [in Program]
PROGRAM.Op_dup2 [in Program]
PROGRAM.Op_dup_x2 [in Program]
PROGRAM.Op_dup_x1 [in Program]
PROGRAM.Op_dup [in Program]
PROGRAM.Op_nop [in Program]
PROGRAM.Package [in Program]
PROGRAM.Private [in Program]
PROGRAM.Protected [in Program]
PROGRAM.Public [in Program]
PROGRAM.SI_Cmpi [in Program]
PROGRAM.SI_Cast [in Program]
PROGRAM.SI_Binop [in Program]
PROGRAM.SI_Unop [in Program]
PROGRAM.SI_Const [in Program]
PROGRAM.SI_Generic [in Program]
PROGRAM.ValidHandler_Cons [in Program]
PROGRAM.ValidHandler_Found [in Program]
PROGRAM.ValidHandler_Nil [in Program]
PROGRAM.VI_Inc [in Program]
PROGRAM.VI_Store [in Program]
PROGRAM.VI_Load [in Program]

R

REF_ARITHMETIC.CmpValuesInd_nef [in Arithmetic]
REF_ARITHMETIC.CmpValuesInd_net [in Arithmetic]
REF_ARITHMETIC.CmpValuesInd_eqf [in Arithmetic]
REF_ARITHMETIC.CmpValuesInd_eqt [in Arithmetic]
REF_ARITHMETIC.CmpZeroInd_notnullf [in Arithmetic]
REF_ARITHMETIC.CmpZeroInd_notnullt [in Arithmetic]
REF_ARITHMETIC.CmpZeroInd_nullf [in Arithmetic]
REF_ARITHMETIC.CmpZeroInd_nullt [in Arithmetic]
RuntimeStructuresFacts.initVars_two [in RuntimeStructures]
RuntimeStructuresFacts.initVars_one [in RuntimeStructures]
RuntimeStructuresFacts.InitVars_nil [in RuntimeStructures]
RuntimeStructuresFacts.Prefix_cons [in RuntimeStructures]
RuntimeStructuresFacts.Prefix_nil [in RuntimeStructures]
RuntimeStructuresImpl.cmMake [in RuntimeStructuresImpl]
RuntimeStructuresImpl.Exception [in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKShadowMake [in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameMake [in RuntimeStructuresImpl]
RuntimeStructuresImpl.jvmMake [in RuntimeStructuresImpl]
RuntimeStructuresImpl.Result [in RuntimeStructuresImpl]
RuntimeStructuresImpl.threadMake [in RuntimeStructuresImpl]
RUNTIME_STRUCTURES.Exception [in RuntimeStructures]
RUNTIME_STRUCTURES.Result [in RuntimeStructures]
RUNTIME_STRUCTURES.jvmMake [in RuntimeStructures]
RUNTIME_STRUCTURES.threadMake [in RuntimeStructures]
RUNTIME_STRUCTURES.cmMake [in RuntimeStructures]
RUNTIME_STRUCTURES.frameKShadowMake [in RuntimeStructures]
RUNTIME_STRUCTURES.frameMake [in RuntimeStructures]

S

SEMANTICS.OneThreadAndHeapChanged_onlyone [in Semantics]
SEMANTICS.OneThreadAndHeapChanged_other [in Semantics]
SEMANTICS.OneThreadAndHeapChanged_this [in Semantics]
SEMANTICS.OneThreadChanged_other [in Semantics]
SEMANTICS.OneThreadChanged_this [in Semantics]
SEMANTICS.OneThreadChanged1_onlyone [in Semantics]
SEMANTICS.selectedThread_onlyone [in Semantics]
SEMANTICS.SelectedThread_other [in Semantics]
SEMANTICS.SelectedThread_this [in Semantics]
SEMANTICS.SemInstr_athrow_null [in Semantics]
SEMANTICS.SemInstr_athrow [in Semantics]
SEMANTICS.SemInstr_return_exn [in Semantics]
SEMANTICS.SemInstr_return [in Semantics]
SEMANTICS.SemInstr_invoke_exn [in Semantics]
SEMANTICS.SemInstr_invoke [in Semantics]
SEMANTICS.SemInstr_heap_exn [in Semantics]
SEMANTICS.SemInstr_heap [in Semantics]
SEMANTICS.SemInstr_frame_exn [in Semantics]
SEMANTICS.SemInstr_frame [in Semantics]
SEMANTICS.SemThrow_null [in Semantics]
SEMANTICS.SemThrow_ok [in Semantics]
SEMANTICS.StepInThread_uncaught_exn [in Semantics]
SEMANTICS.StepInThread_uncaught [in Semantics]
SEMANTICS.StepInThread_caught [in Semantics]
SEMANTICS.StepInThread_instruction_exn [in Semantics]
SEMANTICS.StepInThread_instruction_ok [in Semantics]
SEMANTICS.Step_thread [in Semantics]
SEM_VAR.StaticSemVar_iinc [in Sem_Var]
SEM_VAR.StaticSemVar_store_2 [in Sem_Var]
SEM_VAR.StaticSemVar_store_1 [in Sem_Var]
SEM_VAR.StaticSemVar_load_2 [in Sem_Var]
SEM_VAR.StaticSemVar_load_1 [in Sem_Var]
SEM_VAR.SemVar_iinc [in Sem_Var]
SEM_VAR.SemVar_store_2 [in Sem_Var]
SEM_VAR.SemVar_store_1 [in Sem_Var]
SEM_VAR.SemVar_load_2 [in Sem_Var]
SEM_VAR.SemVar_load_1 [in Sem_Var]
SEM_VAR.IsStorable_Double [in Sem_Var]
SEM_VAR.IsStorable_Long [in Sem_Var]
SEM_VAR.IsStorable_Float [in Sem_Var]
SEM_VAR.IsStorable_Int [in Sem_Var]
SEM_VAR.IsStorable_Addr [in Sem_Var]
SEM_VAR.IsStorable_Ref [in Sem_Var]
SEM_VAR.IsLoadable_Double [in Sem_Var]
SEM_VAR.IsLoadable_Long [in Sem_Var]
SEM_VAR.IsLoadable_Float [in Sem_Var]
SEM_VAR.IsLoadable_Int [in Sem_Var]
SEM_VAR.IsLoadable_Ref [in Sem_Var]
SEM_HEAP.SemHeap_monitor [in Sem_Heap]
SEM_HEAP.SemHeap_new [in Sem_Heap]
SEM_HEAP.SemHeap_put [in Sem_Heap]
SEM_HEAP.SemHeap_get [in Sem_Heap]
SEM_HEAP.SemNew_multiarray_negativeSize [in Sem_Heap]
SEM_HEAP.SemNew_multiarray [in Sem_Heap]
SEM_HEAP.SemNew_refarray_neg [in Sem_Heap]
SEM_HEAP.SemNew_refarray [in Sem_Heap]
SEM_HEAP.SemNew_array_neg [in Sem_Heap]
SEM_HEAP.SemNew_array [in Sem_Heap]
SEM_HEAP.SemNew_object [in Sem_Heap]
SEM_HEAP.MadeMultiArray_end [in Sem_Heap]
SEM_HEAP.MadeMultiArray_step [in Sem_Heap]
SEM_HEAP.SemPut_array_indexOutOfBounds [in Sem_Heap]
SEM_HEAP.SemPut_array_null [in Sem_Heap]
SEM_HEAP.SemPut_array [in Sem_Heap]
SEM_HEAP.SemPut_putfield_null [in Sem_Heap]
SEM_HEAP.SemPut_putfield [in Sem_Heap]
SEM_HEAP.SemPut_putstatic [in Sem_Heap]
SEM_HEAP.SemGet_checkCast_null [in Sem_Heap]
SEM_HEAP.SemGet_checkCast_false [in Sem_Heap]
SEM_HEAP.SemGet_checkCast_true [in Sem_Heap]
SEM_HEAP.SemGet_instanceOf_null [in Sem_Heap]
SEM_HEAP.SemGet_instanceOf_false [in Sem_Heap]
SEM_HEAP.SemGet_instanceOf_true [in Sem_Heap]
SEM_HEAP.SemGet_arrayLength_null [in Sem_Heap]
SEM_HEAP.SemGet_arrayLength [in Sem_Heap]
SEM_HEAP.SemGet_array_out [in Sem_Heap]
SEM_HEAP.SemGet_array_null [in Sem_Heap]
SEM_HEAP.SemGet_array [in Sem_Heap]
SEM_HEAP.SemGet_getfield_null [in Sem_Heap]
SEM_HEAP.SemGet_getfield [in Sem_Heap]
SEM_HEAP.SemGet_getstatic [in Sem_Heap]
SEM_STACKOP.StaticSemStack_CastOp [in Sem_Stackop]
SEM_STACKOP.StaticSemStack_Cmpi [in Sem_Stackop]
SEM_STACKOP.StaticSemStack_BinOp_Exn [in Sem_Stackop]
SEM_STACKOP.StaticSemStack_BinOp [in Sem_Stackop]
SEM_STACKOP.StaticSemStack_UnOp [in Sem_Stackop]
SEM_STACKOP.StaticSemStack_Const [in Sem_Stackop]
SEM_STACKOP.StaticSemStack_Generic [in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_d [in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_f [in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_l [in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_i [in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_s [in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_c [in Sem_Stackop]
SEM_STACKOP.CastOpStaticSem_b [in Sem_Stackop]
SEM_STACKOP.CmpiStaticSem_cmpg [in Sem_Stackop]
SEM_STACKOP.CmpiStaticSem_cmpl [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSemNoResult_rem [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSemNoResult_div [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_ushr [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_shr [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_shl [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_or [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_and [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_xor [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_rem [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_div [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_mul [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_sub [in Sem_Stackop]
SEM_STACKOP.BinOpStaticSem_add [in Sem_Stackop]
SEM_STACKOP.UnOpStaticSem_add [in Sem_Stackop]
SEM_STACKOP.SemStack_Cast [in Sem_Stackop]
SEM_STACKOP.SemStack_Cmpi [in Sem_Stackop]
SEM_STACKOP.SemStack_BinOp_ArithmeticException [in Sem_Stackop]
SEM_STACKOP.SemStack_BinOp [in Sem_Stackop]
SEM_STACKOP.SemStack_UnOp [in Sem_Stackop]
SEM_STACKOP.SemStack_Const [in Sem_Stackop]
SEM_STACKOP.SemStack_Generic [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_swap [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_pop2_form2 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_pop2_form1 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_pop [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x2_form4 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x2_form3 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x2_form2 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x2_form1 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x1_form2 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_x1_form1 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_form2 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup2_form1 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup_x2_form2 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup_x2_form1 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup_x1 [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_dup [in Sem_Stackop]
SEM_STACKOP.SemStackGeneric_nop [in Sem_Stackop]
SEM_CALL.SemReturnValue [in Sem_Call]
SEM_CALL.SemReturnVoid [in Sem_Call]
SEM_CALL.MU_NotSychnronized [in Sem_Call]
SEM_CALL.MU_Synchronized [in Sem_Call]
SEM_CALL.SemInvokeSpecial [in Sem_Call]
SEM_CALL.SemInvokeInterface [in Sem_Call]
SEM_CALL.SemInvokeVirtual [in Sem_Call]
SEM_CALL.SemInvokeStatic [in Sem_Call]
SEM_CALL.CallInstance_notFound [in Sem_Call]
SEM_CALL.CallInstance_null [in Sem_Call]
SEM_CALL.CallInstance_ok [in Sem_Call]
SEM_CALL.CallStatic_ok [in Sem_Call]
SEM_CALL.ML_NotSychnronized [in Sem_Call]
SEM_CALL.ML_Synchronized [in Sem_Call]
SEM_CALL.InvokeSpecial_Virtual [in Sem_Call]
SEM_CALL.InvokeSpecial_Direct [in Sem_Call]
SEM_CALL.GetMethod_virtual [in Sem_Call]
SEM_CALL.GetMethod_direct [in Sem_Call]
SEM_CALL.MLM_Virtual [in Sem_Call]
SEM_CALL.MLM_Direct [in Sem_Call]
SEM_CALL.LookupMethod_fail [in Sem_Call]
SEM_CALL.LookupMethod_step [in Sem_Call]
SEM_CALL.LookupMethod_found [in Sem_Call]
SEM_MONITOR.SemMonitor_null [in Sem_Monitor]
SEM_MONITOR.SemMonitor_unlock_badThd [in Sem_Monitor]
SEM_MONITOR.SemMonitor_unlock [in Sem_Monitor]
SEM_MONITOR.SemMonitor_lock [in Sem_Monitor]
SEM_FRAME.StepFrame_one [in Sem_Frame]
SEM_FRAME.StaticSemFrame_ret [in Sem_Frame]
SEM_FRAME.StaticSemFrame_jsr [in Sem_Frame]
SEM_FRAME.StaticSemFrame_cond [in Sem_Frame]
SEM_FRAME.StaticSemFrame_var [in Sem_Frame]
SEM_FRAME.StaticSemFrame_stackop_exn [in Sem_Frame]
SEM_FRAME.StaticSemFrame_stackop [in Sem_Frame]
SEM_FRAME.SemFrame_ret [in Sem_Frame]
SEM_FRAME.SemFrame_jsr [in Sem_Frame]
SEM_FRAME.SemFrame_cond [in Sem_Frame]
SEM_FRAME.SemFrame_var [in Sem_Frame]
SEM_FRAME.SemFrame_stackop_exn [in Sem_Frame]
SEM_FRAME.SemFrame_stackop [in Sem_Frame]
SEM_COND.StaticSemCond_lookupswitch_default [in Sem_Cond]
SEM_COND.StaticSemCond_lookupswitch_found [in Sem_Cond]
SEM_COND.StaticSemCond_tableswitch_default [in Sem_Cond]
SEM_COND.StaticSemCond_tableswitch_found [in Sem_Cond]
SEM_COND.StaticSemCond_cmp_false [in Sem_Cond]
SEM_COND.StaticSemCond_cmp_true [in Sem_Cond]
SEM_COND.StaticSemCond_if_false [in Sem_Cond]
SEM_COND.StaticSemCond_if_true [in Sem_Cond]
SEM_COND.StaticSemCond_goto [in Sem_Cond]
SEM_COND.CmpStaticSem_Gt [in Sem_Cond]
SEM_COND.CmpStaticSem_Ge [in Sem_Cond]
SEM_COND.CmpStaticSem_Lt [in Sem_Cond]
SEM_COND.CmpStaticSem_Le [in Sem_Cond]
SEM_COND.CmpStaticSem_Ne [in Sem_Cond]
SEM_COND.CmpStaticSem_Eq [in Sem_Cond]
SEM_COND.IfStaticSem_Gt [in Sem_Cond]
SEM_COND.IfStaticSem_Ge [in Sem_Cond]
SEM_COND.IfStaticSem_Lt [in Sem_Cond]
SEM_COND.IfStaticSem_Le [in Sem_Cond]
SEM_COND.IfStaticSem_Ne [in Sem_Cond]
SEM_COND.IfStaticSem_Eq [in Sem_Cond]
SEM_COND.SemCond_lookupswitch_default [in Sem_Cond]
SEM_COND.SemCond_lookupswitch_found [in Sem_Cond]
SEM_COND.SemCond_tableswitch_default [in Sem_Cond]
SEM_COND.SemCond_tableswitch_found [in Sem_Cond]
SEM_COND.SemCond_cmp_false [in Sem_Cond]
SEM_COND.SemCond_cmp_true [in Sem_Cond]
SEM_COND.SemCond_if_false [in Sem_Cond]
SEM_COND.SemCond_if_true [in Sem_Cond]
SEM_COND.SemCond_goto [in Sem_Cond]
stack_values_cons [in Loop_Assertions]
stack_values_nil [in Loop_Assertions]
stack_values_cons [in Loop]
stack_values_nil [in Loop]

T

Two [in Common]

V

VALUES_AND_TYPES.IsCatVIK_Double [in ValuesNTypes]
VALUES_AND_TYPES.IsCatVIK_Long [in ValuesNTypes]
VALUES_AND_TYPES.IsCatVIK_Float [in ValuesNTypes]
VALUES_AND_TYPES.IsCatVIK_Int [in ValuesNTypes]
VALUES_AND_TYPES.IsCatVIK_Ref [in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Double [in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Long [in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Float [in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Int [in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Addr [in ValuesNTypes]
VALUES_AND_TYPES.IsCat_Ref [in ValuesNTypes]
VALUES_AND_TYPES.cat2 [in ValuesNTypes]
VALUES_AND_TYPES.cat1 [in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Double [in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Long [in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Float [in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Int [in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Addr [in ValuesNTypes]
VALUES_AND_TYPES.VVKMap_Ref [in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Double [in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Long [in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Float [in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Int [in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Addr [in ValuesNTypes]
VALUES_AND_TYPES.VVMap_Ref [in ValuesNTypes]
VALUES_AND_TYPES.AIKDouble [in ValuesNTypes]
VALUES_AND_TYPES.AIKLong [in ValuesNTypes]
VALUES_AND_TYPES.AIKFloat [in ValuesNTypes]
VALUES_AND_TYPES.AIKInt [in ValuesNTypes]
VALUES_AND_TYPES.AIKShort [in ValuesNTypes]
VALUES_AND_TYPES.AIKByteBool [in ValuesNTypes]
VALUES_AND_TYPES.AIKChar [in ValuesNTypes]
VALUES_AND_TYPES.AIKRef [in ValuesNTypes]
VALUES_AND_TYPES.VIKDouble [in ValuesNTypes]
VALUES_AND_TYPES.VIKLong [in ValuesNTypes]
VALUES_AND_TYPES.VIKFloat [in ValuesNTypes]
VALUES_AND_TYPES.VIKInt [in ValuesNTypes]
VALUES_AND_TYPES.VIKRef [in ValuesNTypes]
VALUES_AND_TYPES.VKDouble2 [in ValuesNTypes]
VALUES_AND_TYPES.VKDouble1 [in ValuesNTypes]
VALUES_AND_TYPES.VKLong2 [in ValuesNTypes]
VALUES_AND_TYPES.VKLong1 [in ValuesNTypes]
VALUES_AND_TYPES.VKFloat [in ValuesNTypes]
VALUES_AND_TYPES.VKInt [in ValuesNTypes]
VALUES_AND_TYPES.VKAddr [in ValuesNTypes]
VALUES_AND_TYPES.VKRef [in ValuesNTypes]
VALUES_AND_TYPES.KDouble [in ValuesNTypes]
VALUES_AND_TYPES.KLong [in ValuesNTypes]
VALUES_AND_TYPES.KFloat [in ValuesNTypes]
VALUES_AND_TYPES.KInt [in ValuesNTypes]
VALUES_AND_TYPES.KAddr [in ValuesNTypes]
VALUES_AND_TYPES.KRef [in ValuesNTypes]
VALUES_AND_TYPES.BTDouble [in ValuesNTypes]
VALUES_AND_TYPES.BTLong [in ValuesNTypes]
VALUES_AND_TYPES.BTFloat [in ValuesNTypes]
VALUES_AND_TYPES.BTChar [in ValuesNTypes]
VALUES_AND_TYPES.BTInt [in ValuesNTypes]
VALUES_AND_TYPES.BTShort [in ValuesNTypes]
VALUES_AND_TYPES.BTBool [in ValuesNTypes]
VALUES_AND_TYPES.BTByte [in ValuesNTypes]
VALUES_AND_TYPES.RTArray [in ValuesNTypes]
VALUES_AND_TYPES.RTObject [in ValuesNTypes]
VALUES_AND_TYPES.BaseType [in ValuesNTypes]
VALUES_AND_TYPES.ReferenceType [in ValuesNTypes]
VALUES_AND_TYPES.VADouble [in ValuesNTypes]
VALUES_AND_TYPES.VALong [in ValuesNTypes]
VALUES_AND_TYPES.VAFloat [in ValuesNTypes]
VALUES_AND_TYPES.VAInt [in ValuesNTypes]
VALUES_AND_TYPES.VAShort [in ValuesNTypes]
VALUES_AND_TYPES.VAByte [in ValuesNTypes]
VALUES_AND_TYPES.VABool [in ValuesNTypes]
VALUES_AND_TYPES.VAChar [in ValuesNTypes]
VALUES_AND_TYPES.VARef [in ValuesNTypes]
VALUES_AND_TYPES.VVDouble2 [in ValuesNTypes]
VALUES_AND_TYPES.VVDouble1 [in ValuesNTypes]
VALUES_AND_TYPES.VVLong2 [in ValuesNTypes]
VALUES_AND_TYPES.VVLong1 [in ValuesNTypes]
VALUES_AND_TYPES.VVFloat [in ValuesNTypes]
VALUES_AND_TYPES.VVInt [in ValuesNTypes]
VALUES_AND_TYPES.VVAddr [in ValuesNTypes]
VALUES_AND_TYPES.VVRef [in ValuesNTypes]
VALUES_AND_TYPES.VDouble [in ValuesNTypes]
VALUES_AND_TYPES.VLong [in ValuesNTypes]
VALUES_AND_TYPES.VFloat [in ValuesNTypes]
VALUES_AND_TYPES.VInt [in ValuesNTypes]
VALUES_AND_TYPES.VAddr [in ValuesNTypes]
VALUES_AND_TYPES.VRef [in ValuesNTypes]
var_value_def [in Loop_Assertions]
var_value_def [in Loop]

Inductive Index

A

ADDR_ARITHMETIC.castInd [in Arithmetic]
ADDR_ARITHMETIC.cmpiInd [in Arithmetic]
ADDR_ARITHMETIC.cmpValuesInd [in Arithmetic]
ADDR_ARITHMETIC.cmpZeroInd [in Arithmetic]
ADDR_ARITHMETIC.binOpInd [in Arithmetic]
ADDR_ARITHMETIC.unOpInd [in Arithmetic]
ArithmeticOperators.TBinOp [in ArithOps]
ArithmeticOperators.TCastOp [in ArithOps]
ArithmeticOperators.TCmpAOp [in ArithOps]
ArithmeticOperators.TCmpiOp [in ArithOps]
ArithmeticOperators.TCmpOp [in ArithOps]
ArithmeticOperators.TUnOp [in ArithOps]

D

described [in Loop]
DOUBLE_ARITHMETIC.castInd [in Arithmetic]
DOUBLE_ARITHMETIC.cmpiInd [in Arithmetic]
DOUBLE_ARITHMETIC.cmpValuesInd [in Arithmetic]
DOUBLE_ARITHMETIC.cmpZeroInd [in Arithmetic]
DOUBLE_ARITHMETIC.CmpIInd [in Arithmetic]
DOUBLE_ARITHMETIC.binOpInd [in Arithmetic]
DOUBLE_ARITHMETIC.unOpInd [in Arithmetic]

F

FLOAT_ARITHMETIC.castInd [in Arithmetic]
FLOAT_ARITHMETIC.cmpiInd [in Arithmetic]
FLOAT_ARITHMETIC.cmpValuesInd [in Arithmetic]
FLOAT_ARITHMETIC.cmpZeroInd [in Arithmetic]
FLOAT_ARITHMETIC.binOpInd [in Arithmetic]
FLOAT_ARITHMETIC.unOpInd [in Arithmetic]
FMake.isNaN [in FNumeric]
FNUMERIC.isNaN [in FNumeric]

H

HEAP.MonitorLock [in Heap]
HEAP.MonitorUnlock [in Heap]
HEAP.THeapValue [in Heap]

I

INT_ARITHMETIC.castInd [in Arithmetic]
INT_ARITHMETIC.cmpiInd [in Arithmetic]
INT_ARITHMETIC.cmpValuesInd [in Arithmetic]
INT_ARITHMETIC.cmpZeroInd [in Arithmetic]
INT_ARITHMETIC.binOpInd [in Arithmetic]
INT_ARITHMETIC.unOpInd [in Arithmetic]

L

ListPrefix [in Common]
LONG_ARITHMETIC.castInd [in Arithmetic]
LONG_ARITHMETIC.cmpiInd [in Arithmetic]
LONG_ARITHMETIC.cmpValuesInd [in Arithmetic]
LONG_ARITHMETIC.cmpZeroInd [in Arithmetic]
LONG_ARITHMETIC.binOpInd [in Arithmetic]
LONG_ARITHMETIC.unOpInd [in Arithmetic]

P

PROGRAM.TCondInstr [in Program]
PROGRAM.TFrameInstr [in Program]
PROGRAM.TGenericOp [in Program]
PROGRAM.TGetOp [in Program]
PROGRAM.THeapInstr [in Program]
PROGRAM.TInstruction [in Program]
PROGRAM.TInvocationMode [in Program]
PROGRAM.TMonitorOp [in Program]
PROGRAM.TNewOp [in Program]
PROGRAM.TPutOp [in Program]
PROGRAM.TStackInstr [in Program]
PROGRAM.TVarInstr [in Program]
PROGRAM.TVisibility [in Program]
PROGRAM.validHandlerInd [in Program]

R

REF_ARITHMETIC.castInd [in Arithmetic]
REF_ARITHMETIC.cmpiInd [in Arithmetic]
REF_ARITHMETIC.cmpValuesInd [in Arithmetic]
REF_ARITHMETIC.cmpZeroInd [in Arithmetic]
REF_ARITHMETIC.binOpInd [in Arithmetic]
REF_ARITHMETIC.unOpInd [in Arithmetic]
RuntimeStructuresFacts.initVarsInd [in RuntimeStructures]
RuntimeStructuresFacts.prefixInd [in RuntimeStructures]
RuntimeStructuresImpl.TResultOrException [in RuntimeStructuresImpl]
RUNTIME_STRUCTURES.TResultOrException [in RuntimeStructures]

S

SEMANTICS.oneThreadAndHeapChanged [in Semantics]
SEMANTICS.oneThreadAndHeapChanged1 [in Semantics]
SEMANTICS.oneThreadChanged [in Semantics]
SEMANTICS.oneThreadChanged1 [in Semantics]
SEMANTICS.selectedThread [in Semantics]
SEMANTICS.selectedThread1 [in Semantics]
SEMANTICS.semInstr [in Semantics]
SEMANTICS.semThrow [in Semantics]
SEMANTICS.step [in Semantics]
SEMANTICS.stepInThread [in Semantics]
SEM_VAR.staticSemVar [in Sem_Var]
SEM_VAR.semVar [in Sem_Var]
SEM_VAR.isStorable [in Sem_Var]
SEM_VAR.isLoadable [in Sem_Var]
SEM_HEAP.semHeap [in Sem_Heap]
SEM_HEAP.semNew [in Sem_Heap]
SEM_HEAP.madeMultiArrayInd [in Sem_Heap]
SEM_HEAP.semPut [in Sem_Heap]
SEM_HEAP.semGet [in Sem_Heap]
SEM_STACKOP.staticSemStack [in Sem_Stackop]
SEM_STACKOP.staticSemStackCastOp [in Sem_Stackop]
SEM_STACKOP.staticSemStackCmpi [in Sem_Stackop]
SEM_STACKOP.staticSemStackBinOp_NoResult [in Sem_Stackop]
SEM_STACKOP.staticSemStackBinOp [in Sem_Stackop]
SEM_STACKOP.staticSemStackUnOp [in Sem_Stackop]
SEM_STACKOP.semStack [in Sem_Stackop]
SEM_STACKOP.semStackGeneric [in Sem_Stackop]
SEM_CALL.semReturn [in Sem_Call]
SEM_CALL.maybeUnlock [in Sem_Call]
SEM_CALL.semInvoke [in Sem_Call]
SEM_CALL.callInstanceMethod [in Sem_Call]
SEM_CALL.callStaticMethod [in Sem_Call]
SEM_CALL.maybeLock [in Sem_Call]
SEM_CALL.invokeSpecialMode [in Sem_Call]
SEM_CALL.getMethodToCall [in Sem_Call]
SEM_CALL.TMethodLookupMode [in Sem_Call]
SEM_CALL.lookupMethodInd [in Sem_Call]
SEM_MONITOR.semMonitor [in Sem_Monitor]
SEM_FRAME.stepFrame [in Sem_Frame]
SEM_FRAME.staticSemFrame [in Sem_Frame]
SEM_FRAME.semFrame [in Sem_Frame]
SEM_COND.staticSemCond [in Sem_Cond]
SEM_COND.staticSemCondCmp [in Sem_Cond]
SEM_COND.staticSemCondIf [in Sem_Cond]
SEM_COND.semCond [in Sem_Cond]
stack_values_ind [in Loop_Assertions]
stack_values_ind [in Loop]

T

TOneOrTwo [in Common]

V

VALUES_AND_TYPES.isCatVIK [in ValuesNTypes]
VALUES_AND_TYPES.isCat [in ValuesNTypes]
VALUES_AND_TYPES.TValueCategory [in ValuesNTypes]
VALUES_AND_TYPES.ValVarKindMapping [in ValuesNTypes]
VALUES_AND_TYPES.ValVarMapping [in ValuesNTypes]
VALUES_AND_TYPES.TArrayIKind [in ValuesNTypes]
VALUES_AND_TYPES.TVarIKind [in ValuesNTypes]
VALUES_AND_TYPES.TVarKind [in ValuesNTypes]
VALUES_AND_TYPES.TKind [in ValuesNTypes]
VALUES_AND_TYPES.TBaseType [in ValuesNTypes]
VALUES_AND_TYPES.TReferenceType [in ValuesNTypes]
VALUES_AND_TYPES.TType [in ValuesNTypes]
VALUES_AND_TYPES.TAValue [in ValuesNTypes]
VALUES_AND_TYPES.TVarValue [in ValuesNTypes]
VALUES_AND_TYPES.TValue [in ValuesNTypes]
var_value [in Loop_Assertions]
var_value [in Loop]

Projection Index

A

ArithmeticTypes.arithBinOp [in Arithmetic]
ArithmeticTypes.arithCast [in Arithmetic]
ArithmeticTypes.arithCmpi [in Arithmetic]
ArithmeticTypes.arithCmpValues [in Arithmetic]
ArithmeticTypes.arithCmpZero [in Arithmetic]
ArithmeticTypes.arithUnOp [in Arithmetic]

R

RuntimeStructuresImpl.cmCtxObjectLoc [in RuntimeStructuresImpl]
RuntimeStructuresImpl.cmCurrentClass [in RuntimeStructuresImpl]
RuntimeStructuresImpl.cmQName [in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameGetLocalStack [in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameGetPC [in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameGetVars [in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKShadowGetLocalStack [in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKShadowGetPC [in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKShadowGetVars [in RuntimeStructuresImpl]
RuntimeStructuresImpl.jvmGetHeap [in RuntimeStructuresImpl]
RuntimeStructuresImpl.jvmGetThreads [in RuntimeStructuresImpl]
RuntimeStructuresImpl.threadGetCallStack [in RuntimeStructuresImpl]
RuntimeStructuresImpl.threadGetEvalState [in RuntimeStructuresImpl]
RuntimeStructuresImpl.threadGetId [in RuntimeStructuresImpl]
RUNTIME_STRUCTURES.jvmGetThreads [in RuntimeStructures]
RUNTIME_STRUCTURES.jvmGetHeap [in RuntimeStructures]
RUNTIME_STRUCTURES.threadGetCallStack [in RuntimeStructures]
RUNTIME_STRUCTURES.threadGetEvalState [in RuntimeStructures]
RUNTIME_STRUCTURES.threadGetId [in RuntimeStructures]
RUNTIME_STRUCTURES.cmCtxObjectLoc [in RuntimeStructures]
RUNTIME_STRUCTURES.cmCurrentClass [in RuntimeStructures]
RUNTIME_STRUCTURES.cmQName [in RuntimeStructures]
RUNTIME_STRUCTURES.frameKShadowGetPC [in RuntimeStructures]
RUNTIME_STRUCTURES.frameKShadowGetLocalStack [in RuntimeStructures]
RUNTIME_STRUCTURES.frameKShadowGetVars [in RuntimeStructures]
RUNTIME_STRUCTURES.frameGetPC [in RuntimeStructures]
RUNTIME_STRUCTURES.frameGetLocalStack [in RuntimeStructures]
RUNTIME_STRUCTURES.frameGetVars [in RuntimeStructures]

Section Index

D

Dec [in Common]

E

EqDec [in Common]

F

Functions [in Common]

H

HEAP.HeapSpec [in Heap]

L

Lists [in Common]
LoopExample [in Loop_Assertions]
LoopExample [in Loop]

M

MONOLITIC_HEAP.MonoHeapSpec [in Heap]

R

RuntimeStructuresImpl.GenericStackDefinition [in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition [in RuntimeStructuresImpl]
RuntimeStructuresImpl.GenericVarsDefinition.VarsProperties [in RuntimeStructuresImpl]
RUNTIME_STRUCTURES.GenericStackDefinition [in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition.VarsProperties [in RuntimeStructures]
RUNTIME_STRUCTURES.GenericVarsDefinition [in RuntimeStructures]

S

SEM_STACKOP.GenericOps [in Sem_Stackop]

V

VALUES_AND_TYPES.NumericConversions [in ValuesNTypes]

Definition Index

A

ADDR_ARITHMETIC.arithmetic [in Arithmetic]
ADDR_ARITHMETIC.castArithmetic [in Arithmetic]
ADDR_ARITHMETIC.cmpiArithmetic [in Arithmetic]
ADDR_ARITHMETIC.cmpValuesArithmetic [in Arithmetic]
ADDR_ARITHMETIC.cmpZeroArithmetic [in Arithmetic]
ADDR_ARITHMETIC.binOpArithmetic [in Arithmetic]
ADDR_ARITHMETIC.unOpArithmetic [in Arithmetic]
ARITHMETICS.arithmeticForKind [in Arithmetic]
ARITHMETICS.kindOfCastOp [in Arithmetic]
ArithmeticTypes.TBinOpArithmetic [in Arithmetic]
ArithmeticTypes.TCastArithmetic [in Arithmetic]
ArithmeticTypes.TCmpiArithmetic [in Arithmetic]
ArithmeticTypes.TCmpValuesArithmetic [in Arithmetic]
ArithmeticTypes.TCmpZeroArithmetic [in Arithmetic]
ArithmeticTypes.TUnOpArithmetic [in Arithmetic]
ARITHMETIC.arithmetic [in Arithmetic]
A_m_code [in Program_A]

B

bijection [in Common]

C

CHAR.base [in Char]
CHAR.range [in Char]
cm [in IAdd]
code [in Loop_Assertions]
code [in Loop]
code [in IAdd]
Code_to_test_instructions [in Instructions]

D

DOUBLE_ARITHMETIC.arithmetic [in Arithmetic]
DOUBLE_ARITHMETIC.castArithmetic [in Arithmetic]
DOUBLE_ARITHMETIC.cmpiArithmetic [in Arithmetic]
DOUBLE_ARITHMETIC.cmpValuesArithmetic [in Arithmetic]
DOUBLE_ARITHMETIC.cmpZeroArithmetic [in Arithmetic]
DOUBLE_ARITHMETIC.binOpArithmetic [in Arithmetic]
DOUBLE_ARITHMETIC.unOpArithmetic [in Arithmetic]
DOUBLE_ARITHMETIC.kind [in Arithmetic]

E

eqDec [in Common]
eqDecS [in Common]

F

findInListOfPairs [in Common]
flip3 [in Common]
FLOAT_ARITHMETIC.arithmetic [in Arithmetic]
FLOAT_ARITHMETIC.castArithmetic [in Arithmetic]
FLOAT_ARITHMETIC.cmpiArithmetic [in Arithmetic]
FLOAT_ARITHMETIC.cmpValuesArithmetic [in Arithmetic]
FLOAT_ARITHMETIC.cmpZeroArithmetic [in Arithmetic]
FLOAT_ARITHMETIC.binOpArithmetic [in Arithmetic]
FLOAT_ARITHMETIC.unOpArithmetic [in Arithmetic]
FLOAT_ARITHMETIC.kind [in Arithmetic]
FMake.abstract_rem [in FNumeric]
FMake.add [in FNumeric]
FMake.const [in FNumeric]
FMake.div [in FNumeric]
FMake.fit_into [in FNumeric]
FMake.fromDiadic [in FNumeric]
FMake.GeIEEE [in FNumeric]
FMake.GtIEEE [in FNumeric]
FMake.iconst [in FNumeric]
FMake.mul [in FNumeric]
FMake.neg [in FNumeric]
FMake.one [in FNumeric]
FMake.precision [in FNumeric]
FMake.rem [in FNumeric]
FMake.rmode [in FNumeric]
FMake.round_mag_down_int [in FNumeric]
FMake.sign_of [in FNumeric]
FMake.sub [in FNumeric]
FMake.t [in FNumeric]
FMake.toDiadic [in FNumeric]
FMake.toIEEE [in FNumeric]
FMake.truncate [in FNumeric]
FMake.two [in FNumeric]
FMake.zero [in FNumeric]
FNUMERIC.GeIEEE [in FNumeric]
FNUMERIC.GtIEEE [in FNumeric]
FNUMERIC.rmode [in FNumeric]
frame0 [in Loop_Assertions]
frame0 [in Loop]
frame0 [in IAdd]
frame0_props [in IAdd]
frame1 [in IAdd]
frame1_props [in IAdd]
frame2 [in IAdd]
frame2_props [in IAdd]
frame3 [in IAdd]
frame3_props [in IAdd]

H

HEAP.arraySizeFromNat [in Heap]
HEAP.getLocClass [in Heap]
HEAP.getReferenceType [in Heap]
HEAP.TArrayIndex [in Heap]
HEAP.TArraySize [in Heap]
HEAP.validIndex [in Heap]
HEAP.validIndexNat [in Heap]

I

intArith [in Loop_Assertions]
intArith [in Loop]
intArith [in IAdd]
INT_ARITHMETIC.arithmetic [in Arithmetic]
INT_ARITHMETIC.castArithmetic [in Arithmetic]
INT_ARITHMETIC.cmpiArithmetic [in Arithmetic]
INT_ARITHMETIC.cmpValuesArithmetic [in Arithmetic]
INT_ARITHMETIC.cmpZeroArithmetic [in Arithmetic]
INT_ARITHMETIC.binOpArithmetic [in Arithmetic]
INT_ARITHMETIC.unOpArithmetic [in Arithmetic]
INT_ARITHMETIC.kind [in Arithmetic]
inverse [in Common]

J

jvm0 [in IAdd]
jvm0_props [in IAdd]
jvm1 [in IAdd]
jvm1_props [in IAdd]
jvm2 [in IAdd]
jvm2_props [in IAdd]
jvm3 [in IAdd]
jvm3_props [in IAdd]

L

lassertions [in Loop_Assertions]
LONG_ARITHMETIC.arithmetic [in Arithmetic]
LONG_ARITHMETIC.castArithmetic [in Arithmetic]
LONG_ARITHMETIC.cmpiArithmetic [in Arithmetic]
LONG_ARITHMETIC.cmpValuesArithmetic [in Arithmetic]
LONG_ARITHMETIC.cmpZeroArithmetic [in Arithmetic]
LONG_ARITHMETIC.binOpArithmetic [in Arithmetic]
LONG_ARITHMETIC.unOpArithmetic [in Arithmetic]
LONG_ARITHMETIC.kind [in Arithmetic]

M

Make.base [in Char]
Make.base [in Numeric]
Make.clear_false [in Char]
Make.clear_false [in Numeric]
Make.compare [in Numeric]
Make.digits_of_Z [in Char]
Make.digits_of_pos [in Char]
Make.digits_of_Z [in Numeric]
Make.digits_of_pos [in Numeric]
Make.half_base [in Numeric]
Make.isNotZero [in Numeric]
Make.is_gt [in Numeric]
Make.is_ge [in Numeric]
Make.is_lt [in Numeric]
Make.is_le [in Numeric]
Make.is_ne [in Numeric]
Make.is_eq [in Numeric]
Make.minus_one [in Numeric]
Make.one [in Numeric]
Make.pos_Z_of_digits [in Char]
Make.pos_of_digits [in Char]
Make.pos_of_digits [in Numeric]
Make.power [in Char]
Make.power [in Numeric]
Make.range [in Char]
Make.range [in Numeric]
Make.smod [in Numeric]
Make.truncate [in Numeric]
Make.truncateZ [in Char]
Make.truncateZ [in Numeric]
Make.truncate_to_char [in Char]
Make.zero [in Char]
Make.zero [in Numeric]
Make.Z_of_digits [in Numeric]
map_oneOrTwo [in Common]
max [in Loop_Assertions]
max [in Loop]

N

nfour [in IAdd]
ntwo [in IAdd]
NUMERIC.base [in Numeric]
NUMERIC.half_base [in Numeric]
NUMERIC.range [in Numeric]
NUMERIC.smod [in Numeric]

P

pc0 [in Loop_Assertions]
pc0 [in Loop]
pc0 [in IAdd]
pc1 [in IAdd]
pc2 [in IAdd]
pc3 [in IAdd]
ProgramStructuresFacts.StandardNames.arrayInterfaces [in ProgramStructures]
ProgramStructuresFacts.var0 [in ProgramStructures]
ProgramStructuresFacts.var1 [in ProgramStructures]
ProgramStructuresFacts.var2 [in ProgramStructures]
ProgramStructuresFacts.var3 [in ProgramStructures]
ProgramStructuresImpl.nextVar [in ProgramStructuresImpl]
ProgramStructuresImpl.PnatVar [in ProgramStructuresImpl]
ProgramStructuresImpl.PvarNat [in ProgramStructuresImpl]
ProgramStructuresImpl.PVar_eqDec [in ProgramStructuresImpl]
ProgramStructuresImpl.TQualifiedMethodName [in ProgramStructuresImpl]
ProgramStructuresImpl.TSignature [in ProgramStructuresImpl]
ProgramStructuresImpl.TVar [in ProgramStructuresImpl]
ProgramStructuresImpl.varFromNat [in ProgramStructuresImpl]
ProgramStructuresImpl.varToNat [in ProgramStructuresImpl]
PROGRAM_ASSERTIONS.singleTransitions [in ProgramAssertions]
PROGRAM_ASSERTIONS.frameDescribed2 [in ProgramAssertions]
PROGRAM_ASSERTIONS.frameDescribed [in ProgramAssertions]
PROGRAM_ASSERTIONS.codeDescribed [in ProgramAssertions]
PROGRAM_ASSERTIONS.getPositionedAssertion [in ProgramAssertions]
PROGRAM_ASSERTIONS.TCodeAssertion [in ProgramAssertions]
PROGRAM_STRUCTURES.TQualifiedMethodName [in ProgramStructures]
PROGRAM_STRUCTURES.TSignature [in ProgramStructures]
PROGRAM.currentInstruction [in Program]
PROGRAM.getMethodFromProgram [in Program]
PROGRAM.isAncestorClass [in Program]
PROGRAM.isAncestorClassOrSelf [in Program]
PROGRAM.isDirectSuperTypeClass [in Program]
PROGRAM.isParentClass [in Program]
PROGRAM.isSuperTypeClass [in Program]
PROGRAM.isSuperTypeClassOrSelf [in Program]
PROGRAM.subtypeRef [in Program]
PROGRAM.validExceptionHandler [in Program]
propDec [in Common]
propDecS [in Common]

R

reachable [in Loop]
REF_ARITHMETIC.arithmetic [in Arithmetic]
REF_ARITHMETIC.castArithmetic [in Arithmetic]
REF_ARITHMETIC.cmpiArithmetic [in Arithmetic]
REF_ARITHMETIC.cmpValuesArithmetic [in Arithmetic]
REF_ARITHMETIC.cmpZeroArithmetic [in Arithmetic]
REF_ARITHMETIC.binOpArithmetic [in Arithmetic]
REF_ARITHMETIC.unOpArithmetic [in Arithmetic]
REF_ARITHMETIC.kind [in Arithmetic]
RuntimeStructuresFacts.mapROX [in RuntimeStructures]
RuntimeStructuresFacts.prefix [in RuntimeStructures]
RuntimeStructuresFacts.stackTopValues [in RuntimeStructures]
RuntimeStructuresImpl.cmDeclClass [in RuntimeStructuresImpl]
RuntimeStructuresImpl.cmSignature [in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKAbstraction [in RuntimeStructuresImpl]
RuntimeStructuresImpl.frameKConcretisation [in RuntimeStructuresImpl]
RuntimeStructuresImpl.localStackKAbstraction [in RuntimeStructuresImpl]
RuntimeStructuresImpl.localStackKConcretisation [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TEvalState [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TLocalStack [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TLocalStackGeneric [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TLocalStackKShadow [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TLocalStackTShadow [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TRichFrame [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TVars [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TVarsGeneric [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TVarsKShadow [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TVarsTShadow [in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsEmpty [in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsEquiv [in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsGet [in RuntimeStructuresImpl]
RuntimeStructuresImpl.varsSet [in RuntimeStructuresImpl]
RUNTIME_STRUCTURES.TEvalState [in RuntimeStructures]
RUNTIME_STRUCTURES.TRichFrame [in RuntimeStructures]
RUNTIME_STRUCTURES.cmSignature [in RuntimeStructures]
RUNTIME_STRUCTURES.cmDeclClass [in RuntimeStructures]
RUNTIME_STRUCTURES.frameKConcretisation [in RuntimeStructures]
RUNTIME_STRUCTURES.frameKAbstraction [in RuntimeStructures]
RUNTIME_STRUCTURES.localStackKConcretisation [in RuntimeStructures]
RUNTIME_STRUCTURES.localStackKAbstraction [in RuntimeStructures]
RUNTIME_STRUCTURES.TLocalStackTShadow [in RuntimeStructures]
RUNTIME_STRUCTURES.TVarsTShadow [in RuntimeStructures]
RUNTIME_STRUCTURES.TLocalStackKShadow [in RuntimeStructures]
RUNTIME_STRUCTURES.TVarsKShadow [in RuntimeStructures]
RUNTIME_STRUCTURES.TLocalStack [in RuntimeStructures]
RUNTIME_STRUCTURES.TVars [in RuntimeStructures]
RUNTIME_STRUCTURES.TLocalStackGeneric [in RuntimeStructures]
RUNTIME_STRUCTURES.varsEquiv [in RuntimeStructures]

S

SEMANTICS.steps [in Semantics]
SEM_CALL.initFrame [in Sem_Call]
SEM_FRAME.stepsFrame [in Sem_Frame]
SEM_FRAME.calculatePC [in Sem_Frame]
sk0 [in Loop_Assertions]
sk0 [in Loop]
specification [in Loop_Assertions]
stack_values [in Loop_Assertions]
stack_values [in Loop]
s0_prop [in Loop_Assertions]
s0_prop [in Loop]
s1_prop [in Loop_Assertions]
s1_prop [in Loop]
s10_prop [in Loop_Assertions]
s10_prop [in Loop]
s11_prop [in Loop_Assertions]
s11_prop [in Loop]
s12_prop [in Loop_Assertions]
s12_prop [in Loop]
s13_prop [in Loop_Assertions]
s13_prop [in Loop]
s14_prop [in Loop_Assertions]
s14_prop [in Loop]
s15_prop [in Loop_Assertions]
s15_prop [in Loop]
s16_prop [in Loop_Assertions]
s16_prop [in Loop]
s17_prop [in Loop_Assertions]
s17_prop [in Loop]
s18_post_prop [in Loop_Assertions]
s18_prop [in Loop_Assertions]
s18_post_prop [in Loop]
s18_prop [in Loop]
s19_prop [in Loop_Assertions]
s19_prop [in Loop]
s2_prop [in Loop_Assertions]
s2_prop [in Loop]
s20_prop [in Loop_Assertions]
s20_prop [in Loop]
s3_prop [in Loop_Assertions]
s3_prop [in Loop]
s4_prop [in Loop_Assertions]
s4_prop [in Loop]
s5_post_prop [in Loop_Assertions]
s5_prop [in Loop_Assertions]
s5_post_prop [in Loop]
s5_prop [in Loop]
s6_prop [in Loop_Assertions]
s6_prop [in Loop]
s7_prop [in Loop_Assertions]
s7_prop [in Loop]
s8_post_prop [in Loop_Assertions]
s8_prop [in Loop_Assertions]
s8_post_prop [in Loop]
s8_prop [in Loop]
s9_prop [in Loop_Assertions]
s9_prop [in Loop]

T

thstate0 [in IAdd]
thstate0_props [in IAdd]
thstate1 [in IAdd]
thstate1_props [in IAdd]
thstate2 [in IAdd]
thstate2_props [in IAdd]
thstate3 [in IAdd]
thstate3_props [in IAdd]

V

VALUES_AND_TYPES.sizeOfTypes [in ValuesNTypes]
VALUES_AND_TYPES.sizeOfType [in ValuesNTypes]
VALUES_AND_TYPES.sizeOfValues [in ValuesNTypes]
VALUES_AND_TYPES.sizeOfValue [in ValuesNTypes]
VALUES_AND_TYPES.sizeOfKind [in ValuesNTypes]
VALUES_AND_TYPES.catOfKind [in ValuesNTypes]
VALUES_AND_TYPES.sizeOfCat [in ValuesNTypes]
VALUES_AND_TYPES.kindOfArrayKind [in ValuesNTypes]
VALUES_AND_TYPES.transformAFromValue [in ValuesNTypes]
VALUES_AND_TYPES.transformVADouble [in ValuesNTypes]
VALUES_AND_TYPES.transformVALong [in ValuesNTypes]
VALUES_AND_TYPES.transformVAFloat [in ValuesNTypes]
VALUES_AND_TYPES.transformVAInt [in ValuesNTypes]
VALUES_AND_TYPES.transformVAShort [in ValuesNTypes]
VALUES_AND_TYPES.transformVABool [in ValuesNTypes]
VALUES_AND_TYPES.transformVAByte [in ValuesNTypes]
VALUES_AND_TYPES.transformVAChar [in ValuesNTypes]
VALUES_AND_TYPES.transformVARef [in ValuesNTypes]
VALUES_AND_TYPES.transformAToValue [in ValuesNTypes]
VALUES_AND_TYPES.transformKToVarK [in ValuesNTypes]
VALUES_AND_TYPES.transformValToVar [in ValuesNTypes]
VALUES_AND_TYPES.int2double [in ValuesNTypes]
VALUES_AND_TYPES.int2float [in ValuesNTypes]
VALUES_AND_TYPES.long2float [in ValuesNTypes]
VALUES_AND_TYPES.long2double [in ValuesNTypes]
VALUES_AND_TYPES.double2int [in ValuesNTypes]
VALUES_AND_TYPES.double2long [in ValuesNTypes]
VALUES_AND_TYPES.double2float [in ValuesNTypes]
VALUES_AND_TYPES.float2long [in ValuesNTypes]
VALUES_AND_TYPES.float2int [in ValuesNTypes]
VALUES_AND_TYPES.float2double [in ValuesNTypes]
VALUES_AND_TYPES.long2int [in ValuesNTypes]
VALUES_AND_TYPES.int2long [in ValuesNTypes]
VALUES_AND_TYPES.int2ichar [in ValuesNTypes]
VALUES_AND_TYPES.int2char [in ValuesNTypes]
VALUES_AND_TYPES.char2int [in ValuesNTypes]
VALUES_AND_TYPES.int2ishort [in ValuesNTypes]
VALUES_AND_TYPES.int2short [in ValuesNTypes]
VALUES_AND_TYPES.short2int [in ValuesNTypes]
VALUES_AND_TYPES.int2bool [in ValuesNTypes]
VALUES_AND_TYPES.bool2int [in ValuesNTypes]
VALUES_AND_TYPES.int2ibyte [in ValuesNTypes]
VALUES_AND_TYPES.int2byte [in ValuesNTypes]
VALUES_AND_TYPES.byte2int [in ValuesNTypes]
VALUES_AND_TYPES.defaultArrayValueForType [in ValuesNTypes]
VALUES_AND_TYPES.defaultValueForType [in ValuesNTypes]
VALUES_AND_TYPES.defaultForKind [in ValuesNTypes]
VALUES_AND_TYPES.exampleForKind [in ValuesNTypes]
VALUES_AND_TYPES.arrayKindOfType [in ValuesNTypes]
VALUES_AND_TYPES.kindOfTypes [in ValuesNTypes]
VALUES_AND_TYPES.kindOfType [in ValuesNTypes]
VALUES_AND_TYPES.kindOfAValue [in ValuesNTypes]
VALUES_AND_TYPES.kindOfVarValue [in ValuesNTypes]
VALUES_AND_TYPES.kindOfValues [in ValuesNTypes]
VALUES_AND_TYPES.kindOfValue [in ValuesNTypes]
vars0 [in Loop_Assertions]
vars0 [in Loop]
vfour [in IAdd]
vtwo [in IAdd]

Record Index

A

ArithmeticTypes.TArithmetic [in Arithmetic]

R

RuntimeStructuresImpl.TCurrentMethod [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TFrame [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TFrameKShadow [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TJVM [in RuntimeStructuresImpl]
RuntimeStructuresImpl.TThread [in RuntimeStructuresImpl]
RUNTIME_STRUCTURES.TJVM [in RuntimeStructures]
RUNTIME_STRUCTURES.TThread [in RuntimeStructures]
RUNTIME_STRUCTURES.TCurrentMethod [in RuntimeStructures]
RUNTIME_STRUCTURES.TFrameKShadow [in RuntimeStructures]
RUNTIME_STRUCTURES.TFrame [in RuntimeStructures]

Global Index

Q

U

W

X

Y

Z

_

other

(2041 entries)

Module Index

B

E

G

J

K

O

Q

T

U

W

X

Y

Z

_

other

(161 entries)

Variable Index

G

I

J

P

Q

T

U

W

X

Y

Z

_

other

(81 entries)

Library Index

B

D

E

G

J

K

M

O

Q

T

U

W

X

Y

Z

_

other

(28 entries)

Lemma Index

E

K

L

O

Q

U

W

X

Y

Z

_

other

(302 entries)

Axiom Index

B

D

E

G

I

J

K

L

O

Q

U

W

X

Y

Z

_

other

(375 entries)

Constructor Index

B

C

E

G

J

K

M

N

Q

U

W

X

Y

Z

_

other

(527 entries)

Inductive Index

B

C

E

G

J

K

M

N

O

Q

U

W

X

Y

Z

_

other

(133 entries)

Projection Index

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(34 entries)

Section Index

A

B

C

G

I

J

K

N

O

P

Q

T

U

W

X

Y

Z

_

other

(16 entries)

Definition Index

G

K

O

Q

U

W

X

Y

Z

_

other

(373 entries)

Record Index

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(11 entries)

This page has been generated by coqdoc