Index of values

( * ) [Lang.N]

F.p_mul

( * ) [Wp.Lang.N]

F.p_mul

( @* ) [StmtSemantics.Make]

fold bind

( @* ) [Wp.StmtSemantics.Make]

fold bind

($$) [Lang.N]
($$) [Wp.Lang.N]
($) [Lang.N]
($) [Wp.Lang.N]
(&&) [Lang.N]
(&&) [Wp.Lang.N]
(+) [Lang.N]

F.p_add

(+) [Wp.Lang.N]

F.p_add

(-) [Lang.N]

F.p_sub

(-) [Wp.Lang.N]

F.p_sub

(/) [Lang.N]

F.p_div

(/) [Wp.Lang.N]

F.p_div

(<) [Lang.N]
(<) [Wp.Lang.N]
(<=) [Lang.N]
(<=) [Wp.Lang.N]
(<>) [Lang.N]
(<>) [Wp.Lang.N]
(=) [Lang.N]
(=) [Wp.Lang.N]
(>) [Lang.N]

Lang.F.p_lt with inversed argument

(>) [Wp.Lang.N]

Wp.Lang.F.p_lt with inversed argument

(>=) [Lang.N]

Lang.F.p_leq with inversed argument

(>=) [Wp.Lang.N]

Wp.Lang.F.p_leq with inversed argument

(@-) [StmtSemantics.Make]
(@-) [Wp.StmtSemantics.Make]
(@:) [StmtSemantics.Make]

LabelMap.find with refined excpetion.

(@:) [Wp.StmtSemantics.Make]

LabelMap.find with refined excpetion.

(@^) [StmtSemantics.Make]

Same as Cfg.concat

(@^) [Wp.StmtSemantics.Make]

Same as Cfg.concat

(mod) [Lang.N]

F.p_mod

(mod) [Wp.Lang.N]

F.p_mod

(||) [Lang.N]
(||) [Wp.Lang.N]
(~-) [Lang.N]

fun x -> p_sub 0 x

(~-) [Wp.Lang.N]

fun x -> p_sub 0 x

A
a_addr [MemMemory]

Constructor for { base ; offset }

a_base [MemMemory]

Returns the base

a_base_offset [MemMemory]

Returns the offset in bytes from the logic offset (which is a memory cell index, actually)

a_global [MemMemory]

Zero-offset base.

a_null [MemMemory]

Null address.

a_offset [MemMemory]

Returns the offset

a_prover [ProofScript]
a_shift [MemMemory]

Shift: a_shift a k adds k to a.offset

a_tactic [ProofScript]
absurd [Auto]
absurd [Wp.Auto]
acs_copy [Region]
acs_deref [Region]
acs_read [Region]
acs_shift [Region]
acs_write [Region]
acsl_lit [Cfloat]
acsl_lit [Wp.Cfloat]
add [Wpo]
add [Letify.Split]
add [Letify.Defs]
add [Letify.Sigma]
add [Lang.F.Subst]
add [Cil2cfg.HEsig]
add [Warning]
add [Wp.Wpo]
add [Hashtbl.S]
add [Wp.Lang.F.Subst]
add [Wp.Warning]
add [Set.S]

add x s returns a set containing all elements of s, plus x.

add [Map.S]

add x y m returns a map containing the same bindings as m, plus a binding of x to y.

add_alias [LogicBuiltins]
add_alias [Region]
add_alias [Wp.LogicBuiltins]
add_all_axioms [WpStrategy]
add_assigns [Mcfg.S]
add_assigns [WpStrategy]

generic function to add an assigns property.

add_assigns [Wp.Mcfg.S]
add_assigns_any [WpStrategy]

generic function to add a WriteAny assigns property.

add_axiom [Mcfg.S]
add_axiom [WpStrategy]
add_axiom [Wp.Mcfg.S]
add_behavior [MemoryContext]
add_behavior [Wp.MemoryContext]
add_builtin [LogicBuiltins]

Add a new builtin.

add_builtin [Wp.LogicBuiltins]

Add a new builtin.

add_call_assigns_any [WpStrategy]

short cut to add a dynamic call

add_call_assigns_hyp [WpStrategy]

shortcut to add a call assigns property as an hypothesis.

add_composer [Tactical]
add_composer [Wp.Tactical]
add_ctor [LogicBuiltins]
add_ctor [Wp.LogicBuiltins]
add_definitions [Letify]

add_definitions sigma defs xs ps keep all definitions of variables xs from sigma that comes from defs.

add_fct_bhv_assigns_hyp [WpStrategy]
add_filter [Lang.F.Subst]
add_filter [Wp.Lang.F.Subst]
add_fun [Lang.F.Subst]
add_fun [Wp.Lang.F.Subst]
add_goal [Mcfg.S]
add_goal [Wp.Mcfg.S]
add_hook [Wprop.Indexed2]

Hooks are executed once at property creation

add_hook [Wprop.Indexed]

Hooks are executed once at property creation

add_hyp [Mcfg.S]
add_hyp [Wp.Mcfg.S]
add_invalid_proof [WpAnnot]

add an invalid proof result ; can not revert a complete proof

add_library [LogicBuiltins]

Add a new library or update the dependencies of an existing one

add_library [Wp.LogicBuiltins]

Add a new library or update the dependencies of an existing one

add_logic [LogicBuiltins]
add_logic [Wp.LogicBuiltins]
add_loop_annots [WpStrategy]
add_loop_assigns_hyp [WpStrategy]

shortcut to add a loop assigns property as an hypothesis.

add_map [Lang.F.Subst]
add_map [Wp.Lang.F.Subst]
add_node_annots [WpStrategy]

add_node_annots cfg annots v (before, (after, exits)) add the annotations for the node :

add_offset [Region]
add_on_edges [WpStrategy]
add_option [LogicBuiltins]

add a value to an option (group, name)

add_option [Wp.LogicBuiltins]

add a value to an option (group, name)

add_pointed [Region]
add_predicate [LogicBuiltins]
add_predicate [Wp.LogicBuiltins]
add_proof [WpAnnot]

accumulate in the proof the partial proof for this prop_id

add_prop [WpStrategy]

generic function to add a predicate property after normalisation.

add_prop_assert [WpStrategy]
add_prop_call_post [WpStrategy]

Add a postcondition of a called function.

add_prop_call_pre [WpStrategy]
add_prop_dead_call [WpStrategy]

Add Smoke Test for possibly dead call : (posts,exits)

add_prop_dead_code [WpStrategy]

Add Smoke Test for possibly dead code

add_prop_dead_loop [WpStrategy]

Add Smoke Test for loop

add_prop_fct_bhv_pre [WpStrategy]

Add the preconditions of the behavior

add_prop_fct_post [WpStrategy]
add_prop_fct_pre [WpStrategy]

Add the predicate as a function precondition.

add_prop_fct_pre_bhv [WpStrategy]
add_prop_fct_smoke [WpStrategy]

Add Smoke Test behavior

add_prop_loop_inv [WpStrategy]
add_prop_stmt_bhv_requires [WpStrategy]

Add all the b_requires.

add_prop_stmt_post [WpStrategy]

Add the predicate as a stmt precondition.

add_prop_stmt_pre [WpStrategy]

Add the predicate as a stmt precondition.

add_prop_stmt_spec_pre [WpStrategy]

Process the stmt spec precondition as an hypothesis for external properties.

add_script_for [Proof]

new_script goal keys proof qed registers the script proof terminated by qed for goal gid and keywords keys

add_seq [Hashtbl.S]
add_seq [Set.S]

Add the given elements to the set, in order.

add_seq [Map.S]

Add the given bindings to the map, in order.

add_specific_equality [ProverWhy3]

Equality used in the goal, simpler to prove than polymorphic equality

add_step [Register]
add_stmt_spec_assigns_hyp [WpStrategy]

shortcut to add a stmt spec assigns property as an hypothesis.

add_time [Register]
add_tmpnode [CfgCompiler.Cfg]

Set a node as temporary.

add_tmpnode [Wp.CfgCompiler.Cfg]

Set a node as temporary.

add_type [LogicBuiltins]
add_type [Wp.LogicBuiltins]
add_var [Lang.F]
add_var [Wp.Lang.F]
add_vars [Lang.F]
add_vars [Wp.Lang.F]
adt [Lang]

Must not be a builtin

adt [Wp.Lang]

Must not be a builtin

age [Wpo]
age [Wp.Wpo]
ainf [Cvalues]

Array lower-bound, ie `Some(0)`

alias [Region]
alias [Layout.Alias]
alloc [Sigs.Model]

Allocates new chunk for the validity of variables.

alloc [Wp.Sigs.Model]

Allocates new chunk for the validity of variables.

alloc_domain [Plang]
alloc_domain [Wp.Plang]
alloc_e [Plang]
alloc_e [Wp.Plang]
alloc_hyp [Pcond]
alloc_hyp [Wp.Pcond]
alloc_p [Plang]
alloc_p [Wp.Plang]
alloc_seq [Pcond]
alloc_seq [Wp.Pcond]
alloc_xs [Plang]
alloc_xs [Wp.Plang]
alpha [Lang.F]
alpha [Lang]

freshen all variables

alpha [Wp.Lang.F]
alpha [Wp.Lang]

freshen all variables

anchor [ProofEngine]
append [Conditions]

Conjunction

append [Wp.Conditions]

Conjunction

append_after [Parameter_sig.List]

append a list at the end of the current state

append_before [Parameter_sig.List]

append a list in front of the current state

apply [Mstate]
apply [Sigs.Model]

Propagate a sequent substitution inside the memory state.

apply [Cvalues.Logic]
apply [Passive]
apply [Wp.Mstate]
apply [Wp.Sigs.Model]

Propagate a sequent substitution inside the memory state.

apply [Wp.Passive]
apply_add [Cvalues.Logic]
apply_assigns [Sigs.LogicAssigns]

Relates two memory states corresponding to an assigns clause with the specified set of locations.

apply_assigns [Wp.Sigs.LogicAssigns]

Relates two memory states corresponding to an assigns clause with the specified set of locations.

apply_sub [Cvalues.Logic]
are_equal [Lang.F]

Computes equality

are_equal [Wp.Lang.F]

Computes equality

are_selected_names [WpPropId]

are_selected_names asked names checks if names of a property are selected according to asked names.

are_selected_names [Wp.WpPropId]

are_selected_names asked names checks if names of a property are selected according to asked names.

arg [Strategy]
arg [Wp.Strategy]
array [Auto]
array [Wp.Auto]
array_dimensions [Ctypes]

Returns the list of dimensions the array consists of.

array_dimensions [Wp.Ctypes]

Returns the list of dimensions the array consists of.

array_size [Ctypes]
array_size [Wp.Ctypes]
as_atom [Cleaning]
as_have [Cleaning]
as_init [Cleaning]
as_type [Cleaning]
assign [Mcfg.S]
assign [Wp.Mcfg.S]
assigned [MemLoader.Make]
assigned [Sigs.Model]

Return a set of formula that express that two memory state are the same except at the given set of memory location.

assigned [Sigs.Sigma]

Make chunks equal outside of some domain.

assigned [Wp.Sigs.Model]

Return a set of formula that express that two memory state are the same except at the given set of memory location.

assigned [Wp.Sigs.Sigma]

Make chunks equal outside of some domain.

assigned_of_assigns [Sigs.LogicSemantics]

Computes the region assigned by an assigns clause.

assigned_of_assigns [Wp.Sigs.LogicSemantics]

Computes the region assigned by an assigns clause.

assigned_of_froms [Sigs.LogicSemantics]

Computes the region assigned by a list of froms.

assigned_of_froms [Wp.Sigs.LogicSemantics]

Computes the region assigned by a list of froms.

assigned_of_lval [Sigs.LogicSemantics]

Computes the region assigned by a list of froms.

assigned_of_lval [Wp.Sigs.LogicSemantics]

Computes the region assigned by a list of froms.

assigns [StmtSemantics.Make]
assigns [Wp.StmtSemantics.Make]
assigns_info_id [WpPropId]
assigns_info_id [Wp.WpPropId]
assigns_upper_bound [WpStrategy]
assume [StmtSemantics.Make]
assume [CfgCompiler.Cfg]

Represents execution traces T such that, if T contains every node points in the label-map, then the condition holds over the corresponding memory states.

assume [Conditions]

Assumes a predicate in the specified section, with the specified decorations.

assume [Letify.Sigma]
assume [Lang]
assume [Wp.StmtSemantics.Make]
assume [Wp.CfgCompiler.Cfg]

Represents execution traces T such that, if T contains every node points in the label-map, then the condition holds over the corresponding memory states.

assume [Wp.Conditions]

Assumes a predicate in the specified section, with the specified decorations.

assume [Wp.Lang]
assume_ [StmtSemantics.Make]
assume_ [Wp.StmtSemantics.Make]
asup [Cvalues]

Array upper-bound, ie `Some(n-1)`

at [Tactical]
at [Pcfg]
at [Wp.Tactical]
at [Wp.Pcfg]
at_closure [Conditions]

register a transformation applied just before close

at_closure [Wp.Conditions]

register a transformation applied just before close

at_exit [Clabels]
at_exit [Wp.Clabels]
atype [Lang]
atype [Wp.Lang]
auto_range [Auto]
auto_range [Wp.Auto]
auto_split [Auto]
auto_split [Wp.Auto]
autofit [VCS]

Result that fits the default configuration

autofit [Wp.VCS]

Result that fits the default configuration

automaton [StmtSemantics.Make]
automaton [Wp.StmtSemantics.Make]
axiomatic [Definitions]
axiomatic [LogicUsage]
axiomatic [Wp.Definitions]
axiomatic [Wp.LogicUsage]
B
backtrack [ProverSearch]
backward [Letify.Ground]
band [Cint]
band [Wp.Cint]
bar [Wpo]
bar [Wp.Wpo]
base_addr [Sigs.Model]

Return the memory location of the base address of a given memory location.

base_addr [Wp.Sigs.Model]

Return the memory location of the base address of a given memory location.

base_offset [Sigs.Model]

Return the offset of the location, in bytes, from its base_addr.

base_offset [Wp.Sigs.Model]

Return the offset of the location, in bytes, from its base_addr.

basename [Lang.F]
basename [LogicUsage]

Trims the original name

basename [WpContext.IData]
basename [Ctypes]
basename [Wp.Lang.F]
basename [Wp.WpContext.IData]
basename [Wp.LogicUsage]

Trims the original name

basename [Wp.Ctypes]
basename_of_chunk [Sigs.Chunk]

Used when generating fresh variables for a chunk.

basename_of_chunk [Wp.Sigs.Chunk]

Used when generating fresh variables for a chunk.

behavior_name_of_strategy [WpStrategy]
best [VCS]
best [Wp.VCS]
bind [ProofEngine]
bind [StmtSemantics.Make]
bind [Letify]

bind sigma defs xs select definitions in defs targeting variables xs.

bind [Passive]
bind [Context]

Performs the job with local context bound to local value.

bind [Wp.StmtSemantics.Make]
bind [Wp.Passive]
bind [Wp.Context]

Performs the job with local context bound to local value.

bindings [Map.S]

Return the list of all bindings of the given map.

bit_test [Cint]
bit_test [Wp.Cint]
bits_sizeof_array [Ctypes]
bits_sizeof_array [Wp.Ctypes]
bits_sizeof_comp [Ctypes]
bits_sizeof_comp [Wp.Ctypes]
bits_sizeof_object [Ctypes]
bits_sizeof_object [Wp.Ctypes]
block_length [Sigs.Model]

Returns the length (in bytes) of the allocated block containing the given location.

block_length [Wp.Sigs.Model]

Returns the length (in bytes) of the allocated block containing the given location.

block_scope_for_edge [Cil2cfg]
blsl [Cint]
blsl [Wp.Cint]
blsr [Cint]
blsr [Wp.Cint]
bnot [Cint]
bnot [Wp.Cint]
bool_and [Cvalues]
bool_eq [Cvalues]
bool_leq [Cvalues]
bool_lt [Cvalues]
bool_neq [Cvalues]
bool_of_int [Cmath]
bool_or [Cvalues]
bool_val [Cvalues]
bootstrap_logic [LogicCompiler.Make]
bootstrap_logic [Wp.LogicCompiler.Make]
bootstrap_pred [LogicCompiler.Make]
bootstrap_pred [Wp.LogicCompiler.Make]
bootstrap_region [LogicCompiler.Make]
bootstrap_region [Wp.LogicCompiler.Make]
bootstrap_term [LogicCompiler.Make]
bootstrap_term [Wp.LogicCompiler.Make]
bor [Cint]
bor [Wp.Cint]
bound [ProofEngine]
bound_add [Vset]
bound_add [Wp.Vset]
bound_shift [Vset]
bound_shift [Wp.Vset]
bound_sub [Vset]
bound_sub [Wp.Vset]
bounds [Auto.Range]
bounds [Ctypes]

domain, bounds included

bounds [Wp.Auto.Range]
bounds [Wp.Ctypes]

domain, bounds included

branch [CfgCompiler.Cfg]

Structurally corresponds to an if-then-else control-flow.

branch [Conditions]

Construct a branch bundle, with merging of all common parts.

branch [Letify.Ground]
branch [Wp.CfgCompiler.Cfg]

Structurally corresponds to an if-then-else control-flow.

branch [Wp.Conditions]

Construct a branch bundle, with merging of all common parts.

branching [Pcfg]
branching [Wp.Pcfg]
break [Clabels]
break [Wp.Clabels]
build_prop_of_from [Mcfg.S]

build p => alpha(p) for functional dependencies verification.

build_prop_of_from [Wp.Mcfg.S]

build p => alpha(p) for functional dependencies verification.

builtin_types [Lang]
builtin_types [Wp.Lang]
bundle [Conditions]

Closes the bundle and promote it into a well-formed sequence.

bundle [Wp.Conditions]

Closes the bundle and promote it into a well-formed sequence.

bxor [Cint]
bxor [Wp.Cint]
C
c_bool [Ctypes]

Returns the type of int

c_bool [Wp.Ctypes]

Returns the type of int

c_char [Ctypes]

Returns the type of char

c_char [Wp.Ctypes]

Returns the type of char

c_float [Ctypes]

Conforms to

c_float [Wp.Ctypes]

Conforms to

c_int [Ctypes]

Conforms to

c_int [Wp.Ctypes]

Conforms to

c_ptr [Ctypes]

Returns the type of pointers

c_ptr [Wp.Ctypes]

Returns the type of pointers

cache [Layout.Offset]
cache_descr [Wpo.VC_Annot]
cache_descr [Wpo.VC_Lemma]
cache_descr [Wp.Wpo.VC_Annot]
cache_descr [Wp.Wpo.VC_Lemma]
cache_log [Wpo.DISK]
cache_log [Wp.Wpo.DISK]
cached [VCS]

only for true verdicts

cached [Wp.VCS]

only for true verdicts

call [StmtSemantics.Make]
call [LogicCompiler.Make]
call [Sigs.LogicSemantics]

Create call data from the callee point of view, deriving data (gamma and pools) from the current frame.

call [Sigs.CodeSemantics]

Address of a function pointer.

call [Splitter]
call [Mcfg.S]
call [Wp.StmtSemantics.Make]
call [Wp.LogicCompiler.Make]
call [Wp.Sigs.LogicSemantics]

Create call data from the callee point of view, deriving data (gamma and pools) from the current frame.

call [Wp.Sigs.CodeSemantics]

Address of a function pointer.

call [Wp.Splitter]
call [Wp.Mcfg.S]
call_dynamic [Mcfg.S]
call_dynamic [Wp.Mcfg.S]
call_fun [LogicCompiler.Make]
call_fun [Definitions]
call_fun [Wp.LogicCompiler.Make]
call_fun [Wp.Definitions]
call_goal_precond [Mcfg.S]
call_goal_precond [Wp.Mcfg.S]
call_kf [StmtSemantics.Make]
call_kf [Wp.StmtSemantics.Make]
call_post [LogicCompiler.Make]
call_post [Sigs.LogicSemantics]

Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state and post-state.

call_post [Wp.LogicCompiler.Make]
call_post [Wp.Sigs.LogicSemantics]

Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state and post-state.

call_pre [LogicCompiler.Make]
call_pre [Sigs.LogicSemantics]

Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state.

call_pre [Wp.LogicCompiler.Make]
call_pre [Wp.Sigs.LogicSemantics]

Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state.

call_pred [LogicCompiler.Make]
call_pred [Definitions]
call_pred [Wp.LogicCompiler.Make]
call_pred [Wp.Definitions]
callback [WpContext.Registry]
callback [Wp.WpContext.Registry]
cancel [ProofEngine]
cardinal [TacInstance]

less than limit

cardinal [Set.S]

Return the number of elements of a set.

cardinal [Map.S]

