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] |
|
| usage [VarUsage] |
|
| usage [VarUsageRef] |
|
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] |
|
| var_kind [Variables_analysis] |
|
| verdict [VCS] |
|
| verdict [Wp.VCS] |
|
| vset [Vset] |
|
| vset [Wp.Vset] |
|