Formalism of CETS

Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (506 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (25 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (7 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (202 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (145 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (21 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (72 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (22 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (12 entries)

Global Index

A

Abort [constructor, in ISemantics]
accessMem [axiom, in Envs]
accessMemMeta [definition, in Envs]
accessMemMeta_accessMem_None [lemma, in Libs]
accessMemMeta_accessMem_Some [lemma, in Libs]
accessMemMeta_dec [lemma, in Libs]
accessMemMeta_unchanged_destroyFrame [lemma, in WfEnv]
accessMemMeta_unchanged_free [lemma, in WfEnv]
accessMemMeta_unchanged_malloc [lemma, in WfEnv]
accessMemMeta_unchanged_store [lemma, in Libs]
accessMemMeta_uniqBehavior [lemma, in Libs]
accessMemMeta__s_rhs__accessMemMeta [lemma, in Props]
accessMem_accessMemMeta_None [lemma, in Libs]
accessMem_accessMemMeta_Some [lemma, in Libs]
accessNoneSome__s_rhs__accessZero [lemma, in Props]
addAllocMemBlock [definition, in Envs]
addRI [definition, in Envs]
AllocMemBlock [definition, in Envs]
amb [projection, in Envs]
assertion_ptr [definition, in ISemantics]
assertion_ptr_dec [lemma, in Libs]
assertion_spatial_ptr [definition, in ISemantics]
assertion_spatial_ptr_dec [lemma, in Libs]
assertion_temporal_ptr [definition, in ISemantics]
assertion_temporal_ptr_dec [lemma, in Libs]
AType [inductive, in Types]
Axioms [library]
A_Int [constructor, in Types]
A_Pointer [constructor, in Types]


B

BackSim [library]
Base [definition, in Envs]
baseAddress [axiom, in Envs]
Bound [definition, in Envs]


C

createFrame [definition, in Envs]
createFrame_dec [lemma, in Libs]
createFrame__inversion [lemma, in Libs]
createFrame__ucreateFrame_Some [lemma, in Libs]
createFrame__validAddress [lemma, in WfEnv]
createFrame__wfE [lemma, in WfEnv]
createFrame__wfE__wfOverlappedAMB_case [lemma, in WfEnv]
createFrame__wfE__wfOverlapped_case [lemma, in WfEnv]
createFrame__wfE__wfUniqRentryH_case [lemma, in WfEnv]
createFrame__wfFrame [lemma, in WfEnv]
createFrame__wfFrms [lemma, in WfEnv]
createFrame__wfMem [lemma, in WfEnv]
createFrame__wfStack [lemma, in WfEnv]
CSemantics [library]
C_Add [constructor, in Syntax]
C_Alloc [constructor, in Syntax]
C_Assign [constructor, in Syntax]
C_Call [constructor, in Syntax]
C_Cast [constructor, in Syntax]
c_cmd [inductive, in Syntax]
C_Const [constructor, in Syntax]
C_Deref [constructor, in Syntax]
C_Free [constructor, in Syntax]
c_ident [definition, in Types]
c_lhs [inductive, in Syntax]
C_Lhs [constructor, in Syntax]
C_NamePos [constructor, in Syntax]
C_Ref [constructor, in Syntax]
c_rhs [inductive, in Syntax]
C_Seq [constructor, in Syntax]
C_Size [constructor, in Syntax]
C_Skip [constructor, in Syntax]
C_StructPos [constructor, in Syntax]
C_Var [constructor, in Syntax]


D

Data [definition, in ISemantics]
dataCast [definition, in ISemantics]
dataCast__valid [lemma, in Libs]
destroyFrame [definition, in Envs]
destroyFrame_dec [lemma, in Libs]
destroyFrame__inversion [lemma, in Libs]
destroyFrame__udestroyFrame_Some [lemma, in Libs]
destroyFrame__wfE [lemma, in WfEnv]
destroyFrame__wfE__wfOverlappedAMB_case [lemma, in WfEnv]
destroyFrame__wfE__wfOverlapped_case [lemma, in WfEnv]
destroyFrame__wfE__wfUniqRentryH_case [lemma, in WfEnv]
destroyFrame__wfFrame [lemma, in WfEnv]
destroyFrame__wfFrms [lemma, in WfEnv]
destroyFrame__wfMem [lemma, in WfEnv]
destroyFrame__wfStack [lemma, in WfEnv]


E

Env [record, in Envs]
Envs [library]
Env2uEnv [definition, in Envs]
Error [definition, in ISemantics]
ErrorR__inv [lemma, in BackSim]


F

fdata [projection, in Envs]
fr [projection, in Envs]
Frame [record, in Envs]
frame [definition, in Envs]
frames [projection, in Envs]
Frames2uFrames [definition, in Envs]
Frame2frame [definition, in Envs]
Frame2uFrame [definition, in Envs]
free [definition, in Envs]
free_dec [lemma, in Libs]
free__inversion [lemma, in Libs]
free__ufree_Some [lemma, in Libs]
free__wfE [lemma, in WfEnv]
free__wfE__wfOverlappedAMB_case [lemma, in WfEnv]
free__wfE__wfOverlapped_case [lemma, in WfEnv]
free__wfE__wfUniqRentryH_case [lemma, in WfEnv]
free__wfFrame [lemma, in WfEnv]
free__wfMem [lemma, in WfEnv]
free__wfStack [lemma, in WfEnv]
fri [projection, in Envs]
from [projection, in Envs]
funTable [axiom, in Syntax]


G

gdata [projection, in Envs]
getFreshRentry [axiom, in Envs]
getFreshRentry__inversion [axiom, in Axioms]
getStructOffset [definition, in Types]
getStructType [definition, in Types]
getStructType__getStructOffset [lemma, in Libs]
global [projection, in Envs]
Global [record, in Envs]
gri [axiom, in Envs]


I

Introduction [library]
invalidAccessMemMeta__invalidStoreMemMeta [lemma, in Libs]
invalidAccessMem__invalidStoreMem [lemma, in Libs]
invalidStoreMemMeta__invalidAddress [lemma, in Libs]
invalidStoreMem__invalidAddress [lemma, in Libs]
ISemantics [library]
isPtr [definition, in Types]
isPtr_dec [lemma, in Libs]


K

Key [definition, in Envs]


L

le_ge__eq [lemma, in Libs]
lhs_progress [lemma, in Props]
lhs__inversion [lemma, in Props]
lhs__wft [lemma, in Props]
Libs [library]
Loc [definition, in Envs]
LockAddr [definition, in Envs]
LockTable [definition, in Envs]
lookUpFrame [definition, in Envs]
lookUpGlobal [definition, in Envs]
lookUpStack [definition, in Envs]
lookUpuFrame [definition, in Envs]
lookUpuStack [definition, in Envs]


M

malloc [definition, in Envs]
malloc_dec [lemma, in Libs]
malloc__inversion [lemma, in Libs]
malloc__umalloc_Some [lemma, in Libs]
malloc__validAddress [lemma, in WfEnv]
malloc__wfE [lemma, in WfEnv]
malloc__wfE__wfOverlappedAMB_case [lemma, in WfEnv]
malloc__wfE__wfOverlapped_case [lemma, in WfEnv]
malloc__wfE__wfUniqRentryH_case [lemma, in WfEnv]
malloc__wfFrame [lemma, in WfEnv]
malloc__wfMem [lemma, in WfEnv]
malloc__wfStack [lemma, in WfEnv]
maxAddress [axiom, in Envs]
mem [projection, in Envs]
Mem [definition, in Envs]
Meta [definition, in Envs]
minAddress [axiom, in Envs]
MkEnv [constructor, in Envs]
MkFrame [constructor, in Envs]
MkGlobal [constructor, in Envs]
MkStack [constructor, in Envs]
MkuEnv [constructor, in Envs]
MkuFrame [constructor, in Envs]
MkuStack [constructor, in Envs]
MMeta [definition, in Envs]
mmeta [projection, in Envs]
mutual_AType_Struct_ind [definition, in Types]
mutual_wf_AType_Struct_PType_ind [definition, in Types]


N

nateq_plus_inv [lemma, in Libs]
neqzero__largerthanzero [lemma, in Libs]


O

omega_ex1 [lemma, in Libs]
overlapped_interval [lemma, in Libs]
overlapped_interval_sub [lemma, in Libs]


P

Progress [lemma, in Props]
Props [library]
PType [inductive, in Types]
P_AType [constructor, in Types]
P_Name [constructor, in Types]
P_Struct [constructor, in Types]
P_VoidPtr [constructor, in Types]


R

removeAllocMemBlock [definition, in Envs]
removeRI [definition, in Envs]
Result [inductive, in ISemantics]
rev [projection, in Envs]
revInfo [projection, in Envs]
rhs_progress [lemma, in Props]
rhs__wft [lemma, in Props]
RLoc [constructor, in ISemantics]
ROK [constructor, in ISemantics]
RVal [constructor, in ISemantics]
r_lesseq_rev [lemma, in Libs]


S

sizeOfAType [definition, in Types]
sizeOfAType_one [lemma, in Libs]
sizeOfFields__non_zero [lemma, in Libs]
sizeOfPType [definition, in Types]
sizeOfStruct [definition, in Types]
sr [projection, in Envs]
Stack [record, in Envs]
stack [projection, in Envs]
Stack2frame [definition, in Envs]
Stack2uStack [definition, in Envs]
storeMem [axiom, in Envs]
storeMemMeta [definition, in Envs]
storeMemMeta_dec [lemma, in Libs]
storeMemMeta_storeMem_None [lemma, in Libs]
storeMemMeta_storeMem_Some [lemma, in Libs]
storeMemMeta_uniqBehavior [lemma, in Libs]
storeMemMeta__invalidAddress [lemma, in Libs]
storeMemMeta__invalidAddresses [lemma, in Libs]
storeMemMeta__inversion [lemma, in Libs]
storeMemMeta__validAddress [lemma, in Libs]
storeMem_dec [lemma, in Libs]
storeMem_storeMemMeta_None [lemma, in Libs]
storeMem_storeMemMeta_Some [lemma, in Libs]
storeMem_uniqBehavior [axiom, in Axioms]
storeMem__accessMem [axiom, in Axioms]
storeMem__invalidAddress [lemma, in Libs]
storeMem__invalidAddresses [lemma, in Libs]
storeMem__inversion [lemma, in Libs]
storeMem__validAddress [lemma, in Libs]
Struct [inductive, in Types]
struct__subfield [lemma, in Libs]
Syntax [library]
SystemError [constructor, in ISemantics]
S_Add_Int_Int [constructor, in ISemantics]
S_Add_Int_Int_ErrorProp1 [constructor, in ISemantics]
S_Add_Int_Int_ErrorProp2 [constructor, in ISemantics]
S_Add_Ptr_Int [constructor, in ISemantics]
S_Add_Ptr_Int_ErrorProp1 [constructor, in ISemantics]
S_Add_Ptr_Int_ErrorProp2 [constructor, in ISemantics]
S_Alloc [constructor, in ISemantics]
S_Alloc_ErrorProp [constructor, in ISemantics]
S_Alloc_OutofMem [constructor, in ISemantics]
S_Assign_ErrorProp1 [constructor, in ISemantics]
S_Assign_ErrorProp2 [constructor, in ISemantics]
S_Assign_NPtr [constructor, in ISemantics]
S_Assign_Ptr [constructor, in ISemantics]
S_Call [constructor, in ISemantics]
S_Call_ErrorProp [constructor, in ISemantics]
S_Call_Error1 [constructor, in ISemantics]
S_Call_Error2 [constructor, in ISemantics]
S_Cast [constructor, in ISemantics]
S_Cast_ErrorProp [constructor, in ISemantics]
s_cmd [inductive, in ISemantics]
s_cmd__cannot__RVal_or_RLoc [lemma, in BackSim]
s_cmd__G [lemma, in Props]
s_cmd__implies__us_cmd [lemma, in BackSim]
s_cmd__S [lemma, in Props]
s_cmd__S_wfFrms [lemma, in Props]
S_Cons [constructor, in Types]
S_Const [constructor, in ISemantics]
S_Deref [constructor, in ISemantics]
S_Deref_Abort [constructor, in ISemantics]
S_Deref_ErrorProp [constructor, in ISemantics]
S_Free [constructor, in ISemantics]
S_Free_Error [constructor, in ISemantics]
S_Free_ErrorProp [constructor, in ISemantics]
S_GVar [constructor, in ISemantics]
s_lhs [inductive, in ISemantics]
S_Lhs [constructor, in ISemantics]
S_Lhs_ErrorProp [constructor, in ISemantics]
s_lhs__cannot__SystemError [lemma, in BackSim]
s_lhs__implies__us_lhs [lemma, in BackSim]
s_lhs__wf_lhs [lemma, in Props]
S_NamePos [constructor, in ISemantics]
S_NamePos_Abort [constructor, in ISemantics]
S_NamePos_ErrorProp [constructor, in ISemantics]
S_Nil [constructor, in Types]
S_Ref [constructor, in ISemantics]
S_Ref_ErrorProp [constructor, in ISemantics]
s_rhs [inductive, in ISemantics]
s_rhs__G [lemma, in Props]
s_rhs__implies__us_rhs [lemma, in BackSim]
s_rhs__S [lemma, in Props]
s_rhs__wfFrms [lemma, in Props]
S_Seq [constructor, in ISemantics]
S_Seq_ErrorProp1 [constructor, in ISemantics]
S_Seq_ErrorProp2 [constructor, in ISemantics]
S_Size [constructor, in ISemantics]
S_Skip [constructor, in ISemantics]
S_StructPos [constructor, in ISemantics]
S_StructPos_Abort [constructor, in ISemantics]
S_StructPos_ErrorProp [constructor, in ISemantics]
S_SVar [constructor, in ISemantics]


T

Tactics [library]
to [projection, in Envs]
top [projection, in Envs]
Types [library]
typeTable [axiom, in Types]


U

uamb [projection, in Envs]
ucreateFrame [axiom, in Envs]
ucreateFrame__inversion [axiom, in Axioms]
udestroyFrame [axiom, in Envs]
udestroyFrame__inversion [axiom, in Axioms]
uEnv [record, in Envs]
uError [definition, in CSemantics]
ufdata [projection, in Envs]
uFrame [record, in Envs]
uframes [projection, in Envs]
uFrame2frame [definition, in Envs]
ufree [axiom, in Envs]
ufree__inversion [axiom, in Axioms]
ufrom [projection, in Envs]
uglobal [projection, in Envs]
umalloc [axiom, in Envs]
umalloc__inversion [axiom, in Axioms]
umem [projection, in Envs]
updateMetadata [definition, in Envs]
updateMetadatas [definition, in Envs]
uResult [inductive, in CSemantics]
uRLoc [constructor, in CSemantics]
uROK [constructor, in CSemantics]
uROK__isnot__uErrorR [lemma, in BackSim]
uRVal [constructor, in CSemantics]
uStack [record, in Envs]
ustack [projection, in Envs]
uStack2frame [definition, in Envs]
uSystemError [constructor, in CSemantics]
uS_Add_Int_Int [constructor, in CSemantics]
uS_Add_Int_Int_ErrorProp1 [constructor, in CSemantics]
uS_Add_Int_Int_ErrorProp2 [constructor, in CSemantics]
uS_Add_Ptr_Int [constructor, in CSemantics]
uS_Add_Ptr_Int_ErrorProp1 [constructor, in CSemantics]
uS_Add_Ptr_Int_ErrorProp2 [constructor, in CSemantics]
uS_Alloc [constructor, in CSemantics]
uS_Alloc_ErrorProp [constructor, in CSemantics]
uS_Alloc_OutofMem [constructor, in CSemantics]
uS_Assign [constructor, in CSemantics]
uS_Assign_ErrorProp1 [constructor, in CSemantics]
uS_Assign_ErrorProp2 [constructor, in CSemantics]
uS_Call [constructor, in CSemantics]
uS_Call_ErrorProp [constructor, in CSemantics]
uS_Call_Error1 [constructor, in CSemantics]
uS_Call_Error2 [constructor, in CSemantics]
uS_Cast [constructor, in CSemantics]
uS_Cast_ErrorProp [constructor, in CSemantics]
us_cmd [inductive, in CSemantics]
uS_Const [constructor, in CSemantics]
uS_Deref [constructor, in CSemantics]
uS_Free [constructor, in CSemantics]
uS_Free_Error [constructor, in CSemantics]
uS_Free_ErrorProp [constructor, in CSemantics]
uS_GVar [constructor, in CSemantics]
us_lhs [inductive, in CSemantics]
uS_Lhs [constructor, in CSemantics]
uS_NamePos [constructor, in CSemantics]
uS_Ref [constructor, in CSemantics]
us_rhs [inductive, in CSemantics]
uS_Seq [constructor, in CSemantics]
uS_Seq_ErrorProp1 [constructor, in CSemantics]
uS_Seq_ErrorProp2 [constructor, in CSemantics]
uS_Size [constructor, in CSemantics]
uS_Skip [constructor, in CSemantics]
uS_StructPos [constructor, in CSemantics]
uS_SVar [constructor, in CSemantics]
uto [projection, in Envs]
utop [projection, in Envs]


V

validAccessMemMeta__validAccessMem [lemma, in Libs]
validAccessMemMeta__validAddress [lemma, in Libs]
validAccessMemMeta__validStoreMem [lemma, in Libs]
validAccessMemMeta__validStoreMemMeta [lemma, in Libs]
validAccessMem__validAddress [lemma, in Libs]
validAccessMem__validStoreMem [axiom, in Axioms]
validAddress [definition, in Envs]
validAddressRange [axiom, in Axioms]
validAddress__s_rhs__validAddress [lemma, in Props]
validStoreMemMeta__validAccessMem [lemma, in Libs]
validStoreMemMeta__validAddress [lemma, in Libs]
validStoreMemMeta__validStoreMem [lemma, in Libs]
validStoreMem__validAddress [lemma, in Libs]
Value [definition, in Envs]
Var [definition, in Envs]


W

wfAllocMemBlock [definition, in Envs]
wfData [definition, in Envs]
wfData__monorev [lemma, in Props]
wfD__cast__wfD [lemma, in Props]
wfEnv [definition, in Envs]
WfEnv [library]
wfEnv_frF_interval_head [lemma, in Libs]
wfEnv_frF_interval_In [lemma, in Libs]
wfEnv_fromF_interval_In [lemma, in Libs]
wfEnv_F_interval_head [lemma, in Libs]
wfEnv_headTo_lesseq_tailFrom [lemma, in Libs]
wfEnv_lookUpStack__lookUpFrame [lemma, in Props]
wfEnv_topS_eq_fromF_head [lemma, in Libs]
wfEnv_top_interval [lemma, in Libs]
wfE_lookUpGlobal_validAddresses [lemma, in Props]
wfE_lookUpGlobal_wfD [lemma, in Props]
wfE_lookUpStack_validAddresses [lemma, in Props]
wfE_lookUpStack_wfD [lemma, in Props]
wfE_rev_ge_two [lemma, in Props]
wfE__accessMemMeta__wfGlobalPtr [lemma, in Props]
wfE__accessMemMeta__wfNonGlobalPtr [lemma, in Props]
wfE__accessMemMeta__wfNonStackPtr [lemma, in Props]
wfE__accessMemMeta__wfOverlapped [lemma, in Props]
wfE__accessMemMeta__wfOverlappedAMB [lemma, in Props]
wfE__accessMemMeta__wfStackPtr [lemma, in Props]
wfE__accessMemMeta__wfUniqRentryGS [lemma, in Props]
wfE__accessMemMeta__wfUniqRentryH [lemma, in Props]
wfE__storeMemMeta__wfE [lemma, in Libs]
wfE__storeMem__wfE [lemma, in Libs]
wfE__s_cmd__wfE [lemma, in Props]
wfE__s_lhs__monorev [lemma, in Props]
wfE__s_lhs__wfD [lemma, in Props]
wfE__s_lhs__wfGlobalPtr [lemma, in Props]
wfE__s_lhs__wfNonGlobalPtr [lemma, in Props]
wfE__s_lhs__wfNonStackPtr [lemma, in Props]
wfE__s_lhs__wfOverlapped_wfStackPtr [lemma, in Props]
wfE__s_lhs__wfUniqRentryGS [lemma, in Props]
wfE__s_rhs__monoAMB [lemma, in Props]
wfE__s_rhs__monorev [lemma, in Props]
wfE__s_rhs__monoRI [lemma, in Props]
wfE__s_rhs__wfD [lemma, in Props]
wfE__s_rhs__wfE [lemma, in Props]
wfE__s_rhs__wfGlobalPtr [lemma, in Props]
wfE__s_rhs__wfNonGlobalPtr [lemma, in Props]
wfE__s_rhs__wfNonStackPtr [lemma, in Props]
wfE__s_rhs__wfOverlapped [lemma, in Props]
wfE__s_rhs__wfOverlappedAMB [lemma, in Props]
wfE__s_rhs__wfStackPtr [lemma, in Props]
wfE__s_rhs__wfUniqRentryGS [lemma, in Props]
wfE__s_rhs__wfUniqRentryH [lemma, in Props]
wfFrame [definition, in Envs]
wfFrameNoOverlapped [definition, in Envs]
wfFrame__storeMemMeta__wfFrame [lemma, in Libs]
wfFrame__storeMem__wfFrame [lemma, in Libs]
wfFrms [inductive, in Envs]
wfFrms_cons [constructor, in Envs]
wfFrms_fromF_interval_In [lemma, in Libs]
wfFrms_headfr_gt_tailfr [lemma, in Libs]
wfFrms_headTo_lesseq_tailFrom [lemma, in Libs]
wfFrms_nil [constructor, in Envs]
wfFrms_srS_interval [lemma, in Libs]
wfFrms_srS_in_nonempty [lemma, in Libs]
wfFrms_sr_eq_Ffr [lemma, in Libs]
wfFrms_top_interval [lemma, in Libs]
wfFrms__monorev [lemma, in Libs]
wfGlobal [definition, in Envs]
wfGlobalPtr [definition, in Envs]
wfGlobalPtr_dataCast [lemma, in Props]
wfMem [definition, in Envs]
wfNonGlobalPtr [definition, in Envs]
wfNonGlobalPtr_dataCast [lemma, in Props]
wfNonStackPtr [definition, in Envs]
wfNonStackPtr_dataCast [lemma, in Props]
wfOverlapped [definition, in Envs]
wfOverlappedAMB [definition, in Envs]
wfOverlappedAMB_dataCast [lemma, in Props]
wfOverlappedAMB_subset [lemma, in Props]
wfOverlapped_dataCast [lemma, in Props]
wfOverlapped_subset [lemma, in Props]
wfStack [definition, in Envs]
wfStackPtr [definition, in Envs]
wfStackPtr_dataCast [lemma, in Props]
wfStackPtr_subset [lemma, in Props]
wfStack_F_interval_head [lemma, in Libs]
wfStack_lookUpStack__lookUpFrame [lemma, in Props]
wfStack_topS_eq_fromF_head [lemma, in Libs]
wfStack_top_interval [lemma, in Libs]
wfStack__storeMemMeta__wfStack [lemma, in Libs]
wfStack__storeMem__wfStack [lemma, in Libs]
wfuFrameNoOverlapped [definition, in Envs]
wfUniqRentryGS [definition, in Envs]
wfUniqRentryGS_dataCast [lemma, in Props]
wfUniqRentryH [definition, in Envs]
wfUniqRentryH_dataCast [lemma, in Props]
wfUniqRentryH_subset [lemma, in Props]
WF_Add_Int_Int [constructor, in Syntax]
WF_Add_Ptr_Int [constructor, in Syntax]
WF_Alloc [constructor, in Syntax]
WF_Assign [constructor, in Syntax]
wf_AType [inductive, in Types]
wf_AType__some_size [lemma, in Libs]
wf_AType__wf_subAType [lemma, in Libs]
wf_A_Int [constructor, in Types]
wf_A_TamePointer [constructor, in Types]
WF_Call [constructor, in Syntax]
WF_Cast [constructor, in Syntax]
wf_cmd [inductive, in Syntax]
WF_Const [constructor, in Syntax]
WF_Deref [constructor, in Syntax]
WF_Free [constructor, in Syntax]
WF_GVar [constructor, in Syntax]
WF_Lhs [constructor, in Syntax]
wf_lhs [inductive, in Syntax]
wf_lhs_uniq [lemma, in Libs]
wf_lhs__wf_AType [lemma, in Libs]
WF_NamePos [constructor, in Syntax]
wf_PType [inductive, in Types]
wf_PType__sizeOfType [lemma, in Libs]
wf_P_AType [constructor, in Types]
wf_P_Name [constructor, in Types]
wf_P_Struct [constructor, in Types]
wf_P_VoidPtr [constructor, in Types]
WF_Ref [constructor, in Syntax]
wf_rhs [inductive, in Syntax]
wf_rhs__wf_AType [lemma, in Libs]
WF_Seq [constructor, in Syntax]
WF_Size [constructor, in Syntax]
WF_Skip [constructor, in Syntax]
wf_Struct [inductive, in Types]
WF_StructPos [constructor, in Syntax]
WF_SVar [constructor, in Syntax]
wf_S_Cons [constructor, in Types]
wf_S_Nil [constructor, in Types]


_

_free__inversion [lemma, in Libs]



Projection Index

A

amb [in Envs]


F

fdata [in Envs]
fr [in Envs]
frames [in Envs]
fri [in Envs]
from [in Envs]


G

gdata [in Envs]
global [in Envs]


M

mem [in Envs]
mmeta [in Envs]


R

rev [in Envs]
revInfo [in Envs]


S

sr [in Envs]
stack [in Envs]


T

to [in Envs]
top [in Envs]


U

uamb [in Envs]
ufdata [in Envs]
uframes [in Envs]
ufrom [in Envs]
uglobal [in Envs]
umem [in Envs]
ustack [in Envs]
uto [in Envs]
utop [in Envs]



Record Index

E

Env [in Envs]


F

Frame [in Envs]


G

Global [in Envs]


S

Stack [in Envs]


U

uEnv [in Envs]
uFrame [in Envs]
uStack [in Envs]



Lemma Index

A

accessMemMeta_accessMem_None [in Libs]
accessMemMeta_accessMem_Some [in Libs]
accessMemMeta_dec [in Libs]
accessMemMeta_unchanged_destroyFrame [in WfEnv]
accessMemMeta_unchanged_free [in WfEnv]
accessMemMeta_unchanged_malloc [in WfEnv]
accessMemMeta_unchanged_store [in Libs]
accessMemMeta_uniqBehavior [in Libs]
accessMemMeta__s_rhs__accessMemMeta [in Props]
accessMem_accessMemMeta_None [in Libs]
accessMem_accessMemMeta_Some [in Libs]
accessNoneSome__s_rhs__accessZero [in Props]
assertion_ptr_dec [in Libs]
assertion_spatial_ptr_dec [in Libs]
assertion_temporal_ptr_dec [in Libs]


C

createFrame_dec [in Libs]
createFrame__inversion [in Libs]
createFrame__ucreateFrame_Some [in Libs]
createFrame__validAddress [in WfEnv]
createFrame__wfE [in WfEnv]
createFrame__wfE__wfOverlappedAMB_case [in WfEnv]
createFrame__wfE__wfOverlapped_case [in WfEnv]
createFrame__wfE__wfUniqRentryH_case [in WfEnv]
createFrame__wfFrame [in WfEnv]
createFrame__wfFrms [in WfEnv]
createFrame__wfMem [in WfEnv]
createFrame__wfStack [in WfEnv]


D

dataCast__valid [in Libs]
destroyFrame_dec [in Libs]
destroyFrame__inversion [in Libs]
destroyFrame__udestroyFrame_Some [in Libs]
destroyFrame__wfE [in WfEnv]
destroyFrame__wfE__wfOverlappedAMB_case [in WfEnv]
destroyFrame__wfE__wfOverlapped_case [in WfEnv]
destroyFrame__wfE__wfUniqRentryH_case [in WfEnv]
destroyFrame__wfFrame [in WfEnv]
destroyFrame__wfFrms [in WfEnv]
destroyFrame__wfMem [in WfEnv]
destroyFrame__wfStack [in WfEnv]


E

ErrorR__inv [in BackSim]


F

free_dec [in Libs]
free__inversion [in Libs]
free__ufree_Some [in Libs]
free__wfE [in WfEnv]
free__wfE__wfOverlappedAMB_case [in WfEnv]
free__wfE__wfOverlapped_case [in WfEnv]
free__wfE__wfUniqRentryH_case [in WfEnv]
free__wfFrame [in WfEnv]
free__wfMem [in WfEnv]
free__wfStack [in WfEnv]


G

getStructType__getStructOffset [in Libs]


I

invalidAccessMemMeta__invalidStoreMemMeta [in Libs]
invalidAccessMem__invalidStoreMem [in Libs]
invalidStoreMemMeta__invalidAddress [in Libs]
invalidStoreMem__invalidAddress [in Libs]
isPtr_dec [in Libs]


L

le_ge__eq [in Libs]
lhs_progress [in Props]
lhs__inversion [in Props]
lhs__wft [in Props]


M

malloc_dec [in Libs]
malloc__inversion [in Libs]
malloc__umalloc_Some [in Libs]
malloc__validAddress [in WfEnv]
malloc__wfE [in WfEnv]
malloc__wfE__wfOverlappedAMB_case [in WfEnv]
malloc__wfE__wfOverlapped_case [in WfEnv]
malloc__wfE__wfUniqRentryH_case [in WfEnv]
malloc__wfFrame [in WfEnv]
malloc__wfMem [in WfEnv]
malloc__wfStack [in WfEnv]


N

nateq_plus_inv [in Libs]
neqzero__largerthanzero [in Libs]


O

omega_ex1 [in Libs]
overlapped_interval [in Libs]
overlapped_interval_sub [in Libs]


P

Progress [in Props]


R

rhs_progress [in Props]
rhs__wft [in Props]
r_lesseq_rev [in Libs]


S

sizeOfAType_one [in Libs]
sizeOfFields__non_zero [in Libs]
storeMemMeta_dec [in Libs]
storeMemMeta_storeMem_None [in Libs]
storeMemMeta_storeMem_Some [in Libs]
storeMemMeta_uniqBehavior [in Libs]
storeMemMeta__invalidAddress [in Libs]
storeMemMeta__invalidAddresses [in Libs]
storeMemMeta__inversion [in Libs]
storeMemMeta__validAddress [in Libs]
storeMem_dec [in Libs]
storeMem_storeMemMeta_None [in Libs]
storeMem_storeMemMeta_Some [in Libs]
storeMem__invalidAddress [in Libs]
storeMem__invalidAddresses [in Libs]
storeMem__inversion [in Libs]
storeMem__validAddress [in Libs]
struct__subfield [in Libs]
s_cmd__cannot__RVal_or_RLoc [in BackSim]
s_cmd__G [in Props]
s_cmd__implies__us_cmd [in BackSim]
s_cmd__S [in Props]
s_cmd__S_wfFrms [in Props]
s_lhs__cannot__SystemError [in BackSim]
s_lhs__implies__us_lhs [in BackSim]
s_lhs__wf_lhs [in Props]
s_rhs__G [in Props]
s_rhs__implies__us_rhs [in BackSim]
s_rhs__S [in Props]
s_rhs__wfFrms [in Props]


U

uROK__isnot__uErrorR [in BackSim]


V

validAccessMemMeta__validAccessMem [in Libs]
validAccessMemMeta__validAddress [in Libs]
validAccessMemMeta__validStoreMem [in Libs]
validAccessMemMeta__validStoreMemMeta [in Libs]
validAccessMem__validAddress [in Libs]
validAddress__s_rhs__validAddress [in Props]
validStoreMemMeta__validAccessMem [in Libs]
validStoreMemMeta__validAddress [in Libs]
validStoreMemMeta__validStoreMem [in Libs]
validStoreMem__validAddress [in Libs]


W

wfData__monorev [in Props]
wfD__cast__wfD [in Props]
wfEnv_frF_interval_head [in Libs]
wfEnv_frF_interval_In [in Libs]
wfEnv_fromF_interval_In [in Libs]
wfEnv_F_interval_head [in Libs]
wfEnv_headTo_lesseq_tailFrom [in Libs]
wfEnv_lookUpStack__lookUpFrame [in Props]
wfEnv_topS_eq_fromF_head [in Libs]
wfEnv_top_interval [in Libs]
wfE_lookUpGlobal_validAddresses [in Props]
wfE_lookUpGlobal_wfD [in Props]
wfE_lookUpStack_validAddresses [in Props]
wfE_lookUpStack_wfD [in Props]
wfE_rev_ge_two [in Props]
wfE__accessMemMeta__wfGlobalPtr [in Props]
wfE__accessMemMeta__wfNonGlobalPtr [in Props]
wfE__accessMemMeta__wfNonStackPtr [in Props]
wfE__accessMemMeta__wfOverlapped [in Props]
wfE__accessMemMeta__wfOverlappedAMB [in Props]
wfE__accessMemMeta__wfStackPtr [in Props]
wfE__accessMemMeta__wfUniqRentryGS [in Props]
wfE__accessMemMeta__wfUniqRentryH [in Props]
wfE__storeMemMeta__wfE [in Libs]
wfE__storeMem__wfE [in Libs]
wfE__s_cmd__wfE [in Props]
wfE__s_lhs__monorev [in Props]
wfE__s_lhs__wfD [in Props]
wfE__s_lhs__wfGlobalPtr [in Props]
wfE__s_lhs__wfNonGlobalPtr [in Props]
wfE__s_lhs__wfNonStackPtr [in Props]
wfE__s_lhs__wfOverlapped_wfStackPtr [in Props]
wfE__s_lhs__wfUniqRentryGS [in Props]
wfE__s_rhs__monoAMB [in Props]
wfE__s_rhs__monorev [in Props]
wfE__s_rhs__monoRI [in Props]
wfE__s_rhs__wfD [in Props]
wfE__s_rhs__wfE [in Props]
wfE__s_rhs__wfGlobalPtr [in Props]
wfE__s_rhs__wfNonGlobalPtr [in Props]
wfE__s_rhs__wfNonStackPtr [in Props]
wfE__s_rhs__wfOverlapped [in Props]
wfE__s_rhs__wfOverlappedAMB [in Props]
wfE__s_rhs__wfStackPtr [in Props]
wfE__s_rhs__wfUniqRentryGS [in Props]
wfE__s_rhs__wfUniqRentryH [in Props]
wfFrame__storeMemMeta__wfFrame [in Libs]
wfFrame__storeMem__wfFrame [in Libs]
wfFrms_fromF_interval_In [in Libs]
wfFrms_headfr_gt_tailfr [in Libs]
wfFrms_headTo_lesseq_tailFrom [in Libs]
wfFrms_srS_interval [in Libs]
wfFrms_srS_in_nonempty [in Libs]
wfFrms_sr_eq_Ffr [in Libs]
wfFrms_top_interval [in Libs]
wfFrms__monorev [in Libs]
wfGlobalPtr_dataCast [in Props]
wfNonGlobalPtr_dataCast [in Props]
wfNonStackPtr_dataCast [in Props]
wfOverlappedAMB_dataCast [in Props]
wfOverlappedAMB_subset [in Props]
wfOverlapped_dataCast [in Props]
wfOverlapped_subset [in Props]
wfStackPtr_dataCast [in Props]
wfStackPtr_subset [in Props]
wfStack_F_interval_head [in Libs]
wfStack_lookUpStack__lookUpFrame [in Props]
wfStack_topS_eq_fromF_head [in Libs]
wfStack_top_interval [in Libs]
wfStack__storeMemMeta__wfStack [in Libs]
wfStack__storeMem__wfStack [in Libs]
wfUniqRentryGS_dataCast [in Props]
wfUniqRentryH_dataCast [in Props]
wfUniqRentryH_subset [in Props]
wf_AType__some_size [in Libs]
wf_AType__wf_subAType [in Libs]
wf_lhs_uniq [in Libs]
wf_lhs__wf_AType [in Libs]
wf_PType__sizeOfType [in Libs]
wf_rhs__wf_AType [in Libs]


_

_free__inversion [in Libs]



Constructor Index

A

Abort [in ISemantics]
A_Int [in Types]
A_Pointer [in Types]


C

C_Add [in Syntax]
C_Alloc [in Syntax]
C_Assign [in Syntax]
C_Call [in Syntax]
C_Cast [in Syntax]
C_Const [in Syntax]
C_Deref [in Syntax]
C_Free [in Syntax]
C_Lhs [in Syntax]
C_NamePos [in Syntax]
C_Ref [in Syntax]
C_Seq [in Syntax]
C_Size [in Syntax]
C_Skip [in Syntax]
C_StructPos [in Syntax]
C_Var [in Syntax]


M

MkEnv [in Envs]
MkFrame [in Envs]
MkGlobal [in Envs]
MkStack [in Envs]
MkuEnv [in Envs]
MkuFrame [in Envs]
MkuStack [in Envs]


P

P_AType [in Types]
P_Name [in Types]
P_Struct [in Types]
P_VoidPtr [in Types]


R

RLoc [in ISemantics]
ROK [in ISemantics]
RVal [in ISemantics]


S

SystemError [in ISemantics]
S_Add_Int_Int [in ISemantics]
S_Add_Int_Int_ErrorProp1 [in ISemantics]
S_Add_Int_Int_ErrorProp2 [in ISemantics]
S_Add_Ptr_Int [in ISemantics]
S_Add_Ptr_Int_ErrorProp1 [in ISemantics]
S_Add_Ptr_Int_ErrorProp2 [in ISemantics]
S_Alloc [in ISemantics]
S_Alloc_ErrorProp [in ISemantics]
S_Alloc_OutofMem [in ISemantics]
S_Assign_ErrorProp1 [in ISemantics]
S_Assign_ErrorProp2 [in ISemantics]
S_Assign_NPtr [in ISemantics]
S_Assign_Ptr [in ISemantics]
S_Call [in ISemantics]
S_Call_ErrorProp [in ISemantics]
S_Call_Error1 [in ISemantics]
S_Call_Error2 [in ISemantics]
S_Cast [in ISemantics]
S_Cast_ErrorProp [in ISemantics]
S_Cons [in Types]
S_Const [in ISemantics]
S_Deref [in ISemantics]
S_Deref_Abort [in ISemantics]
S_Deref_ErrorProp [in ISemantics]
S_Free [in ISemantics]
S_Free_Error [in ISemantics]
S_Free_ErrorProp [in ISemantics]
S_GVar [in ISemantics]
S_Lhs [in ISemantics]
S_Lhs_ErrorProp [in ISemantics]
S_NamePos [in ISemantics]
S_NamePos_Abort [in ISemantics]
S_NamePos_ErrorProp [in ISemantics]
S_Nil [in Types]
S_Ref [in ISemantics]
S_Ref_ErrorProp [in ISemantics]
S_Seq [in ISemantics]
S_Seq_ErrorProp1 [in ISemantics]
S_Seq_ErrorProp2 [in ISemantics]
S_Size [in ISemantics]
S_Skip [in ISemantics]
S_StructPos [in ISemantics]
S_StructPos_Abort [in ISemantics]
S_StructPos_ErrorProp [in ISemantics]
S_SVar [in ISemantics]


U

uRLoc [in CSemantics]
uROK [in CSemantics]
uRVal [in CSemantics]
uSystemError [in CSemantics]
uS_Add_Int_Int [in CSemantics]
uS_Add_Int_Int_ErrorProp1 [in CSemantics]
uS_Add_Int_Int_ErrorProp2 [in CSemantics]
uS_Add_Ptr_Int [in CSemantics]
uS_Add_Ptr_Int_ErrorProp1 [in CSemantics]
uS_Add_Ptr_Int_ErrorProp2 [in CSemantics]
uS_Alloc [in CSemantics]
uS_Alloc_ErrorProp [in CSemantics]
uS_Alloc_OutofMem [in CSemantics]
uS_Assign [in CSemantics]
uS_Assign_ErrorProp1 [in CSemantics]
uS_Assign_ErrorProp2 [in CSemantics]
uS_Call [in CSemantics]
uS_Call_ErrorProp [in CSemantics]
uS_Call_Error1 [in CSemantics]
uS_Call_Error2 [in CSemantics]
uS_Cast [in CSemantics]
uS_Cast_ErrorProp [in CSemantics]
uS_Const [in CSemantics]
uS_Deref [in CSemantics]
uS_Free [in CSemantics]
uS_Free_Error [in CSemantics]
uS_Free_ErrorProp [in CSemantics]
uS_GVar [in CSemantics]
uS_Lhs [in CSemantics]
uS_NamePos [in CSemantics]
uS_Ref [in CSemantics]
uS_Seq [in CSemantics]
uS_Seq_ErrorProp1 [in CSemantics]
uS_Seq_ErrorProp2 [in CSemantics]
uS_Size [in CSemantics]
uS_Skip [in CSemantics]
uS_StructPos [in CSemantics]
uS_SVar [in CSemantics]


W

wfFrms_cons [in Envs]
wfFrms_nil [in Envs]
WF_Add_Int_Int [in Syntax]
WF_Add_Ptr_Int [in Syntax]
WF_Alloc [in Syntax]
WF_Assign [in Syntax]
wf_A_Int [in Types]
wf_A_TamePointer [in Types]
WF_Call [in Syntax]
WF_Cast [in Syntax]
WF_Const [in Syntax]
WF_Deref [in Syntax]
WF_Free [in Syntax]
WF_GVar [in Syntax]
WF_Lhs [in Syntax]
WF_NamePos [in Syntax]
wf_P_AType [in Types]
wf_P_Name [in Types]
wf_P_Struct [in Types]
wf_P_VoidPtr [in Types]
WF_Ref [in Syntax]
WF_Seq [in Syntax]
WF_Size [in Syntax]
WF_Skip [in Syntax]
WF_StructPos [in Syntax]
WF_SVar [in Syntax]
wf_S_Cons [in Types]
wf_S_Nil [in Types]



Inductive Index

A

AType [in Types]


C

c_cmd [in Syntax]
c_lhs [in Syntax]
c_rhs [in Syntax]


P

PType [in Types]


R

Result [in ISemantics]


S

Struct [in Types]
s_cmd [in ISemantics]
s_lhs [in ISemantics]
s_rhs [in ISemantics]


U

uResult [in CSemantics]
us_cmd [in CSemantics]
us_lhs [in CSemantics]
us_rhs [in CSemantics]


W

wfFrms [in Envs]
wf_AType [in Types]
wf_cmd [in Syntax]
wf_lhs [in Syntax]
wf_PType [in Types]
wf_rhs [in Syntax]
wf_Struct [in Types]



Definition Index

A

accessMemMeta [in Envs]
addAllocMemBlock [in Envs]
addRI [in Envs]
AllocMemBlock [in Envs]
assertion_ptr [in ISemantics]
assertion_spatial_ptr [in ISemantics]
assertion_temporal_ptr [in ISemantics]


B

Base [in Envs]
Bound [in Envs]


C

createFrame [in Envs]
c_ident [in Types]


D

Data [in ISemantics]
dataCast [in ISemantics]
destroyFrame [in Envs]


E

Env2uEnv [in Envs]
Error [in ISemantics]


F

frame [in Envs]
Frames2uFrames [in Envs]
Frame2frame [in Envs]
Frame2uFrame [in Envs]
free [in Envs]


G

getStructOffset [in Types]
getStructType [in Types]


I

isPtr [in Types]


K

Key [in Envs]


L

Loc [in Envs]
LockAddr [in Envs]
LockTable [in Envs]
lookUpFrame [in Envs]
lookUpGlobal [in Envs]
lookUpStack [in Envs]
lookUpuFrame [in Envs]
lookUpuStack [in Envs]


M

malloc [in Envs]
Mem [in Envs]
Meta [in Envs]
MMeta [in Envs]
mutual_AType_Struct_ind [in Types]
mutual_wf_AType_Struct_PType_ind [in Types]


R

removeAllocMemBlock [in Envs]
removeRI [in Envs]


S

sizeOfAType [in Types]
sizeOfPType [in Types]
sizeOfStruct [in Types]
Stack2frame [in Envs]
Stack2uStack [in Envs]
storeMemMeta [in Envs]


U

uError [in CSemantics]
uFrame2frame [in Envs]
updateMetadata [in Envs]
updateMetadatas [in Envs]
uStack2frame [in Envs]


V

validAddress [in Envs]
Value [in Envs]
Var [in Envs]


W

wfAllocMemBlock [in Envs]
wfData [in Envs]
wfEnv [in Envs]
wfFrame [in Envs]
wfFrameNoOverlapped [in Envs]
wfGlobal [in Envs]
wfGlobalPtr [in Envs]
wfMem [in Envs]
wfNonGlobalPtr [in Envs]
wfNonStackPtr [in Envs]
wfOverlapped [in Envs]
wfOverlappedAMB [in Envs]
wfStack [in Envs]
wfStackPtr [in Envs]
wfuFrameNoOverlapped [in Envs]
wfUniqRentryGS [in Envs]
wfUniqRentryH [in Envs]



Axiom Index

A

accessMem [in Envs]


B

baseAddress [in Envs]


F

funTable [in Syntax]


G

getFreshRentry [in Envs]
getFreshRentry__inversion [in Axioms]
gri [in Envs]


M

maxAddress [in Envs]
minAddress [in Envs]


S

storeMem [in Envs]
storeMem_uniqBehavior [in Axioms]
storeMem__accessMem [in Axioms]


T

typeTable [in Types]


U

ucreateFrame [in Envs]
ucreateFrame__inversion [in Axioms]
udestroyFrame [in Envs]
udestroyFrame__inversion [in Axioms]
ufree [in Envs]
ufree__inversion [in Axioms]
umalloc [in Envs]
umalloc__inversion [in Axioms]


V

validAccessMem__validStoreMem [in Axioms]
validAddressRange [in Axioms]



Library Index

A

Axioms


B

BackSim


C

CSemantics


E

Envs


I

Introduction
ISemantics


L

Libs


P

Props


S

Syntax


T

Tactics
Types


W

WfEnv



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (506 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (25 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (7 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (202 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (145 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (21 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (72 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (22 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (12 entries)

This page has been generated by coqdoc