Index of types


A
a_kind [WpPropId]
a_kind [Wp.WpPropId]
access [RefUsage]
access [Wp.RefUsage]
acs [Memory]
acs [Wp.Memory]
adt [Lang]
adt [Wp.Lang]
annot_kind [WpStrategy]
An annotation can be used for different purpose.
annots_tbl [WpStrategy]
arrayflat [Ctypes]
Array objects, with both the head view and the flatten view.
arrayflat [Wp.Ctypes]
Array objects, with both the head view and the flatten view.
arrayinfo [Ctypes]
arrayinfo [Wp.Ctypes]
asked_assigns [WpAnnot]
assigns_desc [WpPropId]
assigns_desc [Wp.WpPropId]
assigns_full_info [WpPropId]
assigns_full_info [Wp.WpPropId]
assigns_info [WpPropId]
assigns_info [Wp.WpPropId]
attributed [Conditions]
attributed [Wp.Conditions]
axiom_info [WpPropId]
axiom_info [Wp.WpPropId]
axiomatic [LogicUsage]
axiomatic [Wp.LogicUsage]
axioms [Definitions]
axioms [Wp.Definitions]

B
balance [Lang]
balance [Wp.Lang]
binop [Lang.F]
binop [Wp.Lang.F]
block_type [Cil2cfg]
Be careful that only Bstmt are real Block statements
builtin [LogicBuiltins]
builtin [Wp.LogicBuiltins]
bundle [Conditions]
bundle [Wp.Conditions]

C
c_float [Ctypes]
Runtime floats.
c_float [Wp.Ctypes]
Runtime floats.
c_int [Ctypes]
Runtime integers.
c_int [Wp.Ctypes]
Runtime integers.
c_label [Clabels]
c_label [Wp.Clabels]
c_object [Ctypes]
Type of variable, inits, field or assignable values.
c_object [Wp.Ctypes]
Type of variable, inits, field or assignable values.
call [GuiSource]
call [LogicSemantics.Make]
call [LogicCompiler.Make]
call [Wp.LogicSemantics.Make]
call [Wp.LogicCompiler.Make]
call_type [Cil2cfg]
category [LogicBuiltins]
category [Wp.LogicBuiltins]
cc [Wp_error]
chunk [LogicCompiler.Make]
chunk [Memory.Model]
chunk [Memory.Sigma]
chunk [Wp.LogicCompiler.Make]
chunk [Wp.Memory.Model]
chunk [Wp.Memory.Sigma]
clause [Separation]
List of regions to be separated.
clause [Wp.Separation]
List of regions to be separated.
cluster [Definitions]
cluster [Wp.Definitions]
cmp [Lang.F]
cmp [Wp.Lang.F]
command [Rformat]
condition [Conditions]
condition [Wp.Conditions]
context [Warning]
context [Wp.Warning]
cst [Cstring]
cst [Wp.Cstring]

D
data [Model.Data]
data [Model.Generator]
data [Model.Entries]
data [Model.Registry]
data [Wp.Model.Data]
data [Wp.Model.Generator]
data [Wp.Model.Entries]
data [Wp.Model.Registry]
decl [Mcfg.Export]
decl [Wp.Mcfg.Export]
definition [Definitions]
definition [Wp.Definitions]
denv [Matrix]
dfun [Definitions]
dfun [Wp.Definitions]
dim [Matrix]
dlemma [Definitions]
dlemma [Wp.Definitions]
domain [Memory.Sigma]
domain [Wp.Memory.Sigma]
doption [LogicBuiltins]
doption [Wp.LogicBuiltins]
dp [ProverWhy3]
driver [Factory]
driver [LogicBuiltins]
driver [Wp.Factory]
driver [Wp.LogicBuiltins]

E
edge [Cil2cfg]
abstract type of the cfg edges
effect_source [WpPropId]
effect_source [Wp.WpPropId]
element [Why3_xml]
env [LogicSemantics.Make]
env [LogicCompiler.Make]
env [Pcond]
env [Lang.F]
env [Wp.LogicSemantics.Make]
env [Wp.LogicCompiler.Make]
env [Wp.Lang.F]
extern [Lang]
extern [Wp.Lang]

