Index of module types

C
Cfg [CfgCompiler]
Cfg [Wp.CfgCompiler]
Chunk [Sigs]

Memory Chunks.

Chunk [Wp.Sigs]

Memory Chunks.

CodeSemantics [Sigs]

Compiler for C expressions

CodeSemantics [Wp.Sigs]

Compiler for C expressions

Compiler [Sigs]

All Compilers Together

Compiler [Wp.Sigs]

All Compilers Together

D
Data [Layout]
Data [WpContext]
Data [Wp.WpContext]
E
Entries [WpContext]
Entries [Wp.WpContext]
Export [Mcfg]
Export [Wp.Mcfg]
G
Generator [WpContext]
Generator [Wp.WpContext]
H
HEsig [Cil2cfg]

signature of a mapping table from cfg edges to some information.

I
IData [WpContext]
IData [Wp.WpContext]
Indexed [Wprop]
Indexed2 [Wprop]
Info [Wprop]
K
Key [WpContext]
Key [Wp.WpContext]
L
LogicAssigns [Sigs]

Compiler for Performing Assigns

LogicAssigns [Wp.Sigs]

Compiler for Performing Assigns

LogicSemantics [Sigs]

Compiler for ACSL expressions

LogicSemantics [Wp.Sigs]

Compiler for ACSL expressions

M
Model [MemLoader]

Loader Model for Atomic Values

Model [Sigs]

Memory Models.

Model [Wp.Sigs]

Memory Models.

R
Registry [WpContext]
Registry [Wp.WpContext]
S
S [Mcfg]

This is what is really needed to propagate something through the CFG.

S [Wp.Mcfg]

This is what is really needed to propagate something through the CFG.

Sigma [Sigs]

Memory Environments.

Sigma [Wp.Sigs]

Memory Environments.

Splitter [Mcfg]
Splitter [Wp.Mcfg]
V
VarUsage [MemVar]
VarUsage [Wp.MemVar]