Index of types


A
a_kind [WpPropId]
access [RefUsage]
acs [Memory]
adt [Lang]
alloc [MemTyped]
annot_kind [WpStrategy]
An annotation can be used for different purpose.
annots [WpStrategy]
Some elements can be used as both Hyp and Goal : because of the selection mecanism, we need to add a boolean as_goal to tell if the element is to be considered as a goal.
annots_tbl [WpStrategy]
arrayflat [Ctypes]
Array objects, with both the head view and the flatten view.
arrayinfo [Ctypes]
asked_assigns [WpAnnot]
asked_bhv [WpAnnot]
asked_prop [WpAnnot]
assigns_desc [WpPropId]
assigns_full_info [WpPropId]
assigns_info [WpPropId]
atom [MemTyped.Layout]
attributed [Conditions]
axiom_info [WpPropId]
axiomatic [LogicUsage]
axioms [Definitions]

B
bal [Driver]
balance [Lang]
binding [Passive]
binop [Lang.F]
block [MemTyped.Layout]
block_type [Cil2cfg]
Be careful that only Bstmt are real Block statements
builtin [LogicBuiltins]
bundle [Conditions]

C
c_float [Ctypes]
Runtime floats.
c_int [Ctypes]
Runtime integers.
c_label [Clabels]
c_object [Ctypes]
Type of variable, inits, field or assignable values.
call [GuiSource]
call_type [Cil2cfg]
call_vcs [CfgWP.VC]
callenv [CfgWP.VC]
callenv [Calculus.Cfg]
card [GuiNavigator]
case [Variables_analysis]
cast [RefUsage]
category [LogicBuiltins]
cc [Wp_error]
cell [CfgLib.Make]
cfg [CfgTypes.Cfg]
cfg [CfgLib.Make]
chunk [Memory.Model]
chunk [Memory.Sigma]
chunk [MemTyped]
chunk [MemVar.Make.Sigma]
chunk [MemVar.Make]
chunk [MemEmpty]
chunk [Sigma.Make]
chunk [LogicCompiler.Make]
cistat [WpReport]
cluster [Definitions]
cmp [Lang.F]
collector [Warning]
command [Rformat]
comparison [MemTyped.Layout]
condition [Conditions]
config [WpReport]
console [Rformat]
context [Warning]
context [RefUsage]
coq_wpo [ProverCoq]
coqcc [ProverCoq]
coqlib [ProverCoq]
coverage [WpReport]
cst [Cstring]
cvsort [LogicSemantics.Make]

D
data [Model.Data]
data [Model.Registry]
data [Model.Entries]
data [Model.Generator]
data [Model.Static]
data [Model.Index]
data [State_builder.Hashtbl]
data [State_builder.Ref]
Type of the referenced value.
database [LogicUsage]
decl [Mcfg.Export]
definition [Definitions]
delta [MemVar.Make]
delta [VarUsage.Context]
denv [Matrix]
depend [ProverWhy3]
depend [ProverCoq]
depend [ProverErgo]
dfun [Definitions]
dim [Matrix]
disjunction [Conditions]
display_state [GuiGoal]
dlemma [Definitions]
domain [Memory.Sigma]
domain [MemVar.Make.Sigma]
domain [Sigma.Make]
domain [VarUsage.Usage]
doption [LogicBuiltins]
dotter [CfgTypes.Cfg]
dotter [CfgLib.Make]
dp [ProverWhy3]
driver [Factory]
driver [LogicBuiltins]
dstats [WpReport]

E
edge [Cil2cfg]
abstract type of the cfg edges
edge_key [Cil2cfg]
edge_type [Cil2cfg]
effect [CfgWP.VC]
effect_source [WpPropId]
element [Why3_xml]
elt [Set.S]
The type of the set elements.
entries [Model.Static]
entries [Model.Index]
entry [WpReport]
env [LogicSemantics.Make]
env [LogicCompiler.Make]
env [Lang.F]
eqsort [LogicSemantics.Make]
error [ProverWhy3]
export [ProverErgo]
extern [Lang]

F
f1 [Fixpoint.Make]
f2 [Fixpoint.Make]
fcstat [WpReport]
field [Lang]
fields [Lang]
file [Why3_session]
filter [GuiNavigator]
fixpoint [Fixpoint.Make]
fn [Fixpoint.Make]
focus [GuiNavigator]
formal_kind [Variables_analysis]
formula [Wpo]
frame [LogicSemantics.Make]
frame [LogicCompiler.Make]
functions [Generator]

