C | |
Chunk [Memory] | |
Chunk [Wp.Memory] | |
Code [LogicAssigns] | |
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 | |
Logic [LogicAssigns] | |
M | |
Model [Memory] | |
Model [Wp.Memory] | |
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 [Memory] | |
Sigma [Wp.Memory] | |
Splitter [Mcfg] | |
Splitter [Wp.Mcfg] | |
V | |
VarUsage [MemVar] | |
VarUsage [Wp.MemVar] |