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] | |
DataflowAnalysis [Interpreted_automata] | Simple dataflow analysis |
Domain [Interpreted_automata] | Input domain for a simple dataflow analysis. |
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 [Sigs] | Memory Models. |
Model [MemLoader] | Loader Model for Atomic Values |
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] | |
State [MemVal] | |
State [Wp.MemVal] | |
V | |
VCgen [CfgWP] | |
Value [MemVal] | |
Value [Wp.MemVal] | |
VarUsage [MemVar] | |
VarUsage [Wp.MemVar] |