Return the number of bindings of a map.

case [Clabels]
case [Wp.Clabels]
cases [Splitter]
cases [Wp.Splitter]
cast [Sigs.CodeSemantics]

Applies a pointer cast or a conversion.

cast [Sigs.Model]

Cast a memory location into another memory location.

cast [Wp.Sigs.CodeSemantics]

Applies a pointer cast or a conversion.

cast [Wp.Sigs.Model]

Cast a memory location into another memory location.

cat_print_generated [Wp_parameters]
cat_print_generated [Wp.Wp_parameters]
catch [Warning]

Set up a context for the job.

catch [Wp.Warning]

Set up a context for the job.

catch_label_error [NormAtLabels]
catch_label_error [Wp.NormAtLabels]
cc_assign [RegionAccess]
cc_dims [Matrix]

Value of size variables

cc_env [Matrix]

Dimension environment

cc_fundec [RegionAccess]
cc_init [RegionAccess]
cc_instr [RegionAccess]
cc_lval [RegionAccess]
cc_pred [RegionAccess]
cc_read [RegionAccess]
cc_region [RegionAccess]
cc_spec [RegionAccess]
cc_tau [Matrix]

Type of matrix

cc_term [RegionAccess]
cdomain [Cvalues]
cfg_kf [Cil2cfg]
cfg_of_strategy [WpStrategy]
cfg_spec_only [Cil2cfg]

returns true is this CFG is degenerated (no code available)

char [Ctypes]
char [Wp.Ctypes]
char_at [Cstring]
char_at [Wp.Cstring]
check_assigns [Sigs.LogicSemantics]

Check assigns inclusion.

check_assigns [Wp.Sigs.LogicSemantics]

Check assigns inclusion.

check_tau [Vlist]
check_term [Vlist]
checkbox [Tactical]

Unless specified, default is false.

checkbox [Wp.Tactical]

Unless specified, default is false.

children [ProofEngine]
choice [Auto]
choice [StmtSemantics.Make]

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp.

choice [Wp.Auto]
choice [Wp.StmtSemantics.Make]

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp.

choose [VCS]
choose [Sigs.Sigma]

Make the union of each sigma, choosing the minimal variable in case of conflict.

choose [Wp.VCS]
choose [Wp.Sigs.Sigma]

Make the union of each sigma, choosing the minimal variable in case of conflict.

choose [Set.S]

Return one element of the given set, or raise Not_found if the set is empty.

choose [Map.S]

Return one binding of the given map, or raise Not_found if the map is empty.

choose_opt [Set.S]

Return one element of the given set, or None if the set is empty.

choose_opt [Map.S]

Return one binding of the given map, or None if the map is empty.

chunk [Region]
chunks [Region]
cint [Tactical]
cint [Wp.Tactical]
clean [Conditions]
clean [Wp.Conditions]
cleanup_cache [Cache]
clear [VC]
clear [Wpo]
clear [Cil2cfg.HEsig]
clear [WpContext.Generator]
clear [WpContext.Registry]
clear [Context]

Clear the current value.

clear [Wp.Wpo]
clear [Wp.VC]
clear [Hashtbl.S]
clear [Wp.WpContext.Generator]
clear [Wp.WpContext.Registry]
clear [Wp.Context]

Clear the current value.

clear_result [Cache]
clear_results [Wpo]
clear_results [Wp.Wpo]
clear_scheduled [Register]
cloc [Sigs.CodeSemantics]

Interpret a value as a location.

cloc [Wp.Sigs.CodeSemantics]

Interpret a value as a location.

close [Script]
close [Conditions]

With free variables quantified.

close [Mcfg.S]
close [Wp.Conditions]

With free variables quantified.

close [Wp.Mcfg.S]
cluster [MemLoader]
cluster [Cstring]

The cluster where all strings are defined.

cluster [Definitions]
cluster [Region]
cluster [Wp.Cstring]

The cluster where all strings are defined.

cluster [Wp.Definitions]
cluster_age [Definitions]
cluster_age [Wp.Definitions]
cluster_compare [Definitions]
cluster_compare [Wp.Definitions]
cluster_id [Definitions]

Unique

cluster_id [Wp.Definitions]

Unique

cluster_position [Definitions]
cluster_position [Wp.Definitions]
cluster_title [Definitions]
cluster_title [Wp.Definitions]
cmdline [Register]
cmdline_run [Register]
cmp_prover [VCS]
cmp_prover [Wp.VCS]
code_lit [Cfloat]
code_lit [Wp.Cfloat]
codomain [Letify.Sigma]
command [VC]

Run the provers with the command-line interface.

command [Rformat]
command [Wp.VC]

Run the provers with the command-line interface.

commit [ProofEngine]
comp [Lang]
comp [Wp.Lang]
comp_id [Lang]
comp_id [Wp.Lang]
comp_init [Lang]
comp_init [Wp.Lang]
comp_init_id [Lang]
comp_init_id [Wp.Lang]
compare [VCS]
compare [Sigs.Chunk]
compare [LogicBuiltins]
compare [Matrix]
compare [Lang.F]
compare [RegionAnnot.Lpath]
compare [Layout.Value]
compare [Layout.Data]
compare [WpContext.Key]
compare [WpContext.Entries]
compare [WpContext.SCOPE]
compare [WpContext.MODEL]
compare [WpContext.S]
compare [Warning]
compare [Why3Provers]
compare [Clabels.T]
compare [Ctypes.AinfoComparable]
compare [Ctypes]
compare [Map.OrderedType]

A total ordering function over the keys.

compare [Wp.VCS]
compare [Wp.Sigs.Chunk]
compare [Wp.LogicBuiltins]
compare [Wp.Lang.F]
compare [Wp.WpContext.Key]
compare [Wp.WpContext.Entries]
compare [Wp.WpContext.SCOPE]
compare [Wp.WpContext.MODEL]
compare [Wp.WpContext.S]
compare [Wp.Warning]
compare [Set.S]

Total ordering between sets.

compare [Map.S]

Total ordering between maps.

compare [Wp.Clabels.T]
compare [Wp.Ctypes.AinfoComparable]
compare [Wp.Ctypes]
compare_c_float [Ctypes]
compare_c_float [Wp.Ctypes]
compare_c_int [Ctypes]
compare_c_int [Wp.Ctypes]
compare_prop_id [WpPropId]
compare_prop_id [Wp.WpPropId]
compare_ptr_conflated [Ctypes]

same as Ctypes.compare but all PTR are considered the same

compare_ptr_conflated [Wp.Ctypes]

same as Wp.Ctypes.compare but all PTR are considered the same

comparep [Lang.F]
comparep [Wp.Lang.F]
compile [CfgCompiler.Cfg]
compile [WpContext.IData]
compile [WpContext.Data]
compile [WpContext.Registry]

with circularity protection

compile [Wp.CfgCompiler.Cfg]
compile [Wp.WpContext.IData]
compile [Wp.WpContext.Data]
compile [Wp.WpContext.Registry]

with circularity protection

compile_lemma [Definitions]
compile_lemma [Wp.Definitions]
compiler [Factory]
compiler [Wp.Factory]
compinfo [Definitions]
compinfo [Wp.Definitions]
complexity [TacInstance]
compose [Tactical]
compose [Wp.Tactical]
composer [Tactical]

Unless specified, default is Empty selection.

composer [Wp.Tactical]

Unless specified, default is Empty selection.

compound [Auto]
compound [Wp.Auto]
compute [Calculus.Cfg]
compute [Auto.Range]
compute [Wpo.GOAL]
compute [Wpo]
compute [WpTarget]
compute [Filtering]
compute [Letify.Ground]
compute [RefUsage]
compute [LogicUsage]

To force computation

compute [MemoryContext]
compute [AssignsCompleteness]
compute [Dyncall]

Forces computation of dynamic calls.

compute [Wp.Wpo.GOAL]
compute [Wp.Wpo]
compute [Wp.Auto.Range]
compute [Wp.Filtering]
compute [Wp.AssignsCompleteness]
compute [Wp.RefUsage]
compute [Wp.LogicUsage]

To force computation

compute [Wp.MemoryContext]
compute_auto [Register]
compute_call [Generator]
compute_descr [Wpo.GOAL]
compute_descr [Wp.Wpo.GOAL]
compute_hypotheses [WpContext]
compute_hypotheses [Wp.WpContext]
compute_ip [Generator]
compute_kf [Generator]
compute_kf [StmtSemantics.Make]

Full Compilation

compute_kf [Wp.StmtSemantics.Make]

Full Compilation

compute_proof [Wpo.GOAL]
compute_proof [Wp.Wpo.GOAL]
compute_provers [Register]
compute_selection [Generator]
computer [Register]
computer [CfgWP]
computing [VCS]
computing [Wp.VCS]
concat [CfgCompiler.Cfg]

The concatenation is the intersection of all possible collection of traces from each cfg.

concat [Conditions]

List conjunction

concat [Wp.CfgCompiler.Cfg]

The concatenation is the intersection of all possible collection of traces from each cfg.

concat [Wp.Conditions]

List conjunction

concretize [Vset]
concretize [Wp.Vset]
cond [Sigs.CodeSemantics]

Evaluate the conditional expression on the given memory state.

cond [Wp.Sigs.CodeSemantics]

Evaluate the conditional expression on the given memory state.

condition [Conditions]

With free variables kept.

condition [Wp.Conditions]

With free variables kept.

conditions [Passive]
conditions [Wp.Passive]
config [Why3Provers]
configure [ProofScript]
configure [VCS]
configure [Sigs.Model]

Initializers to be run before using the model.

configure [Cfloat]
configure [Cint]
configure [Context]

Apply global configure hooks, once per project/ast.

configure [Why3Provers]
configure [Wp.VCS]
configure [Wp.Sigs.Model]

Initializers to be run before using the model.

configure [Wp.Cfloat]
configure [Wp.Cint]
configure [Wp.Context]

Apply global configure hooks, once per project/ast.

configure_driver [Factory]
configure_driver [Wp.Factory]
configure_ia [Sigs.Model]

Given an automaton, return a vertex's binder.

configure_ia [Wp.Sigs.Model]

Given an automaton, return a vertex's binder.

const [Mcfg.S]
const [Wp.Mcfg.S]
constant [Cvalues]
constant [LogicBuiltins]
constant [Lang.F]
constant [Ctypes]
constant [Wp.LogicBuiltins]
constant [Wp.Lang.F]
constant [Wp.Ctypes]
constant_exp [Cvalues]
constant_term [Cvalues]
context [Warning]
context [Wp.Warning]
context_pp [Lang.F]

Context used by pp_term, pp_pred, pp_var, ppvars for printing the term.

context_pp [Wp.Lang.F]

Context used by pp_term, pp_pred, pp_var, ppvars for printing the term.

continue [Clabels]
continue [Wp.Clabels]
contrapose [Auto]
contrapose [Wp.Auto]
convert [Cint]

Independent from model

convert [Wp.Cint]

Independent from model

copied [MemLoader.Make]
copied [Sigs.Model]

Return a set of equations that express a copy between two memory state.

copied [Wp.Sigs.Model]

Return a set of equations that express a copy between two memory state.

copy [Sigs.Sigma]

Duplicate the environment.

copy [Letify.Ground]
copy [Hashtbl.S]
copy [Wp.Sigs.Sigma]

Duplicate the environment.

copy [Datatype.S]

Deep copy: no possible sharing between x and copy x.

create [CfgDump]
create [Tactical.Fmap]
create [CfgCompiler.Cfg.E]

Bundle an equation with the sigma sequence that created it

create [CfgCompiler.Cfg.T]

Bundle a term with the sigma sequence that created it.

create [CfgCompiler.Cfg.P]

Bundle an equation with the sigma sequence that created it.

create [CfgCompiler.Cfg.C]

Bundle an equation with the sigma sequence that created it.

create [CfgCompiler.Cfg.Node]
create [Pcfg]
create [Mstate]
create [Sigs.Sigma]

Initially empty environment.

create [Cleaning]
create [Letify.Split]
create [Cil2cfg.HEsig]
create [Region]
create [Warning]
create [Context]

Creates a new context with name

create [Wp.Tactical.Fmap]
create [Wp.CfgCompiler.Cfg.E]

Bundle an equation with the sigma sequence that created it

create [Wp.CfgCompiler.Cfg.T]

Bundle a term with the sigma sequence that created it.

create [Wp.CfgCompiler.Cfg.P]

Bundle an equation with the sigma sequence that created it.

create [Wp.CfgCompiler.Cfg.C]

Bundle an equation with the sigma sequence that created it.

create [Hashtbl.S]
create [Wp.CfgCompiler.Cfg.Node]
create [Wp.Pcfg]
create [Wp.Mstate]
create [Wp.Sigs.Sigma]

Initially empty environment.

create [Wp.Warning]
create [Wp.Context]

Creates a new context with name

create_option [LogicBuiltins]

add_option_sanitizer ~driver_dir group name add a sanitizer for group group and option name

create_option [Wp.LogicBuiltins]

add_option_sanitizer ~driver_dir group name add a sanitizer for group group and option name

create_proof [WpAnnot]

to be used only once for one of the related prop_id

create_tbl [WpStrategy]
ctor [LogicBuiltins]
ctor [Wp.LogicBuiltins]
ctor_id [Lang]
ctor_id [Wp.Lang]
current [ProofEngine]
current [VCS]

Current parameters

current [LogicCompiler.Make]
current [Sigs.LogicSemantics]

The current memory state.

current [Cint]
current [Wp.VCS]

Current parameters

current [Wp.LogicCompiler.Make]
current [Wp.Sigs.LogicSemantics]

The current memory state.

current [Wp.Cint]
cut [Auto]
cut [Wp.Auto]
cval [Sigs.CodeSemantics]

Evaluate an abstract value.

cval [Wp.Sigs.CodeSemantics]

Evaluate an abstract value.

cvar [Sigs.Model]

Return the location of a C variable.

cvar [Wp.Sigs.Model]

Return the location of a C variable.

D
datatype [MemVar.VarUsage]
datatype [Sigs.Model]

For projectification.

datatype [Lang]
datatype [Wp.MemVar.VarUsage]
datatype [Wp.Sigs.Model]

For projectification.

datatype [Wp.Lang]
debugp [Lang.F]
debugp [Wp.Lang.F]
decide [Lang.F]

Return true if and only the term is e_true.

decide [Wp.Lang.F]

Return true if and only the term is e_true.

decode [ProofScript]
def_into_axiom [Filter_axioms]
default [Factory]

"Var,Typed,Nat,Real" memory model.

default [Tactical]
default [VCS]

all None

default [Layout.Pack]
default [Layout.Flat]
default [Layout.RW]
default [Clabels]
default [Wp.Tactical]
default [Wp.VCS]

all None

default [Wp.Factory]

"Var,Typed,Nat,Real" memory model.

default [Wp.Clabels]
default_script_mode [Register]
define [Lang.F]
define [WpContext.Registry]

no redefinition ; circularity protected

define [Wp.Lang.F]
define [Wp.WpContext.Registry]

no redefinition ; circularity protected

define_lemma [Definitions]
define_lemma [Wp.Definitions]
define_symbol [Definitions]
define_symbol [Wp.Definitions]
define_type [Definitions]
define_type [Wp.Definitions]
defined [Context]

The current value is defined.

defined [Wp.Context]

The current value is defined.

definition [Auto]
definition [Wp.Auto]
defs [Lang.F]
defs [Wp.Lang.F]
delete_script_for [Proof]

delete_script ~gid remove known script for goal.

dependencies [WpAnnot]
dependencies [LogicBuiltins]

Of external theories.

dependencies [Wp.LogicBuiltins]

Of external theories.

deprecated [Register]
deref [Layout.Cluster]
descr [Factory]
descr [Vset]
descr [LogicBuiltins]
descr [WpContext.MODEL]
descr [Wp.Factory]
descr [Wp.Vset]
descr [Wp.LogicBuiltins]
descr [Wp.WpContext.MODEL]
destruct [Tactical]
destruct [Wp.Tactical]
diff [Set.S]

Set difference: diff s1 s2 contains the elements of s1 that are not in s2.

dimension_of_object [Ctypes]

Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells

dimension_of_object [Wp.Ctypes]

Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells

directory [WpContext]

Current model in "-wp-out" directory

directory [Wp.WpContext]

Current model in "-wp-out" directory

disjoint [Vset]
disjoint [Layout.Chunk]
disjoint [Wp.Vset]
disjoint [Set.S]

Test if two sets are disjoint.

dkey_builtins [Register]
dkey_cluster [ProverErgo]
dkey_logicusage [Register]
dkey_main [Register]
dkey_prover [Register]
dkey_raised [Register]
dkey_refusage [Register]
dkey_shell [VCS]
dkey_shell [Wp.VCS]
do_alias [Region]
do_cache_cleanup [Register]
do_list_scheduled [Register]
do_list_scheduled_result [Register]
do_progress [Register]
do_prover_detect [Register]
do_report_cache_usage [Register]
do_report_prover_stats [Register]
do_report_scheduled [Register]
do_report_steps [Register]
do_report_stopped [Register]
do_report_time [Register]
do_update_session [Register]
do_wp_print [Register]
do_wp_print_for [Register]
do_wp_proofs [Register]
do_wp_report [Register]
do_wpo_display [Register]
do_wpo_failed [Register]
do_wpo_result [Register]
do_wpo_smoke [Register]
do_wpo_start [Register]
do_wpo_stat [Register]
do_wpo_success [Register]
do_wpo_wait [Register]
domain [MemLoader.Make]
domain [Conditions]

Assumes a list of predicates in a Type section on top of the bundle.

domain [Sigs.LogicAssigns]

Memory footprint of a region.

domain [Sigs.Model]

Compute the set of chunks that hold the value of an object with the given C-type.

domain [Sigs.Sigma]

Footprint of a memory environment.

domain [Letify.Defs]
domain [Letify.Sigma]
domain [Wp.Conditions]

Assumes a list of predicates in a Type section on top of the bundle.

domain [Wp.Sigs.LogicAssigns]

Memory footprint of a region.

domain [Wp.Sigs.Model]

Compute the set of chunks that hold the value of an object with the given C-type.

domain [Wp.Sigs.Sigma]

Footprint of a memory environment.

doomed_if_valid [WpPropId]

Properties that are False-if-unreachable in case the PO is valid.

doomed_if_valid [Wp.WpPropId]

Properties that are False-if-unreachable in case the PO is valid.

downcast [Cint]

Dependent on model

downcast [Wp.Cint]

Dependent on model

driver [LogicBuiltins]
driver [Wp.LogicBuiltins]
dummy [Wpo.GOAL]
dummy [Definitions]
dummy [Wp.Wpo.GOAL]
dummy [Wp.Definitions]
dump [WpReached]
dump [Pcond]
dump [LogicBuiltins]
dump [RegionDump]
dump [RefUsage]
dump [LogicUsage]

Print on output

dump [Wp.Pcond]
dump [Wp.LogicBuiltins]
dump [Wp.RefUsage]
dump [Wp.LogicUsage]

Print on output

dump_bundle [Pcond]
dump_bundle [Wp.Pcond]
dump_env [CfgCompiler.Cfg]
dump_env [Wp.CfgCompiler.Cfg]
dump_sequence [Pcond]
dump_sequence [Wp.Pcond]
dump_strategies [Register]
E
e_add [Lang.F]
e_add [Wp.Lang.F]
e_and [Lang.F]
e_and [Wp.Lang.F]
e_apply [Letify.Sigma]
e_apply [Letify.Ground]
e_bigint [Lang.F]
e_bigint [Wp.Lang.F]
e_bind [Lang.F]
e_bind [Wp.Lang.F]
e_bool [Lang.F]
e_bool [Wp.Lang.F]
e_close [Lang.F]

Closes all specified binders

e_close [Wp.Lang.F]

Closes all specified binders

e_cnf [WpTac]
e_const [Lang.F]
e_const [Wp.Lang.F]
e_div [Lang.F]
e_div [Wp.Lang.F]
e_dnf [WpTac]
e_eq [Lang.F]
e_eq [Wp.Lang.F]
e_equiv [Lang.F]
e_equiv [Wp.Lang.F]
e_expr [Lang.F]
e_expr [Wp.Lang.F]
e_fact [Lang.F]
e_fact [Wp.Lang.F]
e_false [Lang.F]
e_false [Wp.Lang.F]
e_float [Lang.F]
e_float [Wp.Lang.F]
e_fun [Lang.F]
e_fun [Wp.Lang.F]
e_get [Lang.F]
e_get [Wp.Lang.F]
e_getfield [Lang.F]
e_getfield [Wp.Lang.F]
e_if [Lang.F]
e_if [Wp.Lang.F]
e_imply [Lang.F]
e_imply [Wp.Lang.F]
e_int [Lang.F]
e_int [Wp.Lang.F]
e_int64 [Lang.F]
e_int64 [Wp.Lang.F]
e_leq [Lang.F]
e_leq [Wp.Lang.F]
e_literal [Lang.F]
e_literal [Wp.Lang.F]
e_lt [Lang.F]
e_lt [Wp.Lang.F]
e_minus_one [Lang.F]
e_minus_one [Wp.Lang.F]
e_minus_one_real [Lang.F]
e_minus_one_real [Wp.Lang.F]
e_mod [Lang.F]
e_mod [Wp.Lang.F]
e_mul [Lang.F]
e_mul [Wp.Lang.F]
e_neq [Lang.F]
e_neq [Wp.Lang.F]
e_not [Lang.F]
e_not [Wp.Lang.F]
e_one [Lang.F]
e_one [Wp.Lang.F]
e_one_real [Lang.F]
e_one_real [Wp.Lang.F]
e_open [Lang.F]

Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default).