F
fcstat [WpReport]
field [Lang]
field [Wp.Lang]
fields [Lang]
fields [Wp.Lang]
formula [Wpo]
frame [LogicSemantics.Make]
frame [LogicCompiler.Make]
frame [Wp.LogicSemantics.Make]
frame [Wp.LogicCompiler.Make]
functions [Generator]

G
gamma [Lang]
gamma [Wp.Lang]
goal [ProverWhy3]

I
index [Wpo]
infoprover [Lang]
generic way to have different informations for the provers
infoprover [Wp.Lang]
generic way to have different informations for the provers
input [Script]

J
job [Wp_parameters]

K
key [Model.Data]
key [Model.Generator]
key [Model.Entries]
key [Model.Registry]
key [Wprop.Info]
key [Wprop.Indexed]
key [Map.S]
The type of the map keys.
key [Wp.Model.Data]
key [Wp.Model.Generator]
key [Wp.Model.Entries]
key [Wp.Model.Registry]
key [FCMap.S]
The type of the map keys.
key1 [Wprop.Indexed2]
key2 [Wprop.Indexed2]
kind [LogicBuiltins]
kind [Wp.LogicBuiltins]

L
label_mapping [NormAtLabels]
label_mapping [Wp.NormAtLabels]
language [VCS]
language [Wp.VCS]
lfun [Lang]
lfun [Wp.Lang]
library [Lang]
library [Wp.Lang]
loc [LogicAssigns.Logic]
loc [LogicAssigns.Code]
loc [LogicSemantics.Make]
loc [CodeSemantics.Make]
loc [Memory.Model]
Representation of the memory location in the model.
loc [Wp.LogicSemantics.Make]
loc [Wp.CodeSemantics.Make]
loc [Wp.Memory.Model]
Representation of the memory location in the model.
logic [LogicSemantics.Make]
logic [LogicCompiler.Make]
logic [Memory]
logic [Cvalues.Logic]
logic [Wp.LogicSemantics.Make]
logic [Wp.LogicCompiler.Make]
logic [Wp.Memory]
logic_lemma [LogicUsage]
logic_lemma [Wp.LogicUsage]
logic_section [LogicUsage]
logic_section [Wp.LogicUsage]
logs [ProverTask]

M
matrix [Matrix]
mdt [Lang]
name to print to the provers
mdt [Wp.Lang]
name to print to the provers
mheap [Factory]
mheap [Wp.Factory]
mode [VCS]
mode [Wp.VCS]
model [Cfloat]
model [Cint]
model [Lang]
model [Model]
model [Wp.Cfloat]
model [Wp.Cint]
model [Wp.Lang]
model [Wp.Model]
mvar [Factory]
mvar [Wp.Factory]

N
node [Cil2cfg]
abstract type of the cfg nodes
node_type [Cil2cfg]

O
occur [Letify.Split]
offset [Region]
outcome [Warning]
outcome [Wp.Warning]

P
param [MemVar]
param [Wp.MemVar]
path [Region]
po [Wpo]
Dynamically exported as "Wpo.po"
pointer [MemTyped]
pointer [Wp.MemTyped]
polarity [LogicSemantics]
polarity [LogicCompiler]
polarity [Cvalues]
polarity [Wp.LogicSemantics]
polarity [Wp.LogicCompiler]
pool [Plang]
pp_edge_fun [Cil2cfg]
type of functions to print things related to edges
pred [Lang.F]
pred [Mcfg.Splitter]
pred [Mcfg.Export]
pred [Wp.Lang.F]
pred [Wp.Mcfg.Splitter]
pred [Wp.Mcfg.Export]
pred_info [WpPropId]
pred_info [Wp.WpPropId]
proof [WpAnnot]
A proof accumulator for a set of related prop_id
prop_id [WpPropId]
Property.t information and kind of PO (establishment, preservation, etc)
prop_id [Wp.WpPropId]
Property.t information and kind of PO (establishment, preservation, etc)
prop_kind [WpPropId]
prop_kind [Wp.WpPropId]
property [Wprop]
prover [VCS]
prover [Wp.VCS]
pstat [Register]

