Index of values


( * ) [Lang.N]
F.p_mul
( * ) [Wp.Lang.N]
F.p_mul
( @* ) [StmtSemantics.Make]
fold bind
( @* ) [Wp.StmtSemantics.Make]
fold bind
($$) [Lang.N]
($$) [Wp.Lang.N]
($) [Lang.N]
($) [Wp.Lang.N]
(&&) [Lang.N]
(&&) [Wp.Lang.N]
(+) [Lang.N]
F.p_add
(+) [Wp.Lang.N]
F.p_add
(-) [Lang.N]
F.p_sub
(-) [Wp.Lang.N]
F.p_sub
(/) [Lang.N]
F.p_div
(/) [Wp.Lang.N]
F.p_div
(<) [Lang.N]
(<) [Wp.Lang.N]
(<=) [Lang.N]
(<=) [Wp.Lang.N]
(<>) [Lang.N]
(<>) [Wp.Lang.N]
(=) [Lang.N]
(=) [Wp.Lang.N]
(>) [Lang.N]
Lang.F.p_lt with inversed argument
(>) [Wp.Lang.N]
Wp.Lang.F.p_lt with inversed argument
(>=) [Lang.N]
Lang.F.p_leq with inversed argument
(>=) [Wp.Lang.N]
Wp.Lang.F.p_leq with inversed argument
(@-) [StmtSemantics.Make]
(@-) [Wp.StmtSemantics.Make]
(@:) [StmtSemantics.Make]
LabelMap.find with refined excpetion.
(@:) [Wp.StmtSemantics.Make]
LabelMap.find with refined excpetion.
(@^) [StmtSemantics.Make]
Same as Cfg.concat
(@^) [Wp.StmtSemantics.Make]
Same as Cfg.concat
(mod) [Lang.N]
F.p_mod
(mod) [Wp.Lang.N]
F.p_mod
(||) [Lang.N]
(||) [Wp.Lang.N]
(~-) [Lang.N]
fun x -> p_sub 0 x
(~-) [Wp.Lang.N]
fun x -> p_sub 0 x

A
a_addr [MemMemory]
Constructor for { base ; offset }
a_base [MemMemory]
Returns the base
a_base_offset [MemMemory]
Returns the offset in bytes from the logic offset (which is a memory cell index, actually)
a_global [MemMemory]
Zero-offset base.
a_null [MemMemory]
Null address.
a_offset [MemMemory]
Returns the offset
a_prover [ProofScript]
a_shift [MemMemory]
Shift: a_shift a k adds k to a.offset
a_tactic [ProofScript]
absurd [Auto]
absurd [Wp.Auto]
acs_copy [Region]
acs_deref [Region]
acs_read [Region]
acs_shift [Region]
acs_write [Region]
acsl_lit [Cfloat]
acsl_lit [Wp.Cfloat]
add [Wpo]
add [Letify.Split]
add [Letify.Defs]
add [Letify.Sigma]
add [Lang.F.Subst]
add [Cil2cfg.HEsig]
add [Warning]
add [Wp.Wpo]
add [Hashtbl.S]
add [Wp.Lang.F.Subst]
add [Wp.Warning]
add [Set.S]
add x s returns a set containing all elements of s, plus x.
add [Map.S]
add x y m returns a map containing the same bindings as m, plus a binding of x to y.
add_alias [LogicBuiltins]
add_alias [Region]
add_alias [Wp.LogicBuiltins]
add_all_axioms [WpStrategy]
add_assigns [WpStrategy]
generic function to add an assigns property.
add_assigns [Mcfg.S]
add_assigns [Wp.Mcfg.S]
add_assigns_any [WpStrategy]
generic function to add a WriteAny assigns property.
add_axiom [WpStrategy]
add_axiom [Mcfg.S]
add_axiom [Wp.Mcfg.S]
add_builtin [LogicBuiltins]
Add a new builtin.
add_builtin [Wp.LogicBuiltins]
Add a new builtin.
add_call_assigns_any [WpStrategy]
short cut to add a dynamic call
add_call_assigns_hyp [WpStrategy]
shortcut to add a call assigns property as an hypothesis.
add_composer [Tactical]
add_composer [Wp.Tactical]
add_ctor [LogicBuiltins]
add_ctor [Wp.LogicBuiltins]
add_definitions [Letify]
add_definitions sigma defs xs ps keep all definitions of variables xs from sigma that comes from defs.
add_fct_bhv_assigns_hyp [WpStrategy]
add_filter [Lang.F.Subst]
add_filter [Wp.Lang.F.Subst]
add_fun [Lang.F.Subst]
add_fun [Wp.Lang.F.Subst]
add_goal [Mcfg.S]
add_goal [Wp.Mcfg.S]
add_hook [Wprop.Indexed2]
Hooks are executed once at property creation
add_hook [Wprop.Indexed]
Hooks are executed once at property creation
add_hyp [Mcfg.S]
add_hyp [Wp.Mcfg.S]
add_invalid_proof [WpAnnot]
add an invalid proof result ; can not revert a complete proof
add_library [LogicBuiltins]
Add a new library or update the dependencies of an existing one
add_library [Wp.LogicBuiltins]
Add a new library or update the dependencies of an existing one
add_logic [LogicBuiltins]
add_logic [Wp.LogicBuiltins]
add_loop_annots [WpStrategy]
add_loop_assigns_hyp [WpStrategy]
shortcut to add a loop assigns property as an hypothesis.
add_map [Lang.F.Subst]
add_map [Wp.Lang.F.Subst]
add_node_annots [WpStrategy]
add_node_annots cfg annots v (before, (after, exits)) add the annotations for the node :
add_offset [Region]
add_on_edges [WpStrategy]
add_option [LogicBuiltins]
add a value to an option (group, name)
add_option [Wp.LogicBuiltins]
add a value to an option (group, name)
add_pointed [Region]
add_predicate [LogicBuiltins]
add_predicate [Wp.LogicBuiltins]
add_proof [WpAnnot]
accumulate in the proof the partial proof for this prop_id
add_prop [WpStrategy]
generic function to add a predicate property after normalisation.
add_prop_assert [WpStrategy]
add_prop_call_post [WpStrategy]
Add a postcondition of a called function.
add_prop_call_pre [WpStrategy]
add_prop_dead_call [WpStrategy]
Add Smoke Test for possibly dead call : (posts,exits)
add_prop_dead_code [WpStrategy]
Add Smoke Test for possibly dead code
add_prop_dead_loop [WpStrategy]
Add Smoke Test for loop
add_prop_fct_bhv_pre [WpStrategy]
Add the preconditions of the behavior
add_prop_fct_post [WpStrategy]
add_prop_fct_pre [WpStrategy]
Add the predicate as a function precondition.
add_prop_fct_pre_bhv [WpStrategy]
add_prop_fct_smoke [WpStrategy]
Add Smoke Test behavior
add_prop_loop_inv [WpStrategy]
add_prop_stmt_bhv_requires [WpStrategy]
Add all the b_requires.
add_prop_stmt_post [WpStrategy]
Add the predicate as a stmt precondition.
add_prop_stmt_pre [WpStrategy]
Add the predicate as a stmt precondition.
add_prop_stmt_spec_pre [WpStrategy]
Process the stmt spec precondition as an hypothesis for external properties.
add_script_for [Proof]
new_script goal keys proof qed registers the script proof terminated by qed for goal gid and keywords keys
add_specific_equality [ProverWhy3]
Equality used in the goal, simpler to prove than polymorphic equality
add_step [Register]
add_stmt_spec_assigns_hyp [WpStrategy]
shortcut to add a stmt spec assigns property as an hypothesis.
add_time [Register]
add_tmpnode [CfgCompiler.Cfg]
Set a node as temporary.
add_tmpnode [Wp.CfgCompiler.Cfg]
Set a node as temporary.
add_type [LogicBuiltins]
add_type [Wp.LogicBuiltins]
add_var [Lang.F]
add_var [Wp.Lang.F]
add_vars [Lang.F]
add_vars [Wp.Lang.F]
adt [Lang]
Must not be a builtin
adt [Wp.Lang]
Must not be a builtin
age [Wpo]
age [Wp.Wpo]
ainf [Cvalues]
Array lower-bound, ie `Some(0)`
alias [Region]
alias [Layout.Alias]
alloc [Sigs.Model]
Allocates new chunk for the validity of variables.
alloc [Wp.Sigs.Model]
Allocates new chunk for the validity of variables.
alloc_domain [Plang]
alloc_domain [Wp.Plang]
alloc_e [Plang]
alloc_e [Wp.Plang]
alloc_hyp [Pcond]
alloc_hyp [Wp.Pcond]
alloc_p [Plang]
alloc_p [Wp.Plang]
alloc_seq [Pcond]
alloc_seq [Wp.Pcond]
alloc_xs [Plang]
alloc_xs [Wp.Plang]
alpha [Lang.F]
alpha [Lang]
freshen all variables
alpha [Wp.Lang.F]
alpha [Wp.Lang]
freshen all variables
anchor [ProofEngine]
append [Conditions]
Conjunction
append [Wp.Conditions]
Conjunction
append_after [Parameter_sig.List]
append a list at the end of the current state
append_before [Parameter_sig.List]
append a list in front of the current state
apply [Mstate]
apply [Sigs.Model]
Propagate a sequent substitution inside the memory state.
apply [Cvalues.Logic]
apply [Passive]
apply [Wp.Mstate]
apply [Wp.Sigs.Model]
Propagate a sequent substitution inside the memory state.
apply [Wp.Passive]
apply_add [Cvalues.Logic]
apply_assigns [Sigs.LogicAssigns]
Relates two memory states corresponding to an assigns clause with the specified set of locations.
apply_assigns [Wp.Sigs.LogicAssigns]
Relates two memory states corresponding to an assigns clause with the specified set of locations.
apply_sub [Cvalues.Logic]
are_equal [Lang.F]
Computes equality
are_equal [Wp.Lang.F]
Computes equality
arg [Strategy]
arg [Wp.Strategy]
array [Auto]
array [Wp.Auto]
array_dimensions [Ctypes]
Returns the list of dimensions the array consists of.
array_dimensions [Wp.Ctypes]
Returns the list of dimensions the array consists of.
array_size [Ctypes]
array_size [Wp.Ctypes]
as_atom [Cleaning]
as_have [Cleaning]
as_init [Cleaning]
as_type [Cleaning]
assign [Mcfg.S]
assign [Wp.Mcfg.S]
assigned [MemLoader.Make]
assigned [Sigs.Model]
Return a set of formula that express that two memory state are the same except at the given set of memory location.
assigned [Sigs.Sigma]
Make chunks equal outside of some domain.
assigned [Wp.Sigs.Model]
Return a set of formula that express that two memory state are the same except at the given set of memory location.
assigned [Wp.Sigs.Sigma]
Make chunks equal outside of some domain.
assigned_of_assigns [Sigs.LogicSemantics]
Computes the region assigned by an assigns clause.
assigned_of_assigns [Wp.Sigs.LogicSemantics]
Computes the region assigned by an assigns clause.
assigned_of_froms [Sigs.LogicSemantics]
Computes the region assigned by a list of froms.
assigned_of_froms [Wp.Sigs.LogicSemantics]
Computes the region assigned by a list of froms.
assigned_of_lval [Sigs.LogicSemantics]
Computes the region assigned by a list of froms.
assigned_of_lval [Wp.Sigs.LogicSemantics]
Computes the region assigned by a list of froms.
assigns [StmtSemantics.Make]
assigns [Wp.StmtSemantics.Make]
assigns_info_id [WpPropId]
assigns_info_id [Wp.WpPropId]
assigns_upper_bound [WpStrategy]
assume [StmtSemantics.Make]
assume [CfgCompiler.Cfg]
Represents execution traces T such that, if T contains every node points in the label-map, then the condition holds over the corresponding memory states.
assume [Conditions]
Assumes a predicate in the specified section, with the specified decorations.
assume [Letify.Sigma]
assume [Lang]
assume [Wp.StmtSemantics.Make]
assume [Wp.CfgCompiler.Cfg]
Represents execution traces T such that, if T contains every node points in the label-map, then the condition holds over the corresponding memory states.
assume [Wp.Conditions]
Assumes a predicate in the specified section, with the specified decorations.
assume [Wp.Lang]
assume_ [StmtSemantics.Make]
assume_ [Wp.StmtSemantics.Make]
asup [Cvalues]
Array upper-bound, ie `Some(n-1)`
at [Tactical]
at [Pcfg]
at [Wp.Tactical]
at [Wp.Pcfg]
at_closure [Conditions]
register a transformation applied just before close
at_closure [Wp.Conditions]
register a transformation applied just before close
at_exit [Clabels]
at_exit [Wp.Clabels]
atype [Lang]
atype [Wp.Lang]
auto_range [Auto]
auto_range [Wp.Auto]
auto_split [Auto]
auto_split [Wp.Auto]
autofit [VCS]
Result that fits the default configuration
autofit [Wp.VCS]
Result that fits the default configuration
automaton [StmtSemantics.Make]
automaton [Wp.StmtSemantics.Make]
axiomatic [Definitions]
axiomatic [LogicUsage]
axiomatic [Wp.Definitions]
axiomatic [Wp.LogicUsage]

B
backtrack [ProverSearch]
backward [Letify.Ground]
band [Cint]
band [Wp.Cint]
bar [Wpo]
bar [Wp.Wpo]
base_addr [Sigs.Model]
Return the memory location of the base address of a given memory location.
base_addr [Wp.Sigs.Model]
Return the memory location of the base address of a given memory location.
base_offset [Sigs.Model]
Return the offset of the location, in bytes, from its base_addr.
base_offset [Wp.Sigs.Model]
Return the offset of the location, in bytes, from its base_addr.
basename [Lang.F]
basename [LogicUsage]
Trims the original name
basename [WpContext.IData]
basename [Ctypes]
basename [Wp.Lang.F]
basename [Wp.WpContext.IData]
basename [Wp.LogicUsage]
Trims the original name
basename [Wp.Ctypes]
basename_of_chunk [Sigs.Chunk]
Used when generating fresh variables for a chunk.
basename_of_chunk [Wp.Sigs.Chunk]
Used when generating fresh variables for a chunk.
begin_session [Register]
behavior_name_of_strategy [WpStrategy]
best [VCS]
best [Wp.VCS]
bind [ProofEngine]
bind [StmtSemantics.Make]
bind [Letify]
bind sigma defs xs select definitions in defs targeting variables xs.
bind [Passive]
bind [Context]
Performs the job with local context bound to local value.
bind [Wp.StmtSemantics.Make]
bind [Wp.Passive]
bind [Wp.Context]
Performs the job with local context bound to local value.
bindings [Map.S]
Return the list of all bindings of the given map.
bit_test [Cint]
bit_test [Wp.Cint]
bits_sizeof_array [Ctypes]
bits_sizeof_array [Wp.Ctypes]
bits_sizeof_comp [Ctypes]
bits_sizeof_comp [Wp.Ctypes]
bits_sizeof_object [Ctypes]
bits_sizeof_object [Wp.Ctypes]
block_length [Sigs.Model]
Returns the length (in bytes) of the allocated block containing the given location.
block_length [Wp.Sigs.Model]
Returns the length (in bytes) of the allocated block containing the given location.
block_scope_for_edge [Cil2cfg]
blsl [Cint]
blsl [Wp.Cint]
blsr [Cint]
blsr [Wp.Cint]
bnot [Cint]
bnot [Wp.Cint]
bool_and [Cvalues]
bool_eq [Cvalues]
bool_leq [Cvalues]
bool_lt [Cvalues]
bool_neq [Cvalues]
bool_of_int [Cmath]
bool_or [Cvalues]
bool_val [Cvalues]
bootstrap_logic [LogicCompiler.Make]
bootstrap_logic [Wp.LogicCompiler.Make]
bootstrap_pred [LogicCompiler.Make]
bootstrap_pred [Wp.LogicCompiler.Make]
bootstrap_region [LogicCompiler.Make]
bootstrap_region [Wp.LogicCompiler.Make]
bootstrap_term [LogicCompiler.Make]
bootstrap_term [Wp.LogicCompiler.Make]
bor [Cint]
bor [Wp.Cint]
bound [ProofEngine]
bound_add [Vset]
bound_add [Wp.Vset]
bound_shift [Vset]
bound_shift [Wp.Vset]
bound_sub [Vset]
bound_sub [Wp.Vset]
bounds [Auto.Range]
bounds [Ctypes]
domain, bounds included
bounds [Wp.Auto.Range]
bounds [Wp.Ctypes]
domain, bounds included
branch [CfgCompiler.Cfg]
Structurally corresponds to an if-then-else control-flow.
branch [Conditions]
Construct a branch bundle, with merging of all common parts.
branch [Letify.Ground]
branch [Wp.CfgCompiler.Cfg]
Structurally corresponds to an if-then-else control-flow.
branch [Wp.Conditions]
Construct a branch bundle, with merging of all common parts.
branching [Pcfg]
branching [Wp.Pcfg]
break [Clabels]
break [Wp.Clabels]
build_prop_of_from [Mcfg.S]
build p => alpha(p) for functional dependencies verification.
build_prop_of_from [Wp.Mcfg.S]
build p => alpha(p) for functional dependencies verification.
builtin_types [Lang]
builtin_types [Wp.Lang]
bundle [Pcond]
bundle [Conditions]
Closes the bundle and promote it into a well-formed sequence.
bundle [Wp.Pcond]
bundle [Wp.Conditions]
Closes the bundle and promote it into a well-formed sequence.
bxor [Cint]
bxor [Wp.Cint]