e_open [Wp.Lang.F]

Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default).

e_opp [Lang.F]
e_opp [Wp.Lang.F]
e_or [Lang.F]
e_or [Wp.Lang.F]
e_prod [Lang.F]
e_prod [Wp.Lang.F]
e_prop [Lang.F]
e_prop [Wp.Lang.F]
e_props [Lang.F]
e_props [Wp.Lang.F]
e_range [Lang.F]

e_range a b = b+1-a

e_range [Wp.Lang.F]

e_range a b = b+1-a

e_real [Lang.F]
e_real [Wp.Lang.F]
e_record [Lang.F]
e_record [Wp.Lang.F]
e_set [Lang.F]
e_set [Wp.Lang.F]
e_setfield [Lang.F]
e_setfield [Wp.Lang.F]
e_sub [Lang.F]
e_sub [Wp.Lang.F]
e_subst [Lang.F]
e_subst [Lang]

uses current pool

e_subst [Wp.Lang.F]
e_subst [Wp.Lang]

uses current pool

e_sum [Lang.F]
e_sum [Wp.Lang.F]
e_times [Lang.F]
e_times [Wp.Lang.F]
e_true [Lang.F]
e_true [Wp.Lang.F]
e_var [Lang.F]
e_var [Wp.Lang.F]
e_vars [Lang.F]

Sorted

e_vars [Wp.Lang.F]

Sorted

e_zero [Lang.F]
e_zero [Wp.Lang.F]
e_zero_real [Lang.F]
e_zero_real [Wp.Lang.F]
e_zint [Lang.F]
e_zint [Wp.Lang.F]
eat [Script]
edge_dst [Cil2cfg]
edge_src [Cil2cfg]

node and edges relations

effect [CfgCompiler.Cfg]

Represents all execution trace T such that, if T contains node a, then T also contains b with the given effect on corresponding memory states.

effect [Wp.CfgCompiler.Cfg]

Represents all execution trace T such that, if T contains node a, then T also contains b with the given effect on corresponding memory states.

either [CfgCompiler.Cfg]

Structurally corresponds to an arbitrary choice among the different possible executions.

either [Conditions]

Construct a disjunction bundle, with merging of all common parts.

either [Wp.CfgCompiler.Cfg]

Structurally corresponds to an arbitrary choice among the different possible executions.

either [Wp.Conditions]

Construct a disjunction bundle, with merging of all common parts.

elements [Vlist]
elements [Set.S]

Return the list of all elements of the given set.

emit [Warning]

Emit a warning in current context.

emit [Wp.Warning]

Emit a warning in current context.

empty [Conditions]

empty sequence, equivalent to true assumption

empty [Sigs.Sigma]

Same as Chunk.Set.empty

empty [Letify.Defs]
empty [Letify.Sigma]
empty [Vset]
empty [Splitter]
empty [Passive]
empty [Mcfg.S]
empty [Layout.Chunk]
empty [MemoryContext]
empty [Wp.Conditions]

empty sequence, equivalent to true assumption

empty [Wp.Sigs.Sigma]

Same as Chunk.Set.empty

empty [Wp.Vset]
empty [Wp.Splitter]
empty [Wp.Passive]
empty [Wp.Mcfg.S]
empty [Wp.MemoryContext]
empty [Set.S]

The empty set.

empty [Map.S]

The empty map.

empty_acc [WpStrategy]
empty_assigns_info [WpPropId]
empty_assigns_info [Wp.WpPropId]
empty_env [StmtSemantics.Make]
empty_env [Wp.StmtSemantics.Make]
encode [ProofScript]
env [Lang.F]
env [Wp.Lang.F]
env_at [LogicCompiler.Make]
env_at [Sigs.LogicSemantics]

Returns a new environment where the current memory state is moved to to the corresponding label.

env_at [Wp.LogicCompiler.Make]
env_at [Wp.Sigs.LogicSemantics]

Returns a new environment where the current memory state is moved to to the corresponding label.

env_let [LogicCompiler.Make]
env_let [Wp.LogicCompiler.Make]
env_letp [LogicCompiler.Make]
env_letp [Wp.LogicCompiler.Make]
env_letval [LogicCompiler.Make]
env_letval [Wp.LogicCompiler.Make]
env_script_update [Register]
epsilon [Rformat]
eq_alias [Region]
eqmem [MemLoader.Model]
eqmem_forall [MemLoader.Model]
eqp [Lang.F]
eqp [Wp.Lang.F]
equal [CfgCompiler.Cfg.C]
equal [CfgCompiler.Cfg.Node]
equal [Mstate]
equal [Sigs.Chunk]
equal [Letify.Sigma]
equal [Vset]
equal [Lang.F]

Same as ==

equal [RegionAnnot.Lpath]
equal [Layout.Value]
equal [Layout.Data]
equal [WpContext.SCOPE]
equal [WpContext.MODEL]
equal [WpContext.S]
equal [Clabels]
equal [Ctypes.AinfoComparable]
equal [Ctypes]
equal [Wp.CfgCompiler.Cfg.C]
equal [Wp.CfgCompiler.Cfg.Node]
equal [Wp.Mstate]
equal [Wp.Sigs.Chunk]
equal [Wp.Vset]
equal [Wp.Lang.F]

Same as ==

equal [Wp.WpContext.SCOPE]
equal [Wp.WpContext.MODEL]
equal [Wp.WpContext.S]
equal [Set.S]

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

equal [Map.S]

equal cmp m1 m2 tests whether the maps m1 and m2 are equal, that is, contain equal keys and associate them with equal data.

equal [Wp.Clabels]
equal [Wp.Ctypes.AinfoComparable]
equal [Wp.Ctypes]
equal_array [Cvalues]
equal_comp [Cvalues]
equal_float [Ctypes]
equal_float [Wp.Ctypes]
equal_obj [Sigs.CodeSemantics]

Same as equal_typ with an object type.

equal_obj [Wp.Sigs.CodeSemantics]

Same as equal_typ with an object type.

equal_object [Cvalues]
equal_typ [Sigs.CodeSemantics]

Computes the value of (a==b) provided both a and b are values with the given type.

equal_typ [Wp.Sigs.CodeSemantics]

Computes the value of (a==b) provided both a and b are values with the given type.

equation [Cvalues]
error [Script]
error [Warning]
error [Wp.Warning]
eval_eq [Lang.F]

Same as are_equal is Yes

eval_eq [Wp.Lang.F]

Same as are_equal is Yes

eval_leq [Lang.F]

Same as e_leq is e_true

eval_leq [Wp.Lang.F]

Same as e_leq is e_true

eval_lt [Lang.F]

Same as e_lt is e_true

eval_lt [Wp.Lang.F]

Same as e_lt is e_true

eval_neq [Lang.F]

Same as are_equal is No

eval_neq [Wp.Lang.F]

Same as are_equal is No

exercised [Register]
exist_intro [Conditions]

Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively.

exist_intro [Wp.Conditions]

Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively.

exists [ProofSession]
exists [Splitter]
exists [Wp.Splitter]
exists [Set.S]

exists p s checks if at least one element of the set satisfies the predicate p.

exists [Map.S]

exists p m checks if at least one binding of the map satisfies the predicate p.

exists [Parameter_sig.Set]

Is there some element satisfying the given predicate?

exp [Sigs.CodeSemantics]

Evaluate the expression on the given memory state.

exp [Wp.Sigs.CodeSemantics]

Evaluate the expression on the given memory state.

export [Strategy]
export [Tactical]

Register and returns the tactical

export [WpReport]
export [Vlist]
export [Wp.Strategy]
export [Wp.Tactical]

Register and returns the tactical

export_decl [Mcfg.Export]
export_decl [Wp.Mcfg.Export]
export_goal [Mcfg.Export]
export_goal [Wp.Mcfg.Export]
export_json [WpReport]
export_section [Mcfg.Export]
export_section [Wp.Mcfg.Export]
extern_f [Lang]

balance just give a default when link is not specified

extern_f [Wp.Lang]

balance just give a default when link is not specified

extern_fp [Lang]
extern_fp [Wp.Lang]
extern_p [Lang]
extern_p [Wp.Lang]
extern_s [Lang]
extern_s [Wp.Lang]
extern_t [Lang]
extern_t [Wp.Lang]
extract [Conditions]

Computes a formulae equivalent to the bundle.

extract [Letify.Defs]
extract [Wp.Conditions]

Computes a formulae equivalent to the bundle.

F
f32 [Cfloat]
f32 [Wp.Cfloat]
f64 [Cfloat]
f64 [Wp.Cfloat]
f_addr_of_int [MemMemory]

Physical address

f_base [MemMemory]
f_bits [Cint]

All bit-test functions

f_bits [Ctypes]

size in bits

f_bits [Wp.Cint]

All bit-test functions

f_bits [Wp.Ctypes]

size in bits

f_bitwised [Cint]

All except f_bit_positive

f_bitwised [Wp.Cint]

All except f_bit_positive

f_bytes [Ctypes]

size in bytes

f_bytes [Wp.Ctypes]

size in bytes

f_concat [Vlist]
f_cons [Vlist]
f_convert [Ctypes]
f_convert [Wp.Ctypes]
f_delta [Cfloat]
f_delta [Wp.Cfloat]
f_elt [Vlist]
f_epsilon [Cfloat]
f_epsilon [Wp.Cfloat]
f_global [MemMemory]
f_havoc [MemMemory]
f_iabs [Cmath]
f_int_of_addr [MemMemory]

Physical address

f_iter [Ctypes]
f_iter [Wp.Ctypes]
f_land [Cint]
f_land [Wp.Cint]
f_lnot [Cint]
f_lnot [Wp.Cint]
f_lor [Cint]
f_lor [Wp.Cint]
f_lsl [Cint]
f_lsl [Wp.Cint]
f_lsr [Cint]
f_lsr [Wp.Cint]
f_lxor [Cint]
f_lxor [Wp.Cint]
f_memo [Ctypes]

memoized, not-projectified

f_memo [Wp.Ctypes]

memoized, not-projectified

f_model [Cfloat]
f_model [Wp.Cfloat]
f_name [Ctypes]
f_name [Wp.Ctypes]
f_nil [Vlist]
f_nth [Vlist]
f_null [MemMemory]
f_offset [MemMemory]
f_rabs [Cmath]
f_real_of_int [Cmath]
f_region [MemMemory]
f_repeat [Vlist]
f_set_init [MemMemory]
f_shift [MemMemory]
f_sqrt [Cmath]
fadd [Cfloat]
fadd [Wp.Cfloat]
failed [VCS]
failed [Wp.VCS]
fcstat [WpReport]
fdiv [Cfloat]
fdiv [Wp.Cfloat]
feq [Cfloat]
feq [Wp.Cfloat]
field [MemLoader.Model]
field [Mstate]
field [Sigs.Model]

Return the memory location obtained by field access from a given memory location.

field [Cvalues.Logic]
field [Repr]
field [Lang]
field [Layout.Offset]
field [Wp.Mstate]
field [Wp.Sigs.Model]

Return the memory location obtained by field access from a given memory location.

field [Wp.Repr]
field [Wp.Lang]
field_id [Lang]
field_id [Wp.Lang]
field_init_id [Lang]
field_init_id [Wp.Lang]
field_offset [Region]
field_offset [Layout.Offset]
field_offset [Ctypes]
field_offset [Wp.Ctypes]
fields [TacInstance]
fields_of_adt [Lang]
fields_of_adt [Wp.Lang]
fields_of_field [Lang]
fields_of_field [Wp.Lang]
fields_of_tau [Lang]
fields_of_tau [Wp.Lang]
file_goal [Wpo.DISK]
file_goal [Wp.Wpo.DISK]
file_kf [Wpo.DISK]
file_kf [Wp.Wpo.DISK]
file_logerr [Wpo.DISK]
file_logerr [Wp.Wpo.DISK]
file_logout [Wpo.DISK]
file_logout [Wp.Wpo.DISK]
filename_for_prover [VCS]
filename_for_prover [Wp.VCS]
filter [GuiProver]
filter [Auto]
filter [TacInstance]
filter [Script]
filter [Filtering]
filter [Conditions]
filter [Splitter]
filter [Wp.Auto]
filter [Wp.Filtering]
filter [Wp.Conditions]
filter [Wp.Splitter]
filter [Set.S]

filter p s returns the set of all elements in s that satisfy predicate p.

filter [Map.S]

filter p m returns the map with all the bindings in m that satisfy predicate p.

filter_hypotheses [Lang]
filter_hypotheses [Wp.Lang]
filter_map_inplace [Hashtbl.S]
filter_pred [Cleaning]
filter_status [WpAnnot]
filter_type [Cleaning]
find [TacLemma]
find [Pcfg]
find [Letify.Sigma]
find [Cfloat]
find [Cil2cfg.HEsig]
find [WpContext.Registry]
find [Hashtbl.S]
find [Wp.Pcfg]
find [Wp.Cfloat]
find [Wp.WpContext.Registry]
find [Set.S]

find x s returns the element of s equal to x (according to Ord.compare), or raise Not_found if no such element exists.

find [Map.S]

find x m returns the current binding of x in m, or raises Not_found if no such binding exists.

find_all [Cil2cfg.HEsig]
find_all [Hashtbl.S]
find_fallback [Why3Provers]
find_first [Set.S]

find_first f s, where f is a monotonically increasing function, returns the lowest element e of s such that f e, or raises Not_found if no such element exists.

find_first [Map.S]

find_first f m, where f is a monotonically increasing function, returns the binding of m with the lowest key k such that f k, or raises Not_found if no such key exists.

find_first_opt [Set.S]

find_first_opt f s, where f is a monotonically increasing function, returns an option containing the lowest element e of s such that f e, or None if no such element exists.

find_first_opt [Map.S]

find_first_opt f m, where f is a monotonically increasing function, returns an option containing the binding of m with the lowest key k such that f k, or None if no such key exists.

find_last [Set.S]

find_last f s, where f is a monotonically decreasing function, returns the highest element e of s such that f e, or raises Not_found if no such element exists.

find_last [Map.S]

find_last f m, where f is a monotonically decreasing function, returns the binding of m with the highest key k such that f k, or raises Not_found if no such key exists.

find_last_opt [Set.S]

find_last_opt f s, where f is a monotonically decreasing function, returns an option containing the highest element e of s such that f e, or None if no such element exists.

find_last_opt [Map.S]

find_last_opt f m, where f is a monotonically decreasing function, returns an option containing the binding of m with the highest key k such that f k, or None if no such key exists.

find_lemma [Definitions]
find_lemma [Wp.Definitions]
find_lib [LogicBuiltins]

find a file in the includes of the current drivers

find_lib [Wp.LogicBuiltins]

find a file in the includes of the current drivers

find_name [Definitions]
find_name [Wp.Definitions]
find_opt [Why3Provers]
find_opt [Hashtbl.S]
find_opt [Set.S]

find_opt x s returns the element of s equal to x (according to Ord.compare), or None if no such element exists.

find_opt [Map.S]

find_opt x m returns Some v if the current binding of x in m is v, or None if no such binding exists.

find_symbol [Definitions]
find_symbol [Wp.Definitions]
first [ProverSearch]
fixpoint [Region]
fle [Cfloat]
fle [Wp.Cfloat]
float_lit [Cfloat]

Returns a string literal in decimal notation (without suffix) that reparses to the same value (when added suffix).

float_lit [Wp.Cfloat]

Returns a string literal in decimal notation (without suffix) that reparses to the same value (when added suffix).

float_of_int [Cfloat]
float_of_int [Wp.Cfloat]
float_of_real [Cfloat]
float_of_real [Wp.Cfloat]
floats [Lang]

type of floats

floats [Wp.Lang]

type of floats

flt [Cfloat]
flt [Wp.Cfloat]
flt_add [Cfloat]
flt_add [Wp.Cfloat]
flt_div [Cfloat]
flt_div [Wp.Cfloat]
flt_mul [Cfloat]
flt_mul [Wp.Cfloat]
flt_neg [Cfloat]
flt_neg [Wp.Cfloat]
flt_of_real [Cfloat]
flt_of_real [Wp.Cfloat]
flush [Warning]
flush [Wp.Warning]
fmode [TacCut]
fmul [Cfloat]
fmul [Wp.Cfloat]
fneq [Cfloat]
fneq [Wp.Cfloat]
fold [Splitter]
fold [Hashtbl.S]
fold [Wp.Splitter]
fold [Set.S]

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s, in increasing order.

fold [Map.S]

fold f m a computes (f kN dN ... (f k1 d1 a)...), where k1 ... kN are the keys of all bindings in m (in increasing order), and d1 ... dN are the associated data.

fold_bhv_post_cond [WpStrategy]

apply f_normal on the Normal postconditions, f_exits on the Exits postconditions, and warn on the others.

fold_lemmas [LogicUsage]
fold_lemmas [Wp.LogicUsage]
fold_nodes [Cil2cfg]

iterators

fopp [Cfloat]
fopp [Wp.Cfloat]
for_all [Splitter]
for_all [Wp.Splitter]
for_all [Set.S]

for_all p s checks if all elements of the set satisfy the predicate p.

for_all [Map.S]

for_all p m checks if all the bindings of the map satisfy the predicate p.

forall_intro [Conditions]

Introduce universally quantified formulae: head forall quantifiers are instanciated to fresh variables in current pool and left-implies are extracted, recursively.

forall_intro [Wp.Conditions]

Introduce universally quantified formulae: head forall quantifiers are instanciated to fresh variables in current pool and left-implies are extracted, recursively.

fork [ProofEngine]
formal [LogicCompiler.Make]
formal [Clabels]
formal [Wp.LogicCompiler.Make]
formal [Wp.Clabels]
forward [ProofEngine]
forward [Letify.Ground]
fq32 [Cfloat]
fq32 [Wp.Cfloat]
fq64 [Cfloat]
fq64 [Wp.Cfloat]
frame [LogicCompiler.Make]
frame [Sigs.LogicSemantics]

Make a fresh frame with the given function.

frame [Sigs.Model]

Assert the memory is a proper heap state preceeding the function entry point.

frame [Wp.LogicCompiler.Make]
frame [Wp.Sigs.LogicSemantics]

Make a fresh frame with the given function.

frame [Wp.Sigs.Model]

Assert the memory is a proper heap state preceeding the function entry point.

framed [Layout.Root]
frames [MemMemory]
frames [MemLoader.Model]
free [Context]

Performs the job with local context cleared.

free [Wp.Context]

Performs the job with local context cleared.

fresh [Lang.F]
fresh [Wp.Lang.F]
freshen [Lang]
freshen [Wp.Lang]
freshvar [Lang]
freshvar [Wp.Lang]
from [Layout.Root]
froms [StmtSemantics.Make]
froms [Wp.StmtSemantics.Make]
fsub [Cfloat]
fsub [Wp.Cfloat]
ftau [Cfloat]

model independant

ftau [Wp.Cfloat]

model independant

fusion [Region]
fusionned [Region]
G
garbled [Layout.Compound]
gcd [Layout.Matrix]
generate [WpRTE]
generate_all [WpRTE]

Invoke RTE on all selected functions

generate_call [VC]
generate_call [Wp.VC]
generate_ip [VC]
generate_ip [Wp.VC]
generate_kf [VC]
generate_kf [Wp.VC]
generated_f [Lang]
generated_f [Wp.Lang]
generated_p [Lang]
generated_p [Wp.Lang]
get [ProverScript]
get [ProofEngine]
get [ProofSession]
get [Tactical.Fmap]

raises Not_found if absent

get [CfgCompiler.Cfg.E]
get [CfgCompiler.Cfg.T]
get [CfgCompiler.Cfg.P]
get [CfgCompiler.Cfg.C]
get [Sigs.Sigma]

Lazily get the variable for a chunk.

get [Lang.F.Subst]
get [Cil2cfg]
get [RegionAnalysis]
get [RefUsage]
get [WpContext.Generator]
get [WpContext.Registry]
get [Context]

