A |
a_kind [WpPropId] |
|
a_kind [Wp.WpPropId] |
|
access [RefUsage] |
|
access [Wp.RefUsage] |
|
acs [Memory] |
|
acs [Wp.Memory] |
|
adt [Lang] |
|
adt [Wp.Lang] |
|
alternative [ProofScript] |
|
annot_kind [WpStrategy] |
An annotation can be used for different purpose.
|
annots_tbl [WpStrategy] |
|
argument [Strategy] |
|
argument [Wp.Strategy] |
|
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] |
|
bindings [TacInstance] |
|
binop [Lang.F] |
|
binop [Wp.Lang.F] |
|
block_type [Cil2cfg] |
Be careful that only Bstmt are real Block statements
|
browser [Tactical] |
|
browser [Wp.Tactical] |
|
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] |
|
chunk [LogicCompiler.Make] |
|
chunk [Memory.Model] |
|
chunk [Memory.Sigma] |
|
chunk [Wp.LogicCompiler.Make] |
|
chunk [Wp.Memory.Model] |
|
chunk [Wp.Memory.Sigma] |
|
clause [Tactical] |
|
clause [Separation] |
List of regions to be separated.
|
clause [Wp.Tactical] |
|
clause [Wp.Separation] |
List of regions to be separated.
|
cluster [Definitions] |
|
cluster [Wp.Definitions] |
|
cmp [Lang.F] |
|
cmp [Wp.Lang.F] |
|
command [Rformat] |
|
compose [Tactical] |
|
compose [Wp.Tactical] |
|
condition [Conditions] |
|
condition [Wp.Conditions] |
|
config [VCS] |
|
config [Wp.VCS] |
|
context [Warning] |
|
context [Wp.Warning] |
|
cst [Cstring] |
|
cst [Wp.Cstring] |
|
current [ProofEngine] |
|
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] |
|
dir [TacRewrite] |
|
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] |
|
elt [Set.S] |
The type of the set elements.
|
env [GuiSequent] |
|
env [LogicSemantics.Make] |
|
env [LogicCompiler.Make] |
|
env [Pcond] |
|
env [Pcfg] |
|
env [Letify.Ground] |
|
env [Repr] |
Environment for binder resolution, see Forall & Exists
|
env [Lang.F] |
|
env [Wp.LogicSemantics.Make] |
|
env [Wp.LogicCompiler.Make] |
|
env [Wp.Repr] |
Environment for binder resolution, see Forall & Exists
|
env [Wp.Lang.F] |
|
extern [Lang] |
|
extern [Wp.Lang] |
|
F |
fcstat [WpReport] |
|
field [Tactical] |
|
field [Repr] |
|
field [Lang] |
|
field [Wp.Tactical] |
|
field [Wp.Repr] |
|
field [Wp.Lang] |
|
fields [Lang] |
|
fields [Wp.Lang] |
|
fork [ProofEngine] |
|
formatter [Tactical] |
|
formatter [Wp.Tactical] |
|
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] |
|
H |
host [Memory] |
|
host [Wp.Memory] |
|
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] |
|
jscript [ProofScript] |
|
jtactic [ProofScript] |
|
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 [Pcfg] |
|
label_mapping [NormAtLabels] |
|
label_mapping [Wp.NormAtLabels] |
|
language [VCS] |
|
language [Wp.VCS] |
|
lemma [TacLemma] |
|
lfun [Repr] |
|
lfun [Lang] |
|
lfun [Wp.Repr] |
|
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] |
|
lval [Memory] |
|
lval [Wp.Memory] |
|
M |
marks [Lang.F] |
|
marks [Wp.Lang.F] |
|
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 [Register] |
|
mode [TacCut] |
|
mode [VCS] |
|
mode [Wp.VCS] |
|
model [Mstate] |
|
model [Cfloat] |
|
model [Cint] |
|
model [Lang] |
|
model [Model] |
|
model [Wp.Mstate] |
|
model [Wp.Cfloat] |
|
model [Wp.Cint] |
|
model [Wp.Lang] |
|
model [Wp.Model] |
|
mval [Memory] |
|
mval [Wp.Memory] |
|
mvar [Factory] |
|
mvar [Wp.Factory] |
|
N |
named [Tactical] |
|
named [Wp.Tactical] |
|
node [ProofEngine] |
A proof node
|
node [Cil2cfg] |
abstract type of the cfg nodes
|
node_type [Cil2cfg] |
|
O |
occur [Letify.Split] |
|
occurrence [Footprint] |
k -th occurrence of the footprint in a term
|
offset [Memory] |
|
offset [Region] |
|
offset [Wp.Memory] |
|
operator [Lang.F] |
|
operator [Wp.Lang.F] |
|
outcome [Warning] |
|
outcome [Wp.Warning] |
|
P |
param [MemVar] |
|
param [Wp.MemVar] |
|
parameter [Tactical] |
|
parameter [Wp.Tactical] |
|
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] |
|
pool [Lang.F] |
|
pool [Wp.Lang.F] |
|
position [ProofEngine] |
|
pred [Repr] |
|
pred [Lang.F] |
|
pred [Mcfg.Splitter] |
|
pred [Mcfg.Export] |
|
pred [Wp.Repr] |
|
pred [Wp.Lang.F] |
|
pred [Wp.Mcfg.Splitter] |
|
pred [Wp.Mcfg.Export] |
|
pred_info [WpPropId] |
|
pred_info [Wp.WpPropId] |
|
printer [GuiSequent] |
|
process [ProverScript] |
|
process [Tactical] |
|
process [Wp.Tactical] |
|
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 |
range [Tactical] |
|
range [Wp.Tactical] |
|
record [Lang.F] |
|
record [Wp.Lang.F] |
|
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
|
repr [Repr] |
|
repr [Wp.Repr] |
|
result [VCS] |
|
result [Wp.VCS] |
|
rg [Auto.Range] |
|
rg [Wp.Auto.Range] |
|
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] |
|
selection [Tactical] |
|
selection [Wp.Tactical] |
|
separation [Model] |
|
separation [Wp.Model] |
|
sequence [Conditions] |
List of steps
|
sequence [Memory] |
|
sequence [Wp.Conditions] |
List of steps
|
sequence [Wp.Memory] |
|
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 [Lang.Subst] |
|
sigma [Lang.F] |
|
sigma [Wp.LogicSemantics.Make] |
|
sigma [Wp.LogicCompiler.Make] |
|
sigma [Wp.CodeSemantics.Make] |
|
sigma [Wp.Memory.Model] |
|
sigma [Wp.Lang.Subst] |
|
sigma [Wp.Lang.F] |
|
sloc [Memory] |
|
sloc [Wp.Memory] |
|
source [Lang] |
|
source [Wp.Lang] |
|
state [ProofEngine] |
|
state [Mstate] |
|
state [Memory.Model] |
|
state [Wp.Mstate] |
|
state [Wp.Memory.Model] |
|
status [ProofEngine] |
|
status [Tactical] |
|
status [Wp.Tactical] |
|
step [Conditions] |
|
step [Wp.Conditions] |
|
strategy [Strategy] |
|
strategy [WpStrategy] |
|
strategy [Wp.Strategy] |
|
strategy_for_froms [WpStrategy] |
|
strategy_kind [WpStrategy] |
|
subst [Letify.Ground] |
|
T |
t [VC] |
elementary proof obligation
|
t [ProverWhy3.Goal] |
|
t [Why3_xml] |
|
t [Strategy] |
|
t [Tactical.Fmap] |
|
t [Tactical] |
|
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 [Wp.Strategy] |
|
t [Wp.Tactical.Fmap] |
|
t [Wp.Tactical] |
|
t [Map.S] |
The type of maps from type key to type 'a .
|
t [Set.S] |
The type of sets.
|
t [Wp.Memory.Sigma] |
|
t [Wp.Memory.Chunk] |
|
t [Wp.Splitter] |
|
t [Wp.Passive] |
|
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] |
|
target [GuiSequent] |
|
tau [Repr] |
|
tau [Lang.F] |
|
tau [Lang] |
|
tau [Wp.Repr] |
|
tau [Wp.Lang.F] |
|
tau [Wp.Lang] |
|
term [Repr] |
|
term [Lang.F] |
|
term [Wp.Repr] |
|
term [Wp.Lang.F] |
|
ti [Cil2cfg.HEsig] |
|
token [Script] |
|
tree [ProofEngine] |
A proof tree
|
trigger [Definitions] |
|
trigger [Wp.Definitions] |
|
tuning [Model] |
|
tuning [Wp.Model] |
|
typedef [Definitions] |
|
typedef [Wp.Definitions] |
|
U |
unop [Lang.F] |
|
unop [Wp.Lang.F] |
|
update [Memory] |
|
update [Wp.Memory] |
|
usage [Cleaning] |
|
V |
value [LogicSemantics.Make] |
|
value [LogicCompiler.Make] |
|
value [CodeSemantics.Make] |
|
value [Pcfg] |
|
value [Memory] |
|
value [Context] |
|
value [Wp.LogicSemantics.Make] |
|
value [Wp.LogicCompiler.Make] |
|
value [Wp.CodeSemantics.Make] |
|
value [Wp.Memory] |
|
value [Wp.Context] |
|
var [Repr] |
|
var [Lang.F] |
|
var [Wp.Repr] |
|
var [Wp.Lang.F] |
|
verdict [VCS] |
|
verdict [Wp.VCS] |
|
vset [Vset] |
|
vset [Wp.Vset] |
|