G
gamma [Lang]
goal [Why3_session]
goal_id [ProverWhy3]
graph [Cil2cfg.WeiMaoZouChenInput]
graph [Cil2cfg.LoopInfo]
group [CfgWP.VC]

H
hints [WpPropId]
hypotheses [Conditions]

I
included [ProverCoq]
index [Wpo]
inductive_case [LogicUsage]
infoprover [Lang]
generic way to have different informations for the provers
input [Driver]
input [Script]
instance [Factory]
istat [WpReport]

J
job [Wp_parameters]

K
key [Map.S]
The type of the map keys.
key [Model.Data]
key [Model.Registry]
key [Model.Entries]
key [Model.Generator]
key [Model.Static]
key [Model.Index]
key [Hashtbl.S]
key [Cil2cfg.PMAP]
key [FCMap.S]
The type of the map keys.
key [Wprop.Info]
key [State_builder.Hashtbl]
key [Wprop.Indexed]
key1 [Wprop.Indexed2]
key2 [Wprop.Indexed2]
kind [LogicBuiltins]

L
l_builtin [Cint]
label [CfgLib.Labels]
label_mapping [NormAtLabels]
language [VCS]
layout [MemTyped.Layout]
lfun [Lang]
library [Lang]
link [Conditions]
linker [Conditions]
linkinfo [Lang]
loader [Cvalues.Logic]
loc [Memory.Model]
Representation of the memory location in the model.
loc [MemTyped]
loc [MemVar.Make]
loc [MemEmpty]
loc [LogicAssigns.Logic]
loc [LogicAssigns.Code]
loc [LogicSemantics.Make]
loc [CodeSemantics.Make]
logic [Memory]
logic [LogicSemantics.Make]
logic [LogicCompiler.Make]
logic [Cvalues.Logic]
logic_lemma [LogicUsage]
logic_section [LogicUsage]
logs [ProverTask]
lv_value [LogicSemantics.Make]

M
marks [CfgTypes.Cfg]
Markers for CFG exploration.
marks [CfgLib.Make]
matrix [Matrix]
mdt [Lang]
name to print to the provers
memory [GuiPanel]
mheap [Factory]
mode [VCS]
model [Cfloat]
model [Cint]
model [Lang]
model [Model]
model [RefUsage]
mprover [GuiConfig]
mvar [Factory]

N
node [CfgTypes.Cfg]
node [Cil2cfg.WeiMaoZouChenInput]
node [Cil2cfg.LoopInfo]
node [Cil2cfg]
abstract type of the cfg nodes
node [CfgLib.Make]
node_id [Cil2cfg]
node_info [Cil2cfg]
node_type [Cil2cfg]
notask [Why3_session]

O
occur [Cleaning]
occur [Letify.Split]
offset [Region]
ofs [MemVar.Make]
outcome [Conditions]
outcome [Warning]

P
param [MemVar]
part [Wpo]
partition [WTO]
path [Region]
po [Wpo]
Dynamically exported as "Wpo.po"
pointer [MemTyped]
pp_cfg [CfgTypes.Cfg]
pp_cfg [CfgLib.Make]
pp_edge_fun [Cil2cfg]
type of functions to print things related to edges
pred [Mcfg.Splitter]
pred [Mcfg.Export]
pred [Lang.F]
pred_info [WpPropId]
proof [WpAnnot]
A proof accumulator for a set of related prop_id
proofpart [WpAnnot]
prop_id [WpPropId]
Property.t information and kind of PO (establishment, preservation, etc)
prop_kind [WpPropId]
property [Wprop]
prover [VCS]
prover_state [GuiGoal]
pstat [Register]
pstats [WpReport]

R
range [MemTyped]
recursion [Definitions]
region [LogicAssigns.Make]
region [LogicSemantics.Make]
region [Cvalues.Logic]
region [Region]
registered_shift [MemTyped]
res [WpReport]
result [VCS]
return [Cil2cfg.PMAP]
rloc [Memory]
roffset [Region]
rpath [Region]
rules [Fixpoint.Make]