Retrieves the current value of the context.

get [Dyncall]

Returns None if there is no specified dynamic call.

get [Wp.Tactical.Fmap]

raises Not_found if absent

get [Wp.CfgCompiler.Cfg.E]
get [Wp.CfgCompiler.Cfg.T]
get [Wp.CfgCompiler.Cfg.P]
get [Wp.CfgCompiler.Cfg.C]
get [Wp.Sigs.Sigma]

Lazily get the variable for a chunk.

get [Wp.Lang.F.Subst]
get [Wp.WpContext.Generator]
get [Wp.WpContext.Registry]
get [Wp.Context]

Retrieves the current value of the context.

get [Wp.RefUsage]
get_addrof [Region]
get_alias [Region]
get_annots [WpStrategy]
get_array [Ctypes]
get_array [Wp.Ctypes]
get_array_dim [Ctypes]
get_array_dim [Wp.Ctypes]
get_array_size [Ctypes]
get_array_size [Wp.Ctypes]
get_asgn_goal [WpStrategy]
get_asgn_hyp [WpStrategy]
get_bhv [WpStrategy]
get_both_hyp_goals [WpStrategy]
get_builtin_type [Lang]
get_builtin_type [Wp.Lang]
get_call_asgn [WpStrategy]
get_call_hyp [WpStrategy]

To be used as hypotheses around a call, (the pre are in get_call_pre_goal)

get_call_out_edges [Cil2cfg]

similar to succ_e g v but gives the edge to VcallOut first and the edge to Vexit second.

get_call_post [WpStrategy]

Post-checks of a called function to be considered as goal only

get_call_pre [WpStrategy]

Preconditions of a called function to be considered as hyp and goal (similar to get_both_hyp_goals).

get_call_pre_strategies [WpAnnot]
get_call_type [Cil2cfg]
get_called_assigns [WpAnnot]

Properties for assigns of kf

get_called_exit_conditions [WpAnnot]
get_called_post_conditions [WpAnnot]
get_called_preconditions_at [WpAnnot]
get_context [VC]
get_context [Wpo]
get_context [WpContext]
get_context [Wp.Wpo]
get_context [Wp.VC]
get_context [Wp.WpContext]
get_copies [Region]
get_cut [WpStrategy]

