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