Up
Index of types
A
a_kind
[
WpPropId
]
access
[
RefUsage
]
acs
[
Memory
]
adt
[
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.
arrayinfo
[
Ctypes
]
asked_assigns
[
WpAnnot
]
assigns_desc
[
WpPropId
]
assigns_full_info
[
WpPropId
]
assigns_info
[
WpPropId
]
attributed
[
Conditions
]
axiom_info
[
WpPropId
]
axiomatic
[
LogicUsage
]
axioms
[
Definitions
]
B
balance
[
Lang
]
binop
[
Lang.F
]
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
[
LogicSemantics.Make
]
call
[
LogicCompiler.Make
]
call_type
[
Cil2cfg
]
category
[
LogicBuiltins
]
cc
[
Wp_error
]
chunk
[
Memory.Model
]
chunk
[
Memory.Sigma
]
chunk
[
LogicCompiler.Make
]
cluster
[
Definitions
]
cmp
[
Lang.F
]
command
[
Rformat
]
context
[
Warning
]
cst
[
Cstring
]
D
data
[
Model.Data
]
data
[
Model.Generator
]
data
[
Model.Entries
]
data
[
Model.Registry
]
decl
[
Mcfg.Export
]
definition
[
Definitions
]
denv
[
Matrix
]
dfun
[
Definitions
]
dim
[
Matrix
]
dlemma
[
Definitions
]
domain
[
Memory.Sigma
]
doption
[
LogicBuiltins
]
dp
[
ProverWhy3
]
driver
[
Factory
]
driver
[
LogicBuiltins
]
E
edge
[
Cil2cfg
]
abstract type of the cfg edges
effect_source
[
WpPropId
]
element
[
Why3_xml
]
env
[
LogicSemantics.Make
]
env
[
LogicCompiler.Make
]
env
[
Lang.F
]
extern
[
Lang
]
F
fcstat
[
WpReport
]
field
[
Lang
]
fields
[
Lang
]
file
[
Why3_session
]
formula
[
Wpo
]
frame
[
LogicSemantics.Make
]
frame
[
LogicCompiler.Make
]
functions
[
Generator
]
G
gamma
[
Lang
]
goal
[
Why3_session
]
goal_id
[
ProverWhy3
]
H
hypotheses
[
Conditions
]
I
index
[
Wpo
]
infoprover
[
Lang
]
generic way to have different informations for the provers
input
[
Script
]
J
job
[
Wp_parameters
]
K
key
[
Map.S
]
The type of the map keys.
key
[
Model.Data
]
key
[
Model.Generator
]
key
[
Model.Entries
]
key
[
Model.Registry
]
key
[
FCMap.S
]
The type of the map keys.
key
[
Wprop.Info
]
key
[
Wprop.Indexed
]
key1
[
Wprop.Indexed2
]
key2
[
Wprop.Indexed2
]
kind
[
LogicBuiltins
]
L
label_mapping
[
NormAtLabels
]
language
[
VCS
]
lfun
[
Lang
]
library
[
Lang
]
link
[
Conditions
]
linker
[
Conditions
]
loc
[
Memory.Model
]
Representation of the memory location in the model.
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
]
M
matrix
[
Matrix
]
mdt
[
Lang
]
name to print to the provers
mheap
[
Factory
]
mode
[
VCS
]
model
[
Cfloat
]
model
[
Cint
]
model
[
Lang
]
model
[
Model
]
mvar
[
Factory
]
N
node
[
Cil2cfg
]
abstract type of the cfg nodes
node_type
[
Cil2cfg
]
O
occur
[
Letify.Split
]
offset
[
Region
]
outcome
[
Warning
]
P
param
[
MemVar
]
path
[
Region
]
po
[
Wpo
]
Dynamically exported as
"Wpo.po"
pointer
[
MemTyped
]
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
prop_id
[
WpPropId
]
Property.t information and kind of PO (establishment, preservation, etc)
prop_kind
[
WpPropId
]
property
[
Wprop
]
prover
[
VCS
]
pstat
[
Register
]
R
recursion
[
Definitions
]
region
[
LogicAssigns.Make
]
region
[
LogicSemantics.Make
]
region
[
Cvalues.Logic
]
region
[
Region
]
result
[
VCS
]
rloc
[
Memory
]
roffset
[
Region
]
rpath
[
Region
]
S
scope
[
Mcfg
]
scope
[
Model
]
segment
[
Memory.Model
]
selection
[
GuiSource
]
sequence
[
Memory
]
sequent
[
Conditions
]
session
[
Why3_session
]
set
[
Vset
]
setup
[
Factory
]
sigma
[
Memory.Model
]
sigma
[
LogicSemantics.Make
]
sigma
[
LogicCompiler.Make
]
sigma
[
CodeSemantics.Make
]
sloc
[
Memory
]
source
[
Lang
]
strategy
[
WpStrategy
]
strategy_for_froms
[
WpStrategy
]
strategy_kind
[
WpStrategy
]
T
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
[
Map.S
]
The type of maps from type
key
to type
'
a
.
t
[
Memory.Chunk
]
t
[
Memory.Sigma
]
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
[
FCMap.S
]
The type of maps from type
key
to type
'
a
.
t
[
Clabels.T
]
t
[
Ctypes.AinfoComparable
]
t_annots
[
WpStrategy
]
a set of annotations to be added to a program point.
t_env
[
Mcfg.S
]
t_prop
[
Mcfg.S
]
tag
[
Splitter
]
tau
[
Lang
]
theory
[
Why3_session
]
ti
[
Cil2cfg.HEsig
]
token
[
Script
]
trigger
[
Definitions
]
tuning
[
Model
]
typedef
[
Definitions
]
U
unop
[
Lang.F
]
usage
[
Cleaning
]
usage
[
VarUsage
]
usage
[
VarUsageRef
]
V
value
[
Memory
]
value
[
LogicSemantics.Make
]
value
[
LogicCompiler.Make
]
value
[
CodeSemantics.Make
]
value
[
Context
]
var_kind
[
Variables_analysis
]
verdict
[
VCS
]
vset
[
Vset
]