Index of module types


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]