Index of values


A
access [Region]
acsl_lit [Cfloat]
acsl_lit [Wp.Cfloat]
add [Wpo]
add [Letify.Split]
add [Letify.Defs]
add [Letify.Sigma]
add [Warning]
add [Cil2cfg.HEsig]
add [Map.S]
add x y m returns a map containing the same bindings as m, plus a binding of x to y.
add [Wp.Warning]
add [FCMap.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 [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_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_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_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_node_annots [WpStrategy]
add_node_annots cfg annots v (before, (after, exits)) add the annotations for the node :
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_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_fct_bhv_pre [WpStrategy]
Add the preconditions of the behavior : if impl_assumes, add b_assumes => b_requires else add both the b_requires and the b_assumes
add_prop_fct_post [WpStrategy]
add_prop_fct_pre [WpStrategy]
Add the predicate as a function precondition.
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 [Proof]
new_script goal keys proof qed registers the script proof terminated by qed for goal goal and keywords keys
add_step [Register]
add_stmt_spec_assigns_hyp [WpStrategy]
shortcut to add a stmt spec assigns property as an hypothesis.
add_time [Register]
add_type [LogicBuiltins]
add_type [Wp.LogicBuiltins]
age [Wpo]
ainf [Cvalues]
Array lower-bound, ie `Some(0)`
already_valid [Register]
append [Conditions]
append [Wp.Conditions]
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 [Cvalues.Logic]
apply [Passive]
apply [Wp.Passive]
apply_add [Cvalues.Logic]
apply_sub [Cvalues.Logic]
array [Lang]
array [Wp.Lang]
array_dim [Ctypes]
array_dim [Wp.Ctypes]
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]
assemble_wpo [ProverWhy3]
None if the po is trivial
assign [Mcfg.S]
assign [Wp.Mcfg.S]
assigned [LogicAssigns.Make]
assigned [Memory.Model]
Return a set of formula that express that two memory state are the same except at the given set of memory location.
assigned [Memory.Sigma]
equal chunks outside domain
assigned [Wp.Memory.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.Memory.Sigma]
equal chunks outside domain
assigns [LogicSemantics.Make]
assigns [Wp.LogicSemantics.Make]
assigns_from [LogicSemantics.Make]
assigns_from [Wp.LogicSemantics.Make]
assigns_info_id [WpPropId]
assigns_info_id [Wp.WpPropId]
assigns_upper_bound [WpStrategy]
assume [Conditions]
assume [Letify.Sigma]
assume [Lang]
assume [Wp.Conditions]
assume [Wp.Lang]
asup [Cvalues]
Array upper-bound, ie `Some(n-1)`
atype [Lang]
atype [Wp.Lang]
auto_check [Register]
axiomatic [Definitions]
axiomatic [LogicUsage]
axiomatic [Wp.Definitions]
axiomatic [Wp.LogicUsage]

B
band [Cint]
band [Wp.Cint]
bar [Wpo]
base_addr [Memory.Model]
Return the memory location of the base address of a given memory location
base_addr [Wp.Memory.Model]
Return the memory location of the base address of a given memory location
basename [LogicUsage]
Trims the original name
basename [Ctypes]
basename [Wp.LogicUsage]
Trims the original name
basename [Wp.Ctypes]
basename_of_chunk [Memory.Chunk]
basename_of_chunk [Wp.Memory.Chunk]
begin_session [Register]
behavior_name_of_strategy [WpStrategy]
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.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.
bindings [FCMap.S]
Return the list of all bindings of the given map.
block_length [Memory.Model]
Returns the length (in bytes) of the allocated block containing the given location
block_length [Wp.Memory.Model]
Returns the length (in bytes) of the allocated block containing the given location
blocks_closed_by_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_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_add [Vset]
bound_add [Wp.Vset]
bound_shift [Vset]
bound_shift [Wp.Vset]
bound_sub [Vset]
bound_sub [Wp.Vset]
branch [Conditions]
branch [Wp.Conditions]
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_type [Lang]
builtin_type [Wp.Lang]
bundle [Pcond]
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_int_all [Ctypes]
c_int_all [Wp.Ctypes]
c_int_bounds [Ctypes]
c_int_bounds [Wp.Ctypes]
c_label [Clabels]
Assumes the logic label only comes from normalized labels.
c_label [Wp.Clabels]
Assumes the logic label only comes from normalized labels.
c_ptr [Ctypes]
Returns the type of pointers
c_ptr [Wp.Ctypes]
Returns the type of pointers
cache_descr [Wpo.VC_Annot]
cache_descr [Wpo.VC_Lemma]
cache_log [Wpo.DISK]
call [LogicSemantics.Make]
call [LogicCompiler.Make]
call [CodeSemantics.Make]
call [Splitter]
call [Mcfg.S]
call [Wp.LogicSemantics.Make]
call [Wp.LogicCompiler.Make]
call [Wp.CodeSemantics.Make]
call [Wp.Splitter]
call [Wp.Mcfg.S]
call_dynamic [Mcfg.S]
call_dynamic [Wp.Mcfg.S]
call_env [LogicSemantics.Make]
call_env [Wp.LogicSemantics.Make]
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_post [LogicSemantics.Make]
call_post [LogicCompiler.Make]
call_post [Wp.LogicSemantics.Make]
call_post [Wp.LogicCompiler.Make]
call_pre [LogicSemantics.Make]
call_pre [LogicCompiler.Make]
call_pre [Wp.LogicSemantics.Make]
call_pre [Wp.LogicCompiler.Make]
call_pred [LogicCompiler.Make]
call_pred [Definitions]
call_pred [Wp.LogicCompiler.Make]
call_pred [Wp.Definitions]
callback [Model.Registry]
callback [Wp.Model.Registry]
cardinal [Map.S]
Return the number of bindings of a map.
cardinal [FCMap.S]
Return the number of bindings of a map.
cases [Splitter]
cases [Wp.Splitter]
cast [CodeSemantics.Make]
cast [Memory.Model]
Cast a memory location into another memory location.
cast [Wp.CodeSemantics.Make]
cast [Wp.Memory.Model]
Cast a memory location into another memory location.
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]
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_tau [Vlist]
check_term [Vlist]
checked [VCS]
checked [Wp.VCS]
choose [Map.S]
Return one binding of the given map, or raise Not_found if the map is empty.
choose [FCMap.S]
Return one binding of the given map, or raise Not_found if the map is empty.
clean [Conditions]
clean [Wp.Conditions]
clear [VC]
clear [Wpo]
clear [Proof]
clear [Context]
Clear the current value.
clear [Cil2cfg.HEsig]
clear [Wp.VC]
clear [Wp.Context]
Clear the current value.
clear_scheduled [Register]
clear_session [Register]
cloc [CodeSemantics.Make]
cloc [Wp.CodeSemantics.Make]
close [Script]
close [Conditions]
With free variables quantified.
close [Mcfg.S]
close [Wp.Conditions]
With free variables quantified.
close [Wp.Mcfg.S]
cluster [Cstring]
The cluster where all strings are defined.
cluster [Definitions]
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
comp [Lang]
comp [Wp.Lang]
comp_id [Lang]
comp_id [Wp.Lang]
compare [ProverWhy3.Goal]
compare [Map.OrderedType]
A total ordering function over the keys.
compare [VCS]
compare [Memory.Chunk]
compare [LogicBuiltins]
compare [Model.Key]
compare [Model.Entries]
compare [Warning]
compare [Clabels.T]
compare [Ctypes.AinfoComparable]
compare [Ctypes]
compare [Map.S]
Total ordering between maps.
compare [Wp.VCS]
compare [Wp.Memory.Chunk]
compare [Wp.LogicBuiltins]
compare [Wp.Model.Key]
compare [Wp.Model.Entries]
compare [Wp.Warning]
compare [FCMap.S]
Total ordering between maps.
compare [Wp.Clabels.T]
compare [Wp.Ctypes.AinfoComparable]
compare [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 [Model.Data]
compile [Model.Registry]
with circularity protection
compile [Wp.Model.Data]
compile [Wp.Model.Registry]
with circularity protection
compile_lemma [Definitions]
compile_lemma [Wp.Definitions]
compinfo [Definitions]
compinfo [Wp.Definitions]
compute [Calculus.Cfg]
compute [Wpo.GOAL]
compute [RefUsage]
compute [LogicUsage]
To force computation
compute [Dyncall]
Forces computation of dynamic calls.
compute [Wp.RefUsage]
compute [Wp.LogicUsage]
To force computation
compute_call [Generator]
compute_descr [Wpo.GOAL]
compute_ip [Generator]
compute_kf [Generator]
compute_proof [Wpo.GOAL]
compute_provers [Register]
compute_selection [Generator]
computer [Register]
computer [CfgWP]
computing [VCS]
computing [Wp.VCS]
concat [Conditions]
concat [Wp.Conditions]
concretize [Vset]
concretize [Wp.Vset]
cond [CodeSemantics.Make]
cond [Wp.CodeSemantics.Make]
condition [Conditions]
With free variables kept.
condition [Wp.Conditions]
With free variables kept.
conditions [Passive]
conditions [Wp.Passive]
configure [Factory]
configure [Memory.Model]
configure [Vlist]
configure [Cfloat]
configure [Cint]
configure [Wp.Factory]
configure [Wp.Cfloat]
configure [Wp.Cint]
configure [Wp.Memory.Model]
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]
convert [Cfloat]
convert [Cint]
Indenpendent from model
convert [Lang.Alpha]
convert [Wp.Cfloat]
convert [Wp.Cint]
Indenpendent from model
convert [Wp.Lang.Alpha]
convertp [Lang.Alpha]
convertp [Wp.Lang.Alpha]
copied [Memory.Model]
Return a set of formula that express a copy between two memory state.
copied [Wp.Memory.Model]
Return a set of formula that express a copy between two memory state.
copy [Memory.Sigma]
copy [Wp.Memory.Sigma]
copy [Datatype.S]
Deep copy: no possible sharing between x and copy x.
create [CfgDump]
create [Memory.Sigma]
create [LogicBuiltins]
Create a new driver.
create [Cleaning]
create [Letify.Split]
create [Lang.Alpha]
create [Context]
Creates a new context with name
create [Cil2cfg.HEsig]
create [Wp.Memory.Sigma]
create [Wp.LogicBuiltins]
Create a new driver.
create [Wp.Lang.Alpha]
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]
current [Cint]
current [Wp.Cint]
cval [CodeSemantics.Make]
cval [Wp.CodeSemantics.Make]
cvar [Memory.Model]
Return the location of a C variable
cvar [Wp.Memory.Model]
Return the location of a C variable