C
c_bool [Ctypes]
Returns the type of int
c_bool [Wp.Ctypes]
Returns the type of int
c_char [Ctypes]
Returns the type of char
c_char [Wp.Ctypes]
Returns the type of char
c_float [Ctypes]
Conforms to
c_float [Wp.Ctypes]
Conforms to
c_int [Ctypes]
Conforms to
c_int [Wp.Ctypes]
Conforms to
c_ptr [Ctypes]
Returns the type of pointers
c_ptr [Wp.Ctypes]
Returns the type of pointers
cache [Layout.Offset]
cache_descr [Wpo.VC_Annot]
cache_descr [Wpo.VC_Lemma]
cache_descr [Wp.Wpo.VC_Annot]
cache_descr [Wp.Wpo.VC_Lemma]
cache_log [Wpo.DISK]
cache_log [Wp.Wpo.DISK]
cached [VCS]
only for true verdicts
cached [Wp.VCS]
only for true verdicts
call [StmtSemantics.Make]
call [LogicCompiler.Make]
call [Sigs.LogicSemantics]
Create call data from the callee point of view, deriving data (gamma and pools) from the current frame.
call [Sigs.CodeSemantics]
Address of a function pointer.
call [Splitter]
call [Mcfg.S]
call [Wp.StmtSemantics.Make]
call [Wp.LogicCompiler.Make]
call [Wp.Sigs.LogicSemantics]
Create call data from the callee point of view, deriving data (gamma and pools) from the current frame.
call [Wp.Sigs.CodeSemantics]
Address of a function pointer.
call [Wp.Splitter]
call [Wp.Mcfg.S]
call_dynamic [Mcfg.S]
call_dynamic [Wp.Mcfg.S]
call_fun [LogicCompiler.Make]
call_fun [Definitions]
call_fun [Wp.LogicCompiler.Make]
call_fun [Wp.Definitions]
call_goal_precond [Mcfg.S]
call_goal_precond [Wp.Mcfg.S]
call_kf [StmtSemantics.Make]
call_kf [Wp.StmtSemantics.Make]
call_post [LogicCompiler.Make]
call_post [Sigs.LogicSemantics]
Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state and post-state.
call_post [Wp.LogicCompiler.Make]
call_post [Wp.Sigs.LogicSemantics]
Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state and post-state.
call_pre [LogicCompiler.Make]
call_pre [Sigs.LogicSemantics]
Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state.
call_pre [Wp.LogicCompiler.Make]
call_pre [Wp.Sigs.LogicSemantics]
Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state.
call_pred [LogicCompiler.Make]
call_pred [Definitions]
call_pred [Wp.LogicCompiler.Make]
call_pred [Wp.Definitions]
callback [WpContext.Registry]
callback [Wp.WpContext.Registry]
cancel [ProofEngine]
cardinal [TacInstance]
less than limit
cardinal [Set.S]
Return the number of elements of a set.
cardinal [Map.S]
Return the number of bindings of a map.
case [Clabels]
case [Wp.Clabels]
cases [Splitter]
cases [Wp.Splitter]
cast [Sigs.CodeSemantics]
Applies a pointer cast or a conversion.
cast [Sigs.Model]
Cast a memory location into another memory location.
cast [Wp.Sigs.CodeSemantics]
Applies a pointer cast or a conversion.
cast [Wp.Sigs.Model]
Cast a memory location into another memory location.
cat_print_generated [Wp_parameters]
cat_print_generated [Wp.Wp_parameters]
catch [Warning]
Set up a context for the job.
catch [Wp.Warning]
Set up a context for the job.
catch_label_error [NormAtLabels]
catch_label_error [Wp.NormAtLabels]
cc_assign [RegionAccess]
cc_fundec [RegionAccess]
cc_init [RegionAccess]
cc_instr [RegionAccess]
cc_lval [RegionAccess]
cc_pred [RegionAccess]
cc_read [RegionAccess]
cc_region [RegionAccess]
cc_spec [RegionAccess]
cc_term [RegionAccess]
cdomain [Cvalues]
cfg_kf [Cil2cfg]
cfg_of_strategy [WpStrategy]
cfg_spec_only [Cil2cfg]
returns true is this CFG is degenerated (no code available)
char [Ctypes]
char [Wp.Ctypes]
char_at [Cstring]
char_at [Wp.Cstring]
check_assigns [Sigs.LogicSemantics]
Check assigns inclusion.
check_assigns [Wp.Sigs.LogicSemantics]
Check assigns inclusion.
check_tau [Vlist]
check_term [Vlist]
checkbox [Tactical]
Unless specified, default is false.
checkbox [Wp.Tactical]
Unless specified, default is false.
children [ProofEngine]
choice [Auto]
choice [StmtSemantics.Make]
Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp.
choice [Wp.Auto]
choice [Wp.StmtSemantics.Make]
Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp.
choose [VCS]
choose [Sigs.Sigma]
Make the union of each sigma, choosing the minimal variable in case of conflict.
choose [Wp.VCS]
choose [Wp.Sigs.Sigma]
Make the union of each sigma, choosing the minimal variable in case of conflict.
choose [Set.S]
Return one element of the given set, or raise Not_found if the set is empty.
choose [Map.S]
Return one binding of the given map, or raise Not_found if the map is empty.
choose_opt [Set.S]
Return one element of the given set, or None if the set is empty.
choose_opt [Map.S]
Return one binding of the given map, or None if the map is empty.
chunk [Region]
chunks [Region]
cint [Tactical]
cint [Wp.Tactical]
clean [Conditions]
clean [Wp.Conditions]
cleanup_cache [ProverWhy3]
clear [VC]
clear [Wpo]
clear [Cil2cfg.HEsig]
clear [WpContext.Generator]
clear [WpContext.Registry]
clear [Context]
Clear the current value.
clear [Wp.Wpo]
clear [Wp.VC]
clear [Hashtbl.S]
clear [Wp.WpContext.Generator]
clear [Wp.WpContext.Registry]
clear [Wp.Context]
Clear the current value.
clear_results [Wpo]
clear_results [Wp.Wpo]
clear_scheduled [Register]
clear_session [Register]
cloc [Sigs.CodeSemantics]
Interpret a value as a location.
cloc [Wp.Sigs.CodeSemantics]
Interpret a value as a location.
close [Script]
close [Conditions]
With free variables quantified.
close [Mcfg.S]
close [Wp.Conditions]
With free variables quantified.
close [Wp.Mcfg.S]
cluster [MemLoader]
cluster [Cstring]
The cluster where all strings are defined.
cluster [Definitions]
cluster [Region]
cluster [Wp.Cstring]
The cluster where all strings are defined.
cluster [Wp.Definitions]
cluster_age [Definitions]
cluster_age [Wp.Definitions]
cluster_compare [Definitions]
cluster_compare [Wp.Definitions]
cluster_id [Definitions]
Unique
cluster_id [Wp.Definitions]
Unique
cluster_position [Definitions]
cluster_position [Wp.Definitions]
cluster_title [Definitions]
cluster_title [Wp.Definitions]
cmdline [Register]
cmdline_run [Register]
cmp_prover [VCS]
cmp_prover [Wp.VCS]
code_lit [Cfloat]
code_lit [Wp.Cfloat]
codomain [Letify.Sigma]
command [VC]
Run the provers with the command-line interface.
command [Rformat]
command [Wp.VC]
Run the provers with the command-line interface.
commit [ProofEngine]
comp [Lang]
comp [Wp.Lang]
comp_id [Lang]
comp_id [Wp.Lang]
compare [VCS]
compare [Sigs.Chunk]
compare [LogicBuiltins]
compare [Lang.F]
compare [RegionAnnot.Lpath]
compare [Layout.Value]
compare [Layout.Data]
compare [WpContext.Key]
compare [WpContext.Entries]
compare [WpContext.SCOPE]
compare [WpContext.MODEL]
compare [WpContext.S]
compare [Warning]
compare [Why3Provers]
compare [Clabels.T]
compare [Ctypes.AinfoComparable]
compare [Ctypes]
compare [Map.OrderedType]
A total ordering function over the keys.
compare [Wp.VCS]
compare [Wp.Sigs.Chunk]
compare [Wp.LogicBuiltins]
compare [Wp.Lang.F]
compare [Wp.WpContext.Key]
compare [Wp.WpContext.Entries]
compare [Wp.WpContext.SCOPE]
compare [Wp.WpContext.MODEL]
compare [Wp.WpContext.S]
compare [Wp.Warning]
compare [Set.S]
Total ordering between sets.
compare [Map.S]
Total ordering between maps.
compare [Wp.Clabels.T]
compare [Wp.Ctypes.AinfoComparable]
compare [Wp.Ctypes]
compare_c_float [Ctypes]
compare_c_float [Wp.Ctypes]
compare_c_int [Ctypes]
compare_c_int [Wp.Ctypes]
compare_prop_id [WpPropId]
compare_prop_id [Wp.WpPropId]
compare_ptr_conflated [Ctypes]
same as Ctypes.compare but all PTR are considered the same
compare_ptr_conflated [Wp.Ctypes]
same as Wp.Ctypes.compare but all PTR are considered the same
comparep [Lang.F]
comparep [Wp.Lang.F]
compile [CfgCompiler.Cfg]
compile [WpContext.IData]
compile [WpContext.Data]
compile [WpContext.Registry]
with circularity protection
compile [Wp.CfgCompiler.Cfg]
compile [Wp.WpContext.IData]
compile [Wp.WpContext.Data]
compile [Wp.WpContext.Registry]
with circularity protection
compile_lemma [Definitions]
compile_lemma [Wp.Definitions]
compiler [Factory]
compiler [Wp.Factory]
compinfo [Definitions]
compinfo [Wp.Definitions]
complexity [TacInstance]
compose [Tactical]
compose [Wp.Tactical]
composer [Tactical]
Unless specified, default is Empty selection.
composer [Wp.Tactical]
Unless specified, default is Empty selection.
compound [Auto]
compound [Wp.Auto]
compute [Calculus.Cfg]
compute [Auto.Range]
compute [Wpo.GOAL]
compute [Wpo]
compute [Filtering]
compute [Letify.Ground]
compute [RefUsage]
compute [LogicUsage]
To force computation
compute [Dyncall]
Forces computation of dynamic calls.
compute [Wp.Wpo.GOAL]
compute [Wp.Wpo]
compute [Wp.Auto.Range]
compute [Wp.Filtering]
compute [Wp.RefUsage]
compute [Wp.LogicUsage]
To force computation
compute_auto [Register]
compute_call [Generator]
compute_descr [Wpo.GOAL]
compute_descr [Wp.Wpo.GOAL]
compute_hypotheses [WpContext]
compute_hypotheses [Wp.WpContext]
compute_ip [Generator]
compute_kf [Generator]
compute_kf [StmtSemantics.Make]
Full Compilation
compute_kf [Wp.StmtSemantics.Make]
Full Compilation
compute_proof [Wpo.GOAL]
compute_proof [Wp.Wpo.GOAL]
compute_provers [Register]
compute_selection [Generator]
computer [Register]
computer [CfgWP]
computing [VCS]
computing [Wp.VCS]
concat [CfgCompiler.Cfg]
The concatenation is the intersection of all possible collection of traces from each cfg.
concat [Conditions]
List conjunction
concat [Wp.CfgCompiler.Cfg]
The concatenation is the intersection of all possible collection of traces from each cfg.
concat [Wp.Conditions]
List conjunction
concretize [Vset]
concretize [Wp.Vset]
cond [Sigs.CodeSemantics]
Evaluate the conditional expression on the given memory state.
cond [Wp.Sigs.CodeSemantics]
Evaluate the conditional expression on the given memory state.
condition [Conditions]
With free variables kept.
condition [Wp.Conditions]
With free variables kept.
conditions [Passive]
conditions [Wp.Passive]
config [Why3Provers]
configure [ProofScript]
configure [VCS]
configure [Sigs.Model]
Initializers to be run before using the model.
configure [Cfloat]
configure [Cint]
configure [Context]
Apply global configure hooks, once per project/ast.
configure [Why3Provers]
configure [Wp.VCS]
configure [Wp.Sigs.Model]
Initializers to be run before using the model.
configure [Wp.Cfloat]
configure [Wp.Cint]
configure [Wp.Context]
Apply global configure hooks, once per project/ast.
configure_driver [Factory]
configure_driver [Wp.Factory]
configure_ia [Sigs.Model]
Given an automaton, return a vertex's binder.
configure_ia [Wp.Sigs.Model]
Given an automaton, return a vertex's binder.
const [Mcfg.S]
const [Wp.Mcfg.S]
constant [Cvalues]
constant [LogicBuiltins]
constant [Lang.F]
constant [Ctypes]
constant [Wp.LogicBuiltins]
constant [Wp.Lang.F]
constant [Wp.Ctypes]
constant_exp [Cvalues]
constant_term [Cvalues]
context [Warning]
context [Wp.Warning]
context_pp [Lang.F]
Context used by pp_term, pp_pred, pp_var, ppvars for printing the term.
context_pp [Wp.Lang.F]
Context used by pp_term, pp_pred, pp_var, ppvars for printing the term.
continue [Clabels]
continue [Wp.Clabels]
contrapose [Auto]
contrapose [Wp.Auto]
convert [Cint]
Independent from model
convert [Wp.Cint]
Independent from model
copied [MemLoader.Make]
copied [Sigs.Model]
Return a set of equations that express a copy between two memory state.
copied [Wp.Sigs.Model]
Return a set of equations that express a copy between two memory state.
copy [Sigs.Sigma]
Duplicate the environment.
copy [Letify.Ground]
copy [Hashtbl.S]
copy [Wp.Sigs.Sigma]
Duplicate the environment.
copy [Datatype.S]
Deep copy: no possible sharing between x and copy x.
create [CfgDump]
create [Tactical.Fmap]
create [CfgCompiler.Cfg.E]
Bundle an equation with the sigma sequence that created it
create [CfgCompiler.Cfg.T]
Bundle a term with the sigma sequence that created it.
create [CfgCompiler.Cfg.P]
Bundle an equation with the sigma sequence that created it.
create [CfgCompiler.Cfg.C]
Bundle an equation with the sigma sequence that created it.
create [CfgCompiler.Cfg.Node]
create [Pcfg]
create [Mstate]
create [Sigs.Sigma]
Initially empty environment.
create [Cleaning]
create [Letify.Split]
create [Cil2cfg.HEsig]
create [Region]
create [Warning]
create [Context]
Creates a new context with name
create [Wp.Tactical.Fmap]
create [Wp.CfgCompiler.Cfg.E]
Bundle an equation with the sigma sequence that created it
create [Wp.CfgCompiler.Cfg.T]
Bundle a term with the sigma sequence that created it.
create [Wp.CfgCompiler.Cfg.P]
Bundle an equation with the sigma sequence that created it.
create [Wp.CfgCompiler.Cfg.C]
Bundle an equation with the sigma sequence that created it.
create [Hashtbl.S]
create [Wp.CfgCompiler.Cfg.Node]
create [Wp.Pcfg]
create [Wp.Mstate]
create [Wp.Sigs.Sigma]
Initially empty environment.
create [Wp.Warning]
create [Wp.Context]
Creates a new context with name
create_option [LogicBuiltins]
add_option_sanitizer ~driver_dir group name add a sanitizer for group group and option name
create_option [Wp.LogicBuiltins]
add_option_sanitizer ~driver_dir group name add a sanitizer for group group and option name
create_proof [WpAnnot]
to be used only once for one of the related prop_id
create_tbl [WpStrategy]
ctor [LogicBuiltins]
ctor [Wp.LogicBuiltins]
ctor_id [Lang]
ctor_id [Wp.Lang]
current [ProofEngine]
current [VCS]
Current parameters
current [LogicCompiler.Make]
current [Sigs.LogicSemantics]
The current memory state.
current [Cint]
current [Wp.VCS]
Current parameters
current [Wp.LogicCompiler.Make]
current [Wp.Sigs.LogicSemantics]
The current memory state.
current [Wp.Cint]
cut [Auto]
cut [Wp.Auto]
cval [Sigs.CodeSemantics]
Evaluate an abstract value.
cval [Wp.Sigs.CodeSemantics]
Evaluate an abstract value.
cvar [Sigs.Model]
Return the location of a C variable.
cvar [Wp.Sigs.Model]
Return the location of a C variable.

D
datatype [MemVar.VarUsage]
datatype [Sigs.Model]
For projectification.
datatype [Lang]
datatype [Wp.MemVar.VarUsage]
datatype [Wp.Sigs.Model]
For projectification.
datatype [Wp.Lang]
debugp [Lang.F]
debugp [Wp.Lang.F]
decide [Lang.F]
Return true if and only the term is e_true.
decide [Wp.Lang.F]
Return true if and only the term is e_true.
decode [ProofScript]
def_into_axiom [Filter_axioms]
default [Factory]
"Var,Typed,Nat,Real" memory model.
default [Tactical]
default [VCS]
all None
default [Layout.Pack]
default [Layout.Flat]
default [Layout.RW]
default [Clabels]
default [Wp.Tactical]
default [Wp.VCS]
all None
default [Wp.Factory]
"Var,Typed,Nat,Real" memory model.
default [Wp.Clabels]
default_mode [Register]
define [Lang.F]
define [WpContext.Registry]
no redefinition ; circularity protected
define [Wp.Lang.F]
define [Wp.WpContext.Registry]
no redefinition ; circularity protected
define_lemma [Definitions]
define_lemma [Wp.Definitions]
define_symbol [Definitions]
define_symbol [Wp.Definitions]
define_type [Definitions]
define_type [Wp.Definitions]
defined [Context]
The current value is defined.
defined [Wp.Context]
The current value is defined.
definition [Auto]
definition [Wp.Auto]
defs [Lang.F]
defs [Wp.Lang.F]
delete_script_for [Proof]
delete_script ~gid remove known script for goal.
denv [Matrix]
dependencies [WpAnnot]
dependencies [LogicBuiltins]
Of external theories.
dependencies [Wp.LogicBuiltins]
Of external theories.
deprecated [Register]
deprecated_wp_clear [Register]
deprecated_wp_compute [Register]
deprecated_wp_compute_call [Register]
deprecated_wp_compute_ip [Register]
deprecated_wp_compute_kf [Register]
deref [Layout.Cluster]
descr [Factory]
descr [Vset]
descr [LogicBuiltins]
descr [WpContext.MODEL]
descr [Wp.Factory]
descr [Wp.Vset]
descr [Wp.LogicBuiltins]
descr [Wp.WpContext.MODEL]
destruct [Tactical]
destruct [Wp.Tactical]
diff [Set.S]
Set difference.
dimension_of_object [Ctypes]
Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells
dimension_of_object [Wp.Ctypes]
Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells
directory [WpContext]
Current model in "-wp-out" directory
directory [Wp.WpContext]
Current model in "-wp-out" directory
disjoint [Vset]
disjoint [Layout.Chunk]
disjoint [Wp.Vset]
dkey_builtins [Register]
dkey_cluster [ProverErgo]
dkey_logicusage [Register]
dkey_main [Register]
dkey_no_cache_info [VCS]
dkey_no_cache_info [Wp.VCS]
dkey_no_goals_info [VCS]
dkey_no_goals_info [Wp.VCS]
dkey_no_step_info [VCS]
dkey_no_step_info [Wp.VCS]
dkey_no_time_info [VCS]
dkey_no_time_info [Wp.VCS]
dkey_prover [Register]
dkey_raised [Register]
dkey_refusage [Register]
dkey_shell [Register]
dkey_success_only [VCS]
dkey_success_only [Wp.VCS]
do_alias [Region]
do_cache_cleanup [Register]
do_list_scheduled [Register]
do_list_scheduled_result [Register]
do_progress [Register]
do_prover_detect [Register]
do_report_cache_usage [Register]
do_report_prover_stats [Register]
do_report_scheduled [Register]
do_report_steps [Register]
do_report_stopped [Register]
do_report_time [Register]
do_update_session [Register]
do_wp_print [Register]
do_wp_print_for [Register]
do_wp_proofs [Register]
do_wp_proofs_for [Register]
do_wp_proofs_iter [Register]
do_wp_report [Register]
do_wpo_display [Register]
do_wpo_failed [Register]
do_wpo_result [Register]
do_wpo_smoke [Register]
do_wpo_start [Register]
do_wpo_stat [Register]
do_wpo_success [Register]
do_wpo_wait [Register]
domain [MemLoader.Model]
domain [Conditions]
Assumes a list of predicates in a Type section on top of the bundle.
domain [Sigs.LogicAssigns]
Memory footprint of a region.
domain [Sigs.Model]
Compute the set of chunks that hold the value of an object with the given C-type.
domain [Sigs.Sigma]
Footprint of a memory environment.
domain [Letify.Defs]
domain [Letify.Sigma]
domain [Wp.Conditions]
Assumes a list of predicates in a Type section on top of the bundle.
domain [Wp.Sigs.LogicAssigns]
Memory footprint of a region.
domain [Wp.Sigs.Model]
Compute the set of chunks that hold the value of an object with the given C-type.
domain [Wp.Sigs.Sigma]
Footprint of a memory environment.
doomed_if_valid [WpPropId]
Properties that are False-if-unreachable in case the PO is valid.
doomed_if_valid [Wp.WpPropId]
Properties that are False-if-unreachable in case the PO is valid.
downcast [Cint]
Dependent on model
downcast [Wp.Cint]
Dependent on model
driver [LogicBuiltins]
driver [Wp.LogicBuiltins]
dummy [Wpo.GOAL]
dummy [Definitions]
dummy [Wp.Wpo.GOAL]
dummy [Wp.Definitions]
dump [WpReached]
dump [Pcond]
dump [LogicBuiltins]
dump [RegionDump]
dump [RefUsage]
dump [LogicUsage]
Print on output
dump [Wp.Pcond]
dump [Wp.LogicBuiltins]
dump [Wp.RefUsage]
dump [Wp.LogicUsage]
Print on output
dump_env [CfgCompiler.Cfg]
dump_env [Wp.CfgCompiler.Cfg]
dump_strategies [Register]

