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] |