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