R
recursion [Definitions]
recursion [Wp.Definitions]
region [LogicAssigns.Make]
region [LogicSemantics.Make]
region [Cvalues.Logic]
region [Region]
region [Separation]
Elementary regions
region [Wp.LogicSemantics.Make]
region [Wp.Separation]
Elementary regions
result [VCS]
result [Wp.VCS]
rloc [Memory]
rloc [Wp.Memory]
roffset [Region]
rpath [Region]

S
scope [Plang]
scope [Model]
scope [Mcfg]
scope [Wp.Model]
scope [Wp.Mcfg]
segment [Memory.Model]
segment [Wp.Memory.Model]
selection [GuiSource]
separation [Model]
separation [Wp.Model]
sequence [Memory]
sequence [Conditions]
List of steps
sequence [Wp.Memory]
sequence [Wp.Conditions]
List of steps
sequent [Conditions]
sequent [Wp.Conditions]
set [Vset]
set [Wp.Vset]
setup [Factory]
setup [Wp.Factory]
sigma [LogicSemantics.Make]
sigma [LogicCompiler.Make]
sigma [CodeSemantics.Make]
sigma [Memory.Model]
sigma [Wp.LogicSemantics.Make]
sigma [Wp.LogicCompiler.Make]
sigma [Wp.CodeSemantics.Make]
sigma [Wp.Memory.Model]
sloc [Memory]
sloc [Wp.Memory]
source [Lang]
source [Wp.Lang]
step [Conditions]
step [Wp.Conditions]
strategy [WpStrategy]
strategy_for_froms [WpStrategy]
strategy_kind [WpStrategy]

T
t [VC]
elementary proof obligation
t [ProverWhy3.Goal]
t [Why3_xml]
t [Map.OrderedType]
The type of the map keys.
t [Wpo.VC_Check]
t [Wpo.VC_Annot]
t [Wpo.VC_Lemma]
t [Wpo.GOAL]
t [Wpo]
t [Memory.Sigma]
t [Memory.Chunk]
t [Letify.Defs]
t [Letify.Sigma]
t [Splitter]
t [Passive]
t [Lang.Alpha]
t [Model.Key]
t [Model]
t [Warning]
t [Cil2cfg.HEsig]
t [Cil2cfg]
abstract type of a cfg
t [Clabels.T]
t [Ctypes.AinfoComparable]
t [Wp.VC]
elementary proof obligation
t [Map.S]
The type of maps from type key to type 'a.
t [Wp.Memory.Sigma]
t [Wp.Memory.Chunk]
t [Wp.Passive]
t [Wp.Splitter]
t [Wp.Lang.Alpha]
t [Wp.Model.Key]
t [Wp.Model]
t [Wp.Warning]
t [FCMap.S]
The type of maps from type key to type 'a.
t [Wp.Clabels.T]
t [Wp.Ctypes.AinfoComparable]
t_annots [WpStrategy]
a set of annotations to be added to a program point.
t_env [Mcfg.S]
t_env [Wp.Mcfg.S]
t_prop [Mcfg.S]
t_prop [Wp.Mcfg.S]
tag [Splitter]
tag [Wp.Splitter]
tau [Lang]
tau [Wp.Lang]
ti [Cil2cfg.HEsig]
token [Script]
trigger [Definitions]
trigger [Wp.Definitions]
tuning [Model]
tuning [Wp.Model]
typedef [Definitions]
typedef [Wp.Definitions]

U
unop [Lang.F]
unop [Wp.Lang.F]
usage [Cleaning]

V
value [LogicSemantics.Make]
value [LogicCompiler.Make]
value [CodeSemantics.Make]
value [Memory]
value [Context]
value [Wp.LogicSemantics.Make]
value [Wp.LogicCompiler.Make]
value [Wp.CodeSemantics.Make]
value [Wp.Memory]
value [Wp.Context]
verdict [VCS]
verdict [Wp.VCS]
vset [Vset]
vset [Wp.Vset]