Index of modules


A
A [CfgWP.VC]
ADT [Lang]
ALLOC [MemVar.Make]
ARRAY [MemTyped]
Access [RefUsage]
AddrTaken [Variables_analysis]
AinfoComparable [Ctypes]
Alpha [Lang]
AltErgoFlags [Wp_parameters]
AltErgoLibs [Wp_parameters]
AnyVar [Variables_analysis]
ArgAReference [Variables_analysis]
ArgPReference [Variables_analysis]
Attr [CfgLib]
Axiomatic [LogicCompiler.Make]

B
BASE [MemTyped]
Behaviors [Wp_parameters]
Bits [Wp_parameters]
Bundle [Conditions]
ByAReference [Variables_analysis]
ByPReference [Variables_analysis]
ByValue [Variables_analysis]

C
C [CfgWP.VC]
C [LogicSemantics.Make]
CFG [Cil2cfg]
CInfo [Dyncall]
CLUSTERS [ProverWhy3]
CLUSTERS [ProverCoq]
CLUSTERS [ProverErgo]
COBJ [Matrix]
COMP [MemTyped]
C_object [Ctypes]
Calculus
Wp computation using the CFG
CallPoints [Dyncall]
Calls [Dyncall]
Cfg [Calculus]
CfgDump
CfgLib
Creating CFG
CfgTypes
Reversed with repetitions
CfgWP
Cfloat
Floatting Arithmetic Model
ChainCalls [Variables_analysis]
Check [Wp_parameters]
Chunk [Memory.Model]
Chunk [MemTyped]
Chunk [MemVar.Make]
Chunk [MemEmpty]
Cil2cfg
Build a CFG of a function keeping some information of the initial structure.
Cint
Integer arithmetics
Clabels
Normalized C-labels
Clean [Wp_parameters]
Cleaning
Cluster [Definitions]
Cmap [Wpo.Results]
CodeSemantics
Computer [CfgWP]
Conditions
Bundles
Context
Current Loc
Context [VarUsage]
CoqLibs [Wp_parameters]
CoqTactic [Wp_parameters]
CoqTimeout [Wp_parameters]
Cstring
Since its a generated it is the unique name given "Lit_%04X" id
Ctypes
C-Types
Cvalues
Int-As-Boolans

D
D [CfgWP.VC]
D [Model]
DATA [Lang.F]
DC [Definitions]
DEPS [GuiSource]
DF [Definitions]
DISK [Wpo]
DR [Definitions]
DS [Definitions]
DT [Definitions]
Database [LogicUsage]
DatabaseType [LogicUsage]
Datatype [State_builder.S]
Definitions
return type of an abstract function
Defs [Conditions]
Defs [Letify]
Depth [Wp_parameters]
Detect [Wp_parameters]
Dom [LogicAssigns.Make]
Domain [VarUsage]
Driver
Memoized loading of drivers according to current WP options.
Drivers [Wp_parameters]
DynCall [Wp_parameters]
Dyncall
Returns an property identifier for the precondition.

E
E [Model.Registry]
E [Model.Static]
E [Model.Index]
E [Cil2cfg.Printer]
E [RefUsage]
EFFECT [CfgWP.VC]
EL [Cil2cfg]
the CFG edges
ENTRIES [Model.Static]
ENTRIES [Model.Index]
EQARRAY [Cvalues]
Eset [CfgWP.VC]
Eset [Cil2cfg]
Set of edges.
ExtEqual [Wp_parameters]
ExternArrays [Wp_parameters]

F
F [Lang]
Factory
Fc_config [Wp_parameters]
Field [Lang]
Fixpoint
add x y requires x >= y
Fmap [Wpo]
ForCall [WpStrategy]
Fun [Lang]
FunFile [ProverWhy3]
FunMap [Cint]
Functions [Wp_parameters]

G
G [CfgWP.VC]
G [Model.Generator]
GOAL [Wpo]
GOALS [Register]
GS [WpAnnot]
Generate [Wp_parameters]
Generator
Generator [Model]
Gmap [CfgWP.VC]
Gmap [Wpo]
Gset [CfgWP.VC]
GuiConfig
Edit enabled provers
GuiGoal
GuiList
GuiNavigator
GuiPanel
GuiSource

H
H [Model.MODELS]
H [Wprop.Indexed]
HE [Cil2cfg]
HEAP [MemVar.Make]
HEloop [Cil2cfg]
Hannots [WpStrategy]
This is an Hashtbl where some predicates are stored on CFG edges.
Hashtbl [Datatype.S_with_collections]
HdefAnnotBhv [WpAnnot]
Heap [Memory.Model]
Heap [MemTyped]
Heap [MemVar.Make]
Heap [MemEmpty]
Hints [Wp_parameters]
Hmap [LogicAssigns.Make]
Hproof [Wpo]