D
datatype [MemVar.VarUsage]
datatype [Memory.Model]
for projectification
datatype [Lang]
datatype [Wp.MemVar.VarUsage]
datatype [Wp.Memory.Model]
for projectification
datatype [Wp.Lang]
debugp [Lang.F]
debugp [Wp.Lang.F]
default [Factory]
"Var,Typed,Nat,Real" memory model.
default [Wp.Factory]
"Var,Typed,Nat,Real" memory model.
define [Lang.F]
define [Model.Registry]
no redefinition ; circularity protected
define [Wp.Lang.F]
define [Wp.Model.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.
delete_script [Proof]
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]
descr [Factory]
descr [Vset]
descr [LogicBuiltins]
descr [Wp.Factory]
descr [Wp.Vset]
descr [Wp.LogicBuiltins]
detect_provers [ProverWhy3]
detect_why3 [ProverWhy3]
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 [Model]
Current model in "-wp-out" directory
directory [Wp.Model]
Current model in "-wp-out" directory
disjoint [Region]
disjoint [Vset]
disjoint [Wp.Vset]
do_list_scheduled [Register]
do_list_scheduled_result [Register]
do_prover_detect [Register]
do_why3_result [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_prover [Register]
do_wpo_result [Register]
do_wpo_start [Register]
do_wpo_stat [Register]
do_wpo_success [Register]
do_wpo_wait [Register]
domain [LogicAssigns.Make]
domain [Memory.Model]
Give the set of chunk where an object of the given type at the given location is stored.
domain [Memory.Sigma]
domain [Conditions]
domain [Letify.Defs]
domain [Letify.Sigma]
domain [Wp.Memory.Model]
Give the set of chunk where an object of the given type at the given location is stored.
domain [Wp.Memory.Sigma]
domain [Wp.Conditions]
downcast [Cint]
Dependent on model
downcast [Wp.Cint]
Dependent on model
driver [LogicBuiltins]
driver [Wp.LogicBuiltins]
dummy [Wpo.GOAL]
dump [LogicBuiltins]
dump [Pcond]
dump [RefUsage]
dump [LogicUsage]
Print on output
dump [Wp.LogicBuiltins]
dump [Wp.RefUsage]
dump [Wp.LogicUsage]
Print on output
dump_scripts [Proof]
dump_scripts f saves all scripts from the database into file f.

E
e_apply [Letify.Sigma]
e_bigint [Lang.F]
e_bigint [Wp.Lang.F]
e_fact [Lang.F]
e_fact [Wp.Lang.F]
e_hexfloat [Lang.F]
e_hexfloat [Wp.Lang.F]
e_int64 [Lang.F]
e_int64 [Wp.Lang.F]
e_minus_one [Lang.F]
e_minus_one [Wp.Lang.F]
e_mthfloat [Lang.F]
e_mthfloat [Wp.Lang.F]
e_one [Lang.F]
e_one [Wp.Lang.F]
e_one_real [Lang.F]
e_one_real [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_setfield [Lang.F]
e_setfield [Wp.Lang.F]
e_subst [Lang.F]
e_subst [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]
eat [Script]
edge_dst [Cil2cfg]
edge_src [Cil2cfg]
node and edges relations
either [Conditions]
either [Wp.Conditions]
emit [Warning]
Emit a warning in current context.
emit [Wp.Warning]
Emit a warning in current context.
empty [Memory.Sigma]
empty [Region]
empty [Vset]
empty [Conditions]
empty [Letify.Defs]
empty [Letify.Sigma]
empty [Splitter]
empty [Passive]
empty [Mcfg.S]
empty [Map.S]
The empty map.
empty [Wp.Memory.Sigma]
empty [Wp.Passive]
empty [Wp.Vset]
empty [Wp.Conditions]
empty [Wp.Splitter]
empty [Wp.Mcfg.S]
empty [FCMap.S]
The empty map.
empty_acc [WpStrategy]
empty_assigns_info [WpPropId]
empty_assigns_info [Wp.WpPropId]
end_session [Register]
env [Lang.F]
env [Wp.Lang.F]
env_at [LogicCompiler.Make]
env_at [Wp.LogicCompiler.Make]
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]
epred [Lang.F]
epred [Wp.Lang.F]
epsilon [Lang]
epsilon [Rformat]
epsilon [Wp.Lang]
eqp [Lang.F]
eqp [Wp.Lang.F]
equal [Vset]
equal [Letify.Sigma]
equal [Clabels]
equal [Ctypes.AinfoComparable]
equal [Ctypes]
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.Vset]
equal [FCMap.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_but [Region]
equal_comp [Cvalues]
equal_obj [LogicAssigns.Code]
equal_obj [CodeSemantics.Make]
equal_obj [Wp.CodeSemantics.Make]
equal_object [Cvalues]
equal_typ [CodeSemantics.Make]
equal_typ [Wp.CodeSemantics.Make]
error [Script]
error [Warning]
error [Wp.Warning]
exercised [Register]
exists [Splitter]
exists [Parameter_sig.Set]
Is there some element satisfying the given predicate?
exists [Map.S]
exists p m checks if at least one binding of the map satisfy the predicate p.
exists [Wp.Splitter]
exists [FCMap.S]
exists p m checks if at least one binding of the map satisfy the predicate p.
exp [CodeSemantics.Make]
exp [Wp.CodeSemantics.Make]
export [WpReport]
export_decl [Mcfg.Export]
export_decl [Wp.Mcfg.Export]
export_goal [Mcfg.Export]
export_goal [Wp.Mcfg.Export]
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]
extract [Conditions]
extract [Letify.Defs]
extract [Wp.Conditions]