S
scc [WTO]
scope [Mcfg]
section [WpReport]
segment [Memory.Model]
segment [MemTyped]
segment [MemVar.Make]
segment [MemEmpty]
selection [GuiSource]
sem [Fixpoint.Make]
seq [MemVar.Make]
sequence [Memory]
sequence [Conditions]
sequent [Conditions]
session [Why3_session]
set [Vset]
setup [Factory]
sig_param [LogicCompiler.Make]
sigfun [LogicBuiltins]
sigma [Memory.Model]
sigma [MemTyped]
sigma [MemVar.Make]
sigma [MemEmpty]
sigma [LogicSemantics.Make]
sigma [LogicCompiler.Make]
sigma [CodeSemantics.Make]
signature [LogicCompiler.Make]
sistat [WpReport]
sloc [Memory]
source [Lang]
stats [WpReport]
step [Conditions]
strategy [WpStrategy]
strategy [Fixpoint.Make]
strategy_for_froms [WpStrategy]
strategy_info [WpAnnot]
strategy_kind [WpStrategy]
succ [WTO]
system [Wpo]
system [Fixpoint.Make]

T
t [Indexer.Make]
t [Memory.Sigma]
t [Memory.Chunk]
t [CfgWP.VC.EFFECT]
t [CfgWP.VC.TARGET]
t [Calculus.Cfg.R]
t [Why3_xml]
t [Set.S]
The type of sets.
t [Map.S]
The type of maps from type key to type 'a.
t [Wpo.Results]
t [Wpo.Index]
t [Wpo.VC_Check]
t [Wpo.VC_Annot]
t [Wpo.VC_Lemma]
t [Wpo.GOAL]
t [Wpo]
t [MemTyped.LITERAL]
t [MemTyped.Chunk]
t [MemVar.Make.Sigma]
t [MemVar.Make.Chunk]
t [MemVar.Make.VALLOC]
t [MemVar.Make.VAR]
t [MemEmpty.Chunk]
t [Sigma.Make]
t [Cstring.STR]
t [Conditions.Bundle]
t [Letify.Defs]
t [Letify.Sigma]
t [Splitter]
t [Passive]
t [Matrix.KEY]
t [Lang.Alpha]
t [Lang.Fun]
t [Lang.Field]
t [Lang.ADT]
t [Model.Key]
t [Model.Static.KEY]
t [Model.Index.KEY]
t [Model]
t [Warning.SELF]
t [Cil2cfg.HEsig]
t [Cil2cfg.Printer]
t [Cil2cfg.HE]
t [Hashtbl.S]
t [Cil2cfg.PMAP]
t [Cil2cfg.EL]
t [Cil2cfg.VL]
t [Cil2cfg]
The final CFG is composed of the graph, but also : the function that it represents, an hashtable to find a CFG node knowing its hashcode
t [RefUsage.E]
t [RefUsage.Access]
t [RefUsage.Var]
t [VarUsage.Occur]
t [VarUsage.Context]
t [VarUsage.Root]
t [FCMap.S]
The type of maps from type key to type 'a.
t [Clabels.T]
t [Ctypes.AinfoComparable]
t [String]
An alias for the type of strings.
t [Fixpoint.Domain]
t [CfgLib.Transform]
t [CfgLib.Labels]
t [CfgLib.Attr]
t_annots [WpStrategy]
a set of annotations to be added to a program point.
t_env [Mcfg.S]
t_env [CfgWP.VC]
t_env [CfgDump.VC]
t_prop [Mcfg.S]
t_prop [CfgWP.VC]
t_prop [CfgDump.VC]
tag [Splitter]
target [CfgWP.VC]
target [VarUsage.Context]
tau [Lang]
tenv [Cil2cfg.WeiMaoZouChenInput]
tenv [Cil2cfg.LoopInfo]
test_behav_res [WpAnnot]
Tells weather the property belonging to the behaviors in bhv_name_list has to be considered according to config.
theory [Why3_session]
ti [Cil2cfg.HEsig]
ti [Cil2cfg.HE]
token [Driver]
token [Script]
transition [CfgTypes.Cfg]
transition [CfgTypes.Transition]
transition [CfgLib.Make]
trigger [Definitions]
tuning [Model]
typedef [Definitions]

U
unop [Lang.F]
usage [Cleaning]
usage [Variables_analysis]
usage [VarUsage]

V
value [Memory]
value [LogicSemantics.Make]
value [LogicCompiler.Make]
value [CodeSemantics.Make]
value [Context]
value [RefUsage]
value [VarUsage.Model]
var [RefUsage]
var [Fixpoint.Make]
var_kind [Variables_analysis]
var_type [Variables_analysis]
vc [CfgWP.VC]
verdict [VCS]
visit [WTO]
vset [Vset]