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 [Model]
Data [Wp.Model]
E
Entries [Model]
Entries [Wp.Model]
Export [Mcfg]
Export [Wp.Mcfg]
G
Generator [Model]
Generator [Wp.Model]
H
HEsig [Cil2cfg]

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

I
Indexed [Wprop]
Indexed2 [Wprop]
Info [Wprop]
K
Key [Model]
Key [Wp.Model]
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 [Sigs]

Memory Models.

Model [Wp.Sigs]

Memory Models.

R
Registry [Model]
Registry [Wp.Model]
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]