F
f_bit [Cint]
f_bit [Wp.Cint]
f_concat [Vlist]
f_convert [Ctypes]
f_convert [Wp.Ctypes]
f_delta [Cfloat]
f_delta [Wp.Cfloat]
f_epsilon [Cfloat]
f_epsilon [Wp.Cfloat]
f_iabs [Cfloat]
f_iabs [Wp.Cfloat]
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_model [Cfloat]
f_model [Wp.Cfloat]
f_rabs [Cfloat]
f_rabs [Wp.Cfloat]
f_sqrt [Cfloat]
f_sqrt [Wp.Cfloat]
fadd [Cfloat]
fadd [Wp.Cfloat]
failed [VCS]
failed [Wp.VCS]
farray [Lang]
farray [Wp.Lang]
fcstat [WpReport]
fdiv [Cfloat]
fdiv [Wp.Cfloat]
field [Memory.Model]
Return the memory location obtained by field access from a given memory location
field [Cvalues.Logic]
field [Lang]
field [Wp.Memory.Model]
Return the memory location obtained by field access from a given memory location
field [Wp.Lang]
field_id [Lang]
field_id [Wp.Lang]
field_offset [Ctypes]
field_offset [Wp.Ctypes]
fields_of_field [Lang]
fields_of_field [Wp.Lang]
fields_of_tau [Lang]
fields_of_tau [Wp.Lang]
file_goal [Wpo.DISK]
file_kf [Wpo.DISK]
file_logerr [Wpo.DISK]
file_logout [Wpo.DISK]
filename_for_prover [VCS]
filename_for_prover [Wp.VCS]
filter [Script]
filter [Conditions]
filter [Splitter]
filter [Map.S]
filter p m returns the map with all the bindings in m that satisfy predicate p.
filter [Wp.Conditions]
filter [Wp.Splitter]
filter [FCMap.S]
filter p m returns the map with all the bindings in m that satisfy predicate p.
filter_pred [Cleaning]
filter_status [WpAnnot]
filter_type [Cleaning]
find [ProverWhy3]
find [Letify.Sigma]
find [Model.Registry]
find [Model]
find [Cil2cfg.HEsig]
find [Map.S]
find x m returns the current binding of x in m, or raises Not_found if no such binding exists.
find [Wp.Model.Registry]
find [Wp.Model]
find [FCMap.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_lemma [Definitions]
raises Not_found
find_lemma [Wp.Definitions]
raises Not_found
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_script_for_goal [Proof]
Retrieve script file for one specific goal.
find_script_with_hints [Proof]
Retrieve matchable script files for w.r.t provided required and hints keywords.
fiter [Ctypes]
fiter [Wp.Ctypes]
float_of_int [Cfloat]
float_of_int [Wp.Cfloat]
flt_add [Cfloat]
flt_add [Wp.Cfloat]
flt_div [Cfloat]
flt_div [Wp.Cfloat]
flt_mul [Cfloat]
flt_mul [Wp.Cfloat]
flt_rnd [Cfloat]
flt_rnd [Wp.Cfloat]
flt_sqrt [Cfloat]
flt_sqrt [Wp.Cfloat]
flush [Warning]
flush [Wp.Warning]
fmemo [Ctypes]
memoization function, projectified
fmemo [Wp.Ctypes]
memoization function, projectified
fmul [Cfloat]
fmul [Wp.Cfloat]
fold [Splitter]
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 [Wp.Splitter]
fold [FCMap.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 [Map.S]
for_all p m checks if all the bindings of the map satisfy the predicate p.
for_all [Wp.Splitter]
for_all [FCMap.S]
for_all p m checks if all the bindings of the map satisfy the predicate p.
formal [LogicCompiler.Make]
formal [Wp.LogicCompiler.Make]
frame [LogicSemantics.Make]
frame [LogicCompiler.Make]
frame [Wp.LogicSemantics.Make]
frame [Wp.LogicCompiler.Make]
free [Context]
Performs the job with local context cleared.
free [Wp.Context]
Performs the job with local context cleared.
freshen [Lang]
freshen [Wp.Lang]
freshvar [Lang]
freshvar [Wp.Lang]
from_file [Why3_xml]
returns the list of XML elements from the given file.
fsub [Cfloat]
fsub [Wp.Cfloat]
full [Region]

G
generate [WpRTE]
Invoke RTE to generate missing annotations for the given function and model.
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 [Memory.Sigma]
get [Lang.Alpha]
get [Model.Generator]
get [Model.Registry]
get [Context]
Retrieves the current value of the context.
get [Cil2cfg]
get [RefUsage]
get [Dyncall]
Returns empty list if there is no specified dynamic call.
get [Wp.Memory.Sigma]
get [Wp.Lang.Alpha]
get [Wp.Model.Generator]
get [Wp.Model.Registry]
get [Wp.Context]
Retrieves the current value of the context.
get [Wp.RefUsage]
get_annots [WpStrategy]
get_array [Ctypes]
get_array [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_call_asgn [WpStrategy]
get_call_hyp [WpStrategy]
To be used as hypotheses arround 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_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_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 [Model]
get_descr [Wp.Model]
get_description [VC]
get_description [Wp.VC]
get_edge_labels [Cil2cfg]
get_edge_next_stmt [Cil2cfg]
get_emitter [Model]
get_emitter [Wp.Model]
get_env [Wp_parameters]
get_exit_edges [Cil2cfg]
Find the edges e that goes to the Vexit node inside the statement begining at node n
get_file_logerr [Wpo]
only filename, might not exists
get_file_logout [Wpo]
only filename, might not exists
get_files [Wpo]
get_formula [VC]
get_formula [Wp.VC]
get_frame [LogicSemantics.Make]
get_frame [LogicCompiler.Make]
get_frame [Wp.LogicSemantics.Make]
get_frame [Wp.LogicCompiler.Make]
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_goal_only [WpStrategy]
get_hyp_only [WpStrategy]
get_hypotheses [Lang]
get_hypotheses [Wp.Lang]
get_id [VC]
get_id [Model]
get_id [Wp.VC]
get_id [Wp.Model]
get_id_prop_strategies [WpAnnot]
get_includes [Wp_parameters]
get_index [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 [Ctypes]
get_int [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_label [Wpo]
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_model [VC]
get_model [Wpo]
get_model [Model]
Current model
get_model [Wp.VC]
get_model [Wp.Model]
Current model
get_model_id [Wpo]
get_model_name [Wpo]
get_name [LogicUsage]
get_name [Wp.LogicUsage]
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_dir [Wp_parameters]
get_plain_string [Parameter_sig.String]
always return the argument, even if the argument is not a function name.
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_logic_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_property [VC]
get_property [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_result [VC]
get_result [Wpo]
Dynamically exported.
get_result [Wp.VC]
get_results [VC]
get_results [Wpo]
get_results [Wp.VC]
get_scope [Model]
get_scope [Wp.Model]
get_separation [Model]
get_separation [Wp.Model]
get_steps [Wpo]
get_switch_edges [Cil2cfg]
similar to succ_e g v but give the switch cases and the default edge
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_variables [Lang]
get_variables [Wp.Lang]
global [Memory.Model]
Given a pointer value p, assumes this pointer p (when valid) is allocated outside the function frame under analysis.
global [Wp.Memory.Model]
Given a pointer value p, assumes this pointer p (when valid) is allocated outside the function frame under analysis.
global_axioms [WpStrategy]
goals_of_property [Wpo]
All POs related to a given property.
group [Splitter]
group [Wp.Splitter]
guards [LogicSemantics.Make]
guards [LogicCompiler.Make]
guards [Wp.LogicSemantics.Make]
guards [Wp.LogicCompiler.Make]

H
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_ctype [Cvalues]
has_dkey [Wp_parameters]
has_exit [Cil2cfg]
wether an exit edge exists or not
has_init [Mcfg.S]
has_init [Wp.Mcfg.S]
has_ltype [Cvalues]
has_print_generated [Wp_parameters]
Debugging Categories
hash [Memory.Chunk]
hash [Ctypes.AinfoComparable]
hash [Ctypes]
hash [Wp.Memory.Chunk]
hash [Wp.Ctypes.AinfoComparable]
hash [Wp.Ctypes]
havoc [Memory.Sigma]
havoc [Wp.Memory.Sigma]
havoc_any [Memory.Sigma]
havoc_any [Wp.Memory.Sigma]
havoc_chunk [Memory.Sigma]
havoc_chunk [Wp.Memory.Sigma]
hints_for [Proof]
hypotheses [Lang]
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]
iadd [Cint]
iadd [Wp.Cint]
id [LogicBuiltins]
id [Matrix]
unique w.r.t equal
id [Wp.LogicBuiltins]
ident [Factory]
ident [Script]
ident [Wp.Factory]
idents [Script]
idiv [Cint]
idiv [Wp.Cint]
idp [Lang.F]
idp [Wp.Lang.F]
if_else [Splitter]
if_else [Wp.Splitter]
if_then [Splitter]
if_then [Wp.Splitter]
iiter [Ctypes]
iiter [Wp.Ctypes]
imemo [Ctypes]
imemo [Wp.Ctypes]
imod [Cint]
imod [Wp.Cint]
imul [Cint]
imul [Wp.Cint]
in_frame [LogicSemantics.Make]
in_frame [LogicCompiler.Make]
in_frame [Wp.LogicSemantics.Make]
in_frame [Wp.LogicCompiler.Make]
in_range [Vset]
in_range [Wp.Vset]
in_size [Vset]
in_size [Wp.Vset]
included [LogicSemantics.Make]
included [Memory.Model]
Return the formula that tests if two segment are included
included [Cvalues.Logic]
included [Wp.LogicSemantics.Make]
included [Wp.Memory.Model]
Return the formula that tests if two segment are included
incr [Parameter_sig.Int]
Increment the integer.
infoprover [Lang]
same information for all the provers
infoprover [Wp.Lang]
same information for all the provers
init [LogicBuiltins]
Reset the context to a newly created driver
init [Wp.LogicBuiltins]
Reset the context to a newly created driver
init_const [Mcfg.S]
the (entire) variable has its initial value
init_const [Wp.Mcfg.S]
the (entire) variable has its initial value
init_range [Mcfg.S]
init_range env lv t_elt a b wp : put default values of type t_elt in lvk with a <= k < b
init_range [Wp.Mcfg.S]
init_range env lv t_elt a b wp : put default values of type t_elt in lvk with a <= k < b
init_value [Mcfg.S]
init_value env lv t v_opt wp: put value of type t (or default if None) in lv
init_value [Wp.Mcfg.S]
init_value env lv t v_opt wp: put value of type t (or default if None) in lv
instance [Factory]
instance [Wp.Factory]
instance_of [CodeSemantics.Make]
instance_of [Wp.CodeSemantics.Make]
int_of_loc [Memory.Model]
Cast a memory location into an integer of the given type
int_of_loc [Wp.Memory.Model]
Cast a memory location into an integer of the given type
inter [Cvalues.Logic]
inter [Vset]
inter [Wp.Vset]
intersect [Conditions]
intersect [Lang.F]
intersect [Wp.Conditions]
intersect [Wp.Lang.F]
intersectp [Lang.F]
intersectp [Wp.Lang.F]
intros [Conditions]
intros [Wp.Conditions]
invalid [VCS]
invalid [Wp.VCS]
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 positionned, and the variable is global, not extern, with a "const" type (see hasConstAttribute).
is_array [Ctypes]
is_array [Wp.Ctypes]
is_assigns [WpPropId]
is_assigns [Wp.WpPropId]
is_back_edge [Cil2cfg]
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 [Wpo]
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 redondant with other conditions.
is_cint_simplifier [Wp.Cint]
Remove the is_cint in formulas that are redondant with other conditions.
is_comp [Ctypes]
is_comp [Wp.Ctypes]
is_composed [WpAnnot]
whether a proof needs several lemma to be complete
is_default [LogicBuiltins]
is_default [Wp.LogicBuiltins]
is_default_behavior [WpStrategy]
is_empty [Proof]
is_empty [Conditions]
is_empty [Map.S]
Test whether a map is empty or not.
is_empty [Wp.Conditions]
is_empty [FCMap.S]
Test whether a map is empty or not.
is_equal [Lang.F]
is_equal [Wp.Lang.F]
is_exp_range [CodeSemantics.Make]
is_exp_range [Wp.CodeSemantics.Make]
is_false [Cvalues]
p ? 0 : 1
is_framed [Memory.Chunk]
Whether the Chunk is local to a function.
is_framed [Wp.Memory.Chunk]
Whether the Chunk is local to a function.
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_model_defined [Model]
is_model_defined [Wp.Model]
is_null [Memory.Model]
Return the formula that check if a given location is null
is_null [Cvalues]
is_null [Wp.Memory.Model]
Return the formula that check if a given location is null
is_object [Cvalues]
is_out [Wp_parameters]
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_precond_generated [WpRTE]
is_proved [WpAnnot]
wether all partial proofs have been accumulated or not
is_ptrue [Lang.F]
is_ptrue [Wp.Lang.F]
is_recursive [LogicUsage]
is_recursive [Wp.LogicUsage]
is_requires [WpPropId]
is_requires [Wp.WpPropId]
is_set [Lang.F.Check]
is_set [Wp.Lang.F.Check]
is_trivial [VC]
is_trivial [Wpo.VC_Annot]
is_trivial [Wpo.VC_Lemma]
is_trivial [Wpo.GOAL]
is_trivial [Wpo]
is_trivial [Wp.VC]
is_true [Cvalues]
p ? 1 : 0
is_true [Separation]
Returns true if the clause is degenerated.
is_true [Wp.Separation]
Returns true if the clause is degenerated.
is_valid [Wpo]
true if the result is valid.
is_verdict [VCS]
is_verdict [Wp.VCS]
is_void [Ctypes]
is_void [Wp.Ctypes]
is_zero [CodeSemantics.Make]
is_zero [Lang.F]
is_zero [Wp.CodeSemantics.Make]
is_zero [Wp.Lang.F]
isub [Cint]
isub [Wp.Cint]
iter [Wpo]
iter [Memory.Sigma]
iter [Definitions]
iter [Conditions]
iter [Letify.Sigma]
iter [Splitter]
iter [Lang.Alpha]
iter [Lang.F.Check]
iter [Model.Registry]
iter [Model]
iter [RefUsage]
iter [Map.S]
iter f m applies f to all bindings in map m.
iter [Wp.Memory.Sigma]
iter [Wp.Conditions]
iter [Wp.Definitions]
iter [Wp.Splitter]
iter [Wp.Lang.Alpha]
iter [Wp.Lang.F.Check]
iter [Wp.Model.Registry]
iter [Wp.Model]
iter [Wp.RefUsage]
iter [FCMap.S]
iter f m applies f to all bindings in map m.
iter2 [Memory.Sigma]
iter2 [Wp.Memory.Sigma]
iter_edges [Cil2cfg]
iter_ip [VC]
iter_ip [Wp.VC]
iter_kf [VC]
iter_kf [Wp.VC]
iter_lemmas [LogicUsage]
iter_lemmas [Wp.LogicUsage]
iter_nodes [Cil2cfg]
iter_on_goals [Wpo]
Dynamically exported.
iter_session [Register]
iter_sorted [Model.Registry]
iter_sorted [Wp.Model.Registry]
iteri [Conditions]
iteri [Wp.Conditions]

J
job [Wp_parameters]
job_key [Register]
join [Memory.Sigma]
pairwise equal
join [Passive]
join [Wp.Memory.Sigma]
pairwise equal
join [Wp.Passive]

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

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_assigns [NormAtLabels]
labels_loop_assigns [Wp.NormAtLabels]
labels_loop_inv [NormAtLabels]
labels_loop_inv [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]
language_of_name [VCS]
language_of_name [Wp.VCS]
language_of_prover [VCS]
language_of_prover [Wp.VCS]
language_of_prover_name [VCS]
language_of_prover_name [Wp.VCS]
launch [Register]
ldomain [Cvalues]
lemma [LogicSemantics.Make]
lemma [LogicCompiler.Make]
lemma [Wp.LogicSemantics.Make]
lemma [Wp.LogicCompiler.Make]
lemma_id [Lang]
lemma_id [Wp.Lang]
length [Splitter]
length [Wp.Splitter]
letify [Conditions]
letify [Wp.Conditions]
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]
literal [Memory.Model]
Return the memory location of a constant string, the id is a unique identifier.
literal [Wp.Memory.Model]
Return the memory location of a constant string, the id is a unique identifier.
load [Memory.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.Memory.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.
loadscripts [Proof]
Load scripts from -wp-script f.
loc [Cvalues.Logic]
loc [Splitter]
loc [Wp.Splitter]
loc_diff [Memory.Model]
Compute the length in bytes between two memory locations
loc_diff [Wp.Memory.Model]
Compute the length in bytes between two memory locations
loc_eq [Memory.Model]
loc_eq [Wp.Memory.Model]
loc_leq [Memory.Model]
Memory location comparisons
loc_leq [Wp.Memory.Model]
Memory location comparisons
loc_lt [Memory.Model]
loc_lt [Wp.Memory.Model]
loc_neq [Memory.Model]
loc_neq [Wp.Memory.Model]
loc_of_exp [CodeSemantics.Make]
loc_of_exp [Wp.CodeSemantics.Make]
loc_of_int [Memory.Model]
Cast a term representing a pointer to a c_object into a memory location
loc_of_int [Wp.Memory.Model]
Cast a term representing a pointer to a c_object into a memory location
loc_of_term [LogicSemantics.Make]
loc_of_term [Wp.LogicSemantics.Make]
local [Lang]
local [Wp.Lang]
location [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 [Clabels]
lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.
lookup [Wp.Clabels]
lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.
lookup_name [Clabels]
lookup_name [Wp.Clabels]
loop_entry [Mcfg.S]
loop_entry [Wp.Mcfg.S]
loop_head_label [Clabels]
loop_head_label [Wp.Clabels]
loop_step [Mcfg.S]
loop_step [Wp.Mcfg.S]
lval [CodeSemantics.Make]
lval [Wp.CodeSemantics.Make]

M
main [Register]
make [GuiNavigator]
make [Wpo.GOAL]
make_output_dir [Wp_parameters]
make_type [Datatype.Hashtbl]
map [Cvalues.Logic]
map [Vset]
map [Splitter]
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 [Wp.Vset]
map [Wp.Splitter]
map [FCMap.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_l2t [Cvalues.Logic]
map_loc [Cvalues.Logic]
map_logic [Cvalues]
map_opp [Cvalues.Logic]
map_opp [Vset]
map_opp [Wp.Vset]
map_sloc [Cvalues]
map_t2l [Cvalues.Logic]
map_value [Cvalues]
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.
mapi [FCMap.S]
Same as FCMap.S.map, but the function receives as arguments both the key and the associated value for each binding of the map.
mark [Splitter]
mark [Wp.Splitter]
mark_e [Lang.F]
mark_e [Wp.Lang.F]
mark_p [Lang.F]
mark_p [Wp.Lang.F]
marker [Lang.F]
marker [Wp.Lang.F]
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 [FCMap.S]
Same as FCMap.S.min_binding, but returns the largest binding of the given map.
max_elt [FCSet.S]
Same as , but returns the largest element of the given set.
mem [Memory.Sigma]
mem [Model.Registry]
mem [Parameter_sig.Set]
Does the given element belong to the set?
mem [Wprop.Indexed2]
mem [Wprop.Indexed]
mem [Map.S]
mem x m returns true if m contains a binding for x, and false otherwise.
mem [Wp.Memory.Sigma]
mem [Wp.Model.Registry]
mem [FCMap.S]
mem x m returns true if m contains a binding for x, and false otherwise.
mem_at [LogicSemantics.Make]
mem_at [LogicCompiler.Make]
mem_at [Wp.LogicSemantics.Make]
mem_at [Wp.LogicCompiler.Make]
mem_at_frame [LogicSemantics.Make]
mem_at_frame [LogicCompiler.Make]
mem_at_frame [Wp.LogicSemantics.Make]
mem_at_frame [Wp.LogicCompiler.Make]
mem_frame [LogicSemantics.Make]
mem_frame [LogicCompiler.Make]
mem_frame [Wp.LogicSemantics.Make]
mem_frame [Wp.LogicCompiler.Make]
member [Vset]
member [Wp.Vset]
memo [Datatype.Hashtbl]
memo tbl k f returns the binding of k in tbl.
memoize [Model.Registry]
with circularity protection
memoize [Wp.Model.Registry]
with circularity protection
memory [Factory]
memory [Wp.Factory]
merge [Memory.Sigma]
merge [Region]
merge [Conditions]
merge [Letify.Defs]
merge [Splitter]
merge [Matrix]
merge [Mcfg.S]
merge [Ctypes]
merge [Map.S]
merge f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.
merge [Wp.Memory.Sigma]
merge [Wp.Conditions]
merge [Wp.Splitter]
merge [Wp.Mcfg.S]
merge [FCMap.S]
merge f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.
merge [Wp.Ctypes]
merge_all [Splitter]
merge_all [Wp.Splitter]
merge_assign_info [WpPropId]
merge_assign_info [Wp.WpPropId]
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 [FCMap.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_elt [FCSet.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.
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_establish_id [WpPropId]
Invariant establishment
mk_establish_id [Wp.WpPropId]
Invariant establishment
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_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_logic_label [Clabels]
create a virtual label to a statement (it can have no label)
mk_logic_label [Wp.Clabels]
create a virtual label to a statement (it can have no label)
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_label [Clabels]
mk_loop_label [Wp.Clabels]
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_preserve_id [WpPropId]
Invariant preservation
mk_preserve_id [Wp.WpPropId]
Invariant preservation
mk_property [WpPropId]
mk_property [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_label [Clabels]
mk_stmt_label [Wp.Clabels]
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 [LogicSemantics.Make]
move [LogicCompiler.Make]
move [Wp.LogicSemantics.Make]
move [Wp.LogicCompiler.Make]

N
name [Model.Data]
name [Model.Entries]
name [Context]
name [Wp_error]
name [Wp.Model.Data]
name [Wp.Model.Entries]
name [Wp.Context]
name_of_mode [VCS]
name_of_mode [Wp.VCS]
name_of_prover [VCS]
name_of_prover [Wp.VCS]
natural_id [Matrix]
name for elements in NATURAL
nearest_elt_ge [FCSet.S]
nearest_elt_ge v s returns the smallest element of s that is bigger or equal to v.
nearest_elt_le [FCSet.S]
nearest_elt_le v s returns the largest element of s that is smaller or equal to v.
negate [Cvalues]
new_env [LogicSemantics.Make]
new_env [LogicCompiler.Make]
new_env [Mcfg.S]
optionally init env with user logic variables
new_env [Wp.LogicSemantics.Make]
new_env [Wp.LogicCompiler.Make]
new_env [Wp.Mcfg.S]
optionally init env with user logic variables
new_gamma [Lang]
new_gamma [Wp.Lang]
new_loop_computation [WpStrategy]
new_pool [Lang]
new_pool [Wp.Lang]
nil [Conditions]
nil [Wp.Conditions]
no_infinite_array [Ctypes]
no_infinite_array [Wp.Ctypes]
no_result [VCS]
no_result [Wp.VCS]
node_stmt_opt [Cil2cfg]
node_type [Cil2cfg]
normalize [WpStrategy]
not_yet_implemented [Wp_error]
null [Memory.Model]
Return the location of the null pointer
null [Cvalues]
test for null pointer value
null [Wp.Memory.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 [LogicSemantics.Make]
occurs [Memory.Model]
Test if a location depend on a given logic variable
occurs [Region]
occurs [Vset]
occurs [Conditions]
occurs [Lang.F]
occurs [Wp.LogicSemantics.Make]
occurs [Wp.Memory.Model]
Test if a location depend on a given logic variable
occurs [Wp.Vset]
occurs [Wp.Conditions]
occurs [Wp.Lang.F]
occursp [Lang.F]
occursp [Wp.Lang.F]
of_array [Matrix]
of_pred [Definitions.Trigger]
of_pred [Wp.Definitions.Trigger]
of_real [Cint]
of_real [Wp.Cint]
of_term [Definitions.Trigger]
of_term [Wp.Definitions.Trigger]
off [Parameter_sig.Bool]
Set the boolean to false.
on [Parameter_sig.Bool]
Set the boolean to true.
on_global [Model]
on_scope None
on_global [Wp.Model]
on_scope None
on_kf [Model]
on_scope (Some kf)
on_kf [Wp.Model]
on_scope (Some kf)
on_model [Model]
on_model [Wp.Model]
on_reload [GuiPanel]
on_scope [Model]
on_scope [Wp.Model]
on_update [GuiPanel]
once [Context]
A global configure, executed once.
once [Wp.Context]
A global configure, executed once.
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 <=

P
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_bind [Lang.F]
p_bind [Wp.Lang.F]
p_bool [Lang.F]
p_bool [Wp.Lang.F]
p_bools [Lang.F]
p_bools [Wp.Lang.F]
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_equal [Lang.F]
p_equal [Wp.Lang.F]
p_equiv [Lang.F]
p_equiv [Wp.Lang.F]
p_exists [Lang.F]
p_exists [Wp.Lang.F]
p_false [Lang.F]
p_false [Wp.Lang.F]
p_float [ProverTask]
Float group pattern \([0-9.]+\)
p_forall [Lang.F]
p_forall [Wp.Lang.F]
p_group [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_int [ProverTask]
Int group pattern \([0-9]+\)
p_iter [Lang.F]
p_iter [Wp.Lang.F]
p_leq [Lang.F]
p_leq [Wp.Lang.F]
p_lt [Lang.F]
p_lt [Wp.Lang.F]
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_string [ProverTask]
String group pattern "\(...\)"
p_subst [Lang.F]
p_subst [Wp.Lang.F]
p_true [Lang.F]
p_true [Wp.Lang.F]
p_until_space [ProverTask]
No space group pattern "\\(^ \t\n*\\)"
p_vars [Lang.F]
Sorted
p_vars [Wp.Lang.F]
Sorted
param [MemVar.VarUsage]
param [Wp.MemVar.VarUsage]
parameters [Lang]
definitions
parameters [Wp.Lang]
definitions
parse [Factory]
Apply specifications to default setup.
parse [ProverWhy3]
parse [Wp.Factory]
Apply specifications to default setup.
parse_coqproof [Proof]
parse_coqproof f parses a coq-file f and fetch the first proof.
parse_scripts [Proof]
parse_scripts f parses all scripts from file f and put them in the database.
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.
partition [FCMap.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' infomation.
parts_of_id [Wp.WpPropId]
get the 'part' infomation.
path [Region]
Empty, but Full for the path
plain [Cvalues]
pointer [MemTyped]
pointer [Lang]
type of pointers
pointer [Wp.MemTyped]
pointer [Wp.Lang]
type of pointers
pointer_loc [Memory.Model]
???
pointer_loc [Wp.Memory.Model]
???
pointer_val [Memory.Model]
???
pointer_val [Wp.Memory.Model]
???
poly [Lang]
polymorphism
poly [Wp.Lang]
polymorphism
pool [Plang]
pop [Context]
pop [Wp.Context]
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_bound [Vset]
pp_bound [Wp.Vset]
pp_call_type [Cil2cfg]
pp_calls [Dyncall]
pp_clause [Separation]
Prints the separation in ACSL format.
pp_clause [Wp.Separation]
Prints the separation in ACSL format.
pp_cluster [Definitions]
pp_cluster [Wp.Definitions]
pp_concat [Vlist]
pp_depend [Wpo]
pp_dependencies [Wpo]
pp_dependency [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_float [Ctypes]
pp_float [Wp.Ctypes]
pp_frame [LogicSemantics.Make]
pp_frame [LogicCompiler.Make]
pp_frame [Wp.LogicSemantics.Make]
pp_frame [Wp.LogicCompiler.Make]
pp_function [Wpo]
pp_goal [Wpo]
pp_goal_flow [Wpo]
pp_index [Wpo]
pp_info_of_strategy [WpStrategy]
pp_int [Ctypes]
pp_int [Wp.Ctypes]
pp_language [VCS]
pp_language [Wp.VCS]
pp_logfile [Wpo]
pp_logic [LogicAssigns.Logic]
pp_logic [LogicSemantics.Make]
pp_logic [Wp.LogicSemantics.Make]
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_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 [LogicAssigns.Logic]
pp_region [LogicSemantics.Make]
pp_region [Separation]
Prints region in ACSL format
pp_region [Wp.LogicSemantics.Make]
pp_region [Wp.Separation]
Prints region in ACSL format
pp_result [VCS]
pp_result [Wp.VCS]
pp_sloc [LogicAssigns.Logic]
pp_sloc [LogicSemantics.Make]
pp_sloc [Wp.LogicSemantics.Make]
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_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_wp_parameters [Register]
pred [LogicSemantics.Make]
pred [LogicCompiler.Make]
pred [Lang.F]
pred [Wp.LogicSemantics.Make]
pred [Wp.LogicCompiler.Make]
pred [Wp.Lang.F]
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]
preproc_label [NormAtLabels]
preproc_label [Wp.NormAtLabels]
pretty [ProverWhy3.Goal]
pretty [Why3_xml]
pretty [Wpo.DISK]
pretty [Memory.Model]
pretty printing of memory location
pretty [Memory.Sigma]
pretty [Memory.Chunk]
pretty [Cstring]
pretty [Region]
pretty [Vset]
pretty [Pcond]
pretty [Letify.Sigma]
pretty [Splitter]
pretty [Passive]
pretty [Model.Key]
pretty [Model.Entries]
pretty [Warning]
pretty [Mcfg.S]
pretty [WpPropId]
pretty [Clabels]
pretty [Ctypes]
pretty [Rformat]
pretty [Wp.Memory.Model]
pretty printing of memory location
pretty [Wp.Memory.Sigma]
pretty [Wp.Memory.Chunk]
pretty [Wp.Passive]
pretty [Wp.Cstring]
pretty [Wp.Vset]
pretty [Wp.Splitter]
pretty [Wp.Model.Key]
pretty [Wp.Model.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]
print_generated [Wp_parameters]
print the given file if the debugging category "print-generated" is set
promote [Ctypes]
promote [Wp.Ctypes]
proof [VC]
List of proof obligations computed for a given property.
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 [Dyncall]
Returns an property identifier for the precondition.
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.
protect [Wp_error]
protect_function [Wp_error]
protect_map [Wp_error]
protect_translation [Wp_error]
protect_translation3 [Wp_error]
protect_translation4 [Wp_error]
protect_translation5 [Wp_error]
prove [VC]
Returns a ready-to-schedule task.
prove [Prover]
prove [ProverWhy3ide]
prove [ProverWhy3]
The string must be a valid why3 prover identifier Return NoResult if it is already proved by Qed
prove [ProverCoq]
prove [ProverErgo]
prove [Wp.VC]
Returns a ready-to-schedule task.
proved [Register]
prover_of_name [Wpo]
Dynamically exported.
prover_of_name [VCS]
prover_of_name [Wp.VCS]
provers [Register]
pruning [Conditions]
pruning [Wp.Conditions]
push [Context]
push [Wp.Context]

Q
qed_time [Wpo.GOAL]

R
range [Vset]
range [Cfloat]
range [Cint]
Dependent on model
range [Wp.Cfloat]
range [Wp.Cint]
Dependent on model
range [Wp.Vset]
rdescr [Cvalues.Logic]
real_of_int [Cfloat]
real_of_int [Wp.Cfloat]
record [Lang]
record [Wp.Lang]
region [LogicSemantics.Make]
region [LogicCompiler.Make]
region [Wp.LogicSemantics.Make]
region [Wp.LogicCompiler.Make]
register [GuiPanel]
register [Register]
register [Model]
register [Wp.Model]
release [Lang.F]
release [Wp.Lang.F]
reload [GuiPanel]
remove [VC]
remove [Wpo]
remove [Cil2cfg.HEsig]
remove [Wp.VC]
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 [FCMap.S]
remove x m returns a map containing the same bindings as m, except for x which is unbound in the returned map.
replace [Cil2cfg.HEsig]
repr [Model]
repr [Wp.Model]
requires [Separation]
Filter out is_true clauses
requires [Wp.Separation]
Filter out is_true clauses
reset [Lang.F.Check]
reset [Wp_parameters]
reset [Wp.Lang.F.Check]
resolve [Wpo.VC_Annot]
resolve [Wpo]
result [VCS]
result [LogicSemantics.Make]
result [LogicCompiler.Make]
result [Wp.VCS]
result [Wp.LogicSemantics.Make]
result [Wp.LogicCompiler.Make]
return [LogicSemantics.Make]
return [LogicCompiler.Make]
return [CodeSemantics.Make]
return [Mcfg.S]
return [Wp.LogicSemantics.Make]
return [Wp.LogicCompiler.Make]
return [Wp.CodeSemantics.Make]
return [Wp.Mcfg.S]
rpath [Region]
Empty, but Full for the r-paths
run [Register]
run [ProverWhy3ide]
run_and_prove [GuiPanel]
run_once_for_each_ast [Model]
run the function once for each ast
run_once_for_each_ast [Wp.Model]
run the function once for each ast

S
same_edge [Cil2cfg]
same_node [Cil2cfg]
savescripts [Proof]
If necessary, dump the scripts database into the file specified by -wp-script f.
scheduled [Register]
scope [Memory.Model]
Manage the scope of variables.
scope [Mcfg.S]
scope [Wp.Memory.Model]
Manage the scope of variables.
scope [Wp.Mcfg.S]
script_for [Proof]
script_for_ide [Proof]
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).
self [Memory.Chunk]
Chunk names, for pretty-printing
self [Wp.Memory.Chunk]
Chunk names, for pretty-printing
separated [LogicSemantics.Make]
separated [Memory.Model]
Return the formula that tests if two segment are separated
separated [Cvalues.Logic]
separated [Wp.LogicSemantics.Make]
separated [Wp.Memory.Model]
Return the formula that tests if two segment are separated
separation [MemVar.VarUsage]
separation [Memory.Model]
separation [Wp.MemVar.VarUsage]
separation [Wp.Memory.Model]
seq_branch [Conditions]
seq_branch [Wp.Conditions]
seq_list [Conditions]
seq_list [Wp.Conditions]
sequence [Register]
sequence [Pcond]
sequence [Conditions]
sequence [Wp.Conditions]
server [VC]
Default number of parallel tasks is given by -wp-par command-line option.
server [ProverTask]
server [Wp.VC]
Default number of parallel tasks is given by -wp-par command-line option.
session [Register]
set [Lang.F.Check]
set [Context]
Define the current value.
set [Wp.Lang.F.Check]
set [Wp.Context]
Define the current value.
set_builtin_1 [Lang.F]
set_builtin_1 [Wp.Lang.F]
set_builtin_2 [Lang.F]
set_builtin_2 [Wp.Lang.F]
set_builtin_eqp [Lang.F]
set_builtin_eqp [Wp.Lang.F]
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_range [Parameter_sig.Int]
Set what is the possible range of values for this parameter.
set_result [Wpo]
severe [Warning]
severe [Wp.Warning]
shift [Memory.Model]
Return the memory location obtained by array access at an index represented by the given term.
shift [Cvalues.Logic]
shift [Wp.Memory.Model]
Return the memory location obtained by array access at an index represented by the given term.
sigma [LogicSemantics.Make]
sigma [LogicCompiler.Make]
sigma [Wp.LogicSemantics.Make]
sigma [Wp.LogicCompiler.Make]
signed [Ctypes]
true if signed
signed [Wp.Ctypes]
true if signed
simplify [Mcfg.Splitter]
simplify [Wp.Mcfg.Splitter]
singleton [Vset]
singleton [Splitter]
singleton [Map.S]
singleton x y returns the one-element map that contains a binding y for x.
singleton [Wp.Vset]
singleton [Wp.Splitter]
singleton [FCMap.S]
singleton x y returns the one-element map that contains a binding y for x.
size [Matrix]
sizeof_defined [Ctypes]
sizeof_defined [Wp.Ctypes]
sizeof_object [Ctypes]
sizeof_object [Wp.Ctypes]
skip [Script]
sloc [Cvalues.Logic]
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 [Prover]
spawn [ProverTask]
Spawn all the tasks over the server and retain the first 'validated' one.
spawn [Wp.VC]
Same as prove but schedule the tasks into the global server returned by server function below.
spawn_wp_proofs_iter [Register]
split [WpAnnot]
splits a prop_id goals into prop_id parts for each sub-goals
split [Mcfg.Splitter]
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 [Wp.Mcfg.Splitter]
split [FCMap.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.
spy [Register]
start_edge [Cil2cfg]
get the starting edges
start_stmt_of_node [Cil2cfg]
status [LogicSemantics.Make]
status [LogicCompiler.Make]
status [Wp.LogicSemantics.Make]
status [Wp.LogicCompiler.Make]
step [Conditions]
step [Wp.Conditions]
stepout [VCS]
stepout [Wp.VCS]
stored [Memory.Model]
Return a set of formula that express a modification between two memory state.
stored [Wp.Memory.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]
str_len [Wp.Cstring]
str_val [Cstring]
The array containing all char of the constant
str_val [Wp.Cstring]
The array containing all 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_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_float [Ctypes]
sub_c_float [Wp.Ctypes]
sub_c_int [Ctypes]
sub_c_int [Wp.Ctypes]
sub_range [Vset]
sub_range [Wp.Vset]
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 [Region]
subset [Vset]
subset [Wp.Vset]
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
target [WpAnnot]
tau [Matrix]
tau_of_chunk [Memory.Chunk]
tau_of_chunk [Wp.Memory.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_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]
term [LogicSemantics.Make]
term [LogicCompiler.Make]
term [Wp.LogicSemantics.Make]
term [Wp.LogicCompiler.Make]
test [Mcfg.S]
test [Wp.Mcfg.S]
timeout [VCS]
timeout [Wp.VCS]
to_cint [Cint]
Raises Not_found if not.
to_cint [Wp.Cint]
Raises Not_found if not.
token [Script]
tracelog [Register]
trigger [LogicCompiler.Make]
trigger [Wp.LogicCompiler.Make]
trivial [Wpo.GOAL]
try_sequence [Register]
type_id [Lang]
type_id [Wp.Lang]

U
union [Memory.Sigma]
union [Cvalues.Logic]
union [Vset]
union [Splitter]
union [Passive]
union [Map.S]
union f m1 m2 computes a map whose keys is the union of keys of m1 and of m2.
union [Wp.Memory.Sigma]
union [Wp.Passive]
union [Wp.Vset]
union [Wp.Splitter]
unknown [VCS]
unknown [Wp.VCS]
unreachable_nodes [Cil2cfg]
unsupported [Wp_error]
update [GuiPanel]
update [Region]
update [Model.Registry]
set current value, with no protection
update [Context]
Modification of the current value
update [Wp.Model.Registry]
set current value, with no protection
update [Wp.Context]
Modification of the current value
update_hints_for_goal [Proof]
Update the hints for one specific goal.
update_symbol [Definitions]
update_symbol [Wp.Definitions]
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 [CodeSemantics.Make]
val_of_exp [Wp.CodeSemantics.Make]
val_of_term [LogicSemantics.Make]
val_of_term [Wp.LogicSemantics.Make]
valid [VCS]
valid [LogicSemantics.Make]
valid [Memory.Model]
Return the formula that tests if a memory state is valid (according to Memory.acs) in the given memory state at the given segment.
valid [Cvalues.Logic]
valid [Wp.VCS]
valid [Wp.LogicSemantics.Make]
valid [Wp.Memory.Model]
Return the formula that tests if a memory state is valid (according to Wp.Memory.acs) in the given memory state at the given segment.
value [Memory.Sigma]
value [Cvalues.Logic]
value [Wp.Memory.Sigma]
variables [Lang]
variables [Wp.Lang]
vars [LogicAssigns.Logic]
vars [LogicAssigns.Make]
vars [LogicSemantics.Make]
vars [Memory.Model]
Return the logic variables from which the given location depend on.
vars [Region]
vars [Vset]
vars [Definitions.Trigger]
vars [Wp.LogicSemantics.Make]
vars [Wp.Memory.Model]
Return the logic variables from which the given location depend on.
vars [Wp.Vset]
vars [Wp.Definitions.Trigger]
vars_hyp [Conditions]
vars_hyp [Wp.Conditions]
vars_seq [Conditions]
vars_seq [Wp.Conditions]
varsp [Lang.F]
varsp [Wp.Lang.F]
very_strange_loops [Cil2cfg]
detect is there are natural loops where we didn't manage to compute back edges (see mark_loops).
vset [Cvalues.Logic]

W
warnings [Wpo]
with_current_loc [Context]
with_current_loc [Wp.Context]
with_model [Model]
with_model [Wp.Model]
without_assume [Lang]
without_assume [Wp.Lang]
wp_iter_model [Register]
wp_print_separation [Register]

X
xmark [Plang]
xmark_e [Plang]
xmark_hyp [Pcond]
xmark_p [Plang]
xmark_seq [Pcond]