the bool in get_cut results says if the property has to be considered as a both goal and hyp (goal=true, or hyp only (goal=false)

get_descr [Wpo.GOAL]
get_descr [WpContext]
get_descr [Wp.Wpo.GOAL]
get_descr [Wp.WpContext]
get_description [VC]
get_description [Wp.VC]
get_dir [Cache]
get_edge_labels [Cil2cfg]
get_edge_next_stmt [Cil2cfg]
get_edge_stmt [Cil2cfg]

Complete get_edge_labels and returns the associated stmt, if any.

get_emitter [WpContext]
get_emitter [Wp.WpContext]
get_exit_edges [Cil2cfg]

Find the edges e that goes to the Vexit node inside the statement beginning at node n

get_fct [Wp_parameters]
get_fct [Wp.Wp_parameters]
get_file_logerr [Wpo]

only filename, might not exists

get_file_logerr [Wp.Wpo]

only filename, might not exists

get_file_logout [Wpo]

only filename, might not exists

get_file_logout [Wp.Wpo]

only filename, might not exists

get_files [Wpo]
get_files [Wp.Wpo]
get_formula [VC]
get_formula [Wp.VC]
get_frame [LogicCompiler.Make]
get_frame [Sigs.LogicSemantics]

Get the current frame, or raise a fatal error if none.

get_frame [Wp.LogicCompiler.Make]
get_frame [Wp.Sigs.LogicSemantics]

Get the current frame, or raise a fatal error if none.

get_froms [Region]
get_function_name [Parameter_sig.String]

returns the given argument only if it is a valid function name (see Parameter_customize.get_c_ified_functions for more information), and abort otherwise.

get_function_strategies [WpAnnot]
get_gamma [Lang]
get_gamma [Wp.Lang]
get_gid [Wpo]

Dynamically exported

get_gid [Wp.Wpo]

Dynamically exported

get_goal_only [WpStrategy]
get_hits [Cache]
get_hyp_only [WpStrategy]
get_hypotheses [Lang]
get_hypotheses [Wp.Lang]
get_id [VC]
get_id [Wp.VC]
get_id_prop_strategies [WpAnnot]
get_index [Wpo]
get_index [Wp.Wpo]
get_induction [WpPropId]

Quite don't understand what is going on here...

get_induction [Wp.WpPropId]
get_induction_labels [LogicUsage]

Given an inductive phi{...A...}.

get_induction_labels [Wp.LogicUsage]

Given an inductive phi{...A...}.

get_int [Tactical]
get_int [Ctypes]
get_int [Wp.Tactical]
get_int [Wp.Ctypes]
get_int64 [Ctypes]
get_int64 [Wp.Ctypes]
get_internal_edges [Cil2cfg]

Find the edges e of the statement node n postcondition and the set of edges that are inside the statement (e excluded).

get_kf [WpStrategy]
get_label [Wpo]
get_label [Wp.Wpo]
get_legacy [WpPropId]

Unique legacy identifier of prop_id

get_legacy [Wp.WpPropId]

Unique legacy identifier of prop_id

get_logerr [VC]

only file name, might not exists

get_logerr [Wp.VC]

only file name, might not exists

get_logout [VC]

only file name, might not exists

get_logout [Wp.VC]

only file name, might not exists

get_merged [Region]
get_miss [Cache]
get_mode [Cache]
get_model [VC]
get_model [Wpo]
get_model [WpContext]
get_model [Wp.Wpo]
get_model [Wp.VC]
get_model [Wp.WpContext]
get_name [LogicUsage]
get_name [Wp.LogicUsage]
get_offset [Region]
get_opt [Context]

Retrieves the current value of the context.

get_opt [Wp.Context]

Retrieves the current value of the context.

get_option [LogicBuiltins]

return the values of option (group, name), return the empty list if not set

get_option [Wp.LogicBuiltins]

return the values of option (group, name), return the empty list if not set

get_output [Wp_parameters]
get_output [Wp.Wp_parameters]
get_output_dir [Wp_parameters]
get_output_dir [Wp.Wp_parameters]
get_overflows [Wp_parameters]
get_overflows [Wp.Wp_parameters]
get_plain_string [Parameter_sig.String]

always return the argument, even if the argument is not a function name.

get_pointed [Region]
get_pool [Lang]
get_pool [Wp.Lang]
get_possible_values [Parameter_sig.String]

What are the acceptable values for this parameter.

get_post_edges [Cil2cfg]

Find the edges where the postconditions of the node statement have to be checked.

get_post_label [Cil2cfg]

Get the label to be used for the Post state of the node contract if any.

get_pre_edges [Cil2cfg]

Find the edges where the precondition of the node statement have to be checked.

get_proof [Wpo]
get_proof [Wp.Wpo]
get_property [VC]
get_property [Wpo]

Dynamically exported

get_property [Wp.Wpo]

Dynamically exported

get_property [Wp.VC]
get_propid [WpPropId]

Unique identifier of prop_id

get_propid [Wp.WpPropId]

Unique identifier of prop_id

get_prover_names [Register]
get_pstat [Register]
get_range [Parameter_sig.Int]

What is the possible range of values for this parameter.

get_removed [Cache]
get_result [VC]
get_result [Cache]
get_result [Wpo]
get_result [Wp.Wpo]
get_result [Wp.VC]
get_results [VC]
get_results [Wpo]
get_results [Wp.Wpo]
get_results [Wp.VC]
get_roots [Region]
get_scope [VC]
get_scope [Wpo]
get_scope [WpContext]
get_scope [Wp.Wpo]
get_scope [Wp.VC]
get_scope [Wp.WpContext]
get_sequent [VC]
get_sequent [Wp.VC]
get_session [Wp_parameters]
get_session [Wp.Wp_parameters]
get_session_dir [Wp_parameters]
get_session_dir [Wp.Wp_parameters]
get_stepout [VCS]

0 means no-stepout

get_stepout [Wp.VCS]

0 means no-stepout

get_steps [Wpo]
get_steps [Wp.Wpo]
get_strategies [ProofEngine]
get_switch_edges [Cil2cfg]

similar to succ_e g v but give the switch cases and the default edge

get_target [Wpo]
get_target [Wp.Wpo]
get_test_edges [Cil2cfg]

similar to succ_e g v but tests the branch to return (then-edge, else-edge)

get_time [Wpo]
get_time [Rformat]

get_time T t returns k such that T[k-1] <= t <= T[k], T is extended with T[-1]=0 and T[N]=+oo.

get_time [Wp.Wpo]
get_timeout [VCS]

0 means no-timeout

get_timeout [Wp.VCS]

0 means no-timeout

global [Sigs.Model]

Given a pointer value p, assumes this pointer p (when valid) is allocated outside the function frame under analysis.

global [Wp.Sigs.Model]

Given a pointer value p, assumes this pointer p (when valid) is allocated outside the function frame under analysis.

global_axioms [WpStrategy]
goal [ProofEngine]
goals_nodes [StmtSemantics.Make]
goals_nodes [Wp.StmtSemantics.Make]
goals_of_property [Wpo]

All POs related to a given property.

goals_of_property [Wp.Wpo]

All POs related to a given property.

goto [ProofEngine]
goto [CfgCompiler.Cfg]

Represents all execution traces T such that, if T contains node a, T also contains node b and memory states at a and b are equal.

goto [Wp.CfgCompiler.Cfg]

Represents all execution traces T such that, if T contains node a, T also contains node b and memory states at a and b are equal.

group [Splitter]
group [Wp.Splitter]
guard [CfgCompiler.Cfg]

Structurally corresponds to an assume control-flow.

guard [Wp.CfgCompiler.Cfg]

Structurally corresponds to an assume control-flow.

guard' [CfgCompiler.Cfg]

Same than guard but the condition is negated

guard' [Wp.CfgCompiler.Cfg]

Same than guard but the condition is negated

guards [LogicCompiler.Make]
guards [Sigs.LogicSemantics]

Returns the current gamma environment from the current frame.

guards [Wp.LogicCompiler.Make]
guards [Wp.Sigs.LogicSemantics]

Returns the current gamma environment from the current frame.

H
hack [LogicBuiltins]

Replace a logic definition or predicate by a built-in function.

hack [Wp.LogicBuiltins]

Replace a logic definition or predicate by a built-in function.

hack_type [LogicBuiltins]

Replace a logic type definition or predicate by a built-in type.

hack_type [Wp.LogicBuiltins]

Replace a logic type definition or predicate by a built-in type.

handle [Warning]

Handle the error and emit a warning with specified severity and effect if a context has been set.

handle [Wp.Warning]

Handle the error and emit a warning with specified severity and effect if a context has been set.

has_at_frame [LogicCompiler.Make]
has_at_frame [Sigs.LogicSemantics]

Chek if a frame already has a specific envioronement for the given label.

has_at_frame [Wp.LogicCompiler.Make]
has_at_frame [Wp.Sigs.LogicSemantics]

Chek if a frame already has a specific envioronement for the given label.

has_copies [Region]
has_ctype [Cvalues]
has_deref [Region]
has_dkey [Wp_parameters]
has_dkey [Wp.Wp_parameters]
has_exit [Cil2cfg]

whether an exit edge exists or not

has_gamma [Lang]
has_gamma [Wp.Lang]
has_init [Mcfg.S]
has_init [Wp.Mcfg.S]
has_layout [Region]
has_ltype [LogicCompiler.Make]
has_ltype [Wp.LogicCompiler.Make]
has_names [Region]
has_offset [Region]
has_out [Wp_parameters]
has_out [Wp.Wp_parameters]
has_pointed [Region]
has_print_generated [Wp_parameters]

Debugging Categories

has_print_generated [Wp.Wp_parameters]

Debugging Categories

has_proof [ProofScript]

Has a tactical alternative

has_return [Region]
has_roots [Region]
has_session [Wp_parameters]
has_session [Wp.Wp_parameters]
has_shortcut [Why3Provers]
has_verdict [Wpo]
has_verdict [Wp.Wpo]
hash [Sigs.Chunk]
hash [Lang.F]

Constant time

hash [WpContext.SCOPE]
hash [WpContext.MODEL]
hash [WpContext.S]
hash [Ctypes.AinfoComparable]
hash [Ctypes]
hash [Wp.Sigs.Chunk]
hash [Wp.Lang.F]

Constant time

hash [Wp.WpContext.SCOPE]
hash [Wp.WpContext.MODEL]
hash [Wp.WpContext.S]
hash [Wp.Ctypes.AinfoComparable]
hash [Wp.Ctypes]
have [Conditions]

Predicate for Have and such, True for any other

have [Wp.Conditions]

Predicate for Have and such, True for any other

havoc [Auto]
havoc [CfgCompiler.Cfg]

Inserts an assigns effect between nodes a and b, correspondings to all the written memory chunks accessible in execution paths delimited by the effects sequence of nodes.

havoc [MemLoader.Model]
havoc [MemLoader.Make]
havoc [Sigs.Sigma]

All the chunks in the provided footprint are generated and made fresh.

havoc [Wp.Auto]
havoc [Wp.CfgCompiler.Cfg]

Inserts an assigns effect between nodes a and b, correspondings to all the written memory chunks accessible in execution paths delimited by the effects sequence of nodes.

havoc [Wp.Sigs.Sigma]

All the chunks in the provided footprint are generated and made fresh.

havoc_any [Sigs.Sigma]

All the chunks are made fresh.

havoc_any [Wp.Sigs.Sigma]

All the chunks are made fresh.

havoc_chunk [Sigs.Sigma]

Generate a new fresh variable for the given chunk.

havoc_chunk [Wp.Sigs.Sigma]

Generate a new fresh variable for the given chunk.

havoc_length [MemLoader.Make]
head [ProofEngine]
head [Tactical]
head [Footprint]

Head only footprint

head [Conditions]

Predicate for Have and such, Condition for Branch, True for Either

head [Wp.Tactical]
head [Wp.Conditions]

Predicate for Have and such, Condition for Branch, True for Either

here [Clabels]
here [Wp.Clabels]
hints_for [Proof]
hypotheses [Sigs.Model]

Computes the memory model partitionning of the memory locations.

hypotheses [Lang]
hypotheses [Wp.Sigs.Model]

Computes the memory model partitionning of the memory locations.

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

i_name [Ctypes]
i_name [Wp.Ctypes]
iadd [Cint]
iadd [Wp.Cint]
id [LogicBuiltins]
id [Region]
id [WpContext.Registry]
id [WpContext.SCOPE]
id [WpContext.MODEL]
id [WpContext.S]
id [Wp.LogicBuiltins]
id [Wp.WpContext.Registry]
id [Wp.WpContext.SCOPE]
id [Wp.WpContext.MODEL]
id [Wp.WpContext.S]
ident [Factory]
ident [Tactical]
ident [Script]
ident [Wp.Tactical]
ident [Wp.Factory]
idents [Script]
idiv [Cint]
idiv [Wp.Cint]
if_else [Splitter]
if_else [Wp.Splitter]
if_then [Splitter]
if_then [Wp.Splitter]
imod [Cint]
imod [Wp.Cint]
implies [CfgCompiler.Cfg]

implies is the dual of either.

implies [Wp.CfgCompiler.Cfg]

implies is the dual of either.

imul [Cint]
imul [Wp.Cint]
in_frame [LogicCompiler.Make]
in_frame [Sigs.LogicSemantics]

Execute the given closure with the specified current frame.

in_frame [Wp.LogicCompiler.Make]
in_frame [Wp.Sigs.LogicSemantics]

Execute the given closure with the specified current frame.

in_range [Vset]
in_range [Wp.Vset]
in_size [Vset]
in_size [Wp.Vset]
in_state [Lang.For_export]
in_state [Wp.Lang.For_export]
included [MemMemory]
included [Sigs.Model]

Return the formula that tests if two segment are included

included [Cvalues.Logic]
included [Layout.Range]
included [Wp.Sigs.Model]

Return the formula that tests if two segment are included

incr [Parameter_sig.Int]

Increment the integer.

index [ProverSearch]
index [Conditions]

Compute steps' id of sequent left hand-side.

index [Mstate]
index [Layout.Offset]
index [Wp.Conditions]

Compute steps' id of sequent left hand-side.

index [Wp.Mstate]
indexed [Layout.Root]
infoprover [Lang]

same information for all the provers

infoprover [Wp.Lang]

same information for all the provers

init [StmtSemantics.Make]

connect init to here.

init [CfgCompiler.Cfg.T]
init [Sigs.CodeSemantics]

Express that some variable has some initial value at the given memory state.

init [Mcfg.S]
init [Clabels]
init [Wp.StmtSemantics.Make]
init [Wp.CfgCompiler.Cfg.T]
init [Wp.Sigs.CodeSemantics]

Express that some variable has some initial value at the given memory state.

init [Wp.Mcfg.S]
init [Wp.Clabels]
init' [CfgCompiler.Cfg.T]
init' [Wp.CfgCompiler.Cfg.T]
init_filter [Conditions]
init_filter [Wp.Conditions]
init_footprint [MemLoader.Model]
init_of_ctype [Lang]
init_of_ctype [Wp.Lang]
init_of_object [Lang]
init_of_object [Wp.Lang]
initialized [MemLoader.Make]
initialized [Sigs.Model]

Return the formula that tests if a memory state is initialized (according to Sigs.acs) in the given memory state at the given segment.

initialized [Cvalues.Logic]
initialized [Wp.Sigs.Model]

Return the formula that tests if a memory state is initialized (according to Wp.Sigs.acs) in the given memory state at the given segment.

initialized_obj [Cvalues]
insert [Tactical]
insert [Conditions]

Insert a step in the sequent immediately at the specified position.

insert [Wp.Tactical]
insert [Wp.Conditions]

Insert a step in the sequent immediately at the specified position.

instance [Factory]
instance [Auto]
instance [Wp.Auto]
instance [Wp.Factory]
instance_goal [TacInstance]
instance_have [TacInstance]
instance_of [Sigs.CodeSemantics]

Check whether a function pointer is (an instance of) some kernel function.

instance_of [Wp.Sigs.CodeSemantics]

Check whether a function pointer is (an instance of) some kernel function.

instr [StmtSemantics.Make]
instr [Wp.StmtSemantics.Make]
int [Tactical]
int [Wp.Tactical]
int_of_bool [Cmath]
int_of_loc [Sigs.Model]

Cast a memory location into its absolute memory address, given as an integer with the given C-type.

int_of_loc [Wp.Sigs.Model]

Cast a memory location into its absolute memory address, given as an integer with the given C-type.

int_of_real [Cmath]
inter [Cvalues.Logic]
inter [Vset]
inter [Wp.Vset]
inter [Set.S]

Set intersection.

intersect [Conditions]

Variables of predicate and the bundle intersects

intersect [Lang.F]
intersect [Wp.Conditions]

Variables of predicate and the bundle intersects

intersect [Wp.Lang.F]
intersectp [Lang.F]
intersectp [Wp.Lang.F]
introduction [Conditions]

Performs existential, universal and hypotheses introductions

introduction [Wp.Conditions]

Performs existential, universal and hypotheses introductions

introduction_eq [Conditions]

Same as introduction but returns the same sequent is None

introduction_eq [Wp.Conditions]

Same as introduction but returns the same sequent is None

intros [Conditions]

Assumes a list of predicates in a Have section on top of the bundle.

intros [Wp.Conditions]

Assumes a list of predicates in a Have section on top of the bundle.

intuition [Auto]
intuition [Wp.Auto]
invalid [VCS]
invalid [Sigs.Model]

Returns the formula that tests if the entire memory is invalid for write access.

invalid [Cvalues.Logic]
invalid [Wp.VCS]
invalid [Wp.Sigs.Model]

Returns the formula that tests if the entire memory is invalid for write access.

iopp [Cint]
iopp [Wp.Cint]
ip_lemma [LogicUsage]
ip_lemma [Wp.LogicUsage]
isGlobalInitConst [WpStrategy]

True if the variable is global, not extern, with a "const" qualifier type.

isInitConst [WpStrategy]

True if both options -const-readonly and -wp-init are positioned, and the variable is global, not extern, with a "const" type (see hasConstAttribute).

is_absorbant [Lang.F]
is_absorbant [Wp.Lang.F]
is_aliased [Region]
is_aliased [Layout.Usage]
is_aliased [Layout.Alias]
is_arith [Lang.F]

Integer or Real sort

is_arith [Wp.Lang.F]

Integer or Real sort

is_array [Ctypes]
is_array [Wp.Ctypes]
is_assigns [WpPropId]
is_assigns [Wp.WpPropId]
is_atomic [Lang.F]

Constants and variables

is_atomic [Wp.Lang.F]

Constants and variables

is_auto [VCS]
is_auto [Wp.VCS]
is_available [Why3Provers]
is_back_edge [Cil2cfg]
is_builtin [Lang]
is_builtin [Wp.Lang]
is_builtin_type [Lang]
is_builtin_type [Wp.Lang]
is_call_assigns [WpPropId]
is_call_assigns [Wp.WpPropId]
is_char [Ctypes]
is_char [Wp.Ctypes]
is_check [WpPropId]
is_check [Wp.WpPropId]
is_cint [Cint]

Raises Not_found if not.

is_cint [Wp.Cint]

Raises Not_found if not.

is_cint_simplifier [Cint]

Remove the is_cint in formulas that are redundant with other conditions.

is_cint_simplifier [Wp.Cint]

Remove the is_cint in formulas that are redundant with other conditions.

is_closed [Lang.F]

No bound variables

is_closed [Wp.Lang.F]

No bound variables

is_cnf [WpTac]
is_comp [Ctypes]
is_comp [Wp.Ctypes]
is_complete [AssignsCompleteness]
is_complete [Wp.AssignsCompleteness]
is_composed [WpAnnot]

whether a proof needs several lemma to be complete

is_compound [Ctypes]
is_compound [Wp.Ctypes]
is_computed [RefUsage]
is_computed [Wp.RefUsage]
is_computing [VCS]
is_computing [Wp.VCS]
is_dead_annot [WpReached]

False assertions and loop invariant.

is_dead_code [WpReached]

Checks whether the stmt has a dead-code annotation.

is_default [LogicBuiltins]
is_default [Wp.LogicBuiltins]
is_default_behavior [WpStrategy]
is_defined [WpContext]
is_defined [Wp.WpContext]
is_dnf [WpTac]
is_empty [Tactical]
is_empty [Conditions]

No step at all

is_empty [Vset]
is_empty [Passive]
is_empty [Region]
is_empty [Layout.Cluster]
is_empty [Wp.Tactical]
is_empty [Wp.Conditions]

No step at all

is_empty [Wp.Vset]
is_empty [Wp.Passive]
is_empty [Set.S]

Test whether a set is empty or not.

is_empty [Map.S]

Test whether a map is empty or not.

is_empty_script [Proof]

Check a proof script text for emptyness

is_equal [Lang.F]
is_equal [Wp.Lang.F]
is_exp_range [Sigs.CodeSemantics]

Express that all objects in a range of locations have a given value.

is_exp_range [Wp.Sigs.CodeSemantics]

Express that all objects in a range of locations have a given value.

is_false [Cvalues]

p ? 0 : 1

is_false [Lang.F]

Constant time.

is_false [Wp.Lang.F]

Constant time.

is_framed [Sigs.Chunk]

Whether the chunk is local to a function call.

is_framed [Wp.Sigs.Chunk]

Whether the chunk is local to a function call.

is_garbled [Region]
is_garbled [Layout.Cluster]
is_here [Clabels]
is_here [Wp.Clabels]
is_init_atom [MemLoader.Model]
is_init_range [MemLoader.Model]
is_int [Lang.F]

Integer sort

is_int [Wp.Lang.F]

Integer sort

is_invalid [WpAnnot]

whether an invalid proof result has been registered or not

is_literal [Lang]
is_literal [Wp.Lang]
is_loop_preservation [WpPropId]
is_loop_preservation [Wp.WpPropId]
is_main_init [WpStrategy]

The function is the main entry point AND it is not a lib entry

is_mainstream [Why3Provers]
is_neutral [Lang.F]
is_neutral [Wp.Lang.F]
is_null [Sigs.Model]

Return the formula that check if a given location is null

is_null [Cvalues]
is_null [Wp.Sigs.Model]

Return the formula that check if a given location is null

is_object [Cvalues]
is_passed [Wpo]

proved, or unknown for smoke tests

is_passed [Wp.Wpo]

proved, or unknown for smoke tests

is_pfalse [Lang.F]
is_pfalse [Wp.Lang.F]
is_pointer [Ctypes]
is_pointer [Wp.Ctypes]
is_positive_or_null [Cint]
is_positive_or_null [Wp.Cint]
is_predicate [WpReached]

If returns true the predicate has always the given boolean value.

is_primitive [Lang.F]

Constants only

is_primitive [Wp.Lang.F]

Constants only

is_prop [Lang.F]

Boolean or Property

is_prop [Wp.Lang.F]

Boolean or Property

is_proved [VC]
is_proved [Wpo]

do not tries simplification, check prover results

is_proved [VCS]
is_proved [WpAnnot]

whether all partial proofs have been accumulated or not

is_proved [Wp.Wpo]

do not tries simplification, check prover results

is_proved [Wp.VC]
is_proved [Wp.VCS]
is_prover [ProofScript]
is_ptrue [Lang.F]
is_ptrue [Wp.Lang.F]
is_read [Region]
is_real [Lang.F]

Real sort

is_real [Wp.Lang.F]

Real sort

is_recursive [LogicUsage]
is_recursive [Wp.LogicUsage]
is_requires [WpPropId]
is_requires [Wp.WpPropId]
is_shifted [Region]
is_shifted [Layout.Usage]
is_simple [Lang.F]

Constants, variables, functions of arity 0

is_simple [Wp.Lang.F]

Constants, variables, functions of arity 0

is_smoke_test [Wpo]
is_smoke_test [WpPropId]
is_smoke_test [Wp.Wpo]
is_smoke_test [Wp.WpPropId]
is_subterm [Lang.F]
is_subterm [Wp.Lang.F]
is_tactic [ProofScript]
is_tactic [Wpo]
is_tactic [WpPropId]
is_tactic [Wp.Wpo]
is_tactic [Wp.WpPropId]
is_trivial [VC]
is_trivial [Wpo.VC_Annot]
is_trivial [Wpo.VC_Lemma]
is_trivial [Wpo.GOAL]
is_trivial [Wpo]

do not tries simplification, do not check prover results

is_trivial [Conditions]

Goal is true or hypotheses contains false.

is_trivial [Wp.Wpo.VC_Annot]
is_trivial [Wp.Wpo.VC_Lemma]
is_trivial [Wp.Wpo.GOAL]
is_trivial [Wp.Wpo]

do not tries simplification, do not check prover results

is_trivial [Wp.VC]
is_trivial [Wp.Conditions]

Goal is true or hypotheses contains false.

is_true [Conditions]

Contains only true or empty steps

is_true [Cvalues]

p ? 1 : 0

is_true [Lang.F]

Constant time.

is_true [Wp.Conditions]

Contains only true or empty steps

is_true [Wp.Lang.F]

Constant time.

is_unknown [Wpo]

at least one prover returns « Unknown »

is_unknown [Wp.Wpo]

at least one prover returns « Unknown »

is_updating [Cache]
is_valid [Wpo]

true if the result is valid.

is_valid [VCS]
is_valid [Wp.Wpo]

true if the result is valid.

is_valid [Wp.VCS]
is_verdict [VCS]
is_verdict [Wp.VCS]
is_well_formed [Sigs.Model]

Provides the constraint corresponding to the kind of data stored by all chunks in sigma.

is_well_formed [Wp.Sigs.Model]

Provides the constraint corresponding to the kind of data stored by all chunks in sigma.

is_written [Region]
is_zero [Sigs.CodeSemantics]

Express that the object (of specified type) at the given location is filled with zeroes.

is_zero [Lang.F]
is_zero [Wp.Sigs.CodeSemantics]

Express that the object (of specified type) at the given location is filled with zeroes.

is_zero [Wp.Lang.F]
isub [Cint]
isub [Wp.Cint]
iter [ProofEngine]
iter [Strategy]
iter [Tactical]
iter [Footprint]

Width-first full iterator.

iter [Wpo]
iter [WpTarget]
iter [MemVar.VarUsage]
iter [Pcfg]
iter [Conditions]

Iterate only over the head steps of the sequence.

iter [Mstate]
iter [Sigs.Model]

Debug

iter [Sigs.Sigma]

Iterates over the chunks and associated variables already accessed so far in the environment.

iter [Letify.Sigma]
iter [Definitions]
iter [Splitter]
iter [Passive]
iter [Region]
iter [RefUsage]
iter [WpContext.Registry]
iter [Wp.Wpo]
iter [Wp.Strategy]
iter [Wp.Tactical]
iter [Hashtbl.S]
iter [Wp.MemVar.VarUsage]
iter [Wp.Pcfg]
iter [Wp.Conditions]

Iterate only over the head steps of the sequence.

iter [Wp.Mstate]
iter [Wp.Sigs.Model]

Debug

iter [Wp.Sigs.Sigma]

Iterates over the chunks and associated variables already accessed so far in the environment.

iter [Wp.Definitions]
iter [Wp.Splitter]
iter [Wp.Passive]
iter [Wp.WpContext.Registry]
iter [Wp.RefUsage]
iter [Set.S]

iter f s applies f in turn to all elements of s.

iter [Map.S]

iter f m applies f to all bindings in map m.

iter2 [Sigs.Sigma]

Same as iter for both environments.

iter2 [Wp.Sigs.Sigma]

Same as iter for both environments.

iter_composer [Tactical]
iter_composer [Wp.Tactical]
iter_consequence_literals [Lang]

iter_consequence_literals assume_from_litteral hypothesis applies the function assume_from_litteral on literals that are a consequence of the hypothesis (i.e.

iter_consequence_literals [Wp.Lang]

iter_consequence_literals assume_from_litteral hypothesis applies the function assume_from_litteral on literals that are a consequence of the hypothesis (i.e.

iter_copies [Region]
iter_deref [Region]
iter_edges [Cil2cfg]
iter_fct [Wp_parameters]
iter_fct [Wp.Wp_parameters]
iter_fusion [Region]
iter_ip [VC]
iter_ip [Wp.VC]
iter_kf [VC]
iter_kf [Wp_parameters]
iter_kf [Wp.VC]
iter_kf [Wp.Wp_parameters]
iter_lemmas [LogicUsage]
iter_lemmas [Wp.LogicUsage]
iter_names [Region]
iter_nodes [Cil2cfg]
iter_offset [Region]
iter_on_goals [Wpo]

Dynamically exported.

iter_on_goals [Wp.Wpo]

Dynamically exported.

iter_read [Region]
iter_shift [Region]
iter_sorted [WpContext.Registry]
iter_sorted [Wp.WpContext.Registry]
iter_strings [Region]
iter_vars [Region]
iter_write [Region]
J
join [Sigs.Sigma]

Make two environment pairwise equal via the passive form.

join [Passive]
join [Wp.Sigs.Sigma]

Make two environment pairwise equal via the passive form.

join [Wp.Passive]
json_of_param [ProofScript]
json_of_parameters [ProofScript]
json_of_result [ProofScript]
json_of_selection [ProofScript]
json_of_tactic [ProofScript]
jtactic [ProofScript]
K
key [Script]
kf_context [Wpo]
kf_context [Wp.Wpo]
kfailed [VCS]
kfailed [Wp.VCS]
kind_of_id [WpPropId]

get the 'kind' information.

kind_of_id [Wp.WpPropId]

get the 'kind' information.

kind_of_tau [LogicBuiltins]
kind_of_tau [Wp.LogicBuiltins]
ko_status [GuiProver]
L
l_and [Cint]
l_and [Wp.Cint]
l_lsl [Cint]
l_lsl [Wp.Cint]
l_lsr [Cint]
l_lsr [Wp.Cint]
l_not [Cint]
l_not [Wp.Cint]
l_or [Cint]
l_or [Wp.Cint]
l_xor [Cint]
l_xor [Wp.Cint]
label [Mcfg.S]
label [Wp.Mcfg.S]
label_of_prop_id [WpPropId]

Short description of the kind of PO

label_of_prop_id [Wp.WpPropId]

Short description of the kind of PO

labels_assert_after [NormAtLabels]
labels_assert_after [Wp.NormAtLabels]
labels_assert_before [NormAtLabels]
labels_assert_before [Wp.NormAtLabels]
labels_axiom [NormAtLabels]
labels_axiom [Wp.NormAtLabels]
labels_empty [NormAtLabels]
labels_empty [Wp.NormAtLabels]
labels_fct_assigns [NormAtLabels]
labels_fct_assigns [Wp.NormAtLabels]
labels_fct_post [NormAtLabels]
labels_fct_post [Wp.NormAtLabels]
labels_fct_pre [NormAtLabels]
labels_fct_pre [Wp.NormAtLabels]
labels_loop [NormAtLabels]
labels_loop [Wp.NormAtLabels]
labels_predicate [NormAtLabels]
labels_predicate [Wp.NormAtLabels]
labels_stmt_assigns [NormAtLabels]
labels_stmt_assigns [Wp.NormAtLabels]
labels_stmt_post [NormAtLabels]
labels_stmt_post [Wp.NormAtLabels]
labels_stmt_pre [NormAtLabels]
labels_stmt_pre [Wp.NormAtLabels]
last [MemLoader.Model]
launch [Register]
lc_closed [Lang.F]
lc_closed [Wp.Lang.F]
lc_iter [Lang.F]
lc_iter [Wp.Lang.F]
ldomain [Cvalues]
lemma [Auto]
lemma [LogicCompiler.Make]
lemma [Conditions]

Performs existential, universal and hypotheses introductions

lemma [Sigs.LogicSemantics]

Compile a lemma definition.

lemma [Wp.Auto]
lemma [Wp.LogicCompiler.Make]
lemma [Wp.Conditions]

Performs existential, universal and hypotheses introductions

lemma [Wp.Sigs.LogicSemantics]

Compile a lemma definition.

lemma_id [Lang]
lemma_id [Wp.Lang]
length [Splitter]
length [Hashtbl.S]
length [Wp.Splitter]
lfun [Repr]
lfun [Wp.Repr]
lift [Vset]
lift [Lang.F]
lift [Wp.Vset]
lift [Wp.Lang.F]
lift_add [Vset]
lift_add [Wp.Vset]
lift_sub [Vset]
lift_sub [Wp.Vset]
list [Conditions]

Same domain than iter.

list [Wp.Conditions]

Same domain than iter.

literal [Sigs.Model]

Return the memory location of a constant string, the id is a unique identifier.

literal [Wp.Sigs.Model]

Return the memory location of a constant string, the id is a unique identifier.

load [ProofSession]
load [MemLoader.Make]
load [Sigs.Model]

Return the value of the object of the given type at the given location in the given memory state.

load [Cvalues.Logic]
load [Wp.Sigs.Model]

Return the value of the object of the given type at the given location in the given memory state.

load_driver [Driver]

Memoized loading of drivers according to current WP options.

load_driver [Wp.Driver]

Memoized loading of drivers according to current WP options.

load_float [MemLoader.Model]
load_int [MemLoader.Model]
load_pointer [MemLoader.Model]
loadvalue [MemLoader.Make]
loc [Cvalues.Logic]
loc [Splitter]
loc [Wp.Splitter]
loc_diff [Sigs.Model]

Compute the length in bytes between two memory locations

loc_diff [Wp.Sigs.Model]

Compute the length in bytes between two memory locations

loc_eq [Sigs.Model]
loc_eq [Wp.Sigs.Model]
loc_leq [Sigs.Model]

Memory location comparisons

loc_leq [Wp.Sigs.Model]

Memory location comparisons

loc_lt [Sigs.Model]
loc_lt [Wp.Sigs.Model]
loc_neq [Sigs.Model]
loc_neq [Wp.Sigs.Model]
loc_of_exp [Sigs.CodeSemantics]

Compile an expression as a location.

loc_of_exp [Wp.Sigs.CodeSemantics]

Compile an expression as a location.

loc_of_int [Sigs.Model]

Cast a term representing an absolute memory address (to some c_object) given as an integer, into an abstract memory location.

loc_of_int [Wp.Sigs.Model]

Cast a term representing an absolute memory address (to some c_object) given as an integer, into an abstract memory location.

loc_of_term [Sigs.LogicSemantics]

Same as term above but expects a single loc or a single pointer value.

loc_of_term [Wp.Sigs.LogicSemantics]

Same as term above but expects a single loc or a single pointer value.

local [LogicCompiler.Make]
local [Sigs.LogicSemantics]

Make a local frame reusing the current pool and gamma.

local [Lang]
local [Wp.LogicCompiler.Make]
local [Wp.Sigs.LogicSemantics]

Make a local frame reusing the current pool and gamma.

local [Wp.Lang]
locate [Footprint]

Locate the occurrence of select footprint inside a term.

location [ProverTask]
location [Wp.ProverTask]
logic [LogicCompiler.Make]
logic [LogicBuiltins]
logic [Wp.LogicCompiler.Make]
logic [Wp.LogicBuiltins]
logic_constant [Cvalues]
logic_id [Lang]
logic_id [Wp.Lang]
logic_info [LogicCompiler.Make]
logic_info [Wp.LogicCompiler.Make]
logic_lemma [LogicUsage]
logic_lemma [Wp.LogicUsage]
logic_var [LogicCompiler.Make]
logic_var [Wp.LogicCompiler.Make]
lookup [Strategy]
lookup [Tactical]
lookup [Footprint]

Retrieve back the k-th occurrence of a footprint inside a term.

lookup [Mstate]
lookup [Sigs.Model]

Try to interpret a term as an in-memory operation located at this program point.

lookup [LogicBuiltins]
lookup [Clabels]

lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.

lookup [Wp.Strategy]
lookup [Wp.Tactical]
lookup [Wp.Mstate]
lookup [Wp.Sigs.Model]

Try to interpret a term as an in-memory operation located at this program point.

lookup [Wp.LogicBuiltins]
lookup [Wp.Clabels]

lookup bindings lparam retrieves the actual label for the label in bindings for label parameter lparam.

loop_current [Clabels]
loop_current [Wp.Clabels]
loop_entry [Mcfg.S]
loop_entry [Clabels]
loop_entry [Wp.Mcfg.S]
loop_entry [Wp.Clabels]
loop_step [Mcfg.S]
loop_step [Wp.Mcfg.S]
loopcurrent [Clabels]
loopcurrent [Wp.Clabels]
loopentry [Clabels]
loopentry [Wp.Clabels]
lval [Sigs.LogicSemantics]

Compile a term l-value into a (typed) abstract location

lval [Sigs.CodeSemantics]

Evaluate the left-value on the given memory state.

lval [Wp.Sigs.LogicSemantics]

Compile a term l-value into a (typed) abstract location

lval [Wp.Sigs.CodeSemantics]

Evaluate the left-value on the given memory state.

M
main [Register]
main [ProofEngine]
make [GuiNavigator]
make [Strategy]
make [Wpo.GOAL]
make [Wp.Wpo.GOAL]
make [Wp.Strategy]
make_output_dir [Wp_parameters]
make_output_dir [Wp.Wp_parameters]
make_type [Datatype.Hashtbl]
map [Cvalues.Logic]
map [Vset]
map [Splitter]
map [Wp.Vset]
map [Wp.Splitter]
map [Set.S]

map f s is the set whose elements are f a0,f a1...

map [Map.S]

map f m returns a map with same domain as m, where the associated value a of all bindings of m has been replaced by the result of the application of f to a.

map_condition [Conditions]

Rewrite all root predicates in condition

map_condition [Wp.Conditions]

Rewrite all root predicates in condition

map_l2t [Cvalues.Logic]
map_loc [Cvalues.Logic]
map_logic [Cvalues]
map_opp [Cvalues.Logic]
map_opp [Vset]
map_opp [Wp.Vset]
map_sequence [Conditions]

Rewrite all root predicates in sequence

map_sequence [Wp.Conditions]

Rewrite all root predicates in sequence

map_sequent [Conditions]

Rewrite all root predocates in hypotheses and goal

map_sequent [Wp.Conditions]

Rewrite all root predocates in hypotheses and goal

map_sloc [Cvalues]
map_step [Conditions]

Rewrite all root predicates in step

map_step [Wp.Conditions]

Rewrite all root predicates in step

map_t2l [Cvalues.Logic]
map_value [Cvalues]
mapi [Tactical]
mapi [Wp.Tactical]
mapi [Map.S]

Same as Map.S.map, but the function receives as arguments both the key and the associated value for each binding of the map.

mark_e [Lang.F]
mark_e [Wp.Lang.F]
mark_p [Lang.F]

Returns a list of terms to be shared among all shared or marked subterms.

mark_p [Wp.Lang.F]

Returns a list of terms to be shared among all shared or marked subterms.

marker [Lang.F]
marker [Wp.Lang.F]
mask_simplifier [Cint]
mask_simplifier [Wp.Cint]
matches [Footprint]

Head match

matrix [Definitions]
matrix [Wp.Definitions]
max_binding [Map.S]

Same as Map.S.min_binding, but returns the binding with the largest key in the given map.

max_binding_opt [Map.S]

Same as Map.S.min_binding_opt, but returns the binding with the largest key in the given map.

max_elt [Set.S]

Same as Set.S.min_elt, but returns the largest element of the given set.

max_elt_opt [Set.S]

Same as Set.S.min_elt_opt, but returns the largest element of the given set.

mem [Sigs.Sigma]

Whether a chunk has been assigned.

mem [Layout.Chunk]
mem [WpContext.Generator]
mem [WpContext.Registry]
mem [Clabels]
mem [Wprop.Indexed2]
mem [Wprop.Indexed]
mem [Hashtbl.S]
mem [Wp.Sigs.Sigma]

Whether a chunk has been assigned.

mem [Wp.WpContext.Generator]
mem [Wp.WpContext.Registry]
mem [Set.S]

mem x s tests whether x belongs to the set s.

mem [Map.S]

mem x m returns true if m contains a binding for x, and false otherwise.

mem [Wp.Clabels]
mem [Parameter_sig.Set]

Does the given element belong to the set?

mem_at [LogicCompiler.Make]
mem_at [Sigs.LogicSemantics]

Returns the memory state at the requested label.

mem_at [Wp.LogicCompiler.Make]
mem_at [Wp.Sigs.LogicSemantics]

Returns the memory state at the requested label.

mem_at_frame [LogicCompiler.Make]
mem_at_frame [Sigs.LogicSemantics]

Get the memory environment at the given label.

mem_at_frame [Wp.LogicCompiler.Make]
mem_at_frame [Wp.Sigs.LogicSemantics]

Get the memory environment at the given label.

mem_builtin_type [Lang]
mem_builtin_type [Wp.Lang]
mem_frame [LogicCompiler.Make]
mem_frame [Sigs.LogicSemantics]

Same as mem_at_frame but for the current frame.

mem_frame [Wp.LogicCompiler.Make]
mem_frame [Wp.Sigs.LogicSemantics]

Same as mem_at_frame but for the current frame.

member [Vset]
member [Wp.Vset]
memoize [WpContext.Registry]

with circularity protection

memoize [Wp.WpContext.Registry]

with circularity protection

merge [VCS]
merge [Conditions]

Performs a diff-based disjunction, introducing If-Then-Else or Either branches when possible.

merge [Sigs.Sigma]

Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins.

merge [Letify.Defs]
merge [Splitter]
merge [Matrix]
merge [Mcfg.S]
merge [Layout.Pack]
merge [Layout.Flat]
merge [Layout.RW]
merge [Layout.Root]
merge [Layout.Cluster]
merge [Layout.Overlay]
merge [Layout.Matrix]
merge [Layout.Value]
merge [Layout.Usage]
merge [Layout.Alias]
merge [Wp.VCS]
merge [Wp.Conditions]

Performs a diff-based disjunction, introducing If-Then-Else or Either branches when possible.

merge [Wp.Sigs.Sigma]

Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins.

merge [Wp.Splitter]
merge [Wp.Mcfg.S]
merge [Map.S]

merge f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.

merge_all [Splitter]
merge_all [Wp.Splitter]
merge_assign_info [WpPropId]
merge_assign_info [Wp.WpPropId]
merge_list [Sigs.Sigma]

Same than Sigs.Sigma.merge but for a list of sigmas.

merge_list [Wp.Sigs.Sigma]

Same than Wp.Sigs.Sigma.merge but for a list of sigmas.

meta [CfgCompiler.Cfg]

Attach meta informations to a node.

meta [Wp.CfgCompiler.Cfg]

Attach meta informations to a node.

min_binding [Map.S]

Return the binding with the smallest key in a given map (with respect to the Ord.compare ordering), or raise Not_found if the map is empty.

min_binding_opt [Map.S]

Return the binding with the smallest key in the given map (with respect to the Ord.compare ordering), or None if the map is empty.

min_elt [Set.S]

Return the smallest element of the given set (with respect to the Ord.compare ordering), or raise Not_found if the set is empty.

min_elt_opt [Set.S]

Return the smallest element of the given set (with respect to the Ord.compare ordering), or None if the set is empty.

missing_guards [WpRTE]

Returns true if RTE annotations should be generated for the given function and model (and are not generated yet).

mk_asm_assigns_desc [WpPropId]
mk_asm_assigns_desc [Wp.WpPropId]
mk_assert_id [WpPropId]
mk_assert_id [Wp.WpPropId]
mk_assigns_info [WpPropId]
mk_assigns_info [Wp.WpPropId]
mk_axiom_info [WpPropId]
mk_axiom_info [Wp.WpPropId]
mk_bhv_from_id [WpPropId]

\from property of function or statement behavior assigns.

mk_bhv_from_id [Wp.WpPropId]

\from property of function or statement behavior assigns.

mk_call_pre_id [WpPropId]

mk_call_pre_id called_kf s_call called_pre

mk_call_pre_id [Wp.WpPropId]

mk_call_pre_id called_kf s_call called_pre

mk_check [WpPropId]
mk_check [Wp.WpPropId]
mk_code_annot_ids [WpPropId]
mk_code_annot_ids [Wp.WpPropId]
mk_compl_bhv_id [WpPropId]

complete behaviors property.

mk_compl_bhv_id [Wp.WpPropId]

complete behaviors property.

mk_decrease_id [WpPropId]
mk_decrease_id [Wp.WpPropId]
mk_disj_bhv_id [WpPropId]

disjoint behaviors property.

mk_disj_bhv_id [Wp.WpPropId]

disjoint behaviors property.

mk_env [LogicCompiler.Make]
mk_env [Sigs.LogicSemantics]

Create a new environment.

mk_env [Wp.LogicCompiler.Make]
mk_env [Wp.Sigs.LogicSemantics]

Create a new environment.

mk_fct_assigns_id [WpPropId]

function assigns

mk_fct_assigns_id [Wp.WpPropId]

function assigns

mk_fct_from_id [WpPropId]

\from property of function behavior assigns.

mk_fct_from_id [Wp.WpPropId]

\from property of function behavior assigns.

mk_fct_post_id [WpPropId]
mk_fct_post_id [Wp.WpPropId]
mk_frame [LogicCompiler.Make]
mk_frame [Sigs.LogicSemantics]

Full featured constructor for frames, with fresh pool and gamma.

mk_frame [Wp.LogicCompiler.Make]
mk_frame [Wp.Sigs.LogicSemantics]

Full featured constructor for frames, with fresh pool and gamma.

mk_init_assigns [WpPropId]
mk_init_assigns [Wp.WpPropId]
mk_inv_hyp_id [WpPropId]

Invariant used as hypothesis

mk_inv_hyp_id [Wp.WpPropId]

Invariant used as hypothesis

mk_kf_any_assigns_info [WpPropId]
mk_kf_any_assigns_info [Wp.WpPropId]
mk_kf_assigns_desc [WpPropId]
mk_kf_assigns_desc [Wp.WpPropId]
mk_lemma_id [WpPropId]

axiom identification

mk_lemma_id [Wp.WpPropId]

axiom identification

mk_loop_any_assigns_info [WpPropId]
mk_loop_any_assigns_info [Wp.WpPropId]
mk_loop_assigns_desc [WpPropId]
mk_loop_assigns_desc [Wp.WpPropId]
mk_loop_assigns_id [WpPropId]
mk_loop_assigns_id [Wp.WpPropId]
mk_loop_from_id [WpPropId]

\from property of loop assigns.

mk_loop_from_id [Wp.WpPropId]

\from property of loop assigns.

mk_loop_inv_id [WpPropId]

Invariant establishment and preservation

mk_loop_inv_id [Wp.WpPropId]

Invariant establishment and preservation

mk_part [WpPropId]

mk_part pid (k, n) build the identification for the k/n part of pid.

mk_part [Wp.WpPropId]

mk_part pid (k, n) build the identification for the k/n part of pid.

mk_pre_id [WpPropId]
mk_pre_id [Wp.WpPropId]
mk_pred_info [WpPropId]
mk_pred_info [Wp.WpPropId]
mk_property [WpPropId]
mk_property [Wp.WpPropId]
mk_smoke [WpPropId]
mk_smoke [Wp.WpPropId]
mk_stmt_any_assigns_info [WpPropId]
mk_stmt_any_assigns_info [Wp.WpPropId]
mk_stmt_assigns_desc [WpPropId]
mk_stmt_assigns_desc [Wp.WpPropId]
mk_stmt_assigns_id [WpPropId]
mk_stmt_assigns_id [Wp.WpPropId]
mk_stmt_post_id [WpPropId]
mk_stmt_post_id [Wp.WpPropId]
mk_strategy [WpStrategy]
mk_var_decr_id [WpPropId]

Variant decrease

mk_var_decr_id [Wp.WpPropId]

Variant decrease

mk_var_pos_id [WpPropId]

Variant positive

mk_var_pos_id [Wp.WpPropId]

Variant positive

mk_variant_properties [WpStrategy]
monotonic_init [MemLoader.Model]
move_at [LogicCompiler.Make]
move_at [Sigs.LogicSemantics]

Move the compilation environment to the specified Here memory state.

move_at [Wp.LogicCompiler.Make]
move_at [Wp.Sigs.LogicSemantics]

Move the compilation environment to the specified Here memory state.

N
name [MemLoader.Model]
name [WpContext.IData]
name [WpContext.Data]
name [WpContext.Entries]
name [Context]
name [Why3Provers]
name [Clabels]
name [Wp_error]
name [Wp.WpContext.IData]
name [Wp.WpContext.Data]
name [Wp.WpContext.Entries]
name [Wp.Context]
name [Wp.Clabels]
name_of_field [Lang]
name_of_field [Wp.Lang]
name_of_lfun [Lang]
name_of_lfun [Wp.Lang]
name_of_prover [VCS]
name_of_prover [Wp.VCS]
named [TacLemma]
nearest_elt_ge [Datatype.Set]
nearest_elt_le [Datatype.Set]
negate [Cvalues]
new_driver [LogicBuiltins]

Creates a configured driver from an existing one.

new_driver [Wp.LogicBuiltins]

Creates a configured driver from an existing one.

new_env [Mcfg.S]

optionally init env with user logic variables

new_env [Wp.Mcfg.S]

optionally init env with user logic variables

new_gamma [Lang]
new_gamma [Wp.Lang]
new_pool [Lang]
new_pool [Wp.Lang]
next [Pcfg]
next [Clabels]
next [Wp.Pcfg]
next [Wp.Clabels]
nil [Conditions]

Same as empty

nil [Wp.Conditions]

Same as empty

no_infinite_array [Ctypes]
no_infinite_array [Wp.Ctypes]
no_result [VCS]
no_result [Wp.VCS]
no_status [GuiProver]
node [CfgCompiler.Cfg]

fresh node

node [Wp.CfgCompiler.Cfg]

fresh node

node_context [ProofEngine]
node_stmt_opt [Cil2cfg]
node_type [Cil2cfg]
nodes [CfgCompiler.Cfg.P]
nodes [Wp.CfgCompiler.Cfg.P]
noid [Region]
nop [CfgCompiler.Cfg]

Structurally, nop is an empty execution trace.

nop [Wp.CfgCompiler.Cfg]

Structurally, nop is an empty execution trace.

normalize [WpStrategy]
not [Lang.N]
not [Wp.Lang.N]
not_equal_obj [Sigs.CodeSemantics]

Same as not_equal_typ with an object type.

not_equal_obj [Wp.Sigs.CodeSemantics]

Same as not_equal_typ with an object type.

not_equal_typ [Sigs.CodeSemantics]

Computes the value of (a==b) provided both a and b are values with the given type.

not_equal_typ [Wp.Sigs.CodeSemantics]

Computes the value of (a==b) provided both a and b are values with the given type.

not_yet_implemented [Wp_error]
null [Sigs.Model]

Return the location of the null pointer

null [Cvalues]

test for null pointer value

null [Wp.Sigs.Model]

Return the location of the null pointer

num_of_bhv_from [WpPropId]
num_of_bhv_from [Wp.WpPropId]
O
object_of [Ctypes]
object_of [Wp.Ctypes]
object_of_array_elem [Ctypes]
object_of_array_elem [Wp.Ctypes]
object_of_logic_pointed [Ctypes]
object_of_logic_pointed [Wp.Ctypes]
object_of_logic_type [Ctypes]
object_of_logic_type [Wp.Ctypes]
object_of_pointed [Ctypes]
object_of_pointed [Wp.Ctypes]
occurs [Conditions]
occurs [Sigs.LogicSemantics]

Member of vars.

occurs [Sigs.Model]

Test if a location depend on a given logic variable

occurs [Vset]
occurs [Lang.F]
occurs [Wp.Conditions]
occurs [Wp.Sigs.LogicSemantics]

Member of vars.

occurs [Wp.Sigs.Model]

Test if a location depend on a given logic variable

occurs [Wp.Vset]
occurs [Wp.Lang.F]
occurs_e [Strategy]
occurs_e [Wp.Strategy]
occurs_p [Strategy]
occurs_p [Wp.Strategy]
occurs_q [Strategy]
occurs_q [Wp.Strategy]
occurs_x [Strategy]
occurs_x [Wp.Strategy]
occurs_y [Strategy]
occurs_y [Wp.Strategy]
occursp [Lang.F]
occursp [Wp.Lang.F]
of_behavior [RegionAnnot]
of_class [Region]
of_cstring [Region]
of_cvar [Region]
of_dims [Matrix]
of_extension [RegionAnnot]
of_integer [Cint]
of_integer [Wp.Cint]
of_list [Set.S]

of_list l creates a set from a list of elements.

of_logic [Clabels]

Assumes the logic label only comes from normalized or non-ambiguous labels.

of_logic [Wp.Clabels]

Assumes the logic label only comes from normalized or non-ambiguous labels.

of_name [Region]
of_null [Region]
of_pred [Definitions.Trigger]
of_pred [Wp.Definitions.Trigger]
of_real [Cint]
of_real [Wp.Cint]
of_region_pointer [MemLoader.Model]
of_return [Region]
of_seq [Hashtbl.S]
of_seq [Set.S]

Build a set from the given bindings

of_seq [Map.S]

Build a map from the given bindings

of_term [Definitions.Trigger]
of_term [Wp.Definitions.Trigger]
off [Parameter_sig.Bool]

Set the boolean to false.

ok_status [GuiProver]
old [Clabels]
old [Wp.Clabels]
on [Parameter_sig.Bool]

Set the boolean to true.

on_context [WpContext]
on_context [Wp.WpContext]
on_reload [GuiPanel]
on_remove [Wpo]
on_remove [Wp.Wpo]
on_update [GuiPanel]
once [Footprint]

Width-first once iterator.

once [Layout.Overlay]
open_file [Script]
ordered [Vset]

- limit: result when either parameter is None strict: if true, comparison is < instead of <=

ordered [Wp.Vset]

- limit: result when either parameter is None strict: if true, comparison is < instead of <=

output_dot [CfgCompiler.Cfg]
output_dot [Wp.CfgCompiler.Cfg]
overflow [TacOverflow]
overlap [Layout.Range]
P
p_addr_le [MemMemory]
p_addr_lt [MemMemory]
p_all [Lang.F]
p_all [Wp.Lang.F]
p_and [Lang.F]
p_and [Wp.Lang.F]
p_any [Lang.F]
p_any [Wp.Lang.F]
p_apply [Letify.Sigma]
p_apply [Letify.Ground]
p_bind [Lang.F]
p_bind [Wp.Lang.F]
p_bits [Ctypes]

pointer size in bits

p_bits [Wp.Ctypes]

pointer size in bits

p_bool [Lang.F]
p_bool [Wp.Lang.F]
p_bools [Lang.F]
p_bools [Wp.Lang.F]
p_bytes [Ctypes]

pointer size in bits

p_bytes [Wp.Ctypes]

pointer size in bits

p_call [Lang.F]
p_call [Wp.Lang.F]
p_cinits [MemMemory]
p_close [Lang.F]

Quantify over (sorted) free variables

p_close [Wp.Lang.F]

Quantify over (sorted) free variables

p_conj [Lang.F]
p_conj [Wp.Lang.F]
p_disj [Lang.F]
p_disj [Wp.Lang.F]
p_eqmem [MemMemory]
p_equal [Lang.F]
p_equal [Wp.Lang.F]
p_equals [Lang.F]
p_equals [Wp.Lang.F]
p_equiv [Lang.F]
p_equiv [Wp.Lang.F]
p_exists [Lang.F]
p_exists [Wp.Lang.F]
p_expr [Lang.F]
p_expr [Wp.Lang.F]
p_false [Lang.F]
p_false [Wp.Lang.F]
p_float [ProverTask]

Float group pattern \([0-9.]+\)

p_float [Wp.ProverTask]

Float group pattern \([0-9.]+\)

p_forall [Lang.F]
p_forall [Wp.Lang.F]
p_framed [MemMemory]
p_group [ProverTask]

Put pattern in group \(p\)

p_group [Wp.ProverTask]

Put pattern in group \(p\)

p_hyps [Lang.F]
p_hyps [Wp.Lang.F]
p_if [Lang.F]
p_if [Wp.Lang.F]
p_imply [Lang.F]
p_imply [Wp.Lang.F]
p_included [MemMemory]
p_int [ProverTask]

Int group pattern \([0-9]+\)

p_int [Wp.ProverTask]

Int group pattern \([0-9]+\)

p_invalid [MemMemory]
p_is_init_r [MemMemory]
p_leq [Lang.F]
p_leq [Wp.Lang.F]
p_linked [MemMemory]
p_lt [Lang.F]
p_lt [Wp.Lang.F]
p_monotonic [MemMemory]
p_name [RegionAnnot]
p_neq [Lang.F]
p_neq [Wp.Lang.F]
p_not [Lang.F]
p_not [Wp.Lang.F]
p_or [Lang.F]
p_or [Wp.Lang.F]
p_positive [Lang.F]
p_positive [Wp.Lang.F]
p_sconst [MemMemory]
p_separated [MemMemory]
p_string [ProverTask]

String group pattern "\(...\)"

p_string [Wp.ProverTask]

String group pattern "\(...\)"

p_subst [Lang.F]
p_subst [Lang]

uses current pool

p_subst [Wp.Lang.F]
p_subst [Wp.Lang]

uses current pool

p_subst_var [Lang.F]
p_subst_var [Wp.Lang.F]
p_true [Lang.F]
p_true [Wp.Lang.F]
p_until_space [ProverTask]

No space group pattern "\\(^ \t\n*\\)"

p_until_space [Wp.ProverTask]

No space group pattern "\\(^ \t\n*\\)"

p_valid_obj [MemMemory]
p_valid_rd [MemMemory]
p_valid_rw [MemMemory]
p_vars [Lang.F]

Sorted

p_vars [Wp.Lang.F]

Sorted

parallel [StmtSemantics.Make]

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp.

parallel [Wp.StmtSemantics.Make]

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp.

param [MemVar.VarUsage]
param [Wp.MemVar.VarUsage]
param_of_json [ProofScript]
parameters [Lang]

definitions

parameters [Wp.Lang]

definitions

parameters_of_json [ProofScript]
params [TacInstance]
parasite [Conditions]
parasite [Wp.Conditions]
parent [ProofEngine]
parse [Factory]

Apply specifications to default setup.

parse [Wp.Factory]

Apply specifications to default setup.

parse_coqproof [Proof]

parse_coqproof f parses a coq-file f and fetch the first proof.

parse_mode [VCS]
parse_mode [Wp.VCS]
parse_prover [VCS]
parse_prover [Wp.VCS]
partition [Set.S]

partition p s returns a pair of sets (s1, s2), where s1 is the set of all the elements of s that satisfy the predicate p, and s2 is the set of all the elements of s that do not satisfy p.

partition [Map.S]

partition p m returns a pair of maps (m1, m2), where m1 contains all the bindings of s that satisfy the predicate p, and m2 is the map with all the bindings of s that do not satisfy p.

parts_of_id [WpPropId]

get the 'part' information.

parts_of_id [Wp.WpPropId]

get the 'part' information.

pattern [Footprint]

Generate head footprint up to size

pending [ProofEngine]

0 means proved

pending [ProofScript]

pending goals

pending_any [ProofScript]

minimum of pending goals

plain [Cvalues]
pointed [Layout.Value]
pointer [MemTyped]
pointer [Lang]

type of pointers

pointer [Wp.MemTyped]
pointer [Wp.Lang]

type of pointers

pointer_loc [Sigs.Model]

Interpret an address value (a pointer) as an abstract location.

pointer_loc [Wp.Sigs.Model]

Interpret an address value (a pointer) as an abstract location.

pointer_val [Sigs.Model]

Return the adress value (a pointer) of an abstract location.

pointer_val [Wp.Sigs.Model]

Return the adress value (a pointer) of an abstract location.

poly [Lang]

polymorphism

poly [Wp.Lang]

polymorphism

pool [ProofEngine]
pool [Plang]
pool [Lang.F]
pool [Wp.Plang]
pool [Wp.Lang.F]
pop [Context]
pop [Wp.Context]
post [Clabels]
post [Wp.Clabels]
pp [CfgCompiler.Cfg.Node]
pp [Wp.CfgCompiler.Cfg.Node]
pp_acs [Cvalues]
pp_annots [WpStrategy]
pp_assign_info [WpPropId]
pp_assign_info [Wp.WpPropId]
pp_assigns [Wp_error]
pp_assigns_desc [WpPropId]
pp_assigns_desc [Wp.WpPropId]
pp_axiom_info [WpPropId]
pp_axiom_info [Wp.WpPropId]
pp_axiomatics [Wpo]
pp_axiomatics [Wp.Wpo]
pp_bound [Cvalues]
pp_bound [Vset]
pp_bound [Wp.Vset]
pp_call_type [Cil2cfg]
pp_calls [Dyncall]
pp_chain [Layout.Offset]
pp_clause [Tactical]

Debug only

pp_clause [Wp.Tactical]

Debug only

pp_cluster [Definitions]
pp_cluster [Wp.Definitions]
pp_depend [Wpo]
pp_depend [Wp.Wpo]
pp_dependencies [Wpo]
pp_dependencies [Wp.Wpo]
pp_dependency [Wpo]
pp_dependency [Wp.Wpo]
pp_edge [Cil2cfg]
pp_epred [Lang.F]
pp_epred [Wp.Lang.F]
pp_eterm [Lang.F]
pp_eterm [Wp.Lang.F]
pp_file [ProverTask]
pp_file [Wp.ProverTask]
pp_float [Ctypes]
pp_float [Wp.Ctypes]
pp_frame [LogicCompiler.Make]
pp_frame [Sigs.LogicSemantics]
pp_frame [Wp.LogicCompiler.Make]
pp_frame [Wp.Sigs.LogicSemantics]
pp_function [Wpo]
pp_function [Wp.Wpo]
pp_goal [Wpo]
pp_goal [Wp.Wpo]
pp_goal_flow [Wpo]
pp_goal_flow [Wp.Wpo]
pp_index [Wpo]
pp_index [Wp.Wpo]
pp_info_of_strategy [WpStrategy]
pp_int [Ctypes]
pp_int [Wp.Ctypes]
pp_logfile [Wpo]
pp_logfile [Wp.Wpo]
pp_logic [Cvalues]
pp_logic_label [Wp_error]
pp_mode [VCS]
pp_mode [Wp.VCS]
pp_node [Cil2cfg]
pp_node_type [Cil2cfg]
pp_object [Ctypes]
pp_object [Wp.Ctypes]
pp_param [MemoryContext]
pp_param [Wp.MemoryContext]
pp_pred [Lang.F]
pp_pred [Wp.Lang.F]
pp_pred_info [WpPropId]
pp_pred_info [Wp.WpPropId]
pp_pred_of_pred_info [WpPropId]
pp_pred_of_pred_info [Wp.WpPropId]
pp_profile [LogicUsage]
pp_profile [Wp.LogicUsage]
pp_propid [WpPropId]

Print unique id of prop_id

pp_propid [Wp.WpPropId]

Print unique id of prop_id

pp_prover [VCS]
pp_prover [Wp.VCS]
pp_region [Cvalues]
pp_result [VCS]
pp_result [Wp.VCS]
pp_result_qualif [VCS]
pp_result_qualif [Wp.VCS]
pp_rloc [Cvalues]
pp_script [ProofSession]
pp_script_for [ProofSession]
pp_selection [Tactical]

Debug only

pp_selection [Wp.Tactical]

Debug only

pp_sloc [Cvalues]
pp_string_list [Wp_error]
pp_suffix_id [Matrix]
pp_tau [Lang.F]
pp_tau [Wp.Lang.F]
pp_term [Lang.F]
pp_term [Wp.Lang.F]
pp_time [Rformat]

Pretty print time in hour, minutes, seconds, or milliseconds, as appropriate

pp_time_range [Rformat]
pp_title [Wpo]
pp_title [Wp.Wpo]
pp_value [Sigs.CodeSemantics]
pp_value [Cvalues]
pp_value [Wp.Sigs.CodeSemantics]
pp_var [Lang.F]
pp_var [Wp.Lang.F]
pp_vars [Lang.F]
pp_vars [Wp.Lang.F]
pp_vset [Vset]
pp_vset [Wp.Vset]
pp_warnings [Register]
pp_warnings [Wpo]
pp_warnings [Wp.Wpo]
pp_wp_parameters [Register]
pprepeat [Vlist]
pre [Clabels]
pre [Wp.Clabels]
pred [LogicCompiler.Make]
pred [Sigs.LogicSemantics]

Compile a predicate.

pred [Repr]
pred [Wp.LogicCompiler.Make]
pred [Wp.Sigs.LogicSemantics]

Compile a predicate.

pred [Wp.Repr]
pred_e [Cil2cfg]
pred_info_id [WpPropId]
pred_info_id [Wp.WpPropId]
preproc_annot [NormAtLabels]
preproc_annot [Wp.NormAtLabels]
preproc_assigns [NormAtLabels]
preproc_assigns [Wp.NormAtLabels]
pretty [ProofEngine]
pretty [Wpo.DISK]
pretty [CfgCompiler.Cfg.E]
pretty [CfgCompiler.Cfg.T]
pretty [CfgCompiler.Cfg.P]
pretty [Pcond]
pretty [Conditions]
pretty [Sigs.Model]

pretty printing of memory location

pretty [Sigs.Sigma]

For debugging purpose

pretty [Sigs.Chunk]
pretty [Letify.Sigma]
pretty [Letify.Ground]
pretty [Cstring]
pretty [Vlist]
pretty [Vset]
pretty [Splitter]
pretty [Passive]
pretty [Matrix]
pretty [Mcfg.S]
pretty [WpPropId]
pretty [RegionAnnot.Lpath]
pretty [Layout.Chunk]
pretty [Layout.Root]
pretty [Layout.Cluster]
pretty [Layout.Overlay]
pretty [Layout.Range]
pretty [Layout.Matrix]
pretty [Layout.Value]
pretty [Layout.Usage]
pretty [Layout.Alias]
pretty [Layout.Data]
pretty [WpContext.Key]
pretty [WpContext.Entries]
pretty [Warning]
pretty [Clabels]
pretty [Ctypes]
pretty [Rformat]
pretty [Wp.Wpo.DISK]
pretty [Wp.CfgCompiler.Cfg.E]
pretty [Wp.CfgCompiler.Cfg.T]
pretty [Wp.CfgCompiler.Cfg.P]
pretty [Wp.Pcond]
pretty [Wp.Conditions]
pretty [Wp.Sigs.Model]

pretty printing of memory location

pretty [Wp.Sigs.Sigma]

For debugging purpose

pretty [Wp.Sigs.Chunk]
pretty [Wp.Cstring]
pretty [Wp.Vset]
pretty [Wp.Splitter]
pretty [Wp.Passive]
pretty [Wp.WpContext.Key]
pretty [Wp.WpContext.Entries]
pretty [Wp.Warning]
pretty [Wp.Mcfg.S]
pretty [Wp.WpPropId]
pretty [Wp.Clabels]
pretty [Wp.Ctypes]
pretty_context [WpPropId]
pretty_context [Wp.WpPropId]
pretty_local [WpPropId]
pretty_local [Wp.WpPropId]
prev [Pcfg]
prev [Wp.Pcfg]
print [RefUsage]
print [Wp.RefUsage]
print_generated [Wp_parameters]

print the given file if the debugging category "print-generated" is set

print_generated [Wp.Wp_parameters]

print the given file if the debugging category "print-generated" is set

print_why3 [Why3Provers]
print_wp [Why3Provers]
promote [Ctypes]
promote [Wp.Ctypes]
proof [VC]

List of proof obligations computed for a given property.

proof [ProofEngine]
proof [Wp.VC]

List of proof obligations computed for a given property.

proof_context [LogicUsage]

Lemmas that are not in an axiomatic.

proof_context [Wp.LogicUsage]

Lemmas that are not in an axiomatic.

prop_id_keys [WpPropId]
prop_id_keys [Wp.WpPropId]
property [Wprop.Info]
property [Wprop.Indexed2]
property [Wprop.Indexed]
property_of_id [WpPropId]

returns the annotation which lead to the given PO.

property_of_id [Wp.WpPropId]

returns the annotation which lead to the given PO.

protect [Wp_parameters]
protect [Wp.Wp_parameters]
prove [VC]

Returns a ready-to-schedule task.

prove [ProverScript]
prove [Prover]
prove [ProverWhy3]

Return NoResult if it is already proved by Qed

prove [ProverCoq]
prove [ProverErgo]
prove [Wp.Prover]
prove [Wp.VC]

Returns a ready-to-schedule task.

proved [ProofEngine]
prover_of_json [ProofScript]
prover_of_name [Wpo]

Dynamically exported.

prover_of_name [Wp.Wpo]

Dynamically exported.

provers [Register]
provers [Why3Provers]
provers_set [Why3Provers]
pruning [Conditions]
pruning [Wp.Conditions]
push [Context]
push [Wp.Context]
Q
qed_time [Wpo.GOAL]
qed_time [Wpo]
qed_time [Wp.Wpo.GOAL]
qed_time [Wp.Wpo]
R
range [Auto]
range [Tactical]
range [Vset]
range [Cint]

Dependent on model

range [Layout.Offset]
range [Wp.Auto]
range [Wp.Tactical]
range [Wp.Vset]
range [Wp.Cint]

Dependent on model

ranges [Auto.Range]
ranges [Wp.Auto.Range]
rdescr [Cvalues.Logic]
reached [WpReached]

memoized reached cfg for function

reads [CfgCompiler.Cfg.E]
reads [CfgCompiler.Cfg.T]
reads [CfgCompiler.Cfg.P]
reads [CfgCompiler.Cfg.C]
reads [Wp.CfgCompiler.Cfg.E]
reads [Wp.CfgCompiler.Cfg.T]
reads [Wp.CfgCompiler.Cfg.P]
reads [Wp.CfgCompiler.Cfg.C]
real_of_float [Cfloat]
real_of_float [Wp.Cfloat]
real_of_flt [Cfloat]
real_of_flt [Wp.Cfloat]
real_of_int [Cmath]
rebuild [Lang.For_export]
rebuild [Wp.Lang.For_export]
record [Lang]
record [Wp.Lang]
record_with [Lang.F]
record_with [Wp.Lang.F]
reduce [Wpo]

tries simplification

reduce [Wp.Wpo]

tries simplification

region [LogicCompiler.Make]

When ~unfold:true, decompose compound regions field by field

region [Sigs.LogicSemantics]

Compile a term representing a set of memory locations into an abstract region.

region [Cvalues.Logic]
region [Region]
region [Wp.LogicCompiler.Make]

When ~unfold:true, decompose compound regions field by field

region [Wp.Sigs.LogicSemantics]

Compile a term representing a set of memory locations into an abstract region.

register [GuiPanel]
register [Register]
register [Strategy]
register [Tactical]
register [MemMemory]
register [Pcfg]
register [RegionAnnot]

Auto when `-wp-region`

register [WpContext]

Model registration.

register [Context]

Register a global configure, to be executed once per project/ast.

register [Wp.Strategy]
register [Wp.Tactical]
register [Wp.Pcfg]
register [Wp.WpContext]

Model registration.

register [Wp.Context]

Register a global configure, to be executed once per project/ast.

release [Lang.F]

Empty local caches

release [Wp.Lang.F]

Empty local caches

reload [GuiPanel]
relocate [CfgCompiler.Cfg.E]
relocate [CfgCompiler.Cfg.T]
relocate [CfgCompiler.Cfg.P]

| relocate m' (create m p) | = | p{ } |

relocate [CfgCompiler.Cfg.C]
relocate [Wp.CfgCompiler.Cfg.E]
relocate [Wp.CfgCompiler.Cfg.T]
relocate [Wp.CfgCompiler.Cfg.P]

| relocate m' (create m p) | = | p{ } |

relocate [Wp.CfgCompiler.Cfg.C]
remove [VC]
remove [ProofEngine]
remove [ProofSession]
remove [Wpo]
remove [Cil2cfg.HEsig]
remove [WpContext.Generator]
remove [WpContext.Registry]
remove [Wp.Wpo]
remove [Wp.VC]
remove [Hashtbl.S]
remove [Wp.WpContext.Generator]
remove [Wp.WpContext.Registry]
remove [Set.S]

remove x s returns a set containing all elements of s, except x.

remove [Map.S]

remove x m returns a map containing the same bindings as m, except for x which is unbound in the returned map.

remove_chunks [Sigs.Sigma]

Return a copy of the environment where chunks in the footprint have been removed.

remove_chunks [Wp.Sigs.Sigma]

Return a copy of the environment where chunks in the footprint have been removed.

remove_for_altergo [Filter_axioms]
remove_for_why3 [Filter_axioms]
replace [Tactical]
replace [Conditions]

replace a step in the sequent, the one at the specified position.

replace [Cil2cfg.HEsig]
replace [Wp.Tactical]
replace [Hashtbl.S]
replace [Wp.Conditions]

replace a step in the sequent, the one at the specified position.

replace_seq [Hashtbl.S]
repr [Lang.F]

Constant time

repr [WpContext.MODEL]
repr [Wp.Lang.F]

Constant time

repr [Wp.WpContext.MODEL]
reset [ProofEngine]
reset [Wp_parameters]
reset [Hashtbl.S]
reset [Wp.Wp_parameters]
reshape [Layout.Cluster]
reshape [Layout.Compound]
resolve [Wpo.VC_Annot]
resolve [Wpo]

tries simplification and set result if valid

resolve [Wp.Wpo.VC_Annot]
resolve [Wp.Wpo]

tries simplification and set result if valid

result [VCS]
result [StmtSemantics.Make]
result [LogicCompiler.Make]
result [Sigs.LogicSemantics]

Result location of the current function in the current frame.

result [Sigs.CodeSemantics]

Value of an abstract result container.

result [Wp.VCS]
result [Wp.StmtSemantics.Make]
result [Wp.LogicCompiler.Make]
result [Wp.Sigs.LogicSemantics]

Result location of the current function in the current frame.

result [Wp.Sigs.CodeSemantics]

Value of an abstract result container.

result_of_json [ProofScript]
results [Register]
return [StmtSemantics.Make]
return [LogicCompiler.Make]
return [Sigs.LogicSemantics]

Result type of the current function in the current frame.

return [Sigs.CodeSemantics]

Return an expression with a given type.

return [Mcfg.S]
return [Wp.StmtSemantics.Make]
return [Wp.LogicCompiler.Make]
return [Wp.Sigs.LogicSemantics]

Result type of the current function in the current frame.

return [Wp.Sigs.CodeSemantics]

Return an expression with a given type.

return [Wp.Mcfg.S]
rewrite [Tactical]

For each pattern (descr,guard,src,tgt) replace src with tgt under condition guard, inserted in position at.

rewrite [Wp.Tactical]

For each pattern (descr,guard,src,tgt) replace src with tgt under condition guard, inserted in position at.

run_and_prove [GuiPanel]
S
s_bool [WpTac]
s_cnf_iff [WpTac]
s_cnf_ite [WpTac]
s_cnf_xor [WpTac]
s_dnf_iff [WpTac]
s_dnf_ite [WpTac]
s_dnf_xor [WpTac]
same_edge [Cil2cfg]
same_node [Cil2cfg]
sanitizer [Plang]
sanitizer [Wp.Plang]
save [ProverScript]
save [ProofSession]
saved [ProofEngine]
savescripts [Proof]

If necessary, dump the scripts database into the file specified by -wp-script f.

schedule [ProverTask]
schedule [Wp.ProverTask]
scheduled [Register]
scope [StmtSemantics.Make]
scope [Sigs.Model]

Manage the scope of variables.

scope [Mcfg.S]
scope [Wp.StmtSemantics.Make]
scope [Wp.Sigs.Model]

Manage the scope of variables.

scope [Wp.Mcfg.S]
script [ProofEngine]
script_for [Proof]
script_for_ide [Proof]
search [ProverScript]
search [ProverSearch]
search [TacLemma]
search [Tactical]

Search field.

search [Wp.Tactical]

Search field.

section [Definitions]
section [Wp.Definitions]
section_of_lemma [LogicUsage]
section_of_lemma [Wp.LogicUsage]
section_of_logic [LogicUsage]
section_of_logic [Wp.LogicUsage]
section_of_type [LogicUsage]
section_of_type [Wp.LogicUsage]
select [Letify.Split]
select_by_name [WpPropId]

test if the prop_id has to be selected for the asked name.

select_by_name [Wp.WpPropId]

test if the prop_id has to be selected for the asked name.

select_call_pre [WpPropId]

test if the prop_id has to be selected when we want to select the call precondition the the stmt call (None means all the call preconditions).

select_call_pre [Wp.WpPropId]

test if the prop_id has to be selected when we want to select the call precondition the the stmt call (None means all the call preconditions).

select_default [WpPropId]

test if the prop_id does not have a no_wp: in its name(s).

select_default [Wp.WpPropId]

test if the prop_id does not have a no_wp: in its name(s).

select_e [Strategy]

Lookup the first occurrence of term in the sequent and returns the associated selection.

select_e [Wp.Strategy]

Lookup the first occurrence of term in the sequent and returns the associated selection.

select_p [Strategy]

Same as select_e but for a predicate.

select_p [Wp.Strategy]

Same as select_e but for a predicate.

selected [Tactical]
selected [Wp.Tactical]
selection_of_json [ProofScript]
selection_target [ProofScript]
selector [Tactical]

Unless specified, default is head option.

selector [Wp.Tactical]

Unless specified, default is head option.

self [Sigs.Chunk]

Chunk names, for pretty-printing.

self [Wp.Sigs.Chunk]

Chunk names, for pretty-printing.

separated [Auto]
separated [MemMemory]
separated [Sigs.Model]

Return the formula that tests if two segment are separated

separated [Cvalues.Logic]
separated [Wp.Auto]
separated [Wp.Sigs.Model]

Return the formula that tests if two segment are separated

seq_branch [Conditions]

Creates an If-Then-Else branch located at the provided stmt, if any.

seq_branch [Wp.Conditions]

Creates an If-Then-Else branch located at the provided stmt, if any.

sequence [Register]
sequence [StmtSemantics.Make]

Chain compiler by introducing fresh nodes between each element of the list.

sequence [Conditions]
sequence [Wp.StmtSemantics.Make]

Chain compiler by introducing fresh nodes between each element of the list.

sequence [Wp.Conditions]
server [VC]

Default number of parallel tasks is given by -wp-par command-line option.

server [ProverTask]
server [Wp.ProverTask]
server [Wp.VC]

Default number of parallel tasks is given by -wp-par command-line option.

session [Register]
set [Tactical.Fmap]
set [StmtSemantics.Make]
set [MemoryContext]
set [Context]

Define the current value.

set [Wp.Tactical.Fmap]
set [Wp.StmtSemantics.Make]
set [Wp.Context]

Define the current value.

set [Wp.MemoryContext]
set_at_frame [LogicCompiler.Make]
set_at_frame [Sigs.LogicSemantics]

Update a frame with a specific environment for the given label.

set_at_frame [Wp.LogicCompiler.Make]
set_at_frame [Wp.Sigs.LogicSemantics]

Update a frame with a specific environment for the given label.

set_builtin [Lang.For_export]
set_builtin [Lang.F]
set_builtin [Wp.Lang.For_export]
set_builtin [Wp.Lang.F]
set_builtin' [Lang.For_export]
set_builtin' [Wp.Lang.For_export]
set_builtin_1 [Lang.F]
set_builtin_1 [Wp.Lang.F]
set_builtin_2 [Lang.F]
set_builtin_2 [Wp.Lang.F]
set_builtin_2' [Lang.F]
set_builtin_2' [Wp.Lang.F]
set_builtin_eq [Lang.For_export]
set_builtin_eq [Lang.F]
set_builtin_eq [Wp.Lang.For_export]
set_builtin_eq [Wp.Lang.F]
set_builtin_eqp [Lang.F]
set_builtin_eqp [Wp.Lang.F]
set_builtin_get [Lang.F]
set_builtin_get [Wp.Lang.F]
set_builtin_leq [Lang.For_export]
set_builtin_leq [Lang.F]
set_builtin_leq [Wp.Lang.For_export]
set_builtin_leq [Wp.Lang.F]
set_init [MemLoader.Model]
set_init_atom [MemLoader.Model]
set_mode [Cache]
set_model [Register]
set_model [Wp_error]
set_option [LogicBuiltins]

reset and add a value to an option (group, name)

set_option [Wp.LogicBuiltins]

reset and add a value to an option (group, name)

set_possible_values [Parameter_sig.String]

Set what are the acceptable values for this parameter.

set_procs [Why3Provers]
set_range [Parameter_sig.Int]

Set what is the possible range of values for this parameter.

set_result [Wpo]
set_result [Wp.Wpo]
set_saved [ProofEngine]
set_strategies [ProofEngine]
severe [Warning]
severe [Wp.Warning]
shareable [Vlist]
shift [MemLoader.Model]
shift [Sigs.Model]

Return the memory location obtained by array access at an index represented by the given term.

shift [Cvalues.Logic]
shift [Layout.Cluster]
shift [Wp.Sigs.Model]

Return the memory location obtained by array access at an index represented by the given term.

sigma [Lang]

uses current pool

sigma [Wp.Lang]

uses current pool

signature [Tactical]
signature [Wp.Tactical]
signed [Ctypes]

true if signed

signed [Wp.Ctypes]

true if signed

simplify [Prover]
simplify [Conditions]
simplify [Mcfg.Splitter]
simplify [Wp.Prover]
simplify [Wp.Conditions]
simplify [Wp.Mcfg.Splitter]
singleton [Letify.Ground]
singleton [Vset]
singleton [Splitter]
singleton [Layout.Chunk]
singleton [Wp.Vset]
singleton [Wp.Splitter]
singleton [Set.S]

singleton x returns the one-element set containing only x.

singleton [Map.S]

singleton x y returns the one-element map that contains a binding y for x.

size [Conditions]

Compute the total number of steps in the sequence, including nested sequences from branches and disjunctions.

size [Wp.Conditions]

Compute the total number of steps in the sequence, including nested sequences from branches and disjunctions.

sizeof [MemLoader.Model]
sizeof [Layout.Matrix]
sizeof [Layout.Value]
sizeof [Layout.Offset]
sizeof_defined [Ctypes]
sizeof_defined [Wp.Ctypes]
sizeof_object [Ctypes]
sizeof_object [Wp.Ctypes]
skip [Script]
smoke_status [GuiProver]
smoked [VCS]
smoked [Wp.VCS]
smoking [WpReached]

Returns whether a stmt need a smoke tests to avoid being unreachable.

sort [Lang.F]

Constant time

sort [Wp.Lang.F]

Constant time

source_of_id [WpPropId]
source_of_id [Wp.WpPropId]
spawn [VC]

Same as prove but schedule the tasks into the global server returned by server function below.

spawn [ProverScript]
spawn [Prover]
spawn [ProverTask]
spawn [Wp.Prover]
spawn [Wp.ProverTask]
spawn [Wp.VC]

Same as prove but schedule the tasks into the global server returned by server function below.

spawn_wp_proofs [Register]
spec [StmtSemantics.Make]
spec [Wp.StmtSemantics.Make]
specialize_eq_list [Vlist]
spinner [Tactical]

Unless specified, default is vmin or 0 or vmax, whichever fits.

spinner [Wp.Tactical]

Unless specified, default is vmin or 0 or vmax, whichever fits.

split [Auto]
split [Tactical]
split [Mcfg.Splitter]
split [Wp.Auto]
split [Wp.Tactical]
split [Wp.Mcfg.Splitter]
split [Set.S]

split x s returns a triple (l, present, r), where l is the set of elements of s that are strictly less than x; r is the set of elements of s that are strictly greater than x; present is false if s contains no element equal to x, or true if s contains an element equal to x.

split [Map.S]

split x m returns a triple (l, data, r), where l is the map with all the bindings of m whose key is strictly less than x; r is the map with all the bindings of m whose key is strictly greater than x; data is None if m contains no binding for x, or Some v if m binds v to x.

split_bag [WpPropId]
split_bag [Wp.WpPropId]
split_map [WpPropId]
split_map [Wp.WpPropId]
start_edge [Cil2cfg]

get the starting edges

start_stmt_of_node [Cil2cfg]
startof [Cvalues]

Shift a location with 0-indices wrt to its array type

state [Conditions]

Stack a memory model state on top of the bundle.

state [Mstate]
state [Sigs.Model]

Returns a memory state description from a memory environement.

state [Wp.Conditions]

Stack a memory model state on top of the bundle.

state [Wp.Mstate]
state [Wp.Sigs.Model]

Returns a memory state description from a memory environement.

stats [Hashtbl.S]
status [ProofEngine]
status [LogicCompiler.Make]
status [Sigs.LogicSemantics]

Exit status for the current frame.

status [Wp.LogicCompiler.Make]
status [Wp.Sigs.LogicSemantics]

Exit status for the current frame.

step [Conditions]

Creates a single step

step [Wp.Conditions]

Creates a single step

step_at [Conditions]

Retrieve a step by id in the sequence.

step_at [Wp.Conditions]

Retrieve a step by id in the sequence.

stepout [ProverTask]
stepout [VCS]
stepout [Wp.ProverTask]
stepout [Wp.VCS]
steps [Conditions]

Attributes unique indices to every step.id in the sequence, starting from zero.

steps [Wp.Conditions]

Attributes unique indices to every step.id in the sequence, starting from zero.

stmt [Clabels]
stmt [Wp.Clabels]
store_float [MemLoader.Model]
store_int [MemLoader.Model]
store_pointer [MemLoader.Model]
stored [MemLoader.Make]
stored [Sigs.Model]

Return a set of formula that express a modification between two memory state.

stored [Wp.Sigs.Model]

Return a set of formula that express a modification between two memory state.

str_id [Cstring]

Non-zero integer, unique for each different string literal

str_id [Wp.Cstring]

Non-zero integer, unique for each different string literal

str_len [Cstring]

Property defining the size of the string in bytes, with \0 terminator included.

str_len [Wp.Cstring]

Property defining the size of the string in bytes, with \0 terminator included.

str_val [Cstring]

The array containing the char of the constant

str_val [Wp.Cstring]

The array containing the char of the constant

strange_loops [Cil2cfg]

detect is there are non natural loops or natural loops where we didn't manage to compute back edges (see mark_loops).

strategy [TacCongruence]
strategy [TacShift]
strategy [TacBittest]
strategy [TacBitrange]
strategy [TacBitwised]
strategy [TacRewrite]
strategy [TacNormalForm]
strategy [TacCut]
strategy [TacFilter]
strategy [TacLemma]
strategy [TacInstance]
strategy [TacHavoc.Validity]
strategy [TacHavoc.Separated]
strategy [TacHavoc.Havoc]
strategy [TacUnfold]
strategy [TacCompound]
strategy [TacArray]
strategy [TacRange]
strategy [TacChoice.Contrapose]
strategy [TacChoice.Absurd]
strategy [TacChoice.Choice]
strategy [TacSplit]
strategy_has_asgn_goal [WpStrategy]
strategy_has_prop_goal [WpStrategy]
strategy_kind [WpStrategy]
string_of_termination_kind [WpPropId]

TODO: should probably be somewhere else

string_of_termination_kind [Wp.WpPropId]

TODO: should probably be somewhere else

sub_c_int [Ctypes]
sub_c_int [Wp.Ctypes]
sub_range [Vset]
sub_range [Wp.Vset]
subclause [Tactical]

When subclause clause p, we have clause = Step H and H -> p, or clause = Goal G and -> G.

subclause [Wp.Tactical]

When subclause clause p, we have clause = Step H and H -> p, or clause = Goal G and -> G.

subproof_idx [WpPropId]

subproof index of this propr_id

subproof_idx [Wp.WpPropId]

subproof index of this propr_id

subproofs [WpPropId]

How many subproofs

subproofs [Wp.WpPropId]

How many subproofs

subset [Cvalues.Logic]
subset [Vset]
subset [Wp.Vset]
subset [Set.S]

subset s1 s2 tests whether the set s1 is a subset of the set s2.

subst [Conditions]

Apply the atomic substitution recursively using Lang.F.p_subst f.

subst [Lang]

replace variables

subst [Wp.Conditions]

Apply the atomic substitution recursively using Lang.F.p_subst f.

subst [Wp.Lang]

replace variables

subterms [Pcfg]
subterms [Wp.Pcfg]
succ_e [Cil2cfg]
switch [Mcfg.S]
switch [Wp.Mcfg.S]
switch_cases [Splitter]
switch_cases [Wp.Splitter]
switch_default [Splitter]
switch_default [Wp.Splitter]
T
t32 [Cfloat]
t32 [Wp.Cfloat]
t64 [Cfloat]
t64 [Wp.Cfloat]
t_absurd [Auto]

Find a contradiction.

t_absurd [Wp.Auto]

Find a contradiction.

t_addr [MemMemory]
t_addr [Lang]
t_addr [Wp.Lang]
t_array [Lang]
t_array [Wp.Lang]
t_bool [Lang]
t_bool [Wp.Lang]
t_case [Auto]

Case analysis: t_case p a b applies process a under hypothesis p and process b under hypothesis not p.

t_case [Wp.Auto]

Case analysis: t_case p a b applies process a under hypothesis p and process b under hypothesis not p.

t_cases [Auto]

Complete analysis: applies each process under its guard, and proves that all guards are complete.

t_cases [Wp.Auto]

Complete analysis: applies each process under its guard, and proves that all guards are complete.

t_chain [Auto]

Apply second process to every goal generated by the first one.

t_chain [Wp.Auto]

Apply second process to every goal generated by the first one.

t_comp [Lang]
t_comp [Wp.Lang]
t_cut [Auto]

Prove condition p and use-it as a forward hypothesis.

t_cut [Wp.Auto]

Prove condition p and use-it as a forward hypothesis.

t_datatype [Lang]
t_datatype [Wp.Lang]
t_descr [Auto]

Apply a description to each sub-goal

t_descr [Wp.Auto]

Apply a description to each sub-goal

t_farray [Lang]
t_farray [Wp.Lang]
t_finally [Auto]

Apply a description to a leaf goal.

t_finally [Wp.Auto]

Apply a description to a leaf goal.

t_float [Lang]
t_float [Wp.Lang]
t_id [Auto]

Keep goal unchanged.

t_id [Wp.Auto]

Keep goal unchanged.

t_init [MemMemory]

initialization tables

t_init [Lang]
t_init [Wp.Lang]
t_int [Lang]
t_int [Wp.Lang]
t_malloc [MemMemory]

allocation tables

t_matrix [Lang]
t_matrix [Wp.Lang]
t_mem [MemMemory]

t_addr indexed array

t_prop [Lang]
t_prop [Wp.Lang]
t_range [Auto]
t_range [Wp.Auto]
t_real [Lang]
t_real [Wp.Lang]
t_replace [Auto]

Prove src=tgt then replace src by tgt.

t_replace [Wp.Auto]

Prove src=tgt then replace src by tgt.

t_split [Auto]

Split with p and not p.

t_split [Wp.Auto]

Split with p and not p.

tactical [ProofEngine]
tactical [TacCongruence]
tactical [TacShift]
tactical [TacBittest]
tactical [TacBitrange]
tactical [TacBitwised]
tactical [TacRewrite]
tactical [TacNormalForm]
tactical [TacCut]
tactical [TacFilter]
tactical [TacLemma]
tactical [TacInstance]
tactical [TacHavoc.Validity]
tactical [TacHavoc.Separated]
tactical [TacHavoc.Havoc]
tactical [TacUnfold]
tactical [TacCompound]
tactical [TacArray]
tactical [TacRange]
tactical [TacChoice.Contrapose]
tactical [TacChoice.Absurd]
tactical [TacChoice.Choice]
tactical [TacSplit]
tactical [WpPropId]
tactical [Wp.WpPropId]
target [WpAnnot]
tau_of_chunk [Sigs.Chunk]

The type of data hold in a chunk.

tau_of_chunk [Wp.Sigs.Chunk]

The type of data hold in a chunk.

tau_of_ctype [Lang]
tau_of_ctype [Wp.Lang]
tau_of_field [Lang]
tau_of_field [Wp.Lang]
tau_of_float [Cfloat]

with respect to model

tau_of_float [Wp.Cfloat]

with respect to model

tau_of_lfun [Lang]
tau_of_lfun [Wp.Lang]
tau_of_ltype [Lang]
tau_of_ltype [Wp.Lang]
tau_of_object [Lang]
tau_of_object [Wp.Lang]
tau_of_record [Lang]
tau_of_record [Wp.Lang]
tau_of_return [Lang]
tau_of_return [Wp.Lang]
tau_of_set [Vset]
tau_of_set [Wp.Vset]
tau_of_var [Lang.F]
tau_of_var [Wp.Lang.F]
term [LogicCompiler.Make]
term [Sigs.LogicSemantics]

Compile a term expression.

term [Repr]
term [Wp.LogicCompiler.Make]
term [Wp.Sigs.LogicSemantics]

Compile a term expression.

term [Wp.Repr]
test [Mcfg.S]
test [Wp.Mcfg.S]
timeout [ProverTask]
timeout [VCS]
timeout [Wp.ProverTask]
timeout [Wp.VCS]
title [ProofEngine]
title [Why3Provers]
title_of_mode [VCS]
title_of_mode [Wp.VCS]
title_of_prover [VCS]
title_of_prover [Wp.VCS]
to_addr [MemLoader.Model]
to_cint [Cint]

Raises Not_found if not.

to_cint [Wp.Cint]

Raises Not_found if not.

to_condition [CfgCompiler.Cfg.P]
to_condition [Wp.CfgCompiler.Cfg.P]
to_integer [Cint]
to_integer [Wp.Cint]
to_logic [Clabels]
to_logic [Wp.Clabels]
to_region_pointer [MemLoader.Model]
to_seq [Hashtbl.S]
to_seq [Set.S]

Iterate on the whole set, in ascending order

to_seq [Map.S]

Iterate on the whole map, in ascending order of keys

to_seq_from [Set.S]

to_seq_from x s iterates on a subset of the elements of s in ascending order, from x or above.

to_seq_from [Map.S]

to_seq_from k m iterates on a subset of the bindings of m, in ascending order of keys, from key k or above.

to_seq_keys [Hashtbl.S]
to_seq_values [Hashtbl.S]
token [Script]
top [Letify.Ground]
tracelog [Register]
trans [Filter_axioms]
tree_context [ProofEngine]
trigger [LogicCompiler.Make]
trigger [Wp.LogicCompiler.Make]
trivial [Wpo.GOAL]
trivial [Conditions]

empty implies true

trivial [Wp.Wpo.GOAL]
trivial [Wp.Conditions]

empty implies true

try_sequence [Register]
type_id [Lang]
type_id [Wp.Lang]
typeof [Lang.F]

Try to extract a type of term.

typeof [Layout.Offset]
typeof [Wp.Lang.F]

Try to extract a type of term.

typeof_chain [Layout.Offset]
U
unchanged [Sigs.CodeSemantics]

Express that a given variable has the same value in two memory states.

unchanged [Wp.Sigs.CodeSemantics]

Express that a given variable has the same value in two memory states.

uninitialized_obj [Cvalues]
union [Sigs.Sigma]

Same as Chunk.Set.union

union [Cvalues.Logic]
union [Vset]
union [Splitter]
union [Passive]
union [Layout.Chunk]
union [Wp.Sigs.Sigma]

Same as Chunk.Set.union

union [Wp.Vset]
union [Wp.Splitter]
union [Wp.Passive]
union [Set.S]

Set union.

union [Map.S]

union f m1 m2 computes a map whose keys is the union of keys of m1 and of m2.

union_map [Layout.Chunk]
unknown [VCS]
unknown [Wp.VCS]
unmark [Splitter]

erase all tags

unmark [Wp.Splitter]

erase all tags

unreachable_if_valid [WpPropId]

Stmt that is unreachable in case the PO is valid.

unreachable_if_valid [Wp.WpPropId]

Stmt that is unreachable in case the PO is valid.

unreachable_nodes [Cil2cfg]
unsupported [Wp_error]
update [GuiPanel]
update [WpContext.Registry]

set current value, with no protection

update [Context]

Modification of the current value

update [Wp.WpContext.Registry]

set current value, with no protection

update [Wp.Context]

Modification of the current value

update [Map.S]

update x f m returns a map containing the same bindings as m, except for the binding of x.

update_cond [Conditions]

Updates the condition of a step and merges descr, deps and warn

update_cond [Wp.Conditions]

Updates the condition of a step and merges descr, deps and warn

update_symbol [Definitions]
update_symbol [Wp.Definitions]
updates [Pcfg]
updates [Mstate]
updates [Sigs.Model]

Try to interpret a sequence of states into updates.

updates [Wp.Pcfg]
updates [Wp.Mstate]
updates [Wp.Sigs.Model]

Try to interpret a sequence of states into updates.

use [Layout.Alias]
use_assigns [Mcfg.S]

use_assigns env hid kind assgn goal performs the havoc on the goal.

use_assigns [Wp.Mcfg.S]

use_assigns env hid kind assgn goal performs the havoc on the goal.

user_bhv_names [WpPropId]
user_bhv_names [Wp.WpPropId]
user_prop_names [WpPropId]

This is used to give the name of the property that the user can give to select it from the command line (-wp-prop option)

user_prop_names [Wp.WpPropId]
V
val_of_exp [Sigs.CodeSemantics]

Compile an expression as a term.

val_of_exp [Wp.Sigs.CodeSemantics]

Compile an expression as a term.

val_of_term [Sigs.LogicSemantics]

Same as term above but reject any set of locations.

val_of_term [Wp.Sigs.LogicSemantics]

Same as term above but reject any set of locations.

valid [VCS]
valid [Sigs.Model]

Return the formula that tests if a memory state is valid (according to Sigs.acs) in the given memory state at the given segment.

valid [Cvalues.Logic]
valid [Wp.VCS]
valid [Wp.Sigs.Model]

Return the formula that tests if a memory state is valid (according to Wp.Sigs.acs) in the given memory state at the given segment.

validate [ProofEngine]
value [Sigs.Sigma]

Same as Lang.F.e_var of get.

value [Cvalues.Logic]
value [Wp.Sigs.Sigma]

Same as Lang.F.e_var of get.

value_footprint [MemLoader.Model]
vanti [TacFilter]
vars [Sigs.LogicSemantics]

Qed variables appearing in a region expression.

vars [Sigs.Model]

Return the logic variables from which the given location depend on.

vars [Vset]
vars [Definitions.Trigger]
vars [Lang.F]

Constant time

vars [Wp.Sigs.LogicSemantics]

Qed variables appearing in a region expression.

vars [Wp.Sigs.Model]

Return the logic variables from which the given location depend on.

vars [Wp.Vset]
vars [Wp.Definitions.Trigger]
vars [Wp.Lang.F]

Constant time

vars_hyp [Conditions]

Pre-computed and available in constant time.

vars_hyp [Wp.Conditions]

Pre-computed and available in constant time.

vars_seq [Conditions]

At the cost of the union of hypotheses and goal.

vars_seq [Wp.Conditions]

At the cost of the union of hypotheses and goal.

varsp [Lang.F]

Constant time

varsp [Wp.Lang.F]

Constant time

verdict [VCS]
verdict [Wp.VCS]
version [Why3Provers]
very_strange_loops [Cil2cfg]

detect is there are natural loops where we didn't manage to compute back edges (see mark_loops).

visible [Pcfg]
visible [Wp.Pcfg]
vmax [TacRange]
vmin [TacRange]
volatile [Cvalues]

Check if a volatile access must be properly modelled or ignored.

vset [Cvalues.Logic]
W
warn [MemoryContext]
warn [AssignsCompleteness]

Displays a warning if the given kernel function has incomplete assigns.

warn [Wp.AssignsCompleteness]

Displays a warning if the given kernel function has incomplete assigns.

warn [Wp.MemoryContext]
warnings [Wpo]
warnings [Wp.Wpo]
wg_status [GuiProver]
with_callees [WpTarget]
with_current_loc [Context]
with_current_loc [Wp.Context]
without_assume [Lang]
without_assume [Wp.Lang]
wkey_pedantic [AssignsCompleteness]
wkey_pedantic [Wp.AssignsCompleteness]
wkey_smoke [Register]
wp_compute_memory_context [Register]
wp_insert_memory_context [Register]
wp_iter_model [Register]
wp_warn_memory_context [Register]
wrap [TacInstance]
writes [CfgCompiler.Cfg.E]

as defined by S.writes

writes [Sigs.Sigma]

writes s indicates which chunks are new in s.post compared to s.pre.

writes [Wp.CfgCompiler.Cfg.E]

as defined by S.writes

writes [Wp.Sigs.Sigma]

writes s indicates which chunks are new in s.post compared to s.pre.