I
I [Splitter]
I [Wprop.Indexed2]
Includes [Wp_parameters]
Index [Wpo]
Index [Model]
projectified, depend on the model, not serialized
Indexed [Wprop]
Indexed2 [Wprop]
Init [Wp_parameters]
Invariants [Wp_parameters]

K
KEY [Matrix]
KEY [Model.Static]
KEY [Model.Index]
Key [Datatype.Hashtbl]
Datatype for the keys of the hashtbl.
Key [Datatype.Map]
Datatype for the keys of the map.
KfCfg [Cil2cfg]

L
L [CfgWP.VC]
L [MemTyped]
L [LogicSemantics.Make]
LIT [Cstring]
LITERAL [MemTyped]
LMap [LogicUsage]
LSet [LogicUsage]
LabelMap [Clabels]
LabelSet [Clabels]
Labels [CfgLib]
Lang
name to print to the provers
Layout [MemTyped]
Lemma [Definitions]
Let [Wp_parameters]
Letify
bind sigma defs xs select definitions in defs targeting variables xs.
Literals [Wp_parameters]
Log [Wp_parameters]
Logic [MemEmpty]
Logic [Cvalues]
LogicAssigns
LogicBuiltins
Includes
LogicCompiler
Definitions
LogicParam [Variables_analysis]
LogicSemantics
Debug
LogicUsage
Trims the original name
LoopInfo [Cil2cfg]
To use WeiMaoZouChen algorithm, we need to define how to interact with our CFG graph

M
M [Splitter]
M [Cil2cfg.PMAP]
MACHINE [Matrix]
MAP [Model.Static]
MAP [Model.Index]
MHoareRef [Factory]
MHoareVar [Factory]
MODEL [Factory]
MODELS [Model]
MONOTONIC [MemTyped]
MTypedRef [Factory]
MTypedVar [Factory]
Make [MemVar]
Make [Sigma]
Make [LogicAssigns]
Make [LogicSemantics]
Make [LogicCompiler]
Make [CodeSemantics]
Make [Datatype.Hashtbl]
Build a datatype of the hashtbl according to the datatype of values in the hashtbl.
Make [Datatype.Map]
Build a datatype of the map according to the datatype of values in the map.
Make [Fixpoint]
Make [CfgLib]
Map [Warning]
Map [Datatype.S_with_collections]
Marked [ProverCoq]
Matrix
unique w.r.t equal
Mcfg
This is what is really needed to propagate something through the CFG.
MemEmpty
MemTyped
MemVar
Memory
Memory Values
Mloop [Cil2cfg]
Model
TODO: register and find below?
Model [VarUsage]
Model [Wp_parameters]
MyGraph [Cil2cfg]
the CFG is an ocamlgraph, but be careful to use it through the cfg function because some edges don't have the same meaning as some others...

N
NATURAL [Matrix]
NULL [Cvalues]
Names [WpPropId]
NormAtLabels
push the Tat down to the 'data' operations.
Nset [Cil2cfg]
Set of nodes.
Ntbl [Cil2cfg]
Hashtbl of node

O
OP [Cfloat]
Occur [VarUsage]
Omap [VarUsage]
OutputDir [Wp_parameters]

P
P [CfgWP.VC]
P [Wprop.Indexed2]
PATH [GuiSource]
PInfo [Dyncall]
PM [Register]
PMAP [CfgWP.VC]
PMAP [Cil2cfg]
PODatatype [Wpo]
Passive
Passive Forms
Pmap [Wpo]
Pmap [Wpo.Results]
Pmap [Lang.F]
Point [Dyncall]
Pretty [Lang.F]
Pretty [WpPropId]
Print [Wp_parameters]
Printer [Cil2cfg]
Procs [Wp_parameters]
Proof
Proof Script Database
ProofTrace [Wp_parameters]
PropId [WpPropId]
Properties [Wp_parameters]
Prover
Different instance of why3ide can't be run simultanely
ProverCoq
ProverErgo
ProverTask
never fails
ProverType [Wpo]
ProverWhy3
TODO add them only when needed
Provers [Wp_parameters]
Prune [Wp_parameters]
Pset [Lang.F]

Q
QedChecks [Wp_parameters]