E
e_add [Lang.F]
e_add [Wp.Lang.F]
e_and [Lang.F]
e_and [Wp.Lang.F]
e_apply [Letify.Sigma]
e_apply [Letify.Ground]
e_bigint [Lang.F]
e_bigint [Wp.Lang.F]
e_bind [Lang.F]
e_bind [Wp.Lang.F]
e_bool [Lang.F]
e_bool [Wp.Lang.F]
e_close [Lang.F]
Closes all specified binders
e_close [Wp.Lang.F]
Closes all specified binders
e_cnf [WpTac]
e_const [Lang.F]
e_const [Wp.Lang.F]
e_div [Lang.F]
e_div [Wp.Lang.F]
e_dnf [WpTac]
e_eq [Lang.F]
e_eq [Wp.Lang.F]
e_equiv [Lang.F]
e_equiv [Wp.Lang.F]
e_expr [Lang.F]
e_expr [Wp.Lang.F]
e_fact [Lang.F]
e_fact [Wp.Lang.F]
e_false [Lang.F]
e_false [Wp.Lang.F]
e_float [Lang.F]
e_float [Wp.Lang.F]
e_fun [Lang.F]
e_fun [Wp.Lang.F]
e_get [Lang.F]
e_get [Wp.Lang.F]
e_getfield [Lang.F]
e_getfield [Wp.Lang.F]
e_if [Lang.F]
e_if [Wp.Lang.F]
e_imply [Lang.F]
e_imply [Wp.Lang.F]
e_int [Lang.F]
e_int [Wp.Lang.F]
e_int64 [Lang.F]
e_int64 [Wp.Lang.F]
e_leq [Lang.F]
e_leq [Wp.Lang.F]
e_literal [Lang.F]
e_literal [Wp.Lang.F]
e_lt [Lang.F]
e_lt [Wp.Lang.F]
e_minus_one [Lang.F]
e_minus_one [Wp.Lang.F]
e_minus_one_real [Lang.F]
e_minus_one_real [Wp.Lang.F]
e_mod [Lang.F]
e_mod [Wp.Lang.F]
e_mul [Lang.F]
e_mul [Wp.Lang.F]
e_neq [Lang.F]
e_neq [Wp.Lang.F]
e_not [Lang.F]
e_not [Wp.Lang.F]
e_one [Lang.F]
e_one [Wp.Lang.F]
e_one_real [Lang.F]
e_one_real [Wp.Lang.F]
e_open [Lang.F]
Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default).
e_open [Wp.Lang.F]
Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default).
e_opp [Lang.F]
e_opp [Wp.Lang.F]
e_or [Lang.F]
e_or [Wp.Lang.F]
e_prod [Lang.F]
e_prod [Wp.Lang.F]
e_prop [Lang.F]
e_prop [Wp.Lang.F]
e_props [Lang.F]
e_props [Wp.Lang.F]
e_range [Lang.F]
e_range a b = b+1-a
e_range [Wp.Lang.F]
e_range a b = b+1-a
e_real [Lang.F]
e_real [Wp.Lang.F]
e_record [Lang.F]
e_record [Wp.Lang.F]
e_set [Lang.F]
e_set [Wp.Lang.F]
e_setfield [Lang.F]
e_setfield [Wp.Lang.F]
e_sub [Lang.F]
e_sub [Wp.Lang.F]
e_subst [Lang.F]
e_subst [Lang]
uses current pool
e_subst [Wp.Lang.F]
e_subst [Wp.Lang]
uses current pool
e_sum [Lang.F]
e_sum [Wp.Lang.F]
e_times [Lang.F]
e_times [Wp.Lang.F]
e_true [Lang.F]
e_true [Wp.Lang.F]
e_var [Lang.F]
e_var [Wp.Lang.F]
e_vars [Lang.F]
Sorted
e_vars [Wp.Lang.F]
Sorted
e_zero [Lang.F]
e_zero [Wp.Lang.F]
e_zero_real [Lang.F]
e_zero_real [Wp.Lang.F]
e_zint [Lang.F]
e_zint [Wp.Lang.F]
eat [Script]
edge_dst [Cil2cfg]
edge_src [Cil2cfg]
node and edges relations
effect [CfgCompiler.Cfg]
Represents all execution trace T such that, if T contains node a, then T also contains b with the given effect on corresponding memory states.
effect [Wp.CfgCompiler.Cfg]
Represents all execution trace T such that, if T contains node a, then T also contains b with the given effect on corresponding memory states.
either [CfgCompiler.Cfg]
Structurally corresponds to an arbitrary choice among the different possible executions.
either [Conditions]
Construct a disjunction bundle, with merging of all common parts.
either [Wp.CfgCompiler.Cfg]
Structurally corresponds to an arbitrary choice among the different possible executions.
either [Wp.Conditions]
Construct a disjunction bundle, with merging of all common parts.
elements [Vlist]
elements [Set.S]
Return the list of all elements of the given set.
emit [Warning]
Emit a warning in current context.
emit [Wp.Warning]
Emit a warning in current context.
empty [Conditions]
empty sequence, equivalent to true assumption
empty [Sigs.Sigma]
Same as Chunk.Set.empty
empty [Letify.Defs]
empty [Letify.Sigma]
empty [Vset]
empty [Splitter]
empty [Passive]
empty [Mcfg.S]
empty [Layout.Chunk]
empty [MemoryContext]
empty [Wp.Conditions]
empty sequence, equivalent to true assumption
empty [Wp.Sigs.Sigma]
Same as Chunk.Set.empty
empty [Wp.Vset]
empty [Wp.Splitter]
empty [Wp.Passive]
empty [Wp.Mcfg.S]
empty [Wp.MemoryContext]
empty [Set.S]
The empty set.
empty [Map.S]
The empty map.
empty_acc [WpStrategy]
empty_assigns_info [WpPropId]
empty_assigns_info [Wp.WpPropId]
empty_env [StmtSemantics.Make]
empty_env [Wp.StmtSemantics.Make]
encode [ProofScript]
end_session [Register]
env [Lang.F]
env [Wp.Lang.F]
env_at [LogicCompiler.Make]
env_at [Sigs.LogicSemantics]
Returns a new environment where the current memory state is moved to to the corresponding label.
env_at [Wp.LogicCompiler.Make]
env_at [Wp.Sigs.LogicSemantics]
Returns a new environment where the current memory state is moved to to the corresponding label.
env_let [LogicCompiler.Make]
env_let [Wp.LogicCompiler.Make]
env_letp [LogicCompiler.Make]
env_letp [Wp.LogicCompiler.Make]
env_letval [LogicCompiler.Make]
env_letval [Wp.LogicCompiler.Make]
env_script_update [Register]
epsilon [Rformat]
eq_alias [Region]
eqmem [MemLoader.Model]
eqmem_forall [MemLoader.Model]
eqp [Lang.F]
eqp [Wp.Lang.F]
equal [CfgCompiler.Cfg.C]
equal [CfgCompiler.Cfg.Node]
equal [Mstate]
equal [Sigs.Chunk]
equal [Letify.Sigma]
equal [Vset]
equal [Lang.F]
Same as ==
equal [RegionAnnot.Lpath]
equal [Layout.Value]
equal [Layout.Data]
equal [WpContext.SCOPE]
equal [WpContext.MODEL]
equal [WpContext.S]
equal [Clabels]
equal [Ctypes.AinfoComparable]
equal [Ctypes]
equal [Wp.CfgCompiler.Cfg.C]
equal [Wp.CfgCompiler.Cfg.Node]
equal [Wp.Mstate]
equal [Wp.Sigs.Chunk]
equal [Wp.Vset]
equal [Wp.Lang.F]
Same as ==
equal [Wp.WpContext.SCOPE]
equal [Wp.WpContext.MODEL]
equal [Wp.WpContext.S]
equal [Set.S]
equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.
equal [Map.S]
equal cmp m1 m2 tests whether the maps m1 and m2 are equal, that is, contain equal keys and associate them with equal data.
equal [Wp.Clabels]
equal [Wp.Ctypes.AinfoComparable]
equal [Wp.Ctypes]
equal_array [Cvalues]
equal_comp [Cvalues]
equal_float [Ctypes]
equal_float [Wp.Ctypes]
equal_obj [Sigs.CodeSemantics]
Same as equal_typ with an object type.
equal_obj [Wp.Sigs.CodeSemantics]
Same as equal_typ with an object type.
equal_object [Cvalues]
equal_typ [Sigs.CodeSemantics]
Computes the value of (a==b) provided both a and b are values with the given type.
equal_typ [Wp.Sigs.CodeSemantics]
Computes the value of (a==b) provided both a and b are values with the given type.
equation [Cvalues]
error [Script]
error [Warning]
error [Wp.Warning]
eval_eq [Lang.F]
Same as are_equal is Yes
eval_eq [Wp.Lang.F]
Same as are_equal is Yes
eval_leq [Lang.F]
Same as e_leq is e_true
eval_leq [Wp.Lang.F]
Same as e_leq is e_true
eval_lt [Lang.F]
Same as e_lt is e_true
eval_lt [Wp.Lang.F]
Same as e_lt is e_true
eval_neq [Lang.F]
Same as are_equal is No
eval_neq [Wp.Lang.F]
Same as are_equal is No
exercised [Register]
exist_intro [Conditions]
Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively.
exist_intro [Wp.Conditions]
Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively.
exists [ProofSession]
exists [Splitter]
exists [Wp.Splitter]
exists [Set.S]
exists p s checks if at least one element of the set satisfies the predicate p.
exists [Map.S]
exists p m checks if at least one binding of the map satisfies the predicate p.
exists [Parameter_sig.Set]
Is there some element satisfying the given predicate?
exp [Sigs.CodeSemantics]
Evaluate the expression on the given memory state.
exp [Wp.Sigs.CodeSemantics]
Evaluate the expression on the given memory state.
export [Strategy]
export [Tactical]
Register and returns the tactical
export [WpReport]
export [Vlist]
export [Wp.Strategy]
export [Wp.Tactical]
Register and returns the tactical
export_decl [Mcfg.Export]
export_decl [Wp.Mcfg.Export]
export_goal [Mcfg.Export]
export_goal [Wp.Mcfg.Export]
export_json [WpReport]
export_section [Mcfg.Export]
export_section [Wp.Mcfg.Export]
extern_f [Lang]
balance just give a default when link is not specified
extern_f [Wp.Lang]
balance just give a default when link is not specified
extern_fp [Lang]
extern_fp [Wp.Lang]
extern_p [Lang]
extern_p [Wp.Lang]
extern_s [Lang]
extern_s [Wp.Lang]
extern_t [Lang]
extern_t [Wp.Lang]
extract [Conditions]
Computes a formulae equivalent to the bundle.
extract [Letify.Defs]
extract [Wp.Conditions]
Computes a formulae equivalent to the bundle.

F
f32 [Cfloat]
f32 [Wp.Cfloat]
f64 [Cfloat]
f64 [Wp.Cfloat]
f_addr_of_int [MemMemory]
Physical address
f_base [MemMemory]
f_bits [Cint]
All bit-test functions
f_bits [Ctypes]
size in bits
f_bits [Wp.Cint]
All bit-test functions
f_bits [Wp.Ctypes]
size in bits
f_bitwised [Cint]
All except f_bit_positive
f_bitwised [Wp.Cint]
All except f_bit_positive
f_bytes [Ctypes]
size in bytes
f_bytes [Wp.Ctypes]
size in bytes
f_concat [Vlist]
f_cons [Vlist]
f_convert [Ctypes]
f_convert [Wp.Ctypes]
f_delta [Cfloat]
f_delta [Wp.Cfloat]
f_elt [Vlist]
f_epsilon [Cfloat]
f_epsilon [Wp.Cfloat]
f_global [MemMemory]
f_havoc [MemMemory]
f_iabs [Cmath]
f_int_of_addr [MemMemory]
Physical address
f_iter [Ctypes]
f_iter [Wp.Ctypes]
f_land [Cint]
f_land [Wp.Cint]
f_lnot [Cint]
f_lnot [Wp.Cint]
f_lor [Cint]
f_lor [Wp.Cint]
f_lsl [Cint]
f_lsl [Wp.Cint]
f_lsr [Cint]
f_lsr [Wp.Cint]
f_lxor [Cint]
f_lxor [Wp.Cint]
f_memo [Ctypes]
memoized, not-projectified
f_memo [Wp.Ctypes]
memoized, not-projectified
f_model [Cfloat]
f_model [Wp.Cfloat]
f_nil [Vlist]
f_nth [Vlist]
f_null [MemMemory]
f_offset [MemMemory]
f_rabs [Cmath]
f_real_of_int [Cmath]
f_region [MemMemory]
f_repeat [Vlist]
f_shift [MemMemory]
f_sqrt [Cmath]
fadd [Cfloat]
fadd [Wp.Cfloat]
failed [VCS]
failed [Wp.VCS]
fcstat [WpReport]
fdiv [Cfloat]
fdiv [Wp.Cfloat]
feq [Cfloat]
feq [Wp.Cfloat]
field [MemLoader.Model]
field [Mstate]
field [Sigs.Model]
Return the memory location obtained by field access from a given memory location.
field [Cvalues.Logic]
field [Repr]
field [Lang]
field [Layout.Offset]
field [Wp.Mstate]
field [Wp.Sigs.Model]
Return the memory location obtained by field access from a given memory location.
field [Wp.Repr]
field [Wp.Lang]
field_id [Lang]
field_id [Wp.Lang]
field_offset [Region]
field_offset [Layout.Offset]
field_offset [Ctypes]
field_offset [Wp.Ctypes]
fields [TacInstance]
fields_of_adt [Lang]
fields_of_adt [Wp.Lang]
fields_of_field [Lang]
fields_of_field [Wp.Lang]
fields_of_tau [Lang]
fields_of_tau [Wp.Lang]
file_goal [Wpo.DISK]
file_goal [Wp.Wpo.DISK]
file_kf [Wpo.DISK]
file_kf [Wp.Wpo.DISK]
file_logerr [Wpo.DISK]
file_logerr [Wp.Wpo.DISK]
file_logout [Wpo.DISK]
file_logout [Wp.Wpo.DISK]
filename_for_prover [VCS]
filename_for_prover [Wp.VCS]
filter [GuiProver]
filter [Auto]
filter [TacInstance]
filter [Script]
filter [Filtering]
filter [Conditions]
filter [Splitter]
filter [Wp.Auto]
filter [Wp.Filtering]
filter [Wp.Conditions]
filter [Wp.Splitter]
filter [Set.S]
filter p s returns the set of all elements in s that satisfy predicate p.
filter [Map.S]
filter p m returns the map with all the bindings in m that satisfy predicate p.
filter_hypotheses [Lang]
filter_hypotheses [Wp.Lang]
filter_map_inplace [Hashtbl.S]
filter_pred [Cleaning]
filter_status [WpAnnot]
filter_type [Cleaning]
find [TacLemma]
find [Pcfg]
find [Letify.Sigma]
find [Cfloat]
find [Cil2cfg.HEsig]
find [WpContext.Registry]
find [Hashtbl.S]
find [Wp.Pcfg]
find [Wp.Cfloat]
find [Wp.WpContext.Registry]
find [Set.S]
find x s returns the element of s equal to x (according to Ord.compare), or raise Not_found if no such element exists.
find [Map.S]
find x m returns the current binding of x in m, or raises Not_found if no such binding exists.
find_all [Cil2cfg.HEsig]
find_all [Hashtbl.S]
find_fallback [Why3Provers]
find_first [Set.S]
find_first f s, where f is a monotonically increasing function, returns the lowest element e of s such that f e, or raises Not_found if no such element exists.
find_first [Map.S]
find_first f m, where f is a monotonically increasing function, returns the binding of m with the lowest key k such that f k, or raises Not_found if no such key exists.
find_first_opt [Set.S]
find_first_opt f s, where f is a monotonically increasing function, returns an option containing the lowest element e of s such that f e, or None if no such element exists.
find_first_opt [Map.S]
find_first_opt f m, where f is a monotonically increasing function, returns an option containing the binding of m with the lowest key k such that f k, or None if no such key exists.
find_last [Set.S]
find_last f s, where f is a monotonically decreasing function, returns the highest element e of s such that f e, or raises Not_found if no such element exists.
find_last [Map.S]
find_last f m, where f is a monotonically decreasing function, returns the binding of m with the highest key k such that f k, or raises Not_found if no such key exists.
find_last_opt [Set.S]
find_last_opt f s, where f is a monotonically decreasing function, returns an option containing the highest element e of s such that f e, or None if no such element exists.
find_last_opt [Map.S]
find_last_opt f m, where f is a monotonically decreasing function, returns an option containing the binding of m with the highest key k such that f k, or None if no such key exists.
find_lemma [Definitions]
find_lemma [Wp.Definitions]
find_lib [LogicBuiltins]
find a file in the includes of the current drivers
find_lib [Wp.LogicBuiltins]
find a file in the includes of the current drivers
find_name [Definitions]
find_name [Wp.Definitions]
find_opt [Why3Provers]
find_opt [Hashtbl.S]
find_opt [Set.S]
find_opt x s returns the element of s equal to x (according to Ord.compare), or None if no such element exists.
find_opt [Map.S]
find_opt x m returns Some v if the current binding of x in m is v, or None if no such binding exists.
find_symbol [Definitions]
find_symbol [Wp.Definitions]
first [ProverSearch]
fixpoint [Region]
fle [Cfloat]
fle [Wp.Cfloat]
float_lit [Cfloat]
Returns a string literal in decimal notation (without suffix) that reparses to the same value (when added suffix).
float_lit [Wp.Cfloat]
Returns a string literal in decimal notation (without suffix) that reparses to the same value (when added suffix).
float_of_int [Cfloat]
float_of_int [Wp.Cfloat]
float_of_real [Cfloat]
float_of_real [Wp.Cfloat]
floats [Lang]
type of floats
floats [Wp.Lang]
type of floats
flt [Cfloat]
flt [Wp.Cfloat]
flt_add [Cfloat]
flt_add [Wp.Cfloat]
flt_div [Cfloat]
flt_div [Wp.Cfloat]
flt_mul [Cfloat]
flt_mul [Wp.Cfloat]
flt_neg [Cfloat]
flt_neg [Wp.Cfloat]
flt_of_real [Cfloat]
flt_of_real [Wp.Cfloat]
flush [Warning]
flush [Wp.Warning]
fmode [TacCut]
fmul [Cfloat]
fmul [Wp.Cfloat]
fneq [Cfloat]
fneq [Wp.Cfloat]
fold [Splitter]
fold [Hashtbl.S]
fold [Wp.Splitter]
fold [Set.S]
fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s, in increasing order.
fold [Map.S]
fold f m a computes (f kN dN ... (f k1 d1 a)...), where k1 ... kN are the keys of all bindings in m (in increasing order), and d1 ... dN are the associated data.
fold_bhv_post_cond [WpStrategy]
apply f_normal on the Normal postconditions, f_exits on the Exits postconditions, and warn on the others.
fold_nodes [Cil2cfg]
iterators
fopp [Cfloat]
fopp [Wp.Cfloat]
for_all [Splitter]
for_all [Wp.Splitter]
for_all [Set.S]
for_all p s checks if all elements of the set satisfy the predicate p.
for_all [Map.S]
for_all p m checks if all the bindings of the map satisfy the predicate p.
forall_intro [Conditions]
Introduce universally quantified formulae: head forall quantifiers are instanciated to fresh variables in current pool and left-implies are extracted, recursively.
forall_intro [Wp.Conditions]
Introduce universally quantified formulae: head forall quantifiers are instanciated to fresh variables in current pool and left-implies are extracted, recursively.
fork [ProofEngine]
formal [LogicCompiler.Make]
formal [Clabels]
formal [Wp.LogicCompiler.Make]
formal [Wp.Clabels]
forward [ProofEngine]
forward [Letify.Ground]
fq32 [Cfloat]
fq32 [Wp.Cfloat]
fq64 [Cfloat]
fq64 [Wp.Cfloat]
frame [LogicCompiler.Make]
frame [Sigs.LogicSemantics]
Make a fresh frame with the given function.
frame [Sigs.Model]
Assert the memory is a proper heap state preceeding the function entry point.
frame [Wp.LogicCompiler.Make]
frame [Wp.Sigs.LogicSemantics]
Make a fresh frame with the given function.
frame [Wp.Sigs.Model]
Assert the memory is a proper heap state preceeding the function entry point.
framed [Layout.Root]
frames [MemMemory]
frames [MemLoader.Model]
free [Context]
Performs the job with local context cleared.
free [Wp.Context]
Performs the job with local context cleared.
fresh [Lang.F]
fresh [Wp.Lang.F]
freshen [Lang]
freshen [Wp.Lang]
freshvar [Lang]
freshvar [Wp.Lang]
from [Layout.Root]
froms [StmtSemantics.Make]
froms [Wp.StmtSemantics.Make]
fsub [Cfloat]
fsub [Wp.Cfloat]
ftau [Cfloat]
model independant
ftau [Wp.Cfloat]
model independant
fusion [Region]
fusionned [Region]

