Up
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
]