R
R [Calculus.Cfg]
to store the results of computations : we store a result for each edge, and also a list of proof obligations.
REGISTRY [Model.Static]
REGISTRY [Model.Index]
RTE [Wp_parameters]
RefUsage
Region
Paths
Register
Do on_server_stop save why3 session
RegisterShift [MemTyped]
Report [Wp_parameters]
ReportName [Wp_parameters]
ResultType [Wpo]
Results [Wpo]
Rformat
get_time T t returns k such that T[k-1] <= t <= T[k], T is extended with T[-1]=0 and T[N]=+oo.
Root [VarUsage]
Rte_generated [GuiPanel]

S
S [CfgWP.VC]
S [Why3_session]
S [Wpo]
S [Model]
SELF [Warning]
SET [Model.Static]
SET [Model.Index]
SIGMA [MemVar.Make]
SMap [LogicUsage]
STATE [Lang.F]
STR [Cstring]
STRING [MemTyped]
STRING [Wp_parameters]
STRUCTURAL [Cvalues]
SYSTEM [Wpo]
Script
Script [Wp_parameters]
Set [Warning]
Set [Datatype.S_with_collections]
Shift [MemTyped]
ShiftField [MemTyped]
Sigma [Memory.Model]
Sigma [MemTyped]
Sigma [MemVar.Make]
Sigma [MemEmpty]
Sigma
Sigma [Conditions]
Sigma [Letify]
Signature [LogicCompiler.Make]
Simpl [Wp_parameters]
SkipFunctions [Wp_parameters]
Smap [WpReport]
Split [Letify]
Pruning strategy ; selects most occuring literals to split cases.
Split [Wp_parameters]
Splitter
Static [Model]
projectified, not serialized
StatusAll [Wp_parameters]
StatusFalse [Wp_parameters]
StatusMaybe [Wp_parameters]
StatusTrue [Wp_parameters]
Steps [Wp_parameters]
String [Prover]
Symbol [Definitions]

T
T [CfgTypes.Cfg]
T [Lang.F]
T [Clabels]
T [CfgLib.Make]
TALLOC [MemVar.Make]
TARGET [CfgWP.VC]
TMap [LogicUsage]
TT [Lang.F]
TYPE [Cvalues]
TYPES [ProverWhy3]
TYPES [ProverErgo]
Tags [Splitter]
Timeout [Wp_parameters]
Transform [CfgLib]
Trigger [Definitions]
TruncPropIdFileName [Wp_parameters]
TryHints [Wp_parameters]

U
U [VarUsage]
UpdateScript [Wp_parameters]
Usage [VarUsage]

V
V [CfgWP.VC]
V [Cil2cfg.Printer]
VALLOC [MemVar.Make]
VAR [MemVar.Make]
VC [CfgWP]
VC [CfgDump]
VCG [CfgWP.Computer]
VCS
Verification Conditions Database
VC_Annot [Wpo]
VC_Check [Wpo]
VC_Lemma [Wpo]
VL [Cil2cfg]
the CFG nodes
Var [RefUsage]
VarHoare [Factory]
VarRef0 [Factory]
VarRef2 [Factory]
VarType [Variables_analysis]
VarUsage
Usage Variable Analysis
Variables_analysis
This analysis performs a classification of the variables of the input program.
Vmap [Lang.Alpha]
Vset
Logical Sets

W
W [CfgWP.VC]
W [LogicBuiltins]
WP [CfgWP.Computer]
WP [CfgDump]
WP [Wp_parameters]
WP [Wprop]
WPOmap [Wpo]
WPOset [Wpo]
WP_HoareRef [Factory]
WP_HoareVar [Factory]
WP_TypedRaw [Factory]
WP_TypedRef [Factory]
WP_TypedVar [Factory]
WTO
Returns a weak partial order with Bourdoncle's algorithm.
Warning
Contextual Errors
WeiMaoZouChen [Cil2cfg]
Implementation of "A New Algorithm for Identifying Loops in Decompilation"
Why3_session
Not mutated after the creation
Why3_xml
This file and the implementation have not been modified from the orignal why3 file (except removing the uses of the Debug module)
WhyFlags [Wp_parameters]
WhyLibs [Wp_parameters]
Windex [GuiList]
WpAnnot
Properties for assigns of kf
WpLog [CfgWP]
WpLog [Ctypes]
WpMain [VarUsage]
WpPropId
Beside the property identification, it can be found in different contexts depending on which part of the computation is involved.
WpReport
start chapter stats
WpStrategy
An annotation can be used for different purpose.
Wp_error
To be raised a feature of C/ACSL cannot be supported by a memory model or is not implemented, or ...
Wp_parameters
call the construction of the directory only once
Wpo
Proof Obligations
Wprop
Indexed API

X
XS [Letify]
Xml [Why3_session]

Z
ZInteger [Lang.F]