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