G
garbled [Layout.Compound]
gcd [Layout.Matrix]
generate [WpRTE]
generate_call [VC]
generate_call [Wp.VC]
generate_ip [VC]
generate_ip [Wp.VC]
generate_kf [VC]
generate_kf [Wp.VC]
generated_f [Lang]
generated_f [Wp.Lang]
generated_p [Lang]
generated_p [Wp.Lang]
get [ProverScript]
get [ProofEngine]
get [ProofSession]
get [Tactical.Fmap]
raises Not_found if absent
get [CfgCompiler.Cfg.E]
get [CfgCompiler.Cfg.T]
get [CfgCompiler.Cfg.P]
get [CfgCompiler.Cfg.C]
get [Sigs.Sigma]
Lazily get the variable for a chunk.
get [Lang.F.Subst]
get [Cil2cfg]
get [RegionAnalysis]
get [RefUsage]
get [WpContext.Generator]
get [WpContext.Registry]
get [Context]
Retrieves the current value of the context.
get [Dyncall]
Returns None if there is no specified dynamic call.
get [Wp.Tactical.Fmap]
raises Not_found if absent
get [Wp.CfgCompiler.Cfg.E]
get [Wp.CfgCompiler.Cfg.T]
get [Wp.CfgCompiler.Cfg.P]
get [Wp.CfgCompiler.Cfg.C]
get [Wp.Sigs.Sigma]
Lazily get the variable for a chunk.
get [Wp.Lang.F.Subst]
get [Wp.WpContext.Generator]
get [Wp.WpContext.Registry]
get [Wp.Context]
Retrieves the current value of the context.
get [Wp.RefUsage]
get_addrof [Region]
get_alias [Region]
get_annots [WpStrategy]
get_array [Ctypes]
get_array [Wp.Ctypes]
get_array_dim [Ctypes]
get_array_dim [Wp.Ctypes]
get_array_size [Ctypes]
get_array_size [Wp.Ctypes]
get_asgn_goal [WpStrategy]
get_asgn_hyp [WpStrategy]
get_bhv [WpStrategy]
get_both_hyp_goals [WpStrategy]
get_builtin_type [Lang]
get_builtin_type [Wp.Lang]
get_call_asgn [WpStrategy]
get_call_hyp [WpStrategy]
To be used as hypotheses around a call, (the pre are in get_call_pre_goal)
get_call_out_edges [Cil2cfg]
similar to succ_e g v but gives the edge to VcallOut first and the edge to Vexit second.
get_call_post [WpStrategy]
Post-checks of a called function to be considered as goal only
get_call_pre [WpStrategy]
Preconditions of a called function to be considered as hyp and goal (similar to get_both_hyp_goals).
get_call_pre_strategies [WpAnnot]
get_call_type [Cil2cfg]
get_called_assigns [WpAnnot]
Properties for assigns of kf
get_called_exit_conditions [WpAnnot]
get_called_post_conditions [WpAnnot]
get_called_preconditions_at [WpAnnot]
get_context [VC]
get_context [Wpo]
get_context [WpContext]
get_context [Wp.Wpo]
get_context [Wp.VC]
get_context [Wp.WpContext]
get_copies [Region]
get_cut [WpStrategy]
the bool in get_cut results says if the property has to be considered as a both goal and hyp (goal=true, or hyp only (goal=false)
get_descr [Wpo.GOAL]
get_descr [WpContext]
get_descr [Wp.Wpo.GOAL]
get_descr [Wp.WpContext]
get_description [VC]
get_description [Wp.VC]
get_edge_labels [Cil2cfg]
get_edge_next_stmt [Cil2cfg]
get_edge_stmt [Cil2cfg]
Complete get_edge_labels and returns the associated stmt, if any.
get_emitter [WpContext]
get_emitter [Wp.WpContext]
get_exit_edges [Cil2cfg]
Find the edges e that goes to the Vexit node inside the statement beginning at node n
get_file_logerr [Wpo]
only filename, might not exists
get_file_logerr [Wp.Wpo]
only filename, might not exists
get_file_logout [Wpo]
only filename, might not exists
get_file_logout [Wp.Wpo]
only filename, might not exists
get_files [Wpo]
get_files [Wp.Wpo]
get_formula [VC]
get_formula [Wp.VC]
get_frame [LogicCompiler.Make]
get_frame [Sigs.LogicSemantics]
Get the current frame, or raise a fatal error if none.
get_frame [Wp.LogicCompiler.Make]
get_frame [Wp.Sigs.LogicSemantics]
Get the current frame, or raise a fatal error if none.
get_froms [Region]
get_function_name [Parameter_sig.String]
returns the given argument only if it is a valid function name (see Parameter_customize.get_c_ified_functions for more information), and abort otherwise.
get_function_strategies [WpAnnot]
get_gamma [Lang]
get_gamma [Wp.Lang]
get_gid [Wpo]
Dynamically exported
get_gid [Wp.Wpo]
Dynamically exported
get_goal_only [WpStrategy]
get_hits [ProverWhy3]
get_hyp_only [WpStrategy]
get_hypotheses [Lang]
get_hypotheses [Wp.Lang]
get_id [VC]
get_id [Wp.VC]
get_id_prop_strategies [WpAnnot]
get_index [Wpo]
get_index [Wp.Wpo]
get_induction [WpPropId]
Quite don't understand what is going on here...
get_induction [Wp.WpPropId]
get_induction_labels [LogicUsage]
Given an inductive phi{...A...}.
get_induction_labels [Wp.LogicUsage]
Given an inductive phi{...A...}.
get_int [Tactical]
get_int [Ctypes]
get_int [Wp.Tactical]
get_int [Wp.Ctypes]
get_int64 [Ctypes]
get_int64 [Wp.Ctypes]
get_internal_edges [Cil2cfg]
Find the edges e of the statement node n postcondition and the set of edges that are inside the statement (e excluded).
get_kf [WpStrategy]
get_kf [Wp_parameters]
get_kf [Wp.Wp_parameters]
get_label [Wpo]
get_label [Wp.Wpo]
get_legacy [WpPropId]
Unique legacy identifier of prop_id
get_legacy [Wp.WpPropId]
Unique legacy identifier of prop_id
get_logerr [VC]
only file name, might not exists
get_logerr [Wp.VC]
only file name, might not exists
get_logout [VC]
only file name, might not exists
get_logout [Wp.VC]
only file name, might not exists
get_merged [Region]
get_miss [ProverWhy3]
get_mode [ProverWhy3]
get_model [VC]
get_model [Wpo]
get_model [WpContext]
get_model [Wp.Wpo]
get_model [Wp.VC]
get_model [Wp.WpContext]
get_name [LogicUsage]
get_name [Wp.LogicUsage]
get_offset [Region]
get_opt [Context]
Retrieves the current value of the context.
get_opt [Wp.Context]
Retrieves the current value of the context.
get_option [LogicBuiltins]
return the values of option (group, name), return the empty list if not set
get_option [Wp.LogicBuiltins]
return the values of option (group, name), return the empty list if not set
get_output [Wp_parameters]
get_output [Wp.Wp_parameters]
get_output_dir [Wp_parameters]
get_output_dir [Wp.Wp_parameters]
get_overflows [Wp_parameters]
get_overflows [Wp.Wp_parameters]
get_plain_string [Parameter_sig.String]
always return the argument, even if the argument is not a function name.
get_pointed [Region]
get_pool [Lang]
get_pool [Wp.Lang]
get_possible_values [Parameter_sig.String]
What are the acceptable values for this parameter.
get_post_edges [Cil2cfg]
Find the edges where the postconditions of the node statement have to be checked.
get_post_label [Cil2cfg]
Get the label to be used for the Post state of the node contract if any.
get_pre_edges [Cil2cfg]
Find the edges where the precondition of the node statement have to be checked.
get_proof [Wpo]
get_proof [Wp.Wpo]
get_property [VC]
get_property [Wpo]
Dynamically exported
get_property [Wp.Wpo]
Dynamically exported
get_property [Wp.VC]
get_propid [WpPropId]
Unique identifier of prop_id
get_propid [Wp.WpPropId]
Unique identifier of prop_id
get_prover_names [Register]
get_pstat [Register]
get_range [Parameter_sig.Int]
What is the possible range of values for this parameter.
get_removed [ProverWhy3]
get_result [VC]
get_result [Wpo]
get_result [Wp.Wpo]
get_result [Wp.VC]
get_results [VC]
get_results [Wpo]
get_results [Wp.Wpo]
get_results [Wp.VC]
get_roots [Region]
get_scope [VC]
get_scope [Wpo]
get_scope [WpContext]
get_scope [Wp.Wpo]
get_scope [Wp.VC]
get_scope [Wp.WpContext]
get_sequent [VC]
get_sequent [Wp.VC]
get_session [Wp_parameters]
get_session [Wp.Wp_parameters]
get_session_dir [Wp_parameters]
get_session_dir [Wp.Wp_parameters]
get_stepout [VCS]
0 means no-stepout
get_stepout [Wp.VCS]
0 means no-stepout
get_steps [Wpo]
get_steps [Wp.Wpo]
get_strategies [ProofEngine]
get_switch_edges [Cil2cfg]
similar to succ_e g v but give the switch cases and the default edge
get_target [Wpo]
get_target [Wp.Wpo]
get_test_edges [Cil2cfg]
similar to succ_e g v but tests the branch to return (then-edge, else-edge)
get_time [Wpo]
get_time [Rformat]
get_time T t returns k such that T[k-1] <= t <= T[k], T is extended with T[-1]=0 and T[N]=+oo.
get_time [Wp.Wpo]
get_timeout [VCS]
0 means no-timeout
get_timeout [Wp.VCS]
0 means no-timeout
get_wp [Wp_parameters]
get_wp [Wp.Wp_parameters]
global [Sigs.Model]
Given a pointer value p, assumes this pointer p (when valid) is allocated outside the function frame under analysis.
global [Wp.Sigs.Model]
Given a pointer value p, assumes this pointer p (when valid) is allocated outside the function frame under analysis.
global_axioms [WpStrategy]
goal [ProofEngine]
goals_nodes [StmtSemantics.Make]
goals_nodes [Wp.StmtSemantics.Make]
goals_of_property [Wpo]
All POs related to a given property.
goals_of_property [Wp.Wpo]
All POs related to a given property.
goto [ProofEngine]
goto [CfgCompiler.Cfg]
Represents all execution traces T such that, if T contains node a, T also contains node b and memory states at a and b are equal.
goto [Wp.CfgCompiler.Cfg]
Represents all execution traces T such that, if T contains node a, T also contains node b and memory states at a and b are equal.
group [Splitter]
group [Wp.Splitter]
guard [CfgCompiler.Cfg]
Structurally corresponds to an assume control-flow.
guard [Wp.CfgCompiler.Cfg]
Structurally corresponds to an assume control-flow.
guard' [CfgCompiler.Cfg]
Same than guard but the condition is negated
guard' [Wp.CfgCompiler.Cfg]
Same than guard but the condition is negated
guards [LogicCompiler.Make]
guards [Sigs.LogicSemantics]
Returns the current gamma environment from the current frame.
guards [Wp.LogicCompiler.Make]
guards [Wp.Sigs.LogicSemantics]
Returns the current gamma environment from the current frame.

H
hack [LogicBuiltins]
Replace a logic definition or predicate by a built-in function.
hack [Wp.LogicBuiltins]
Replace a logic definition or predicate by a built-in function.
hack_type [LogicBuiltins]
Replace a logic type definition or predicate by a built-in type.
hack_type [Wp.LogicBuiltins]
Replace a logic type definition or predicate by a built-in type.
handle [Warning]
Handle the error and emit a warning with specified severity and effect if a context has been set.
handle [Wp.Warning]
Handle the error and emit a warning with specified severity and effect if a context has been set.
has_copies [Region]
has_ctype [Cvalues]
has_deref [Region]
has_dkey [Wp_parameters]
has_dkey [Wp.Wp_parameters]
has_exit [Cil2cfg]
whether an exit edge exists or not
has_gamma [Lang]
has_gamma [Wp.Lang]
has_init [Mcfg.S]
has_init [Wp.Mcfg.S]
has_layout [Region]
has_ltype [LogicCompiler.Make]
has_ltype [Wp.LogicCompiler.Make]
has_names [Region]
has_offset [Region]
has_out [Wp_parameters]
has_out [Wp.Wp_parameters]
has_pointed [Region]
has_print_generated [Wp_parameters]
Debugging Categories
has_print_generated [Wp.Wp_parameters]
Debugging Categories
has_proof [ProofScript]
Has a tactical alternative
has_return [Region]
has_roots [Region]
has_session [Wp_parameters]
has_session [Wp.Wp_parameters]
has_shortcut [Why3Provers]
has_verdict [Wpo]
has_verdict [Wp.Wpo]
hash [Sigs.Chunk]
hash [Lang.F]
Constant time
hash [WpContext.SCOPE]
hash [WpContext.MODEL]
hash [WpContext.S]
hash [Ctypes.AinfoComparable]
hash [Ctypes]
hash [Wp.Sigs.Chunk]
hash [Wp.Lang.F]
Constant time
hash [Wp.WpContext.SCOPE]
hash [Wp.WpContext.MODEL]
hash [Wp.WpContext.S]
hash [Wp.Ctypes.AinfoComparable]
hash [Wp.Ctypes]
have [Conditions]
Predicate for Have and such, True for any other
have [Wp.Conditions]
Predicate for Have and such, True for any other
havoc [Auto]
havoc [CfgCompiler.Cfg]
Inserts an assigns effect between nodes a and b, correspondings to all the written memory chunks accessible in execution paths delimited by the effects sequence of nodes.
havoc [MemLoader.Model]
havoc [MemLoader.Make]
havoc [Sigs.Sigma]
All the chunks in the provided footprint are generated and made fresh.
havoc [Wp.Auto]
havoc [Wp.CfgCompiler.Cfg]
Inserts an assigns effect between nodes a and b, correspondings to all the written memory chunks accessible in execution paths delimited by the effects sequence of nodes.
havoc [Wp.Sigs.Sigma]
All the chunks in the provided footprint are generated and made fresh.
havoc_any [Sigs.Sigma]
All the chunks are made fresh.
havoc_any [Wp.Sigs.Sigma]
All the chunks are made fresh.
havoc_chunk [Sigs.Sigma]
Generate a new fresh variable for the given chunk.
havoc_chunk [Wp.Sigs.Sigma]
Generate a new fresh variable for the given chunk.
havoc_length [MemLoader.Make]
head [ProofEngine]
head [Tactical]
head [Footprint]
Head only footprint
head [Conditions]
Predicate for Have and such, Condition for Branch, True for Either
head [Wp.Tactical]
head [Wp.Conditions]
Predicate for Have and such, Condition for Branch, True for Either
here [Clabels]
here [Wp.Clabels]
hints_for [Proof]
hypotheses [MemVar.VarUsage]
hypotheses [Sigs.Model]
Computes the memory model hypotheses including separation and validity clauses to be verified for this model.
hypotheses [Lang]
hypotheses [Wp.MemVar.VarUsage]
hypotheses [Wp.Sigs.Model]
Computes the memory model hypotheses including separation and validity clauses to be verified for this model.
hypotheses [Wp.Lang]

I
i_bits [Ctypes]
size in bits
i_bits [Wp.Ctypes]
size in bits
i_bytes [Ctypes]
size in bytes
i_bytes [Wp.Ctypes]
size in bytes
i_convert [Ctypes]
i_convert [Wp.Ctypes]
i_iter [Ctypes]
i_iter [Wp.Ctypes]
i_memo [Ctypes]
memoized, not-projectified
i_memo [Wp.Ctypes]
memoized, not-projectified
iadd [Cint]
iadd [Wp.Cint]
id [LogicBuiltins]
id [Matrix]
unique w.r.t equal
id [Region]
id [WpContext.Registry]
id [WpContext.SCOPE]
id [WpContext.MODEL]
id [WpContext.S]
id [Wp.LogicBuiltins]
id [Wp.WpContext.Registry]
id [Wp.WpContext.SCOPE]
id [Wp.WpContext.MODEL]
id [Wp.WpContext.S]
ident [Factory]
ident [Tactical]
ident [Script]
ident [Wp.Tactical]
ident [Wp.Factory]
idents [Script]
idiv [Cint]
idiv [Wp.Cint]
if_else [Splitter]
if_else [Wp.Splitter]
if_then [Splitter]
if_then [Wp.Splitter]
imod [Cint]
imod [Wp.Cint]
implies [CfgCompiler.Cfg]
implies is the dual of either.
implies [Wp.CfgCompiler.Cfg]
implies is the dual of either.
imul [Cint]
imul [Wp.Cint]
in_frame [LogicCompiler.Make]
in_frame [Sigs.LogicSemantics]
Execute the given closure with the specified current frame.
in_frame [Wp.LogicCompiler.Make]
in_frame [Wp.Sigs.LogicSemantics]
Execute the given closure with the specified current frame.
in_range [Vset]
in_range [Wp.Vset]
in_size [Vset]
in_size [Wp.Vset]
in_state [Lang.For_export]
in_state [Wp.Lang.For_export]
included [MemMemory]
included [Sigs.Model]
Return the formula that tests if two segment are included
included [Cvalues.Logic]
included [Layout.Range]
included [Wp.Sigs.Model]
Return the formula that tests if two segment are included
incr [Parameter_sig.Int]
Increment the integer.
index [ProverSearch]
index [Conditions]
Compute steps' id of sequent left hand-side.
index [Mstate]
index [Layout.Offset]
index [Wp.Conditions]
Compute steps' id of sequent left hand-side.
index [Wp.Mstate]
indexed [Layout.Root]
infoprover [Lang]
same information for all the provers
infoprover [Wp.Lang]
same information for all the provers
init [StmtSemantics.Make]
connect init to here.
init [CfgCompiler.Cfg.T]
init [Sigs.CodeSemantics]
Express that some variable has some initial value at the given memory state.
init [Mcfg.S]
init [Clabels]
init [Wp.StmtSemantics.Make]
init [Wp.CfgCompiler.Cfg.T]
init [Wp.Sigs.CodeSemantics]
Express that some variable has some initial value at the given memory state.
init [Wp.Mcfg.S]
init [Wp.Clabels]
init' [CfgCompiler.Cfg.T]
init' [Wp.CfgCompiler.Cfg.T]
insert [Tactical]
insert [Conditions]
Insert a step in the sequent immediately at the specified position.
insert [Wp.Tactical]
insert [Wp.Conditions]
Insert a step in the sequent immediately at the specified position.
instance [Factory]
instance [Auto]
instance [Wp.Auto]
instance [Wp.Factory]
instance_goal [TacInstance]
instance_have [TacInstance]
instance_of [Sigs.CodeSemantics]
Check whether a function pointer is (an instance of) some kernel function.
instance_of [Wp.Sigs.CodeSemantics]
Check whether a function pointer is (an instance of) some kernel function.
instr [StmtSemantics.Make]
instr [Wp.StmtSemantics.Make]
int [Tactical]
int [Wp.Tactical]
int_of_bool [Cmath]
int_of_loc [Sigs.Model]
Cast a memory location into its absolute memory address, given as an integer with the given C-type.
int_of_loc [Wp.Sigs.Model]
Cast a memory location into its absolute memory address, given as an integer with the given C-type.
int_of_real [Cmath]
inter [Cvalues.Logic]
inter [Vset]
inter [Wp.Vset]
inter [Set.S]
Set intersection.
intersect [Conditions]
Variables of predicate and the bundle intersects
intersect [Lang.F]
intersect [Wp.Conditions]
Variables of predicate and the bundle intersects
intersect [Wp.Lang.F]
intersectp [Lang.F]
intersectp [Wp.Lang.F]
introduction [Conditions]
Performs existential, universal and hypotheses introductions
introduction [Wp.Conditions]
Performs existential, universal and hypotheses introductions
introduction_eq [Conditions]
Same as introduction but returns the same sequent is None
introduction_eq [Wp.Conditions]
Same as introduction but returns the same sequent is None
intros [Conditions]
Assumes a list of predicates in a Have section on top of the bundle.
intros [Wp.Conditions]
Assumes a list of predicates in a Have section on top of the bundle.
intuition [Auto]
intuition [Wp.Auto]
invalid [VCS]
invalid [Sigs.Model]
Returns the formula that tests if the entire memory is invalid for write access.
invalid [Cvalues.Logic]
invalid [Wp.VCS]
invalid [Wp.Sigs.Model]
Returns the formula that tests if the entire memory is invalid for write access.
iopp [Cint]
iopp [Wp.Cint]
ip_lemma [LogicUsage]
ip_lemma [Wp.LogicUsage]
isGlobalInitConst [WpStrategy]
True if the variable is global, not extern, with a "const" qualifier type.
isInitConst [WpStrategy]
True if both options -const-readonly and -wp-init are positioned, and the variable is global, not extern, with a "const" type (see hasConstAttribute).
is_absorbant [Lang.F]
is_absorbant [Wp.Lang.F]
is_aliased [Region]
is_aliased [Layout.Usage]
is_aliased [Layout.Alias]
is_arith [Lang.F]
Integer or Real sort
is_arith [Wp.Lang.F]
Integer or Real sort
is_array [Ctypes]
is_array [Wp.Ctypes]
is_assigns [WpPropId]
is_assigns [Wp.WpPropId]
is_atomic [Lang.F]
Constants and variables
is_atomic [Wp.Lang.F]
Constants and variables
is_auto [VCS]
is_auto [Wp.VCS]
is_available [Why3Provers]
is_back_edge [Cil2cfg]
is_builtin [Lang]
is_builtin [Wp.Lang]
is_builtin_type [Lang]
is_builtin_type [Wp.Lang]
is_call_assigns [WpPropId]
is_call_assigns [Wp.WpPropId]
is_char [Ctypes]
is_char [Wp.Ctypes]
is_check [WpPropId]
is_check [Wp.WpPropId]
is_cint [Cint]
Raises Not_found if not.
is_cint [Wp.Cint]
Raises Not_found if not.
is_cint_simplifier [Cint]
Remove the is_cint in formulas that are redundant with other conditions.
is_cint_simplifier [Wp.Cint]
Remove the is_cint in formulas that are redundant with other conditions.
is_closed [Lang.F]
No bound variables
is_closed [Wp.Lang.F]
No bound variables
is_cnf [WpTac]
is_comp [Ctypes]
is_comp [Wp.Ctypes]
is_composed [WpAnnot]
whether a proof needs several lemma to be complete
is_compound [Ctypes]
is_compound [Wp.Ctypes]
is_computing [VCS]
is_computing [Wp.VCS]
is_dead_annot [WpReached]
False assertions and loop invariant.
is_dead_code [WpReached]
Checks whether the stmt has a dead-code annotation.
is_default [LogicBuiltins]
is_default [Wp.LogicBuiltins]
is_default_behavior [WpStrategy]
is_defined [WpContext]
is_defined [Wp.WpContext]
is_dnf [WpTac]
is_empty [Tactical]
is_empty [Conditions]
No step at all
is_empty [Vset]
is_empty [Passive]
is_empty [Region]
is_empty [Layout.Cluster]
is_empty [Wp.Tactical]
is_empty [Wp.Conditions]
No step at all
is_empty [Wp.Vset]
is_empty [Wp.Passive]
is_empty [Set.S]
Test whether a set is empty or not.
is_empty [Map.S]
Test whether a map is empty or not.
is_empty_script [Proof]
Check a proof script text for emptyness
is_equal [Lang.F]
is_equal [Wp.Lang.F]
is_exp_range [Sigs.CodeSemantics]
Express that all objects in a range of locations have a given value.
is_exp_range [Wp.Sigs.CodeSemantics]
Express that all objects in a range of locations have a given value.
is_false [Cvalues]
p ? 0 : 1
is_false [Lang.F]
Constant time.
is_false [Wp.Lang.F]
Constant time.
is_framed [Sigs.Chunk]
Whether the chunk is local to a function call.
is_framed [Wp.Sigs.Chunk]
Whether the chunk is local to a function call.
is_garbled [Region]
is_garbled [Layout.Cluster]
is_here [Clabels]
is_here [Wp.Clabels]
is_int [Lang.F]
Integer sort
is_int [Wp.Lang.F]
Integer sort
is_invalid [WpAnnot]
whether an invalid proof result has been registered or not
is_literal [Lang]
is_literal [Wp.Lang]
is_loop_preservation [WpPropId]
is_loop_preservation [Wp.WpPropId]
is_main_init [WpStrategy]
The function is the main entry point AND it is not a lib entry
is_neutral [Lang.F]
is_neutral [Wp.Lang.F]
is_null [Sigs.Model]
Return the formula that check if a given location is null
is_null [Cvalues]
is_null [Wp.Sigs.Model]
Return the formula that check if a given location is null
is_object [Cvalues]
is_pfalse [Lang.F]
is_pfalse [Wp.Lang.F]
is_pointer [Ctypes]
is_pointer [Wp.Ctypes]
is_positive_or_null [Cint]
is_positive_or_null [Wp.Cint]
is_predicate [WpReached]
If returns true the predicate has always the given boolean value.
is_primitive [Lang.F]
Constants only
is_primitive [Wp.Lang.F]
Constants only
is_prop [Lang.F]
Boolean or Property
is_prop [Wp.Lang.F]
Boolean or Property
is_proved [VC]
is_proved [Wpo]
do not tries simplification, check prover results
is_proved [VCS]
is_proved [WpAnnot]
whether all partial proofs have been accumulated or not
is_proved [Wp.Wpo]
do not tries simplification, check prover results
is_proved [Wp.VC]
is_proved [Wp.VCS]
is_prover [ProofScript]
is_ptrue [Lang.F]
is_ptrue [Wp.Lang.F]
is_read [Region]
is_real [Lang.F]
Real sort
is_real [Wp.Lang.F]
Real sort
is_recursive [LogicUsage]
is_recursive [Wp.LogicUsage]
is_requires [WpPropId]
is_requires [Wp.WpPropId]
is_shifted [Region]
is_shifted [Layout.Usage]
is_simple [Lang.F]
Constants, variables, functions of arity 0
is_simple [Wp.Lang.F]
Constants, variables, functions of arity 0
is_smoke_test [Wpo]
is_smoke_test [WpPropId]
is_smoke_test [Wp.Wpo]
is_smoke_test [Wp.WpPropId]
is_subterm [Lang.F]
is_subterm [Wp.Lang.F]
is_tactic [ProofScript]
is_tactic [Wpo]
is_tactic [WpPropId]
is_tactic [Wp.Wpo]
is_tactic [Wp.WpPropId]
is_trivial [VC]
is_trivial [Wpo.VC_Annot]
is_trivial [Wpo.VC_Lemma]
is_trivial [Wpo.GOAL]
is_trivial [Wpo]
do not tries simplification, do not check prover results
is_trivial [Conditions]
Goal is true or hypotheses contains false.
is_trivial [Wp.Wpo.VC_Annot]
is_trivial [Wp.Wpo.VC_Lemma]
is_trivial [Wp.Wpo.GOAL]
is_trivial [Wp.Wpo]
do not tries simplification, do not check prover results
is_trivial [Wp.VC]
is_trivial [Wp.Conditions]
Goal is true or hypotheses contains false.
is_true [Conditions]
Contains only true or empty steps
is_true [Cvalues]
p ? 1 : 0
is_true [Lang.F]
Constant time.
is_true [Wp.Conditions]
Contains only true or empty steps
is_true [Wp.Lang.F]
Constant time.
is_unknown [Wpo]
is_unknown [Wp.Wpo]
is_valid [Wpo]
true if the result is valid.
is_valid [VCS]
is_valid [Wp.Wpo]
true if the result is valid.
is_valid [Wp.VCS]
is_verdict [VCS]
is_verdict [Wp.VCS]
is_well_formed [Sigs.Model]
Provides the constraint corresponding to the kind of data stored by all chunks in sigma.
is_well_formed [Wp.Sigs.Model]
Provides the constraint corresponding to the kind of data stored by all chunks in sigma.
is_written [Region]
is_zero [Sigs.CodeSemantics]
Express that the object (of specified type) at the given location is filled with zeroes.
is_zero [Lang.F]
is_zero [Wp.Sigs.CodeSemantics]
Express that the object (of specified type) at the given location is filled with zeroes.
is_zero [Wp.Lang.F]
isub [Cint]
isub [Wp.Cint]
iter [ProofEngine]
iter [Strategy]
iter [Tactical]
iter [Footprint]
Width-first full iterator.
iter [Wpo]
iter [Pcfg]
iter [Conditions]
Iterate only over the head steps of the sequence.
iter [Mstate]
iter [Sigs.Model]
Debug
iter [Sigs.Sigma]
Iterates over the chunks and associated variables already accessed so far in the environment.
iter [Letify.Sigma]
iter [Definitions]
iter [Splitter]
iter [Passive]
iter [Region]
iter [RefUsage]
iter [WpContext.Registry]
iter [Wp.Wpo]
iter [Wp.Strategy]
iter [Wp.Tactical]
iter [Hashtbl.S]
iter [Wp.Pcfg]
iter [Wp.Conditions]
Iterate only over the head steps of the sequence.
iter [Wp.Mstate]
iter [Wp.Sigs.Model]
Debug
iter [Wp.Sigs.Sigma]
Iterates over the chunks and associated variables already accessed so far in the environment.
iter [Wp.Definitions]
iter [Wp.Splitter]
iter [Wp.Passive]
iter [Wp.WpContext.Registry]
iter [Wp.RefUsage]
iter [Set.S]
iter f s applies f in turn to all elements of s.
iter [Map.S]
iter f m applies f to all bindings in map m.
iter2 [Sigs.Sigma]
Same as iter for both environments.
iter2 [Wp.Sigs.Sigma]
Same as iter for both environments.
iter_composer [Tactical]
iter_composer [Wp.Tactical]
iter_consequence_literals [Lang]
iter_consequence_literals assume_from_litteral hypothesis applies the function assume_from_litteral on literals that are a consequence of the hypothesis (i.e.
iter_consequence_literals [Wp.Lang]
iter_consequence_literals assume_from_litteral hypothesis applies the function assume_from_litteral on literals that are a consequence of the hypothesis (i.e.
iter_copies [Region]
iter_deref [Region]
iter_edges [Cil2cfg]
iter_fct [Wp_parameters]
iter_fct [Wp.Wp_parameters]
iter_fusion [Region]
iter_ip [VC]
iter_ip [Wp.VC]
iter_kf [VC]
iter_kf [Wp_parameters]
iter_kf [Wp.VC]
iter_kf [Wp.Wp_parameters]
iter_lemmas [LogicUsage]
iter_lemmas [Wp.LogicUsage]
iter_names [Region]
iter_nodes [Cil2cfg]
iter_offset [Region]
iter_on_goals [Wpo]
Dynamically exported.
iter_on_goals [Wp.Wpo]
Dynamically exported.
iter_read [Region]
iter_session [Register]
iter_shift [Region]
iter_sorted [WpContext.Registry]
iter_sorted [Wp.WpContext.Registry]
iter_strings [Region]
iter_vars [Region]
iter_wp [Wp_parameters]
iter_wp [Wp.Wp_parameters]
iter_write [Region]

J
join [Sigs.Sigma]
Make two environment pairwise equal via the passive form.
join [Passive]
join [Wp.Sigs.Sigma]
Make two environment pairwise equal via the passive form.
join [Wp.Passive]
json_of_param [ProofScript]
json_of_parameters [ProofScript]
json_of_result [ProofScript]
json_of_selection [ProofScript]
json_of_tactic [ProofScript]
jtactic [ProofScript]

K
key [Script]
kf_context [Wpo]
kf_context [Wp.Wpo]
kfailed [VCS]
kfailed [Wp.VCS]
kind_of_id [WpPropId]
get the 'kind' information.
kind_of_id [Wp.WpPropId]
get the 'kind' information.
kind_of_tau [LogicBuiltins]
kind_of_tau [Wp.LogicBuiltins]
ko_status [GuiProver]

L
l_and [Cint]
l_and [Wp.Cint]
l_lsl [Cint]
l_lsl [Wp.Cint]
l_lsr [Cint]
l_lsr [Wp.Cint]
l_not [Cint]
l_not [Wp.Cint]
l_or [Cint]
l_or [Wp.Cint]
l_xor [Cint]
l_xor [Wp.Cint]
label [Mcfg.S]
label [Wp.Mcfg.S]
label_of_prop_id [WpPropId]
Short description of the kind of PO
label_of_prop_id [Wp.WpPropId]
Short description of the kind of PO
labels_assert_after [NormAtLabels]
labels_assert_after [Wp.NormAtLabels]
labels_assert_before [NormAtLabels]
labels_assert_before [Wp.NormAtLabels]
labels_axiom [NormAtLabels]
labels_axiom [Wp.NormAtLabels]
labels_empty [NormAtLabels]
labels_empty [Wp.NormAtLabels]
labels_fct_assigns [NormAtLabels]
labels_fct_assigns [Wp.NormAtLabels]
labels_fct_post [NormAtLabels]
labels_fct_post [Wp.NormAtLabels]
labels_fct_pre [NormAtLabels]
labels_fct_pre [Wp.NormAtLabels]
labels_loop [NormAtLabels]
labels_loop [Wp.NormAtLabels]
labels_predicate [NormAtLabels]
labels_predicate [Wp.NormAtLabels]
labels_stmt_assigns [NormAtLabels]
labels_stmt_assigns [Wp.NormAtLabels]
labels_stmt_post [NormAtLabels]
labels_stmt_post [Wp.NormAtLabels]
labels_stmt_pre [NormAtLabels]
labels_stmt_pre [Wp.NormAtLabels]
last [MemLoader.Model]
launch [Register]
lc_closed [Lang.F]
lc_closed [Wp.Lang.F]
lc_iter [Lang.F]
lc_iter [Wp.Lang.F]
ldomain [Cvalues]
lemma [Auto]
lemma [LogicCompiler.Make]
lemma [Conditions]
Performs existential, universal and hypotheses introductions
lemma [Sigs.LogicSemantics]
Compile a lemma definition.
lemma [Wp.Auto]
lemma [Wp.LogicCompiler.Make]
lemma [Wp.Conditions]
Performs existential, universal and hypotheses introductions
lemma [Wp.Sigs.LogicSemantics]
Compile a lemma definition.
lemma_id [Lang]
lemma_id [Wp.Lang]
length [Splitter]
length [Hashtbl.S]
length [Wp.Splitter]
lfun [Repr]
lfun [Wp.Repr]
lift [Vset]
lift [Lang.F]
lift [Wp.Vset]
lift [Wp.Lang.F]
lift_add [Vset]
lift_add [Wp.Vset]
lift_sub [Vset]
lift_sub [Wp.Vset]
list [Conditions]
Same domain than iter.
list [Wp.Conditions]
Same domain than iter.
literal [Sigs.Model]
Return the memory location of a constant string, the id is a unique identifier.
literal [Wp.Sigs.Model]
Return the memory location of a constant string, the id is a unique identifier.
load [ProofSession]
load [MemLoader.Make]
load [Sigs.Model]
Return the value of the object of the given type at the given location in the given memory state.
load [Cvalues.Logic]
load [Wp.Sigs.Model]
Return the value of the object of the given type at the given location in the given memory state.
load_driver [Driver]
Memoized loading of drivers according to current WP options.
load_driver [Wp.Driver]
Memoized loading of drivers according to current WP options.
load_float [MemLoader.Model]
load_int [MemLoader.Model]
load_pointer [MemLoader.Model]
loadvalue [MemLoader.Make]
loc [Cvalues.Logic]
loc [Splitter]
loc [Wp.Splitter]
loc_diff [Sigs.Model]
Compute the length in bytes between two memory locations
loc_diff [Wp.Sigs.Model]
Compute the length in bytes between two memory locations
loc_eq [Sigs.Model]
loc_eq [Wp.Sigs.Model]
loc_leq [Sigs.Model]
Memory location comparisons
loc_leq [Wp.Sigs.Model]
Memory location comparisons
loc_lt [Sigs.Model]
loc_lt [Wp.Sigs.Model]
loc_neq [Sigs.Model]
loc_neq [Wp.Sigs.Model]
loc_of_exp [Sigs.CodeSemantics]
Compile an expression as a location.
loc_of_exp [Wp.Sigs.CodeSemantics]
Compile an expression as a location.
loc_of_int [Sigs.Model]
Cast a term representing an absolute memory address (to some c_object) given as an integer, into an abstract memory location.
loc_of_int [Wp.Sigs.Model]
Cast a term representing an absolute memory address (to some c_object) given as an integer, into an abstract memory location.
loc_of_term [Sigs.LogicSemantics]
Same as term above but expects a single loc or a single pointer value.
loc_of_term [Wp.Sigs.LogicSemantics]
Same as term above but expects a single loc or a single pointer value.
local [LogicCompiler.Make]
local [Sigs.LogicSemantics]
Make a local frame reusing the current pool and gamma.
local [Lang]
local [Wp.LogicCompiler.Make]
local [Wp.Sigs.LogicSemantics]
Make a local frame reusing the current pool and gamma.
local [Wp.Lang]
locate [Footprint]
Locate the occurrence of select footprint inside a term.
location [ProverTask]
location [Wp.ProverTask]
logic [LogicCompiler.Make]
logic [LogicBuiltins]
logic [Wp.LogicCompiler.Make]
logic [Wp.LogicBuiltins]
logic_constant [Cvalues]
logic_id [Lang]
logic_id [Wp.Lang]
logic_info [LogicCompiler.Make]
logic_info [Wp.LogicCompiler.Make]
logic_lemma [LogicUsage]
logic_lemma [Wp.LogicUsage]
logic_var [LogicCompiler.Make]
logic_var [Wp.LogicCompiler.Make]
lookup [Strategy]
lookup [Tactical]
lookup [Footprint]
Retrieve back the k-th occurrence of a footprint inside a term.
lookup [Mstate]
lookup [Sigs.Model]
Try to interpret a term as an in-memory operation located at this program point.
lookup [LogicBuiltins]
lookup [Clabels]
lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.
lookup [Wp.Strategy]
lookup [Wp.Tactical]
lookup [Wp.Mstate]
lookup [Wp.Sigs.Model]
Try to interpret a term as an in-memory operation located at this program point.
lookup [Wp.LogicBuiltins]
lookup [Wp.Clabels]
lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.
loop_current [Clabels]
loop_current [Wp.Clabels]
loop_entry [Mcfg.S]
loop_entry [Clabels]
loop_entry [Wp.Mcfg.S]
loop_entry [Wp.Clabels]
loop_step [Mcfg.S]
loop_step [Wp.Mcfg.S]
loopcurrent [Clabels]
loopcurrent [Wp.Clabels]
loopentry [Clabels]
loopentry [Wp.Clabels]
lval [Sigs.LogicSemantics]
Compile a term l-value into a (typed) abstract location
lval [Sigs.CodeSemantics]
Evaluate the left-value on the given memory state.
lval [Wp.Sigs.LogicSemantics]
Compile a term l-value into a (typed) abstract location
lval [Wp.Sigs.CodeSemantics]
Evaluate the left-value on the given memory state.

M
main [Register]
main [ProofEngine]
make [GuiNavigator]
make [Strategy]
make [Wpo.GOAL]
make [Wp.Wpo.GOAL]
make [Wp.Strategy]
make_output_dir [Wp_parameters]
make_output_dir [Wp.Wp_parameters]
make_type [Datatype.Hashtbl]
map [Cvalues.Logic]
map [Vset]
map [Splitter]
map [Wp.Vset]
map [Wp.Splitter]
map [Set.S]
map f s is the set whose elements are f a0,f a1...
map [Map.S]
map f m returns a map with same domain as m, where the associated value a of all bindings of m has been replaced by the result of the application of f to a.
map_condition [Conditions]
Rewrite all root predicates in condition
map_condition [Wp.Conditions]
Rewrite all root predicates in condition
map_l2t [Cvalues.Logic]
map_loc [Cvalues.Logic]
map_logic [Cvalues]
map_opp [Cvalues.Logic]
map_opp [Vset]
map_opp [Wp.Vset]
map_sequence [Conditions]
Rewrite all root predicates in sequence
map_sequence [Wp.Conditions]
Rewrite all root predicates in sequence
map_sequent [Conditions]
Rewrite all root predocates in hypotheses and goal
map_sequent [Wp.Conditions]
Rewrite all root predocates in hypotheses and goal
map_sloc [Cvalues]
map_step [Conditions]
Rewrite all root predicates in step
map_step [Wp.Conditions]
Rewrite all root predicates in step
map_t2l [Cvalues.Logic]
map_value [Cvalues]
mapi [Tactical]
mapi [Wp.Tactical]
mapi [Map.S]
Same as Map.S.map, but the function receives as arguments both the key and the associated value for each binding of the map.
mark_e [Lang.F]
mark_e [Wp.Lang.F]
mark_p [Lang.F]
Returns a list of terms to be shared among all shared or marked subterms.
mark_p [Wp.Lang.F]
Returns a list of terms to be shared among all shared or marked subterms.
marker [Lang.F]
marker [Wp.Lang.F]
mask_simplifier [Cint]
mask_simplifier [Wp.Cint]
matches [Footprint]
Head match
matrix [Definitions]
matrix [Wp.Definitions]
max_binding [Map.S]
Same as Map.S.min_binding, but returns the largest binding of the given map.
max_binding_opt [Map.S]
Same as Map.S.min_binding_opt, but returns the largest binding of the given map.
max_elt [Set.S]
Same as Set.S.min_elt, but returns the largest element of the given set.
max_elt_opt [Set.S]
Same as Set.S.min_elt_opt, but returns the largest element of the given set.
mem [Sigs.Sigma]
Whether a chunk has been assigned.
mem [Layout.Chunk]
mem [WpContext.Generator]
mem [WpContext.Registry]
mem [Clabels]
mem [Wprop.Indexed2]
mem [Wprop.Indexed]
mem [Hashtbl.S]
mem [Wp.Sigs.Sigma]
Whether a chunk has been assigned.
mem [Wp.WpContext.Generator]
mem [Wp.WpContext.Registry]
mem [Set.S]
mem x s tests whether x belongs to the set s.
mem [Map.S]
mem x m returns true if m contains a binding for x, and false otherwise.
mem [Wp.Clabels]
mem [Parameter_sig.Set]
Does the given element belong to the set?
mem_at [LogicCompiler.Make]
mem_at [Sigs.LogicSemantics]
Returns the memory state at the requested label.
mem_at [Wp.LogicCompiler.Make]
mem_at [Wp.Sigs.LogicSemantics]
Returns the memory state at the requested label.
mem_at_frame [LogicCompiler.Make]
mem_at_frame [Sigs.LogicSemantics]
Get the memory environment at the given label.
mem_at_frame [Wp.LogicCompiler.Make]
mem_at_frame [Wp.Sigs.LogicSemantics]
Get the memory environment at the given label.
mem_builtin_type [Lang]
mem_builtin_type [Wp.Lang]
mem_frame [LogicCompiler.Make]
mem_frame [Sigs.LogicSemantics]
Same as mem_at_frame but for the current frame.
mem_frame [Wp.LogicCompiler.Make]
mem_frame [Wp.Sigs.LogicSemantics]
Same as mem_at_frame but for the current frame.
member [Vset]
member [Wp.Vset]
memoize [WpContext.Registry]
with circularity protection
memoize [Wp.WpContext.Registry]
with circularity protection
merge [VCS]
merge [Conditions]
Performs a diff-based disjunction, introducing If-Then-Else or Either branches when possible.
merge [Sigs.Sigma]
Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins.
merge [Letify.Defs]
merge [Splitter]
merge [Matrix]
merge [Mcfg.S]
merge [Layout.Pack]
merge [Layout.Flat]
merge [Layout.RW]
merge [Layout.Root]
merge [Layout.Cluster]
merge [Layout.Overlay]
merge [Layout.Matrix]
merge [Layout.Value]
merge [Layout.Usage]
merge [Layout.Alias]
merge [Wp.VCS]
merge [Wp.Conditions]
Performs a diff-based disjunction, introducing If-Then-Else or Either branches when possible.
merge [Wp.Sigs.Sigma]
Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins.
merge [Wp.Splitter]
merge [Wp.Mcfg.S]
merge [Map.S]
merge f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.
merge_all [Splitter]
merge_all [Wp.Splitter]
merge_assign_info [WpPropId]
merge_assign_info [Wp.WpPropId]
merge_list [Sigs.Sigma]
Same than Sigs.Sigma.merge but for a list of sigmas.
merge_list [Wp.Sigs.Sigma]
Same than Wp.Sigs.Sigma.merge but for a list of sigmas.
meta [CfgCompiler.Cfg]
Attach meta informations to a node.
meta [Wp.CfgCompiler.Cfg]
Attach meta informations to a node.
min_binding [Map.S]
Return the smallest binding of the given map (with respect to the Ord.compare ordering), or raise Not_found if the map is empty.
min_binding_opt [Map.S]
Return the smallest binding of the given map (with respect to the Ord.compare ordering), or None if the map is empty.
min_elt [Set.S]
Return the smallest element of the given set (with respect to the Ord.compare ordering), or raise Not_found if the set is empty.
min_elt_opt [Set.S]
Return the smallest element of the given set (with respect to the Ord.compare ordering), or None if the set is empty.
missing_guards [WpRTE]
Returns true if RTE annotations should be generated for the given function and model (and are not generated yet).
mk_asm_assigns_desc [WpPropId]
mk_asm_assigns_desc [Wp.WpPropId]
mk_assert_id [WpPropId]
mk_assert_id [Wp.WpPropId]
mk_assigns_info [WpPropId]
mk_assigns_info [Wp.WpPropId]
mk_axiom_info [WpPropId]
mk_axiom_info [Wp.WpPropId]
mk_bhv_from_id [WpPropId]
\from property of function or statement behavior assigns.
mk_bhv_from_id [Wp.WpPropId]
\from property of function or statement behavior assigns.
mk_call_pre_id [WpPropId]
mk_call_pre_id called_kf s_call called_pre
mk_call_pre_id [Wp.WpPropId]
mk_call_pre_id called_kf s_call called_pre
mk_check [WpPropId]
mk_check [Wp.WpPropId]
mk_code_annot_ids [WpPropId]
mk_code_annot_ids [Wp.WpPropId]
mk_compl_bhv_id [WpPropId]
complete behaviors property.
mk_compl_bhv_id [Wp.WpPropId]
complete behaviors property.
mk_decrease_id [WpPropId]
mk_decrease_id [Wp.WpPropId]
mk_disj_bhv_id [WpPropId]
disjoint behaviors property.
mk_disj_bhv_id [Wp.WpPropId]
disjoint behaviors property.
mk_env [LogicCompiler.Make]
mk_env [Sigs.LogicSemantics]
Create a new environment.
mk_env [Wp.LogicCompiler.Make]
mk_env [Wp.Sigs.LogicSemantics]
Create a new environment.
mk_fct_assigns_id [WpPropId]
function assigns
mk_fct_assigns_id [Wp.WpPropId]
function assigns
mk_fct_from_id [WpPropId]
\from property of function behavior assigns.
mk_fct_from_id [Wp.WpPropId]
\from property of function behavior assigns.
mk_fct_post_id [WpPropId]
mk_fct_post_id [Wp.WpPropId]
mk_frame [LogicCompiler.Make]
mk_frame [Sigs.LogicSemantics]
Full featured constructor for frames, with fresh pool and gamma.
mk_frame [Wp.LogicCompiler.Make]
mk_frame [Wp.Sigs.LogicSemantics]
Full featured constructor for frames, with fresh pool and gamma.
mk_init_assigns [WpPropId]
mk_init_assigns [Wp.WpPropId]
mk_inv_hyp_id [WpPropId]
Invariant used as hypothesis
mk_inv_hyp_id [Wp.WpPropId]
Invariant used as hypothesis
mk_kf_any_assigns_info [WpPropId]
mk_kf_any_assigns_info [Wp.WpPropId]
mk_kf_assigns_desc [WpPropId]
mk_kf_assigns_desc [Wp.WpPropId]
mk_lemma_id [WpPropId]
axiom identification
mk_lemma_id [Wp.WpPropId]
axiom identification
mk_loop_any_assigns_info [WpPropId]
mk_loop_any_assigns_info [Wp.WpPropId]
mk_loop_assigns_desc [WpPropId]
mk_loop_assigns_desc [Wp.WpPropId]
mk_loop_assigns_id [WpPropId]
mk_loop_assigns_id [Wp.WpPropId]
mk_loop_from_id [WpPropId]
\from property of loop assigns.
mk_loop_from_id [Wp.WpPropId]
\from property of loop assigns.
mk_loop_inv_id [WpPropId]
Invariant establishment and preservation
mk_loop_inv_id [Wp.WpPropId]
Invariant establishment and preservation
mk_part [WpPropId]
mk_part pid (k, n) build the identification for the k/n part of pid.
mk_part [Wp.WpPropId]
mk_part pid (k, n) build the identification for the k/n part of pid.
mk_pre_id [WpPropId]
mk_pre_id [Wp.WpPropId]
mk_pred_info [WpPropId]
mk_pred_info [Wp.WpPropId]
mk_property [WpPropId]
mk_property [Wp.WpPropId]
mk_smoke [WpPropId]
mk_smoke [Wp.WpPropId]
mk_stmt_any_assigns_info [WpPropId]
mk_stmt_any_assigns_info [Wp.WpPropId]
mk_stmt_assigns_desc [WpPropId]
mk_stmt_assigns_desc [Wp.WpPropId]
mk_stmt_assigns_id [WpPropId]
mk_stmt_assigns_id [Wp.WpPropId]
mk_stmt_post_id [WpPropId]
mk_stmt_post_id [Wp.WpPropId]
mk_strategy [WpStrategy]
mk_var_decr_id [WpPropId]
Variant decrease
mk_var_decr_id [Wp.WpPropId]
Variant decrease
mk_var_pos_id [WpPropId]
Variant positive
mk_var_pos_id [Wp.WpPropId]
Variant positive
mk_variant_properties [WpStrategy]
mode_of_prover_name [VCS]
mode_of_prover_name [Wp.VCS]
move_at [LogicCompiler.Make]
move_at [Sigs.LogicSemantics]
Move the compilation environment to the specified Here memory state.
move_at [Wp.LogicCompiler.Make]
move_at [Wp.Sigs.LogicSemantics]
Move the compilation environment to the specified Here memory state.

N
name [MemLoader.Model]
name [WpContext.IData]
name [WpContext.Data]
name [WpContext.Entries]
name [Context]
name [Why3Provers]
name [Clabels]
name [Wp_error]
name [Wp.WpContext.IData]
name [Wp.WpContext.Data]
name [Wp.WpContext.Entries]
name [Wp.Context]
name [Wp.Clabels]
name_of_field [Lang]
name_of_field [Wp.Lang]
name_of_lfun [Lang]
name_of_lfun [Wp.Lang]
name_of_prover [VCS]
name_of_prover [Wp.VCS]
named [TacLemma]
natural_id [Matrix]
name for elements in NATURAL
nearest_elt_ge [Datatype.Set]
nearest_elt_le [Datatype.Set]
negate [Cvalues]
new_driver [LogicBuiltins]
Creates a configured driver from an existing one.
new_driver [Wp.LogicBuiltins]
Creates a configured driver from an existing one.
new_env [Mcfg.S]
optionally init env with user logic variables
new_env [Wp.Mcfg.S]
optionally init env with user logic variables
new_gamma [Lang]
new_gamma [Wp.Lang]
new_pool [Lang]
new_pool [Wp.Lang]
next [Pcfg]
next [Clabels]
next [Wp.Pcfg]
next [Wp.Clabels]
nil [Conditions]
Same as empty
nil [Wp.Conditions]
Same as empty
no_infinite_array [Ctypes]
no_infinite_array [Wp.Ctypes]
no_result [VCS]
no_result [Wp.VCS]
no_status [GuiProver]
node [CfgCompiler.Cfg]
fresh node
node [Wp.CfgCompiler.Cfg]
fresh node
node_context [ProofEngine]
node_stmt_opt [Cil2cfg]
node_type [Cil2cfg]
nodes [CfgCompiler.Cfg.P]
nodes [Wp.CfgCompiler.Cfg.P]
noid [Region]
nop [CfgCompiler.Cfg]
Structurally, nop is an empty execution trace.
nop [Wp.CfgCompiler.Cfg]
Structurally, nop is an empty execution trace.
normalize [WpStrategy]
not [Lang.N]
not [Wp.Lang.N]
not_equal_obj [Sigs.CodeSemantics]
Same as not_equal_typ with an object type.
not_equal_obj [Wp.Sigs.CodeSemantics]
Same as not_equal_typ with an object type.
not_equal_typ [Sigs.CodeSemantics]
Computes the value of (a==b) provided both a and b are values with the given type.
not_equal_typ [Wp.Sigs.CodeSemantics]
Computes the value of (a==b) provided both a and b are values with the given type.
not_yet_implemented [Wp_error]
null [Sigs.Model]
Return the location of the null pointer
null [Cvalues]
test for null pointer value
null [Wp.Sigs.Model]
Return the location of the null pointer
num_of_bhv_from [WpPropId]
num_of_bhv_from [Wp.WpPropId]

O
object_of [Ctypes]
object_of [Wp.Ctypes]
object_of_array_elem [Ctypes]
object_of_array_elem [Wp.Ctypes]
object_of_logic_pointed [Ctypes]
object_of_logic_pointed [Wp.Ctypes]
object_of_logic_type [Ctypes]
object_of_logic_type [Wp.Ctypes]
object_of_pointed [Ctypes]
object_of_pointed [Wp.Ctypes]
occurs [Conditions]
occurs [Sigs.LogicSemantics]
Member of vars.
occurs [Sigs.Model]
Test if a location depend on a given logic variable
occurs [Vset]
occurs [Lang.F]
occurs [Wp.Conditions]
occurs [Wp.Sigs.LogicSemantics]
Member of vars.
occurs [Wp.Sigs.Model]
Test if a location depend on a given logic variable
occurs [Wp.Vset]
occurs [Wp.Lang.F]
occurs_e [Strategy]
occurs_e [Wp.Strategy]
occurs_p [Strategy]
occurs_p [Wp.Strategy]
occurs_q [Strategy]
occurs_q [Wp.Strategy]
occurs_x [Strategy]
occurs_x [Wp.Strategy]
occurs_y [Strategy]
occurs_y [Wp.Strategy]
occursp [Lang.F]
occursp [Wp.Lang.F]
of_array [Matrix]
of_behavior [RegionAnnot]
of_class [Region]
of_cstring [Region]
of_cvar [Region]
of_extension [RegionAnnot]
of_integer [Cint]
of_integer [Wp.Cint]
of_list [Set.S]
of_list l creates a set from a list of elements.
of_logic [Clabels]
Assumes the logic label only comes from normalized or non-ambiguous labels.
of_logic [Wp.Clabels]
Assumes the logic label only comes from normalized or non-ambiguous labels.
of_name [Region]
of_null [Region]
of_pred [Definitions.Trigger]
of_pred [Wp.Definitions.Trigger]
of_real [Cint]
of_real [Wp.Cint]
of_region_pointer [MemLoader.Model]
of_return [Region]
of_term [Definitions.Trigger]
of_term [Wp.Definitions.Trigger]
off [Parameter_sig.Bool]
Set the boolean to false.
ok_status [GuiProver]
old [Clabels]
old [Wp.Clabels]
on [Parameter_sig.Bool]
Set the boolean to true.
on_context [WpContext]
on_context [Wp.WpContext]
on_reload [GuiPanel]
on_remove [Wpo]
on_remove [Wp.Wpo]
on_update [GuiPanel]
once [Footprint]
Width-first once iterator.
once [Layout.Overlay]
open_file [Script]
ordered [Vset]
- limit: result when either parameter is None strict: if true, comparison is < instead of <=
ordered [Wp.Vset]
- limit: result when either parameter is None strict: if true, comparison is < instead of <=
output_dot [CfgCompiler.Cfg]
output_dot [Wp.CfgCompiler.Cfg]
overflow [TacOverflow]
overlap [Layout.Range]

P
p_addr_le [MemMemory]
p_addr_lt [MemMemory]
p_all [Lang.F]
p_all [Wp.Lang.F]
p_and [Lang.F]
p_and [Wp.Lang.F]
p_any [Lang.F]
p_any [Wp.Lang.F]
p_apply [Letify.Sigma]
p_apply [Letify.Ground]
p_bind [Lang.F]
p_bind [Wp.Lang.F]
p_bits [Ctypes]
pointer size in bits
p_bits [Wp.Ctypes]
pointer size in bits
p_bool [Lang.F]
p_bool [Wp.Lang.F]
p_bools [Lang.F]
p_bools [Wp.Lang.F]
p_bytes [Ctypes]
pointer size in bits
p_bytes [Wp.Ctypes]
pointer size in bits
p_call [Lang.F]
p_call [Wp.Lang.F]
p_close [Lang.F]
Quantify over (sorted) free variables
p_close [Wp.Lang.F]
Quantify over (sorted) free variables
p_conj [Lang.F]
p_conj [Wp.Lang.F]
p_disj [Lang.F]
p_disj [Wp.Lang.F]
p_eqmem [MemMemory]
p_equal [Lang.F]
p_equal [Wp.Lang.F]
p_equals [Lang.F]
p_equals [Wp.Lang.F]
p_equiv [Lang.F]
p_equiv [Wp.Lang.F]
p_exists [Lang.F]
p_exists [Wp.Lang.F]
p_expr [Lang.F]
p_expr [Wp.Lang.F]
p_false [Lang.F]
p_false [Wp.Lang.F]
p_float [ProverTask]
Float group pattern \([0-9.]+\)
p_float [Wp.ProverTask]
Float group pattern \([0-9.]+\)
p_forall [Lang.F]
p_forall [Wp.Lang.F]
p_framed [MemMemory]
p_group [ProverTask]
Put pattern in group \(p\)
p_group [Wp.ProverTask]
Put pattern in group \(p\)
p_hyps [Lang.F]
p_hyps [Wp.Lang.F]
p_if [Lang.F]
p_if [Wp.Lang.F]
p_imply [Lang.F]
p_imply [Wp.Lang.F]
p_included [MemMemory]
p_int [ProverTask]
Int group pattern \([0-9]+\)
p_int [Wp.ProverTask]
Int group pattern \([0-9]+\)
p_invalid [MemMemory]
p_leq [Lang.F]
p_leq [Wp.Lang.F]
p_linked [MemMemory]
p_lt [Lang.F]
p_lt [Wp.Lang.F]
p_name [RegionAnnot]
p_neq [Lang.F]
p_neq [Wp.Lang.F]
p_not [Lang.F]
p_not [Wp.Lang.F]
p_or [Lang.F]
p_or [Wp.Lang.F]
p_positive [Lang.F]
p_positive [Wp.Lang.F]
p_sconst [MemMemory]
p_separated [MemMemory]
p_string [ProverTask]
String group pattern "\(...\)"
p_string [Wp.ProverTask]
String group pattern "\(...\)"
p_subst [Lang.F]
p_subst [Lang]
uses current pool
p_subst [Wp.Lang.F]
p_subst [Wp.Lang]
uses current pool
p_subst_var [Lang.F]
p_subst_var [Wp.Lang.F]
p_true [Lang.F]
p_true [Wp.Lang.F]
p_until_space [ProverTask]
No space group pattern "\\(^ \t\n*\\)"
p_until_space [Wp.ProverTask]
No space group pattern "\\(^ \t\n*\\)"
p_valid_obj [MemMemory]
p_valid_rd [MemMemory]
p_valid_rw [MemMemory]
p_vars [Lang.F]
Sorted
p_vars [Wp.Lang.F]
Sorted
parallel [StmtSemantics.Make]
Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp.
parallel [Wp.StmtSemantics.Make]
Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp.
param [MemVar.VarUsage]
Memory Model Hypotheses
param [Wp.MemVar.VarUsage]
Memory Model Hypotheses
param_of_json [ProofScript]
parameters [Lang]
definitions
parameters [Wp.Lang]
definitions
parameters_of_json [ProofScript]
params [TacInstance]
parasite [Conditions]
parasite [Wp.Conditions]
parent [ProofEngine]
parse [Factory]
Apply specifications to default setup.
parse [Wp.Factory]
Apply specifications to default setup.
parse_coqproof [Proof]
parse_coqproof f parses a coq-file f and fetch the first proof.
partition [Set.S]
partition p s returns a pair of sets (s1, s2), where s1 is the set of all the elements of s that satisfy the predicate p, and s2 is the set of all the elements of s that do not satisfy p.
partition [Map.S]
partition p m returns a pair of maps (m1, m2), where m1 contains all the bindings of s that satisfy the predicate p, and m2 is the map with all the bindings of s that do not satisfy p.
parts_of_id [WpPropId]
get the 'part' information.
parts_of_id [Wp.WpPropId]
get the 'part' information.
pattern [Footprint]
Generate head footprint up to size
pending [ProofEngine]
0 means proved
pending [ProofScript]
pending goals
pending_any [ProofScript]
minimum of pending goals
plain [Cvalues]
pointed [Layout.Value]
pointer [MemTyped]
pointer [Lang]
type of pointers
pointer [Wp.MemTyped]
pointer [Wp.Lang]
type of pointers
pointer_loc [Sigs.Model]
Interpret an address value (a pointer) as an abstract location.
pointer_loc [Wp.Sigs.Model]
Interpret an address value (a pointer) as an abstract location.
pointer_val [Sigs.Model]
Return the adress value (a pointer) of an abstract location.
pointer_val [Wp.Sigs.Model]
Return the adress value (a pointer) of an abstract location.
poly [Lang]
polymorphism
poly [Wp.Lang]
polymorphism
pool [ProofEngine]
pool [Plang]
pool [Lang.F]
pool [Wp.Plang]
pool [Wp.Lang.F]
pop [Context]
pop [Wp.Context]
post [Clabels]
post [Wp.Clabels]
pp [CfgCompiler.Cfg.Node]
pp [Wp.CfgCompiler.Cfg.Node]
pp_acs [Cvalues]
pp_annots [WpStrategy]
pp_assign_info [WpPropId]
pp_assign_info [Wp.WpPropId]
pp_assigns [Wp_error]
pp_assigns_desc [WpPropId]
pp_assigns_desc [Wp.WpPropId]
pp_axiom_info [WpPropId]
pp_axiom_info [Wp.WpPropId]
pp_axiomatics [Wpo]
pp_axiomatics [Wp.Wpo]
pp_bound [Cvalues]
pp_bound [Vset]
pp_bound [Wp.Vset]
pp_call_type [Cil2cfg]
pp_calls [Dyncall]
pp_chain [Layout.Offset]
pp_clause [Tactical]
Debug only
pp_clause [MemoryContext]
pp_clause [Wp.Tactical]
Debug only
pp_clause [Wp.MemoryContext]
pp_cluster [Definitions]
pp_cluster [Wp.Definitions]
pp_depend [Wpo]
pp_depend [Wp.Wpo]
pp_dependencies [Wpo]
pp_dependencies [Wp.Wpo]
pp_dependency [Wpo]
pp_dependency [Wp.Wpo]
pp_edge [Cil2cfg]
pp_epred [Lang.F]
pp_epred [Wp.Lang.F]
pp_eterm [Lang.F]
pp_eterm [Wp.Lang.F]
pp_file [ProverTask]
pp_file [Wp.ProverTask]
pp_float [Ctypes]
pp_float [Wp.Ctypes]
pp_frame [LogicCompiler.Make]
pp_frame [Sigs.LogicSemantics]
pp_frame [Wp.LogicCompiler.Make]
pp_frame [Wp.Sigs.LogicSemantics]
pp_function [Wpo]
pp_function [Wp.Wpo]
pp_goal [Wpo]
pp_goal [Wp.Wpo]
pp_goal_flow [Wpo]
pp_goal_flow [Wp.Wpo]
pp_index [Wpo]
pp_index [Wp.Wpo]
pp_info_of_strategy [WpStrategy]
pp_int [Ctypes]
pp_int [Wp.Ctypes]
pp_logfile [Wpo]
pp_logfile [Wp.Wpo]
pp_logic [Cvalues]
pp_logic_label [Wp_error]
pp_mode [VCS]
pp_mode [Wp.VCS]
pp_node [Cil2cfg]
pp_node_type [Cil2cfg]
pp_object [Ctypes]
pp_object [Wp.Ctypes]
pp_param [MemoryContext]
pp_param [Wp.MemoryContext]
pp_pred [Lang.F]
pp_pred [Wp.Lang.F]
pp_pred_info [WpPropId]
pp_pred_info [Wp.WpPropId]
pp_pred_of_pred_info [WpPropId]
pp_pred_of_pred_info [Wp.WpPropId]
pp_profile [LogicUsage]
pp_profile [Wp.LogicUsage]
pp_propid [WpPropId]
Print unique id of prop_id
pp_propid [Wp.WpPropId]
Print unique id of prop_id
pp_prover [VCS]
pp_prover [Wp.VCS]
pp_region [Cvalues]
pp_result [VCS]
pp_result [Wp.VCS]
pp_result_perf [VCS]
pp_result_perf [Wp.VCS]
pp_rloc [Cvalues]
pp_script [ProofSession]
pp_script_for [ProofSession]
pp_selection [Tactical]
Debug only
pp_selection [Wp.Tactical]
Debug only
pp_sloc [Cvalues]
pp_string_list [Wp_error]
pp_tau [Lang.F]
pp_tau [Wp.Lang.F]
pp_term [Lang.F]
pp_term [Wp.Lang.F]
pp_time [Rformat]
Pretty print time in hour, minutes, seconds, or milliseconds, as appropriate
pp_time_range [Rformat]
pp_title [Wpo]
pp_title [Wp.Wpo]
pp_value [Sigs.CodeSemantics]
pp_value [Cvalues]
pp_value [Wp.Sigs.CodeSemantics]
pp_var [Lang.F]
pp_var [Wp.Lang.F]
pp_vars [Lang.F]
pp_vars [Wp.Lang.F]
pp_vset [Vset]
pp_vset [Wp.Vset]
pp_warnings [Register]
pp_warnings [Wpo]
pp_warnings [Wp.Wpo]
pp_wp_parameters [Register]
pp_zone [MemoryContext]
pp_zone [Wp.MemoryContext]
pprepeat [Vlist]
pre [Clabels]
pre [Wp.Clabels]
pred [LogicCompiler.Make]
pred [Sigs.LogicSemantics]
Compile a predicate.
pred [Repr]
pred [Wp.LogicCompiler.Make]
pred [Wp.Sigs.LogicSemantics]
Compile a predicate.
pred [Wp.Repr]
pred_e [Cil2cfg]
pred_info_id [WpPropId]
pred_info_id [Wp.WpPropId]
preproc_annot [NormAtLabels]
preproc_annot [Wp.NormAtLabels]
preproc_assigns [NormAtLabels]
preproc_assigns [Wp.NormAtLabels]
pretty [ProofEngine]
pretty [Wpo.DISK]
pretty [CfgCompiler.Cfg.E]
pretty [CfgCompiler.Cfg.T]
pretty [CfgCompiler.Cfg.P]
pretty [Pcond]
pretty [Conditions]
pretty [Sigs.Model]
pretty printing of memory location
pretty [Sigs.Sigma]
For debugging purpose
pretty [Sigs.Chunk]
pretty [Letify.Sigma]
pretty [Letify.Ground]
pretty [Cstring]
pretty [Vlist]
pretty [Vset]
pretty [Splitter]
pretty [Passive]
pretty [Mcfg.S]
pretty [WpPropId]
pretty [RegionAnnot.Lpath]
pretty [Layout.Chunk]
pretty [Layout.Root]
pretty [Layout.Cluster]
pretty [Layout.Overlay]
pretty [Layout.Range]
pretty [Layout.Matrix]
pretty [Layout.Value]
pretty [Layout.Usage]
pretty [Layout.Alias]
pretty [Layout.Data]
pretty [WpContext.Key]
pretty [WpContext.Entries]
pretty [Warning]
pretty [Clabels]
pretty [Ctypes]
pretty [Rformat]
pretty [Wp.Wpo.DISK]
pretty [Wp.CfgCompiler.Cfg.E]
pretty [Wp.CfgCompiler.Cfg.T]
pretty [Wp.CfgCompiler.Cfg.P]
pretty [Wp.Pcond]
pretty [Wp.Conditions]
pretty [Wp.Sigs.Model]
pretty printing of memory location
pretty [Wp.Sigs.Sigma]
For debugging purpose
pretty [Wp.Sigs.Chunk]
pretty [Wp.Cstring]
pretty [Wp.Vset]
pretty [Wp.Splitter]
pretty [Wp.Passive]
pretty [Wp.WpContext.Key]
pretty [Wp.WpContext.Entries]
pretty [Wp.Warning]
pretty [Wp.Mcfg.S]
pretty [Wp.WpPropId]
pretty [Wp.Clabels]
pretty [Wp.Ctypes]
pretty_context [WpPropId]
pretty_context [Wp.WpPropId]
pretty_local [WpPropId]
pretty_local [Wp.WpPropId]
prev [Pcfg]
prev [Wp.Pcfg]
print [RefUsage]
print [Wp.RefUsage]
print_generated [Wp_parameters]
print the given file if the debugging category "print-generated" is set
print_generated [Wp.Wp_parameters]
print the given file if the debugging category "print-generated" is set
print_why3 [Why3Provers]
print_wp [Why3Provers]
promote [Ctypes]
promote [Wp.Ctypes]
proof [VC]
List of proof obligations computed for a given property.
proof [ProofEngine]
proof [Wp.VC]
List of proof obligations computed for a given property.
proof_context [LogicUsage]
Lemmas that are not in an axiomatic.
proof_context [Wp.LogicUsage]
Lemmas that are not in an axiomatic.
prop_id_keys [WpPropId]
prop_id_keys [Wp.WpPropId]
property [Wprop.Info]
property [Wprop.Indexed2]
property [Wprop.Indexed]
property_of_id [WpPropId]
returns the annotation which lead to the given PO.
property_of_id [Wp.WpPropId]
returns the annotation which lead to the given PO.
prove [VC]
Returns a ready-to-schedule task.
prove [ProverScript]
prove [Prover]
prove [ProverWhy3]
Return NoResult if it is already proved by Qed
prove [ProverCoq]
prove [ProverErgo]
prove [Wp.Prover]
prove [Wp.VC]
Returns a ready-to-schedule task.
proved [Register]
proved [ProofEngine]
prover_of_json [ProofScript]
prover_of_name [Wpo]
Dynamically exported.
prover_of_name [VCS]
prover_of_name [Wp.Wpo]
Dynamically exported.
prover_of_name [Wp.VCS]
provers [Register]
provers [Why3Provers]
provers_set [Why3Provers]
pruning [Conditions]
pruning [Wp.Conditions]
push [Context]
push [Wp.Context]

Q
qed_time [Wpo.GOAL]
qed_time [Wpo]
qed_time [Wp.Wpo.GOAL]
qed_time [Wp.Wpo]

R
range [Auto]
range [Tactical]
range [Vset]
range [Cint]
Dependent on model
range [Layout.Offset]
range [Wp.Auto]
range [Wp.Tactical]
range [Wp.Vset]
range [Wp.Cint]
Dependent on model
ranges [Auto.Range]
ranges [Wp.Auto.Range]
rdescr [Cvalues.Logic]
reached [WpReached]
memoized reached cfg for function
reads [CfgCompiler.Cfg.E]
reads [CfgCompiler.Cfg.T]
reads [CfgCompiler.Cfg.P]
reads [CfgCompiler.Cfg.C]
reads [Wp.CfgCompiler.Cfg.E]
reads [Wp.CfgCompiler.Cfg.T]
reads [Wp.CfgCompiler.Cfg.P]
reads [Wp.CfgCompiler.Cfg.C]
real_of_float [Cfloat]
real_of_float [Wp.Cfloat]
real_of_flt [Cfloat]
real_of_flt [Wp.Cfloat]
real_of_int [Cmath]
rebuild [Lang.For_export]
rebuild [Wp.Lang.For_export]
record [Lang]
record [Wp.Lang]
record_with [Lang.F]
record_with [Wp.Lang.F]
reduce [Wpo]
tries simplification
reduce [Wp.Wpo]
tries simplification
region [LogicCompiler.Make]
When ~unfold:true, decompose compound regions field by field
region [Sigs.LogicSemantics]
Compile a term representing a set of memory locations into an abstract region.
region [Cvalues.Logic]
region [Region]
region [Wp.LogicCompiler.Make]
When ~unfold:true, decompose compound regions field by field
region [Wp.Sigs.LogicSemantics]
Compile a term representing a set of memory locations into an abstract region.
register [GuiPanel]
register [Register]
register [Strategy]
register [Tactical]
register [MemMemory]
register [Pcfg]
register [RegionAnnot]
Auto when `-wp-region`
register [WpContext]
Model registration.
register [Context]
Register a global configure, to be executed once per project/ast.
register [Wp.Strategy]
register [Wp.Tactical]
register [Wp.Pcfg]
register [Wp.WpContext]
Model registration.
register [Wp.Context]
Register a global configure, to be executed once per project/ast.
release [Lang.F]
Empty local caches
release [Wp.Lang.F]
Empty local caches
reload [GuiPanel]
relocate [CfgCompiler.Cfg.E]
relocate [CfgCompiler.Cfg.T]
relocate [CfgCompiler.Cfg.P]
| relocate m' (create m p) | = | p{ } |
relocate [CfgCompiler.Cfg.C]
relocate [Wp.CfgCompiler.Cfg.E]
relocate [Wp.CfgCompiler.Cfg.T]
relocate [Wp.CfgCompiler.Cfg.P]
| relocate m' (create m p) | = | p{ } |
relocate [Wp.CfgCompiler.Cfg.C]
remove [VC]
remove [ProofEngine]
remove [ProofSession]
remove [Wpo]
remove [Cil2cfg.HEsig]
remove [WpContext.Generator]
remove [WpContext.Registry]
remove [Wp.Wpo]
remove [Wp.VC]
remove [Hashtbl.S]
remove [Wp.WpContext.Generator]
remove [Wp.WpContext.Registry]
remove [Set.S]
remove x s returns a set containing all elements of s, except x.
remove [Map.S]
remove x m returns a map containing the same bindings as m, except for x which is unbound in the returned map.
remove_chunks [Sigs.Sigma]
Return a copy of the environment where chunks in the footprint have been removed.
remove_chunks [Wp.Sigs.Sigma]
Return a copy of the environment where chunks in the footprint have been removed.
remove_for_altergo [Filter_axioms]
remove_for_why3 [Filter_axioms]
replace [Tactical]
replace [Conditions]
replace a step in the sequent, the one at the specified position.
replace [Cil2cfg.HEsig]
replace [Wp.Tactical]
replace [Hashtbl.S]
replace [Wp.Conditions]
replace a step in the sequent, the one at the specified position.
repr [Lang.F]
Constant time
repr [WpContext.MODEL]
repr [Wp.Lang.F]
Constant time
repr [Wp.WpContext.MODEL]
requires [MemoryContext]
Build the separation clause from a partition, including the clauses related to the pointer validity
requires [Wp.MemoryContext]
Build the separation clause from a partition, including the clauses related to the pointer validity
reset [ProofEngine]
reset [Wp_parameters]
reset [Hashtbl.S]
reset [Wp.Wp_parameters]
reshape [Layout.Cluster]
reshape [Layout.Compound]
resolve [Wpo.VC_Annot]
resolve [Wpo]
tries simplification and set result if valid
resolve [Wp.Wpo.VC_Annot]
resolve [Wp.Wpo]
tries simplification and set result if valid
result [VCS]
result [StmtSemantics.Make]
result [LogicCompiler.Make]
result [Sigs.LogicSemantics]
Result location of the current function in the current frame.
result [Sigs.CodeSemantics]
Value of an abstract result container.
result [Wp.VCS]
result [Wp.StmtSemantics.Make]
result [Wp.LogicCompiler.Make]
result [Wp.Sigs.LogicSemantics]
Result location of the current function in the current frame.
result [Wp.Sigs.CodeSemantics]
Value of an abstract result container.
result_of_json [ProofScript]
results [Register]
return [StmtSemantics.Make]
return [LogicCompiler.Make]
return [Sigs.LogicSemantics]
Result type of the current function in the current frame.
return [Sigs.CodeSemantics]
Return an expression with a given type.
return [Mcfg.S]
return [Wp.StmtSemantics.Make]
return [Wp.LogicCompiler.Make]
return [Wp.Sigs.LogicSemantics]
Result type of the current function in the current frame.
return [Wp.Sigs.CodeSemantics]
Return an expression with a given type.
return [Wp.Mcfg.S]
rewrite [Tactical]
For each pattern (descr,guard,src,tgt) replace src with tgt under condition guard, inserted in position at.
rewrite [Wp.Tactical]
For each pattern (descr,guard,src,tgt) replace src with tgt under condition guard, inserted in position at.
run [Register]
run_and_prove [GuiPanel]

S
s_bool [WpTac]
s_cnf_iff [WpTac]
s_cnf_ite [WpTac]
s_cnf_xor [WpTac]
s_dnf_iff [WpTac]
s_dnf_ite [WpTac]
s_dnf_xor [WpTac]
same_edge [Cil2cfg]
same_node [Cil2cfg]
sanitizer [Plang]
sanitizer [Wp.Plang]
save [ProverScript]
save [ProofSession]
saved [ProofEngine]
savescripts [Proof]
If necessary, dump the scripts database into the file specified by -wp-script f.
schedule [ProverTask]
schedule [Wp.ProverTask]
scheduled [Register]
scope [StmtSemantics.Make]
scope [Sigs.Model]
Manage the scope of variables.
scope [Mcfg.S]
scope [Wp.StmtSemantics.Make]
scope [Wp.Sigs.Model]
Manage the scope of variables.
scope [Wp.Mcfg.S]
script [ProofEngine]
script_for [Proof]
script_for_ide [Proof]
search [ProverScript]
search [ProverSearch]
search [TacLemma]
search [Tactical]
Search field.
search [Wp.Tactical]
Search field.
section [Definitions]
section [Wp.Definitions]
section_of_lemma [LogicUsage]
section_of_lemma [Wp.LogicUsage]
section_of_logic [LogicUsage]
section_of_logic [Wp.LogicUsage]
section_of_type [LogicUsage]
section_of_type [Wp.LogicUsage]
select [Letify.Split]
select_by_name [WpPropId]
test if the prop_id has to be selected for the asked name.
select_by_name [Wp.WpPropId]
test if the prop_id has to be selected for the asked name.
select_call_pre [WpPropId]
test if the prop_id has to be selected when we want to select the call precondition the the stmt call (None means all the call preconditions).
select_call_pre [Wp.WpPropId]
test if the prop_id has to be selected when we want to select the call precondition the the stmt call (None means all the call preconditions).
select_default [WpPropId]
test if the prop_id does not have a no_wp: in its name(s).
select_default [Wp.WpPropId]
test if the prop_id does not have a no_wp: in its name(s).
select_e [Strategy]
Lookup the first occurrence of term in the sequent and returns the associated selection.
select_e [Wp.Strategy]
Lookup the first occurrence of term in the sequent and returns the associated selection.
select_p [Strategy]
Same as select_e but for a predicate.
select_p [Wp.Strategy]
Same as select_e but for a predicate.
selected [Tactical]
selected [Wp.Tactical]
selection_of_json [ProofScript]
selection_target [ProofScript]
selector [Tactical]
Unless specified, default is head option.
selector [Wp.Tactical]
Unless specified, default is head option.
self [Sigs.Chunk]
Chunk names, for pretty-printing.
self [Wp.Sigs.Chunk]
Chunk names, for pretty-printing.
separated [Auto]
separated [MemMemory]
separated [Sigs.Model]
Return the formula that tests if two segment are separated
separated [Cvalues.Logic]
separated [Wp.Auto]
separated [Wp.Sigs.Model]
Return the formula that tests if two segment are separated
seq_branch [Conditions]
Creates an If-Then-Else branch located at the provided stmt, if any.
seq_branch [Wp.Conditions]
Creates an If-Then-Else branch located at the provided stmt, if any.
sequence [Register]
sequence [StmtSemantics.Make]
Chain compiler by introducing fresh nodes between each element of the list.
sequence [Pcond]
sequence [Conditions]
sequence [Wp.StmtSemantics.Make]
Chain compiler by introducing fresh nodes between each element of the list.
sequence [Wp.Pcond]
sequence [Wp.Conditions]
server [VC]
Default number of parallel tasks is given by -wp-par command-line option.
server [ProverTask]
server [Wp.ProverTask]
server [Wp.VC]
Default number of parallel tasks is given by -wp-par command-line option.
session [Register]
set [Tactical.Fmap]
set [StmtSemantics.Make]
set [MemoryContext]
set [Context]
Define the current value.
set [Wp.Tactical.Fmap]
set [Wp.StmtSemantics.Make]
set [Wp.Context]
Define the current value.
set [Wp.MemoryContext]
set_at_frame [LogicCompiler.Make]
set_at_frame [Sigs.LogicSemantics]
Update a frame with a specific environment for the given label.
set_at_frame [Wp.LogicCompiler.Make]
set_at_frame [Wp.Sigs.LogicSemantics]
Update a frame with a specific environment for the given label.
set_builtin [Lang.For_export]
set_builtin [Lang.F]
set_builtin [Wp.Lang.For_export]
set_builtin [Wp.Lang.F]
set_builtin' [Lang.For_export]
set_builtin' [Wp.Lang.For_export]
set_builtin_1 [Lang.F]
set_builtin_1 [Wp.Lang.F]
set_builtin_2 [Lang.F]
set_builtin_2 [Wp.Lang.F]
set_builtin_2' [Lang.F]
set_builtin_2' [Wp.Lang.F]
set_builtin_eq [Lang.For_export]
set_builtin_eq [Lang.F]
set_builtin_eq [Wp.Lang.For_export]
set_builtin_eq [Wp.Lang.F]
set_builtin_eqp [Lang.F]
set_builtin_eqp [Wp.Lang.F]
set_builtin_get [Lang.F]
set_builtin_get [Wp.Lang.F]
set_builtin_leq [Lang.For_export]
set_builtin_leq [Lang.F]
set_builtin_leq [Wp.Lang.For_export]
set_builtin_leq [Wp.Lang.F]
set_mode [ProverWhy3]
set_model [Register]
set_model [Wp_error]
set_option [LogicBuiltins]
reset and add a value to an option (group, name)
set_option [Wp.LogicBuiltins]
reset and add a value to an option (group, name)
set_possible_values [Parameter_sig.String]
Set what are the acceptable values for this parameter.
set_procs [Why3Provers]
set_range [Parameter_sig.Int]
Set what is the possible range of values for this parameter.
set_result [Wpo]
set_result [Wp.Wpo]
set_saved [ProofEngine]
set_strategies [ProofEngine]
severe [Warning]
severe [Wp.Warning]
shareable [Vlist]
shift [MemLoader.Model]
shift [Sigs.Model]
Return the memory location obtained by array access at an index represented by the given term.
shift [Cvalues.Logic]
shift [Layout.Cluster]
shift [Wp.Sigs.Model]
Return the memory location obtained by array access at an index represented by the given term.
sigma [Lang]
uses current pool
sigma [Wp.Lang]
uses current pool
signature [Tactical]
signature [Wp.Tactical]
signed [Ctypes]
true if signed
signed [Wp.Ctypes]
true if signed
simplify [Conditions]
simplify [Mcfg.Splitter]
simplify [Wp.Conditions]
simplify [Wp.Mcfg.Splitter]
singleton [Letify.Ground]
singleton [Vset]
singleton [Splitter]
singleton [Layout.Chunk]
singleton [Wp.Vset]
singleton [Wp.Splitter]
singleton [Set.S]
singleton x returns the one-element set containing only x.
singleton [Map.S]
singleton x y returns the one-element map that contains a binding y for x.
size [Conditions]
Compute the total number of steps in the sequence, including nested sequences from branches and disjunctions.
size [Matrix]
size [Wp.Conditions]
Compute the total number of steps in the sequence, including nested sequences from branches and disjunctions.
sizeof [MemLoader.Model]
sizeof [Layout.Matrix]
sizeof [Layout.Value]
sizeof [Layout.Offset]
sizeof_defined [Ctypes]
sizeof_defined [Wp.Ctypes]
sizeof_object [Ctypes]
sizeof_object [Wp.Ctypes]
skip [Script]
smoked [VCS]
smoked [Wp.VCS]
smoking [WpReached]
Returns whether a stmt need a smoke tests to avoid being unreachable.
sort [Lang.F]
Constant time
sort [Wp.Lang.F]
Constant time
source_of_id [WpPropId]
source_of_id [Wp.WpPropId]
spawn [VC]
Same as prove but schedule the tasks into the global server returned by server function below.
spawn [ProverScript]
spawn [Prover]
spawn [ProverTask]
spawn [Wp.Prover]
spawn [Wp.ProverTask]
spawn [Wp.VC]
Same as prove but schedule the tasks into the global server returned by server function below.
spawn_wp_proofs_iter [Register]
spec [StmtSemantics.Make]
spec [Wp.StmtSemantics.Make]
specialize_eq_list [Vlist]
spinner [Tactical]
Unless specified, default is vmin or 0 or vmax, whichever fits.
spinner [Wp.Tactical]
Unless specified, default is vmin or 0 or vmax, whichever fits.
split [Auto]
split [Tactical]
split [Mcfg.Splitter]
split [Wp.Auto]
split [Wp.Tactical]
split [Wp.Mcfg.Splitter]
split [Set.S]
split x s returns a triple (l, present, r), where l is the set of elements of s that are strictly less than x; r is the set of elements of s that are strictly greater than x; present is false if s contains no element equal to x, or true if s contains an element equal to x.
split [Map.S]
split x m returns a triple (l, data, r), where l is the map with all the bindings of m whose key is strictly less than x; r is the map with all the bindings of m whose key is strictly greater than x; data is None if m contains no binding for x, or Some v if m binds v to x.
split_bag [WpPropId]
split_bag [Wp.WpPropId]
split_map [WpPropId]
split_map [Wp.WpPropId]
spy [Register]
start_edge [Cil2cfg]
get the starting edges
start_stmt_of_node [Cil2cfg]
startof [Cvalues]
Shift a location with 0-indices wrt to its array type
state [Conditions]
Stack a memory model state on top of the bundle.
state [Mstate]
state [Sigs.Model]
Returns a memory state description from a memory environement.
state [Wp.Conditions]
Stack a memory model state on top of the bundle.
state [Wp.Mstate]
state [Wp.Sigs.Model]
Returns a memory state description from a memory environement.
stats [Hashtbl.S]
status [ProofEngine]
status [WpAnnot]
status [LogicCompiler.Make]
status [Sigs.LogicSemantics]
Exit status for the current frame.
status [Wp.LogicCompiler.Make]
status [Wp.Sigs.LogicSemantics]
Exit status for the current frame.
step [Conditions]
Creates a single step
step [Wp.Conditions]
Creates a single step
step_at [Conditions]
Retrieve a step by id in the sequence.
step_at [Wp.Conditions]
Retrieve a step by id in the sequence.
stepout [ProverTask]
stepout [VCS]
stepout [Wp.ProverTask]
stepout [Wp.VCS]
steps [Conditions]
Attributes unique indices to every step.id in the sequence, starting from zero.
steps [Wp.Conditions]
Attributes unique indices to every step.id in the sequence, starting from zero.
stmt [Clabels]
stmt [Wp.Clabels]
store_float [MemLoader.Model]
store_int [MemLoader.Model]
store_pointer [MemLoader.Model]
stored [MemLoader.Make]
stored [Sigs.Model]
Return a set of formula that express a modification between two memory state.
stored [Wp.Sigs.Model]
Return a set of formula that express a modification between two memory state.
str_id [Cstring]
Non-zero integer, unique for each different string literal
str_id [Wp.Cstring]
Non-zero integer, unique for each different string literal
str_len [Cstring]
Property defining the size of the string in bytes, with \0 terminator included.
str_len [Wp.Cstring]
Property defining the size of the string in bytes, with \0 terminator included.
str_val [Cstring]
The array containing the char of the constant
str_val [Wp.Cstring]
The array containing the char of the constant
strange_loops [Cil2cfg]
detect is there are non natural loops or natural loops where we didn't manage to compute back edges (see mark_loops).
strategy [TacCongruence]
strategy [TacShift]
strategy [TacBitrange]
strategy [TacBitwised]
strategy [TacRewrite]
strategy [TacNormalForm]
strategy [TacCut]
strategy [TacFilter]
strategy [TacLemma]
strategy [TacInstance]
strategy [TacHavoc.Validity]
strategy [TacHavoc.Separated]
strategy [TacHavoc.Havoc]
strategy [TacUnfold]
strategy [TacCompound]
strategy [TacArray]
strategy [TacRange]
strategy [TacChoice.Contrapose]
strategy [TacChoice.Absurd]
strategy [TacChoice.Choice]
strategy [TacSplit]
strategy_has_asgn_goal [WpStrategy]
strategy_has_prop_goal [WpStrategy]
strategy_kind [WpStrategy]
string_of_termination_kind [WpPropId]
TODO: should probably be somewhere else
string_of_termination_kind [Wp.WpPropId]
TODO: should probably be somewhere else
sub_c_int [Ctypes]
sub_c_int [Wp.Ctypes]
sub_range [Vset]
sub_range [Wp.Vset]
subclause [Tactical]
When subclause clause p, we have clause = Step H and H -> p, or clause = Goal G and -> G.
subclause [Wp.Tactical]
When subclause clause p, we have clause = Step H and H -> p, or clause = Goal G and -> G.
subproof_idx [WpPropId]
subproof index of this propr_id
subproof_idx [Wp.WpPropId]
subproof index of this propr_id
subproofs [WpPropId]
How many subproofs
subproofs [Wp.WpPropId]
How many subproofs
subset [Cvalues.Logic]
subset [Vset]
subset [Wp.Vset]
subset [Set.S]
subset s1 s2 tests whether the set s1 is a subset of the set s2.
subst [Conditions]
Apply the atomic substitution recursively using Lang.F.p_subst f.
subst [Lang]
replace variables
subst [Wp.Conditions]
Apply the atomic substitution recursively using Lang.F.p_subst f.
subst [Wp.Lang]
replace variables
subterms [Pcfg]
subterms [Wp.Pcfg]
succ_e [Cil2cfg]
switch [Mcfg.S]
switch [Wp.Mcfg.S]
switch_cases [Splitter]
switch_cases [Wp.Splitter]
switch_default [Splitter]
switch_default [Wp.Splitter]

T
t32 [Cfloat]
t32 [Wp.Cfloat]
t64 [Cfloat]
t64 [Wp.Cfloat]
t_absurd [Auto]
Find a contradiction.
t_absurd [Wp.Auto]
Find a contradiction.
t_addr [MemMemory]
t_addr [Lang]
pointer on Void
t_addr [Wp.Lang]
pointer on Void
t_array [Lang]
t_array [Wp.Lang]
t_bool [Lang]
t_bool [Wp.Lang]
t_case [Auto]
Case analysis: t_case p a b applies process a under hypothesis p and process b under hypothesis not p.
t_case [Wp.Auto]
Case analysis: t_case p a b applies process a under hypothesis p and process b under hypothesis not p.
t_cases [Auto]
Complete analysis: applies each process under its guard, and proves that all guards are complete.
t_cases [Wp.Auto]
Complete analysis: applies each process under its guard, and proves that all guards are complete.
t_chain [Auto]
Apply second process to every goal generated by the first one.
t_chain [Wp.Auto]
Apply second process to every goal generated by the first one.
t_cut [Auto]
Prove condition p and use-it as a forward hypothesis.
t_cut [Wp.Auto]
Prove condition p and use-it as a forward hypothesis.
t_datatype [Lang]
t_datatype [Wp.Lang]
t_descr [Auto]
Apply a description to each sub-goal
t_descr [Wp.Auto]
Apply a description to each sub-goal
t_farray [Lang]
t_farray [Wp.Lang]
t_finally [Auto]
Apply a description to a leaf goal.
t_finally [Wp.Auto]
Apply a description to a leaf goal.
t_id [Auto]
Keep goal unchanged.
t_id [Wp.Auto]
Keep goal unchanged.
t_int [Lang]
t_int [Wp.Lang]
t_malloc [MemMemory]
allocation tables
t_mem [MemMemory]
t_addr indexed array
t_prop [Lang]
t_prop [Wp.Lang]
t_range [Auto]
t_range [Wp.Auto]
t_real [Lang]
t_real [Wp.Lang]
t_replace [Auto]
Prove src=tgt then replace src by tgt.
t_replace [Wp.Auto]
Prove src=tgt then replace src by tgt.
t_split [Auto]
Split with p and not p.
t_split [Wp.Auto]
Split with p and not p.
tactical [ProofEngine]
tactical [TacCongruence]
tactical [TacShift]
tactical [TacBitrange]
tactical [TacBitwised]
tactical [TacRewrite]
tactical [TacNormalForm]
tactical [TacCut]
tactical [TacFilter]
tactical [TacLemma]
tactical [TacInstance]
tactical [TacHavoc.Validity]
tactical [TacHavoc.Separated]
tactical [TacHavoc.Havoc]
tactical [TacUnfold]
tactical [TacCompound]
tactical [TacArray]
tactical [TacRange]
tactical [TacChoice.Contrapose]
tactical [TacChoice.Absurd]
tactical [TacChoice.Choice]
tactical [TacSplit]
tactical [WpPropId]
tactical [Wp.WpPropId]
target [WpAnnot]
tau [Matrix]
tau_of_chunk [Sigs.Chunk]
The type of data hold in a chunk.
tau_of_chunk [Wp.Sigs.Chunk]
The type of data hold in a chunk.
tau_of_comp [Lang]
tau_of_comp [Wp.Lang]
tau_of_ctype [Lang]
tau_of_ctype [Wp.Lang]
tau_of_field [Lang]
tau_of_field [Wp.Lang]
tau_of_float [Cfloat]
with respect to model
tau_of_float [Wp.Cfloat]
with respect to model
tau_of_lfun [Lang]
tau_of_lfun [Wp.Lang]
tau_of_ltype [Lang]
tau_of_ltype [Wp.Lang]
tau_of_object [Lang]
tau_of_object [Wp.Lang]
tau_of_record [Lang]
tau_of_record [Wp.Lang]
tau_of_return [Lang]
tau_of_return [Wp.Lang]
tau_of_set [Vset]
tau_of_set [Wp.Vset]
tau_of_var [Lang.F]
tau_of_var [Wp.Lang.F]
term [LogicCompiler.Make]
term [Sigs.LogicSemantics]
Compile a term expression.
term [Repr]
term [Wp.LogicCompiler.Make]
term [Wp.Sigs.LogicSemantics]
Compile a term expression.
term [Wp.Repr]
test [Mcfg.S]
test [Wp.Mcfg.S]
timeout [ProverTask]
timeout [VCS]
timeout [Wp.ProverTask]
timeout [Wp.VCS]
title [ProofEngine]
title [Why3Provers]
title_of_mode [VCS]
title_of_mode [Wp.VCS]
title_of_prover [VCS]
title_of_prover [Wp.VCS]
to_addr [MemLoader.Model]
to_cint [Cint]
Raises Not_found if not.
to_cint [Wp.Cint]
Raises Not_found if not.
to_condition [CfgCompiler.Cfg.P]
to_condition [Wp.CfgCompiler.Cfg.P]
to_integer [Cint]
to_integer [Wp.Cint]
to_logic [Clabels]
to_logic [Wp.Clabels]
to_region_pointer [MemLoader.Model]
token [Script]
top [Letify.Ground]
tracelog [Register]
trans [Filter_axioms]
tree_context [ProofEngine]
trigger [LogicCompiler.Make]
trigger [Wp.LogicCompiler.Make]
trivial [Wpo.GOAL]
trivial [Conditions]
empty implies true
trivial [Wp.Wpo.GOAL]
trivial [Wp.Conditions]
empty implies true
try_sequence [Register]
type_id [Lang]
type_id [Wp.Lang]
typeof [Lang.F]
Try to extract a type of term.
typeof [Layout.Offset]
typeof [Wp.Lang.F]
Try to extract a type of term.
typeof_chain [Layout.Offset]

U
unchanged [Sigs.CodeSemantics]
Express that a given variable has the same value in two memory states.
unchanged [Wp.Sigs.CodeSemantics]
Express that a given variable has the same value in two memory states.
union [Sigs.Sigma]
Same as Chunk.Set.union
union [Cvalues.Logic]
union [Vset]
union [Splitter]
union [Passive]
union [Layout.Chunk]
union [Wp.Sigs.Sigma]
Same as Chunk.Set.union
union [Wp.Vset]
union [Wp.Splitter]
union [Wp.Passive]
union [Set.S]
Set union.
union [Map.S]
union f m1 m2 computes a map whose keys is the union of keys of m1 and of m2.
union_map [Layout.Chunk]
unknown [VCS]
unknown [Wp.VCS]
unmark [Splitter]
erase all tags
unmark [Wp.Splitter]
erase all tags
unreachable_if_valid [WpPropId]
Stmt that is unreachable in case the PO is valid.
unreachable_if_valid [Wp.WpPropId]
Stmt that is unreachable in case the PO is valid.
unreachable_nodes [Cil2cfg]
unsupported [Wp_error]
update [GuiPanel]
update [WpContext.Registry]
set current value, with no protection
update [Context]
Modification of the current value
update [Wp.WpContext.Registry]
set current value, with no protection
update [Wp.Context]
Modification of the current value
update_cond [Conditions]
Updates the condition of a step and merges descr, deps and warn
update_cond [Wp.Conditions]
Updates the condition of a step and merges descr, deps and warn
update_symbol [Definitions]
update_symbol [Wp.Definitions]
updates [Pcfg]
updates [Mstate]
updates [Sigs.Model]
Try to interpret a sequence of states into updates.
updates [Wp.Pcfg]
updates [Wp.Mstate]
updates [Wp.Sigs.Model]
Try to interpret a sequence of states into updates.
use [Layout.Alias]
use_assigns [Mcfg.S]
use_assigns env hid kind assgn goal performs the havoc on the goal.
use_assigns [Wp.Mcfg.S]
use_assigns env hid kind assgn goal performs the havoc on the goal.

V
val_of_exp [Sigs.CodeSemantics]
Compile an expression as a term.
val_of_exp [Wp.Sigs.CodeSemantics]
Compile an expression as a term.
val_of_term [Sigs.LogicSemantics]
Same as term above but reject any set of locations.
val_of_term [Wp.Sigs.LogicSemantics]
Same as term above but reject any set of locations.
valid [VCS]
valid [Sigs.Model]
Return the formula that tests if a memory state is valid (according to Sigs.acs) in the given memory state at the given segment.
valid [Cvalues.Logic]
valid [Wp.VCS]
valid [Wp.Sigs.Model]
Return the formula that tests if a memory state is valid (according to Wp.Sigs.acs) in the given memory state at the given segment.
validate [ProofEngine]
value [Sigs.Sigma]
Same as Lang.F.e_var of get.
value [Cvalues.Logic]
value [Wp.Sigs.Sigma]
Same as Lang.F.e_var of get.
vanti [TacFilter]
vars [Sigs.LogicSemantics]
Qed variables appearing in a region expression.
vars [Sigs.Model]
Return the logic variables from which the given location depend on.
vars [Vset]
vars [Definitions.Trigger]
vars [Lang.F]
Constant time
vars [Wp.Sigs.LogicSemantics]
Qed variables appearing in a region expression.
vars [Wp.Sigs.Model]
Return the logic variables from which the given location depend on.
vars [Wp.Vset]
vars [Wp.Definitions.Trigger]
vars [Wp.Lang.F]
Constant time
vars_hyp [Conditions]
Pre-computed and available in constant time.
vars_hyp [Wp.Conditions]
Pre-computed and available in constant time.
vars_seq [Conditions]
At the cost of the union of hypotheses and goal.
vars_seq [Wp.Conditions]
At the cost of the union of hypotheses and goal.
varsp [Lang.F]
Constant time
varsp [Wp.Lang.F]
Constant time
verdict [VCS]
verdict [Wp.VCS]
version [Why3Provers]
very_strange_loops [Cil2cfg]
detect is there are natural loops where we didn't manage to compute back edges (see mark_loops).
visible [Pcfg]
visible [Wp.Pcfg]
vmax [TacRange]
vmin [TacRange]
volatile [Cvalues]
Check if a volatile access must be properly modelled or ignored.
vset [Cvalues.Logic]

W
warnings [Wpo]
warnings [Wp.Wpo]
wg_status [GuiProver]
with_current_loc [Context]
with_current_loc [Wp.Context]
without_assume [Lang]
without_assume [Wp.Lang]
wkey_smoke [Register]
wp_iter_model [Register]
wp_print_memory_context [Register]
wp_warn_memory_context [Register]
wrap [TacInstance]
writes [CfgCompiler.Cfg.E]
as defined by S.writes
writes [Sigs.Sigma]
writes s indicates which chunks are new in s.post compared to s.pre.
writes [Wp.CfgCompiler.Cfg.E]
as defined by S.writes
writes [Wp.Sigs.Sigma]
writes s indicates which chunks are new in s.post compared to s.pre.