Up  

Index of values


( * ) [Lang.N]
F.p_mul
( * ) [Wp.Lang.N]
F.p_mul
($$) [Lang.N]
Lang.F.p_call
($$) [Wp.Lang.N]
Wp.Lang.F.p_call
($) [Lang.N]
Lang.F.e_fun
($) [Wp.Lang.N]
Wp.Lang.F.e_fun
(&&) [Lang.N]
Lang.F.p_and
(&&) [Wp.Lang.N]
Wp.Lang.F.p_and
(+) [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]
Lang.F.p_lt
(<) [Wp.Lang.N]
Wp.Lang.F.p_lt
(<=) [Lang.N]
Lang.F.p_leq
(<=) [Wp.Lang.N]
Wp.Lang.F.p_leq
(<>) [Lang.N]
Lang.F.p_neq
(<>) [Wp.Lang.N]
Wp.Lang.F.p_neq
(=) [Lang.N]
Lang.F.p_equal
(=) [Wp.Lang.N]
Wp.Lang.F.p_equal
(>) [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
(mod) [Lang.N]
F.p_mod
(mod) [Wp.Lang.N]
F.p_mod
(||) [Lang.N]
Lang.F.p_or
(||) [Wp.Lang.N]
Wp.Lang.F.p_or
(~-) [Lang.N]
fun x -> p_sub 0 x
(~-) [Wp.Lang.N]
fun x -> p_sub 0 x

A
a_base [MemTyped]
a_base [Wp.MemTyped]
a_offset [MemTyped]
a_offset [Wp.MemTyped]
a_prover [ProofScript]
a_tactic [ProofScript]
absurd [Auto]
absurd [Wp.Auto]
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 [Set.S]
add x s returns a set containing all elements of s, plus x.
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_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_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]
add_var [Lang.F]
add_var [Wp.Lang.F]
add_vars [Lang.F]
add_vars [Wp.Lang.F]
age [Wpo]
ainf [Cvalues]
Array lower-bound, ie `Some(0)`
alloc_domain [Plang]
alloc_e [Plang]
alloc_hyp [Pcond]
alloc_p [Plang]
alloc_seq [Pcond]
alloc_xs [Plang]
anchor [ProofEngine]
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 [Mstate]
apply [Memory.Model]
Propagate a sequent substitution inside the memory state.
apply [Cvalues.Logic]
apply [Passive]
apply [Wp.Mstate]
apply [Wp.Memory.Model]
Propagate a sequent substitution inside the memory state.
apply [Wp.Passive]
apply_add [Cvalues.Logic]
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 [Lang]
array [Wp.Auto]
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_goal [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)`
at [Tactical]
at [Pcfg]
at [Wp.Tactical]
at_closure [Conditions]
register a transformation applied just before close
at_closure [Wp.Conditions]
register a transformation applied just before close
atype [Lang]
atype [Wp.Lang]
auto_check [Register]
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
axiomatic [Definitions]
axiomatic [LogicUsage]
axiomatic [Wp.Definitions]
axiomatic [Wp.LogicUsage]

B
backtrack [ProverSearch]
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 [Lang.F]
basename [LogicUsage]
Trims the original name
basename [Ctypes]
basename [Wp.Lang.F]
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 [ProofEngine]
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 [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 [Conditions]
branch [Wp.Conditions]
branching [Pcfg]
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]
bundle [Conditions]
bundle [Wp.Conditions]
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_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]
cancel [ProofEngine]
cardinal [TacInstance]
less than limit
cardinal [Map.S]
Return the number of bindings of a map.
cardinal [Set.S]
Return the number of elements of a set.
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]
checkbox [Tactical]
Unless specified, default is false.
checkbox [Wp.Tactical]
Unless specified, default is false.
checked [VCS]
checked [Wp.VCS]
children [ProofEngine]
choice [Auto]
choice [Wp.Auto]
choose [Map.S]
Return one binding of the given map, or raise Not_found if the map is empty.
choose [Set.S]
Return one element of the given set, or raise Not_found if the set is empty.
choose [FCMap.S]
Return one binding of the given map, or raise Not_found if the map is empty.
cint [Tactical]
cint [Wp.Tactical]
clean [Conditions]
clean [Wp.Conditions]
clear [VC]
clear [Wpo]
clear [Proof]
clear [Model.Generator]
clear [Model.Registry]
clear [Context]
Clear the current value.
clear [Cil2cfg.HEsig]
clear [Wp.VC]
clear [Wp.Model.Generator]
clear [Wp.Model.Registry]
clear [Wp.Context]
Clear the current value.
clear_results [Wpo]
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
commit [ProofEngine]
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 [Lang.F]
compare [Model.Key]
compare [Model.Entries]
compare [Warning]
compare [Clabels.T]
compare [Ctypes.AinfoComparable]
compare [Ctypes]
compare [Map.S]
Total ordering between maps.
compare [Set.S]
Total ordering between sets.
compare [Wp.VCS]
compare [Wp.Memory.Chunk]
compare [Wp.LogicBuiltins]
compare [Wp.Lang.F]
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]
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.Auto.Range]
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 [ProofScript]
configure [VCS]
configure [Memory.Model]
configure [Cfloat]
configure [Cint]
configure [Context]
Apply global configure hooks, once per project/ast.
configure [Wp.VCS]
configure [Wp.Factory]
configure [Wp.Memory.Model]
configure [Wp.Cfloat]
configure [Wp.Cint]
configure [Wp.Context]
Apply global configure hooks, once per project/ast.
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]
contrapose [Auto]
contrapose [Wp.Auto]
convert [Cfloat]
convert [Cint]
Independent from model
convert [Lang.Alpha]
convert [Wp.Cfloat]
convert [Wp.Cint]
Independent 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 [Tactical.Fmap]
create [Pcfg]
create [Mstate]
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.Tactical.Fmap]
create [Wp.Mstate]
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 [ProofEngine]
current [VCS]
Current parameters
current [Cint]
current [Wp.VCS]
Current parameters
current [Wp.Cint]
cut [Auto]
cut [Wp.Auto]
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]
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]
default [Factory]
"Var,Typed,Nat,Real" memory model.
default [Tactical]
default [VCS]
all None
default [Wp.Tactical]
default [Wp.VCS]
all None
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.
definition [Auto]
definition [Wp.Auto]
defs [Lang.F]
defs [Wp.Lang.F]
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]
depth [ProverTask]
descr [Factory]
descr [Vset]
descr [LogicBuiltins]
descr [Wp.Factory]
descr [Wp.Vset]
descr [Wp.LogicBuiltins]
destruct [Tactical]
destruct [Wp.Tactical]
detect_provers [ProverWhy3]
detect_why3 [ProverWhy3]
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 [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_report_prover_stats [Register]
do_report_scheduled [Register]
do_tac_result [Register]
do_tac_success [Register]
do_update_session [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 [Conditions]
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 [Letify.Defs]
domain [Letify.Sigma]
domain [Wp.Conditions]
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]
downcast [Cint]
Dependent on model
downcast [Wp.Cint]
Dependent on model
driver [LogicBuiltins]
driver [Wp.LogicBuiltins]
dummy [Wpo.GOAL]
dump [Pcond]
dump [LogicBuiltins]
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_add [Lang.F]
e_add [Wp.Lang.F]
e_and [Lang.F]
e_and [Wp.Lang.F]
e_apply [Letify.Sigma]
e_apply [Lang.Subst]
e_apply [Wp.Lang.Subst]
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_cnf [WpTac]
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_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_hexfloat [Lang.F]
e_hexfloat [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_mod [Lang.F]
e_mod [Wp.Lang.F]
e_mthfloat [Lang.F]
e_mthfloat [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_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 [Wp.Lang.F]
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
either [Conditions]
either [Wp.Conditions]
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 [Memory.Sigma]
empty [Region]
empty [Vset]
empty [Letify.Defs]
empty [Letify.Sigma]
empty [Splitter]
empty [Passive]
empty [Mcfg.S]
empty [Map.S]
The empty map.
empty [Set.S]
The empty set.
empty [Wp.Conditions]
empty [Wp.Memory.Sigma]
empty [Wp.Vset]
empty [Wp.Splitter]
empty [Wp.Passive]
empty [Wp.Mcfg.S]
empty [FCMap.S]
The empty map.
empty_acc [WpStrategy]
empty_assigns_info [WpPropId]
empty_assigns_info [Wp.WpPropId]
encode [ProofScript]
end_session [Register]
env [Strategy]
env [Repr]
Create environment from a set of free variables
env [Lang.F]
env [Wp.Strategy]
env [Wp.Repr]
Create environment from a set of free variables
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]
epsilon [Lang]
epsilon [Rformat]
epsilon [Wp.Lang]
eqp [Lang.F]
eqp [Wp.Lang.F]
equal [Mstate]
equal [Vset]
equal [Letify.Sigma]
equal [Lang.F]
Same as ==
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 [Set.S]
equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.
equal [Wp.Mstate]
equal [Wp.Vset]
equal [Wp.Lang.F]
Same as ==
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]
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]
exists [ProofSession]
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 [Set.S]
exists p s checks if at least one element of the set satisfies 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 [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_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_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_iabs [Cfloat]
f_iabs [Wp.Cfloat]
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_rabs [Cfloat]
f_rabs [Wp.Cfloat]
f_repeat [Vlist]
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 [TacHavoc.Havoc]
field [Mstate]
field [Memory.Model]
Return the memory location obtained by field access from a given memory location
field [Cvalues.Logic]
field [Repr]
field [Lang]
field [Wp.Mstate]
field [Wp.Memory.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 [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_kf [Wpo.DISK]
file_logerr [Wpo.DISK]
file_logout [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 [Map.S]
filter p m returns the map with all the bindings in m that satisfy predicate p.
filter [Set.S]
filter p s returns the set of all elements in s 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 [TacLemma]
find [Pcfg]
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 [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 [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]
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_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.
find_symbol [Definitions]
find_symbol [Wp.Definitions]
first [ProverSearch]
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]
fmode [TacCut]
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 [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 [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 [Set.S]
for_all p s checks if all elements of the set 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.
fork [ProofEngine]
formal [LogicCompiler.Make]
formal [Wp.LogicCompiler.Make]
forward [ProofEngine]
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.
fresh [Lang.F]
fresh [Wp.Lang.F]
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 [ProofEngine]
get [Tactical.Fmap]
raises Not_found if absent
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.Tactical.Fmap]
raises Not_found if absent
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 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_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_depth [VCS]
0 means prover default
get_depth [Wp.VCS]
0 means prover default
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 beginning 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]
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_sequent [VC]
get_sequent [Wp.VC]
get_session [Wp_parameters]
get_session_dir [Wp_parameters]
get_stepout [VCS]
0 means no-stepout
get_stepout [Wp.VCS]
0 means no-stepout
get_steps [Wpo]
get_strategies [ProofEngine]
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_timeout [VCS]
0 means no-timeout
get_timeout [Wp.VCS]
0 means no-timeout
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]
go_status [GuiProver]
goal [ProofEngine]
goals_of_property [Wpo]
All POs related to a given property.
goto [ProofEngine]
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]
whether 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
has_verdict [Wpo]
hash [Memory.Chunk]
hash [Lang.F]
Constant time
hash [Ctypes.AinfoComparable]
hash [Ctypes]
hash [Wp.Memory.Chunk]
hash [Wp.Lang.F]
Constant time
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 [Memory.Sigma]
havoc [Wp.Auto]
havoc [Wp.Memory.Sigma]
havoc_any [Memory.Sigma]
havoc_any [Wp.Memory.Sigma]
havoc_chunk [Memory.Sigma]
havoc_chunk [Wp.Memory.Sigma]
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
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]
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 [Wp.LogicBuiltins]
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]
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.
index [Conditions]
Compute steps' id of sequent left hand-side.
index [Mstate]
index [Wp.Conditions]
Compute steps' id of sequent left hand-side.
index [Wp.Mstate]
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
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 [CodeSemantics.Make]
instance_of [Wp.CodeSemantics.Make]
int [Tactical]
int [Wp.Tactical]
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 [Set.S]
Set intersection.
inter [Wp.Vset]
intersect [Conditions]
intersect [Lang.F]
intersect [Wp.Conditions]
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
intros [Conditions]
intros [Wp.Conditions]
intuition [Auto]
intuition [Wp.Auto]
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 positioned, and the variable is global, not extern, with a "const" type (see hasConstAttribute).
is_absorbant [Lang.F]
is_absorbant [Wp.Lang.F]
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_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 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_default [LogicBuiltins]
is_default [Wp.LogicBuiltins]
is_default_behavior [WpStrategy]
is_dnf [WpTac]
is_empty [Tactical]
is_empty [Proof]
is_empty [Conditions]
No step at all
is_empty [Wp.Tactical]
is_empty [Map.S]
Test whether a map is empty or not.
is_empty [Set.S]
Test whether a set is empty or not.
is_empty [Wp.Conditions]
No step at all
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_false [Lang.F]
Constant time.
is_false [Wp.Lang.F]
Constant time.
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_int [Lang.F]
Integer sort
is_int [Wp.Lang.F]
Integer sort
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_neutral [Lang.F]
is_neutral [Wp.Lang.F]
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_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]
is_proved [WpAnnot]
whether all partial proofs have been accumulated or not
is_proved [Wp.VC]
is_prover [ProofScript]
is_ptrue [Lang.F]
is_ptrue [Wp.Lang.F]
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_set [Lang.F.Check]
is_set [Wp.Lang.F.Check]
is_simple [Lang.F]
Constants, variables, functions of arity 0
is_simple [Wp.Lang.F]
Constants, variables, functions of arity 0
is_subterm [Lang.F]
is_subterm [Wp.Lang.F]
is_tactic [ProofScript]
is_tactic [Wpo]
is_tactic [WpPropId]
is_tactic [Wp.WpPropId]
is_trivial [VC]
is_trivial [Wpo.VC_Annot]
is_trivial [Wpo.VC_Lemma]
is_trivial [Wpo.GOAL]
is_trivial [Wpo]
is_trivial [Conditions]
is_trivial [Wp.VC]
is_trivial [Wp.Conditions]
is_true [Conditions]
Only true or empty steps
is_true [Cvalues]
p ? 1 : 0
is_true [Lang.F]
Constant time.
is_true [Separation]
Returns true if the clause is degenerated.
is_true [Wp.Conditions]
Only true or empty steps
is_true [Wp.Lang.F]
Constant time.
is_true [Wp.Separation]
Returns true if the clause is degenerated.
is_valid [Wpo]
true if the result is valid.
is_valid [VCS]
is_valid [Wp.VCS]
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 [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 [Memory.Model]
Debug
iter [Memory.Sigma]
iter [Definitions]
iter [Letify.Sigma]
iter [Splitter]
iter [Lang.Alpha]
iter [Lang.F.Check]
iter [Model.Registry]
iter [Model]
iter [RefUsage]
iter [Wp.Strategy]
iter [Wp.Tactical]
iter [Map.S]
iter f m applies f to all bindings in map m.
iter [Set.S]
iter f s applies f in turn to all elements of s.
iter [Wp.Conditions]
Iterate only over the head steps of the sequence
iter [Wp.Mstate]
iter [Wp.Memory.Model]
Debug
iter [Wp.Memory.Sigma]
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_composer [Tactical]
iter_composer [Wp.Tactical]
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]

J
job [Wp_parameters]
job_key [Register]
join [Memory.Sigma]
pairwise equal
join [Passive]
join [Wp.Memory.Sigma]
pairwise equal
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]
kfailed [VCS]
kfailed [Wp.VCS]
kind_of_id [WpPropId]
get the 'kind' information.
kind_of_id [Wp.WpPropId]
get the 'kind' information.
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_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]
lc_closed [Lang.F]
lc_closed [Wp.Lang.F]
lc_iter [Lang.F]
lc_iter [Wp.Lang.F]
lc_map [Lang.F]
lc_map [Wp.Lang.F]
ldomain [Cvalues]
lemma [Auto]
lemma [LogicSemantics.Make]
lemma [LogicCompiler.Make]
lemma [Conditions]
Performs existential, universal and hypotheses introductions
lemma [Wp.Auto]
lemma [Wp.LogicSemantics.Make]
lemma [Wp.LogicCompiler.Make]
lemma [Wp.Conditions]
Performs existential, universal and hypotheses introductions
lemma_id [Lang]
lemma_id [Wp.Lang]
length [Splitter]
length [Wp.Splitter]
letify [Conditions]
letify [Wp.Conditions]
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]
The internal list of steps
list [Wp.Conditions]
The internal list of steps
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 [ProofSession]
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]
locate [Footprint]
Locate the occurrence of select footprint inside a term.
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 [Strategy]
lookup [Tactical]
lookup [Footprint]
Retrieve back the k-th occurrence of a footprint inside a term.
lookup [Mstate]
lookup [Memory.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.Memory.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.
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]
main [ProofEngine]
make [GuiNavigator]
make [Strategy]
make [Wpo.GOAL]
make [Wp.Strategy]
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 [Set.S]
map f s is the set whose elements are f a0,f a1...
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_condition [Conditions]
map_condition [Wp.Conditions]
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]
map_sequence [Wp.Conditions]
map_sequent [Conditions]
map_sequent [Wp.Conditions]
map_sloc [Cvalues]
map_step [Conditions]
map_step [Wp.Conditions]
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.
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]
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]
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 [FCMap.S]
Same as FCMap.S.min_binding, 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 [FCSet.S]
Same as , but returns the largest element of the given set.
mem [Memory.Sigma]
mem [Model.Generator]
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 [Set.S]
mem x s tests whether x belongs to the set s.
mem [Wp.Memory.Sigma]
mem [Wp.Model.Generator]
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 [Conditions]
merge [Memory.Sigma]
merge [Region]
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.Conditions]
merge [Wp.Memory.Sigma]
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 [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 [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]
model [ProofEngine]
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_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 [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_pool [Lang]
new_pool [Wp.Lang]
next [Pcfg]
nil [Conditions]
nil [Wp.Conditions]
no_infinite_array [Ctypes]
no_infinite_array [Wp.Ctypes]
no_result [VCS]
no_result [Wp.VCS]
no_status [GuiProver]
node_stmt_opt [Cil2cfg]
node_type [Cil2cfg]
normalize [WpStrategy]
not [Lang.N]
Lang.F.p_not
not [Wp.Lang.N]
Wp.Lang.F.p_not
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 [Conditions]
occurs [Memory.Model]
Test if a location depend on a given logic variable
occurs [Region]
occurs [Vset]
occurs [Lang.F]
occurs [Wp.LogicSemantics.Make]
occurs [Wp.Conditions]
occurs [Wp.Memory.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_list [Set.S]
of_list l creates a set from a list of elements.
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.
ok_status [GuiProver]
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_remove [Wpo]
on_scope [Model]
on_scope [Wp.Model]
on_update [GuiPanel]
once [Footprint]
Width-first once iterator.
open_file [Script]
opened [ProofEngine]
not proved
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_apply [Lang.Subst]
p_apply [Lang.F]
p_apply [Wp.Lang.Subst]
p_apply [Wp.Lang.F]
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_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_forall [Lang.F]
p_forall [Wp.Lang.F]
p_group [ProverTask]
Put pattern in group \(p\)
p_havoc [MemTyped]
p_havoc [Wp.MemTyped]
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_separated [MemTyped]
p_separated [Wp.MemTyped]
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]
param_of_json [ProofScript]
parameters [Lang]
definitions
parameters [Wp.Lang]
definitions
parameters_of_json [ProofScript]
params [TacInstance]
parent [ProofEngine]
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 [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 [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' information.
parts_of_id [Wp.WpPropId]
get the 'part' information.
path [Region]
Empty, but Full for the path
pattern [Footprint]
Generate head footprint up to size
pending [ProofEngine]
pending [ProofScript]
pending goals
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]
pool [Lang.F]
pool [Wp.Lang.F]
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 [Tactical]
Debug only
pp_clause [Separation]
Prints the separation in ACSL format.
pp_clause [Wp.Tactical]
Debug only
pp_clause [Wp.Separation]
Prints the separation in ACSL format.
pp_cluster [Definitions]
pp_cluster [Wp.Definitions]
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_param [MemVar]
pp_param [Wp.MemVar]
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_selection [Tactical]
Debug only
pp_selection [Wp.Tactical]
Debug only
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_value [CodeSemantics.Make]
pp_value [Wp.CodeSemantics.Make]
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]
pprepeat [Vlist]
pred [LogicSemantics.Make]
pred [LogicCompiler.Make]
pred [Repr]
pred [Wp.LogicSemantics.Make]
pred [Wp.LogicCompiler.Make]
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]
preproc_label [NormAtLabels]
preproc_label [Wp.NormAtLabels]
pretty [ProverWhy3.Goal]
pretty [Why3_xml]
pretty [ProofSession]
pretty [Wpo.DISK]
pretty [Pcond]
pretty [Memory.Model]
pretty printing of memory location
pretty [Memory.Sigma]
pretty [Memory.Chunk]
pretty [Cstring]
pretty [Region]
pretty [Vlist]
pretty [Vset]
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.Cstring]
pretty [Wp.Vset]
pretty [Wp.Splitter]
pretty [Wp.Passive]
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]
prev [Pcfg]
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 [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 [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.
prove [VC]
Returns a ready-to-schedule task.
prove [ProverScript]
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]
proved [ProofEngine]
not opened
prover [ProverWhy3]
prover_of_json [ProofScript]
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]
qed_time [Wpo]

R
range [Auto]
range [Tactical]
range [Vset]
range [Cfloat]
range [Cint]
Dependent on model
range [Wp.Auto]
range [Wp.Tactical]
range [Wp.Vset]
range [Wp.Cfloat]
range [Wp.Cint]
Dependent on model
ranges [Auto.Range]
ranges [Wp.Auto.Range]
rdescr [Cvalues.Logic]
real_of_int [Cfloat]
real_of_int [Wp.Cfloat]
record [Lang]
record [Wp.Lang]
record_with [Lang.F]
record_with [Wp.Lang.F]
region [LogicSemantics.Make]
region [LogicCompiler.Make]
region [Wp.LogicSemantics.Make]
region [Wp.LogicCompiler.Make]
register [GuiPanel]
register [Register]
register [Strategy]
register [Tactical]
register [Pcfg]
register [Model]
register [Context]
Register a global configure, to be executed once per project/ast.
register [Wp.Strategy]
register [Wp.Tactical]
register [Wp.Model]
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]
remove [VC]
remove [ProofEngine]
remove [ProofSession]
remove [Wpo]
remove [Model.Generator]
remove [Model.Registry]
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 [Set.S]
remove x s returns a set containing all elements of s, except x.
remove [Wp.Model.Generator]
remove [Wp.Model.Registry]
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 [Tactical]
replace [Conditions]
replace a step in the sequent, the one at the specified position.
replace [Cil2cfg.HEsig]
replace [Wp.Tactical]
replace [Wp.Conditions]
replace a step in the sequent, the one at the specified position.
repr [Lang.F]
Constant time
repr [Model]
repr [Wp.Lang.F]
Constant time
repr [Wp.Model]
requires [Separation]
Filter out is_true clauses
requires [Wp.Separation]
Filter out is_true clauses
reset [ProofEngine]
reset [Lang.F.Check]
reset [Wp_parameters]
reset [Wp.Lang.F.Check]
resolve [Wpo.VC_Annot]
resolve [Wpo]
tries simplification
result [VCS]
result [LogicSemantics.Make]
result [LogicCompiler.Make]
result [Wp.VCS]
result [Wp.LogicSemantics.Make]
result [Wp.LogicCompiler.Make]
result_of_json [ProofScript]
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]
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.
rpath [Region]
Empty, but Full for the r-paths
run [Register]
run [ProverWhy3ide]
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]
save [ProverScript]
save [ProofSession]
saved [ProofEngine]
savescripts [Proof]
If necessary, dump the scripts database into the file specified by -wp-script f.
schedule [ProverTask]
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 [ProofEngine]
script_for [Proof]
script_for_ide [Proof]
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_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 [Memory.Chunk]
Chunk names, for pretty-printing
self [Wp.Memory.Chunk]
Chunk names, for pretty-printing
separated [Auto]
separated [LogicSemantics.Make]
separated [Memory.Model]
Return the formula that tests if two segment are separated
separated [Cvalues.Logic]
separated [Wp.Auto]
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]
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 [Tactical.Fmap]
set [Lang.F.Check]
set [Context]
Define the current value.
set [Wp.Tactical.Fmap]
set [Wp.Lang.F.Check]
set [Wp.Context]
Define the current value.
set_arg [Strategy]
set_arg [Wp.Strategy]
set_args [Strategy]
set_args [Wp.Strategy]
set_builtin [Lang.F]
set_builtin [Wp.Lang.F]
set_builtin_1 [Lang.F]
set_builtin_1 [Wp.Lang.F]
set_builtin_2 [Lang.F]
set_builtin_2 [Wp.Lang.F]
set_builtin_eq [Lang.F]
set_builtin_eq [Wp.Lang.F]
set_builtin_eqp [Lang.F]
set_builtin_eqp [Wp.Lang.F]
set_builtin_leq [Lang.F]
set_builtin_leq [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]
set_saved [ProofEngine]
set_strategies [ProofEngine]
severe [Warning]
severe [Wp.Warning]
shareable [Vlist]
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 [Lang.Subst]
sigma [Lang.F]
sigma [Wp.LogicSemantics.Make]
sigma [Wp.LogicCompiler.Make]
sigma [Wp.Lang.Subst]
sigma [Wp.Lang.F]
signature [Tactical]
signature [Wp.Tactical]
signed [Ctypes]
true if signed
signed [Wp.Ctypes]
true if signed
simplify [Mcfg.Splitter]
simplify [Wp.Mcfg.Splitter]
singleton [Vset]
singleton [Letify.Ground]
singleton [Splitter]
singleton [Map.S]
singleton x y returns the one-element map that contains a binding y for x.
singleton [Set.S]
singleton x returns the one-element set containing only 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 [Conditions]
size [Matrix]
size [Wp.Conditions]
sizeof_defined [Ctypes]
sizeof_defined [Wp.Ctypes]
sizeof_object [Ctypes]
sizeof_object [Wp.Ctypes]
skip [Script]
sloc [Cvalues.Logic]
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 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]
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 [WpAnnot]
splits a prop_id goals into prop_id parts for each sub-goals
split [Mcfg.Splitter]
split [Wp.Auto]
split [Wp.Tactical]
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 [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 [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]
state [ProofEngine]
state [Conditions]
state [Mstate]
state [Memory.Model]
returns a memory state description from a memory model vector.
state [Wp.Conditions]
state [Wp.Mstate]
state [Wp.Memory.Model]
returns a memory state description from a memory model vector.
status [ProofEngine]
status [ProofScript]
minimum of pending goals
status [LogicSemantics.Make]
status [LogicCompiler.Make]
status [Wp.LogicSemantics.Make]
status [Wp.LogicCompiler.Make]
step [Conditions]
step [Wp.Conditions]
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.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.
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 [TacRewrite]
strategy [TacNormalForm]
strategy [TacCut]
strategy [TacFilter]
strategy [TacLemma]
strategy [TacInstance]
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_float [Ctypes]
sub_c_float [Wp.Ctypes]
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 p -> G.
subclause [Wp.Tactical]
When subclause clause p, we have clause = Step H and H -> p, or clause = Goal G and p -> 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 [Region]
subset [Vset]
subset [Set.S]
subset s1 s2 tests whether the set s1 is a subset of the set s2.
subset [Wp.Vset]
subst [Conditions]
Apply the atomic substitution recursively using Lang.F.p_subst f.
subst [Wp.Conditions]
Apply the atomic substitution recursively using Lang.F.p_subst f.
subterms [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
t_absurd [Auto]
Find a contradiction.
t_absurd [Wp.Auto]
Find a contradiction.
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_descr [Auto]
Apply a description to each sub-goal
t_descr [Wp.Auto]
Apply a description to each sub-goal
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_range [Auto]
t_range [Wp.Auto]
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 [TacRewrite]
tactical [TacNormalForm]
tactical [TacCut]
tactical [TacFilter]
tactical [TacLemma]
tactical [TacInstance]
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 [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]
tau_of_var [Lang.F]
tau_of_var [Wp.Lang.F]
term [LogicSemantics.Make]
term [LogicCompiler.Make]
term [Repr]
term [Wp.LogicSemantics.Make]
term [Wp.LogicCompiler.Make]
term [Wp.Repr]
test [Mcfg.S]
test [Wp.Mcfg.S]
timeout [ProverTask]
timeout [VCS]
timeout [Wp.VCS]
timer [VCS]
Suitable timeout w.r.t measured time and number of process
timer [Wp.VCS]
Suitable timeout w.r.t measured time and number of process
title [ProofEngine]
title_of_mode [VCS]
title_of_mode [Wp.VCS]
title_of_prover [VCS]
title_of_prover [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]
typeof [Lang.F]
Try to extract a type of term.
typeof [Wp.Lang.F]
Try to extract a type of term.

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 [Set.S]
Set union.
union [Wp.Memory.Sigma]
union [Wp.Vset]
union [Wp.Splitter]
union [Wp.Passive]
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_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_hints_for_goal [Proof]
Update the hints for one specific goal.
update_symbol [Definitions]
update_symbol [Wp.Definitions]
updates [Pcfg]
updates [Mstate]
updates [Memory.Model]
Try to interpret a sequence of states into updates.
updates [Wp.Mstate]
updates [Wp.Memory.Model]
Try to interpret a sequence of states into updates.
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.
validate [ProofEngine]
value [Memory.Sigma]
value [Cvalues.Logic]
value [Wp.Memory.Sigma]
vanti [TacFilter]
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 [Lang.F]
Constant time
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 [Wp.Lang.F]
Constant time
vars_hyp [Conditions]
vars_hyp [Wp.Conditions]
vars_seq [Conditions]
vars_seq [Wp.Conditions]
varsp [Lang.F]
Constant time
varsp [Wp.Lang.F]
Constant time
very_strange_loops [Cil2cfg]
detect is there are natural loops where we didn't manage to compute back edges (see mark_loops).
visible [Pcfg]
vmax [TacRange]
vmin [TacRange]
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]
wrap [TacInstance]