( * ) [Lang.N] | F.p_mul
|
( * ) [Wp.Lang.N] | F.p_mul
|
( @* ) [StmtSemantics.Make] |
fold bind
|
( @* ) [Wp.StmtSemantics.Make] |
fold bind
|
($$) [Lang.N] | |
($$) [Wp.Lang.N] | |
($) [Lang.N] | |
($) [Wp.Lang.N] | |
(&&) [Lang.N] | |
(&&) [Wp.Lang.N] | |
(+) [Lang.N] | F.p_add
|
(+) [Wp.Lang.N] | F.p_add
|
(-) [Lang.N] | F.p_sub
|
(-) [Wp.Lang.N] | F.p_sub
|
(/) [Lang.N] | F.p_div
|
(/) [Wp.Lang.N] | F.p_div
|
(<) [Lang.N] | |
(<) [Wp.Lang.N] | |
(<=) [Lang.N] | |
(<=) [Wp.Lang.N] | |
(<>) [Lang.N] | |
(<>) [Wp.Lang.N] | |
(=) [Lang.N] | |
(=) [Wp.Lang.N] | |
(>) [Lang.N] | Lang.F.p_lt with inversed argument
|
(>) [Wp.Lang.N] | Wp.Lang.F.p_lt with inversed argument
|
(>=) [Lang.N] | Lang.F.p_leq with inversed argument
|
(>=) [Wp.Lang.N] | Wp.Lang.F.p_leq with inversed argument
|
(@-) [StmtSemantics.Make] | |
(@-) [Wp.StmtSemantics.Make] | |
(@:) [StmtSemantics.Make] |
LabelMap.find with refined excpetion.
|
(@:) [Wp.StmtSemantics.Make] |
LabelMap.find with refined excpetion.
|
(@^) [StmtSemantics.Make] |
Same as
Cfg.concat
|
(@^) [Wp.StmtSemantics.Make] |
Same as
Cfg.concat
|
(mod) [Lang.N] | F.p_mod
|
(mod) [Wp.Lang.N] | F.p_mod
|
(||) [Lang.N] | |
(||) [Wp.Lang.N] | |
(~-) [Lang.N] | fun x -> p_sub 0 x
|
(~-) [Wp.Lang.N] | fun x -> p_sub 0 x
|
A | |
a_addr [MemMemory] |
Constructor for
{ base ; offset }
|
a_base [MemMemory] |
Returns the base
|
a_base_offset [MemMemory] |
Returns the offset in bytes from the logic offset
(which is a memory cell index, actually)
|
a_global [MemMemory] |
Zero-offset base.
|
a_null [MemMemory] |
Null address.
|
a_offset [MemMemory] |
Returns the offset
|
a_prover [ProofScript] | |
a_shift [MemMemory] |
Shift:
a_shift a k adds k to a.offset
|
a_tactic [ProofScript] | |
absurd [Auto] | |
absurd [Wp.Auto] | |
acs_copy [Region] | |
acs_deref [Region] | |
acs_read [Region] | |
acs_shift [Region] | |
acs_write [Region] | |
acsl_lit [Cfloat] | |
acsl_lit [Wp.Cfloat] | |
add [Wpo] | |
add [Letify.Split] | |
add [Letify.Defs] | |
add [Letify.Sigma] | |
add [Lang.F.Subst] | |
add [Cil2cfg.HEsig] | |
add [Warning] | |
add [Wp.Wpo] | |
add [Hashtbl.S] | |
add [Wp.Lang.F.Subst] | |
add [Wp.Warning] | |
add [Set.S] | add x s returns a set containing all elements of s ,
plus x .
|
add [Map.S] | add x y m returns a map containing the same bindings as
m , plus a binding of x to y .
|
add_alias [LogicBuiltins] | |
add_alias [Region] | |
add_alias [Wp.LogicBuiltins] | |
add_all_axioms [WpStrategy] | |
add_assigns [WpStrategy] |
generic function to add an assigns property.
|
add_assigns [Mcfg.S] | |
add_assigns [Wp.Mcfg.S] | |
add_assigns_any [WpStrategy] |
generic function to add a WriteAny assigns property.
|
add_axiom [WpStrategy] | |
add_axiom [Mcfg.S] | |
add_axiom [Wp.Mcfg.S] | |
add_builtin [LogicBuiltins] |
Add a new builtin.
|
add_builtin [Wp.LogicBuiltins] |
Add a new builtin.
|
add_call_assigns_any [WpStrategy] |
short cut to add a dynamic call
|
add_call_assigns_hyp [WpStrategy] |
shortcut to add a call assigns property as an hypothesis.
|
add_composer [Tactical] | |
add_composer [Wp.Tactical] | |
add_ctor [LogicBuiltins] | |
add_ctor [Wp.LogicBuiltins] | |
add_definitions [Letify] | add_definitions sigma defs xs ps keep all
definitions of variables xs from sigma that comes from defs .
|
add_fct_bhv_assigns_hyp [WpStrategy] | |
add_filter [Lang.F.Subst] | |
add_filter [Wp.Lang.F.Subst] | |
add_fun [Lang.F.Subst] | |
add_fun [Wp.Lang.F.Subst] | |
add_goal [Mcfg.S] | |
add_goal [Wp.Mcfg.S] | |
add_hook [Wprop.Indexed2] |
Hooks are executed once at property creation
|
add_hook [Wprop.Indexed] |
Hooks are executed once at property creation
|
add_hyp [Mcfg.S] | |
add_hyp [Wp.Mcfg.S] | |
add_invalid_proof [WpAnnot] |
add an invalid proof result ; can not revert a complete proof
|
add_library [LogicBuiltins] |
Add a new library or update the dependencies of an existing one
|
add_library [Wp.LogicBuiltins] |
Add a new library or update the dependencies of an existing one
|
add_logic [LogicBuiltins] | |
add_logic [Wp.LogicBuiltins] | |
add_loop_annots [WpStrategy] | |
add_loop_assigns_hyp [WpStrategy] |
shortcut to add a loop assigns property as an hypothesis.
|
add_map [Lang.F.Subst] | |
add_map [Wp.Lang.F.Subst] | |
add_node_annots [WpStrategy] | add_node_annots cfg annots v (before, (after, exits))
add the annotations for the node :
|
add_offset [Region] | |
add_on_edges [WpStrategy] | |
add_option [LogicBuiltins] |
add a value to an option (group, name)
|
add_option [Wp.LogicBuiltins] |
add a value to an option (group, name)
|
add_pointed [Region] | |
add_predicate [LogicBuiltins] | |
add_predicate [Wp.LogicBuiltins] | |
add_proof [WpAnnot] |
accumulate in the proof the partial proof for this prop_id
|
add_prop [WpStrategy] |
generic function to add a predicate property after normalisation.
|
add_prop_assert [WpStrategy] | |
add_prop_call_post [WpStrategy] |
Add a postcondition of a called function.
|
add_prop_call_pre [WpStrategy] | |
add_prop_dead_call [WpStrategy] |
Add Smoke Test for possibly dead call : (posts,exits)
|
add_prop_dead_code [WpStrategy] |
Add Smoke Test for possibly dead code
|
add_prop_dead_loop [WpStrategy] |
Add Smoke Test for loop
|
add_prop_fct_bhv_pre [WpStrategy] |
Add the preconditions of the behavior
|
add_prop_fct_post [WpStrategy] | |
add_prop_fct_pre [WpStrategy] |
Add the predicate as a function precondition.
|
add_prop_fct_pre_bhv [WpStrategy] | |
add_prop_fct_smoke [WpStrategy] |
Add Smoke Test behavior
|
add_prop_loop_inv [WpStrategy] | |
add_prop_stmt_bhv_requires [WpStrategy] |
Add all the
b_requires .
|
add_prop_stmt_post [WpStrategy] |
Add the predicate as a stmt precondition.
|
add_prop_stmt_pre [WpStrategy] |
Add the predicate as a stmt precondition.
|
add_prop_stmt_spec_pre [WpStrategy] |
Process the stmt spec precondition as an hypothesis for external properties.
|
add_script_for [Proof] | new_script goal keys proof qed registers the script proof
terminated by qed for goal gid and keywords keys
|
add_specific_equality [ProverWhy3] |
Equality used in the goal, simpler to prove than polymorphic equality
|
add_step [Register] | |
add_stmt_spec_assigns_hyp [WpStrategy] |
shortcut to add a stmt spec assigns property as an hypothesis.
|
add_time [Register] | |
add_tmpnode [CfgCompiler.Cfg] |
Set a node as temporary.
|
add_tmpnode [Wp.CfgCompiler.Cfg] |
Set a node as temporary.
|
add_type [LogicBuiltins] | |
add_type [Wp.LogicBuiltins] | |
add_var [Lang.F] | |
add_var [Wp.Lang.F] | |
add_vars [Lang.F] | |
add_vars [Wp.Lang.F] | |
adt [Lang] |
Must not be a builtin
|
adt [Wp.Lang] |
Must not be a builtin
|
age [Wpo] | |
age [Wp.Wpo] | |
ainf [Cvalues] |
Array lower-bound, ie `Some(0)`
|
alias [Region] | |
alias [Layout.Alias] | |
alloc [Sigs.Model] |
Allocates new chunk for the validity of variables.
|
alloc [Wp.Sigs.Model] |
Allocates new chunk for the validity of variables.
|
alloc_domain [Plang] | |
alloc_domain [Wp.Plang] | |
alloc_e [Plang] | |
alloc_e [Wp.Plang] | |
alloc_hyp [Pcond] | |
alloc_hyp [Wp.Pcond] | |
alloc_p [Plang] | |
alloc_p [Wp.Plang] | |
alloc_seq [Pcond] | |
alloc_seq [Wp.Pcond] | |
alloc_xs [Plang] | |
alloc_xs [Wp.Plang] | |
alpha [Lang.F] | |
alpha [Lang] |
freshen all variables
|
alpha [Wp.Lang.F] | |
alpha [Wp.Lang] |
freshen all variables
|
anchor [ProofEngine] | |
append [Conditions] |
Conjunction
|
append [Wp.Conditions] |
Conjunction
|
append_after [Parameter_sig.List] |
append a list at the end of the current state
|
append_before [Parameter_sig.List] |
append a list in front of the current state
|
apply [Mstate] | |
apply [Sigs.Model] |
Propagate a sequent substitution inside the memory state.
|
apply [Cvalues.Logic] | |
apply [Passive] | |
apply [Wp.Mstate] | |
apply [Wp.Sigs.Model] |
Propagate a sequent substitution inside the memory state.
|
apply [Wp.Passive] | |
apply_add [Cvalues.Logic] | |
apply_assigns [Sigs.LogicAssigns] |
Relates two memory states corresponding to an assigns clause
with the specified set of locations.
|
apply_assigns [Wp.Sigs.LogicAssigns] |
Relates two memory states corresponding to an assigns clause
with the specified set of locations.
|
apply_sub [Cvalues.Logic] | |
are_equal [Lang.F] |
Computes equality
|
are_equal [Wp.Lang.F] |
Computes equality
|
arg [Strategy] | |
arg [Wp.Strategy] | |
array [Auto] | |
array [Wp.Auto] | |
array_dimensions [Ctypes] |
Returns the list of dimensions the array consists of.
|
array_dimensions [Wp.Ctypes] |
Returns the list of dimensions the array consists of.
|
array_size [Ctypes] | |
array_size [Wp.Ctypes] | |
as_atom [Cleaning] | |
as_have [Cleaning] | |
as_init [Cleaning] | |
as_type [Cleaning] | |
assign [Mcfg.S] | |
assign [Wp.Mcfg.S] | |
assigned [MemLoader.Make] | |
assigned [Sigs.Model] |
Return a set of formula that express that two memory state are the same
except at the given set of memory location.
|
assigned [Sigs.Sigma] |
Make chunks equal outside of some domain.
|
assigned [Wp.Sigs.Model] |
Return a set of formula that express that two memory state are the same
except at the given set of memory location.
|
assigned [Wp.Sigs.Sigma] |
Make chunks equal outside of some domain.
|
assigned_of_assigns [Sigs.LogicSemantics] |
Computes the region assigned by an assigns clause.
|
assigned_of_assigns [Wp.Sigs.LogicSemantics] |
Computes the region assigned by an assigns clause.
|
assigned_of_froms [Sigs.LogicSemantics] |
Computes the region assigned by a list of froms.
|
assigned_of_froms [Wp.Sigs.LogicSemantics] |
Computes the region assigned by a list of froms.
|
assigned_of_lval [Sigs.LogicSemantics] |
Computes the region assigned by a list of froms.
|
assigned_of_lval [Wp.Sigs.LogicSemantics] |
Computes the region assigned by a list of froms.
|
assigns [StmtSemantics.Make] | |
assigns [Wp.StmtSemantics.Make] | |
assigns_info_id [WpPropId] | |
assigns_info_id [Wp.WpPropId] | |
assigns_upper_bound [WpStrategy] | |
assume [StmtSemantics.Make] | |
assume [CfgCompiler.Cfg] |
Represents execution traces
T such that, if T contains
every node points in the label-map, then the condition holds over the
corresponding memory states.
|
assume [Conditions] |
Assumes a predicate in the specified section,
with the specified decorations.
|
assume [Letify.Sigma] | |
assume [Lang] | |
assume [Wp.StmtSemantics.Make] | |
assume [Wp.CfgCompiler.Cfg] |
Represents execution traces
T such that, if T contains
every node points in the label-map, then the condition holds over the
corresponding memory states.
|
assume [Wp.Conditions] |
Assumes a predicate in the specified section,
with the specified decorations.
|
assume [Wp.Lang] | |
assume_ [StmtSemantics.Make] | |
assume_ [Wp.StmtSemantics.Make] | |
asup [Cvalues] |
Array upper-bound, ie `Some(n-1)`
|
at [Tactical] | |
at [Pcfg] | |
at [Wp.Tactical] | |
at [Wp.Pcfg] | |
at_closure [Conditions] |
register a transformation applied just before close
|
at_closure [Wp.Conditions] |
register a transformation applied just before close
|
at_exit [Clabels] | |
at_exit [Wp.Clabels] | |
atype [Lang] | |
atype [Wp.Lang] | |
auto_range [Auto] | |
auto_range [Wp.Auto] | |
auto_split [Auto] | |
auto_split [Wp.Auto] | |
autofit [VCS] |
Result that fits the default configuration
|
autofit [Wp.VCS] |
Result that fits the default configuration
|
automaton [StmtSemantics.Make] | |
automaton [Wp.StmtSemantics.Make] | |
axiomatic [Definitions] | |
axiomatic [LogicUsage] | |
axiomatic [Wp.Definitions] | |
axiomatic [Wp.LogicUsage] | |
B | |
backtrack [ProverSearch] | |
backward [Letify.Ground] | |
band [Cint] | |
band [Wp.Cint] | |
bar [Wpo] | |
bar [Wp.Wpo] | |
base_addr [Sigs.Model] |
Return the memory location of the base address of a given memory
location.
|
base_addr [Wp.Sigs.Model] |
Return the memory location of the base address of a given memory
location.
|
base_offset [Sigs.Model] |
Return the offset of the location, in bytes, from its base_addr.
|
base_offset [Wp.Sigs.Model] |
Return the offset of the location, in bytes, from its base_addr.
|
basename [Lang.F] | |
basename [LogicUsage] |
Trims the original name
|
basename [WpContext.IData] | |
basename [Ctypes] | |
basename [Wp.Lang.F] | |
basename [Wp.WpContext.IData] | |
basename [Wp.LogicUsage] |
Trims the original name
|
basename [Wp.Ctypes] | |
basename_of_chunk [Sigs.Chunk] |
Used when generating fresh variables for a chunk.
|
basename_of_chunk [Wp.Sigs.Chunk] |
Used when generating fresh variables for a chunk.
|
begin_session [Register] | |
behavior_name_of_strategy [WpStrategy] | |
best [VCS] | |
best [Wp.VCS] | |
bind [ProofEngine] | |
bind [StmtSemantics.Make] | |
bind [Letify] | bind sigma defs xs select definitions in defs
targeting variables xs .
|
bind [Passive] | |
bind [Context] |
Performs the job with local context bound to local value.
|
bind [Wp.StmtSemantics.Make] | |
bind [Wp.Passive] | |
bind [Wp.Context] |
Performs the job with local context bound to local value.
|
bindings [Map.S] |
Return the list of all bindings of the given map.
|
bit_test [Cint] | |
bit_test [Wp.Cint] | |
bits_sizeof_array [Ctypes] | |
bits_sizeof_array [Wp.Ctypes] | |
bits_sizeof_comp [Ctypes] | |
bits_sizeof_comp [Wp.Ctypes] | |
bits_sizeof_object [Ctypes] | |
bits_sizeof_object [Wp.Ctypes] | |
block_length [Sigs.Model] |
Returns the length (in bytes) of the allocated block containing
the given location.
|
block_length [Wp.Sigs.Model] |
Returns the length (in bytes) of the allocated block containing
the given location.
|
block_scope_for_edge [Cil2cfg] | |
blsl [Cint] | |
blsl [Wp.Cint] | |
blsr [Cint] | |
blsr [Wp.Cint] | |
bnot [Cint] | |
bnot [Wp.Cint] | |
bool_and [Cvalues] | |
bool_eq [Cvalues] | |
bool_leq [Cvalues] | |
bool_lt [Cvalues] | |
bool_neq [Cvalues] | |
bool_of_int [Cmath] | |
bool_or [Cvalues] | |
bool_val [Cvalues] | |
bootstrap_logic [LogicCompiler.Make] | |
bootstrap_logic [Wp.LogicCompiler.Make] | |
bootstrap_pred [LogicCompiler.Make] | |
bootstrap_pred [Wp.LogicCompiler.Make] | |
bootstrap_region [LogicCompiler.Make] | |
bootstrap_region [Wp.LogicCompiler.Make] | |
bootstrap_term [LogicCompiler.Make] | |
bootstrap_term [Wp.LogicCompiler.Make] | |
bor [Cint] | |
bor [Wp.Cint] | |
bound [ProofEngine] | |
bound_add [Vset] | |
bound_add [Wp.Vset] | |
bound_shift [Vset] | |
bound_shift [Wp.Vset] | |
bound_sub [Vset] | |
bound_sub [Wp.Vset] | |
bounds [Auto.Range] | |
bounds [Ctypes] |
domain, bounds included
|
bounds [Wp.Auto.Range] | |
bounds [Wp.Ctypes] |
domain, bounds included
|
branch [CfgCompiler.Cfg] |
Structurally corresponds to an if-then-else control-flow.
|
branch [Conditions] |
Construct a branch bundle, with merging of all common parts.
|
branch [Letify.Ground] | |
branch [Wp.CfgCompiler.Cfg] |
Structurally corresponds to an if-then-else control-flow.
|
branch [Wp.Conditions] |
Construct a branch bundle, with merging of all common parts.
|
branching [Pcfg] | |
branching [Wp.Pcfg] | |
break [Clabels] | |
break [Wp.Clabels] | |
build_prop_of_from [Mcfg.S] |
build
p => alpha(p) for functional dependencies verification.
|
build_prop_of_from [Wp.Mcfg.S] |
build
p => alpha(p) for functional dependencies verification.
|
builtin_types [Lang] | |
builtin_types [Wp.Lang] | |
bundle [Pcond] | |
bundle [Conditions] |
Closes the bundle and promote it into a well-formed sequence.
|
bundle [Wp.Pcond] | |
bundle [Wp.Conditions] |
Closes the bundle and promote it into a well-formed sequence.
|
bxor [Cint] | |
bxor [Wp.Cint] | |
C | |
c_bool [Ctypes] |
Returns the type of
int
|
c_bool [Wp.Ctypes] |
Returns the type of
int
|
c_char [Ctypes] |
Returns the type of
char
|
c_char [Wp.Ctypes] |
Returns the type of
char
|
c_float [Ctypes] |
Conforms to
|
c_float [Wp.Ctypes] |
Conforms to
|
c_int [Ctypes] |
Conforms to
|
c_int [Wp.Ctypes] |
Conforms to
|
c_ptr [Ctypes] |
Returns the type of pointers
|
c_ptr [Wp.Ctypes] |
Returns the type of pointers
|
cache [Layout.Offset] | |
cache_descr [Wpo.VC_Annot] | |
cache_descr [Wpo.VC_Lemma] | |
cache_descr [Wp.Wpo.VC_Annot] | |
cache_descr [Wp.Wpo.VC_Lemma] | |
cache_log [Wpo.DISK] | |
cache_log [Wp.Wpo.DISK] | |
cached [VCS] |
only for true verdicts
|
cached [Wp.VCS] |
only for true verdicts
|
call [StmtSemantics.Make] | |
call [LogicCompiler.Make] | |
call [Sigs.LogicSemantics] |
Create call data from the callee point of view,
deriving data (gamma and pools) from the current frame.
|
call [Sigs.CodeSemantics] |
Address of a function pointer.
|
call [Splitter] | |
call [Mcfg.S] | |
call [Wp.StmtSemantics.Make] | |
call [Wp.LogicCompiler.Make] | |
call [Wp.Sigs.LogicSemantics] |
Create call data from the callee point of view,
deriving data (gamma and pools) from the current frame.
|
call [Wp.Sigs.CodeSemantics] |
Address of a function pointer.
|
call [Wp.Splitter] | |
call [Wp.Mcfg.S] | |
call_dynamic [Mcfg.S] | |
call_dynamic [Wp.Mcfg.S] | |
call_fun [LogicCompiler.Make] | |
call_fun [Definitions] | |
call_fun [Wp.LogicCompiler.Make] | |
call_fun [Wp.Definitions] | |
call_goal_precond [Mcfg.S] | |
call_goal_precond [Wp.Mcfg.S] | |
call_kf [StmtSemantics.Make] | |
call_kf [Wp.StmtSemantics.Make] | |
call_post [LogicCompiler.Make] | |
call_post [Sigs.LogicSemantics] |
Derive a frame from the call data suitable for compiling the
called function contracts in the provided pre-state and post-state.
|
call_post [Wp.LogicCompiler.Make] | |
call_post [Wp.Sigs.LogicSemantics] |
Derive a frame from the call data suitable for compiling the
called function contracts in the provided pre-state and post-state.
|
call_pre [LogicCompiler.Make] | |
call_pre [Sigs.LogicSemantics] |
Derive a frame from the call data suitable for compiling the
called function contracts in the provided pre-state.
|
call_pre [Wp.LogicCompiler.Make] | |
call_pre [Wp.Sigs.LogicSemantics] |
Derive a frame from the call data suitable for compiling the
called function contracts in the provided pre-state.
|
call_pred [LogicCompiler.Make] | |
call_pred [Definitions] | |
call_pred [Wp.LogicCompiler.Make] | |
call_pred [Wp.Definitions] | |
callback [WpContext.Registry] | |
callback [Wp.WpContext.Registry] | |
cancel [ProofEngine] | |
cardinal [TacInstance] |
less than limit
|
cardinal [Set.S] |
Return the number of elements of a set.
|
cardinal [Map.S] |
Return the number of bindings of a map.
|
case [Clabels] | |
case [Wp.Clabels] | |
cases [Splitter] | |
cases [Wp.Splitter] | |
cast [Sigs.CodeSemantics] |
Applies a pointer cast or a conversion.
|
cast [Sigs.Model] |
Cast a memory location into another memory location.
|
cast [Wp.Sigs.CodeSemantics] |
Applies a pointer cast or a conversion.
|
cast [Wp.Sigs.Model] |
Cast a memory location into another memory location.
|
cat_print_generated [Wp_parameters] | |
cat_print_generated [Wp.Wp_parameters] | |
catch [Warning] |
Set up a context for the job.
|
catch [Wp.Warning] |
Set up a context for the job.
|
catch_label_error [NormAtLabels] | |
catch_label_error [Wp.NormAtLabels] | |
cc_assign [RegionAccess] | |
cc_fundec [RegionAccess] | |
cc_init [RegionAccess] | |
cc_instr [RegionAccess] | |
cc_lval [RegionAccess] | |
cc_pred [RegionAccess] | |
cc_read [RegionAccess] | |
cc_region [RegionAccess] | |
cc_spec [RegionAccess] | |
cc_term [RegionAccess] | |
cdomain [Cvalues] | |
cfg_kf [Cil2cfg] | |
cfg_of_strategy [WpStrategy] | |
cfg_spec_only [Cil2cfg] |
returns
true is this CFG is degenerated (no code available)
|
char [Ctypes] | |
char [Wp.Ctypes] | |
char_at [Cstring] | |
char_at [Wp.Cstring] | |
check_assigns [Sigs.LogicSemantics] |
Check assigns inclusion.
|
check_assigns [Wp.Sigs.LogicSemantics] |
Check assigns inclusion.
|
check_tau [Vlist] | |
check_term [Vlist] | |
checkbox [Tactical] |
Unless specified, default is
false .
|
checkbox [Wp.Tactical] |
Unless specified, default is
false .
|
children [ProofEngine] | |
choice [Auto] | |
choice [StmtSemantics.Make] |
Chain compiler in parallel, between labels
~pre and ~post , which
defaults to resp.
|
choice [Wp.Auto] | |
choice [Wp.StmtSemantics.Make] |
Chain compiler in parallel, between labels
~pre and ~post , which
defaults to resp.
|
choose [VCS] | |
choose [Sigs.Sigma] |
Make the union of each sigma, choosing the minimal variable
in case of conflict.
|
choose [Wp.VCS] | |
choose [Wp.Sigs.Sigma] |
Make the union of each sigma, choosing the minimal variable
in case of conflict.
|
choose [Set.S] |
Return one element of the given set, or raise
Not_found if
the set is empty.
|
choose [Map.S] |
Return one binding of the given map, or raise
Not_found if
the map is empty.
|
choose_opt [Set.S] |
Return one element of the given set, or
None if
the set is empty.
|
choose_opt [Map.S] |
Return one binding of the given map, or
None if
the map is empty.
|
chunk [Region] | |
chunks [Region] | |
cint [Tactical] | |
cint [Wp.Tactical] | |
clean [Conditions] | |
clean [Wp.Conditions] | |
cleanup_cache [ProverWhy3] | |
clear [VC] | |
clear [Wpo] | |
clear [Cil2cfg.HEsig] | |
clear [WpContext.Generator] | |
clear [WpContext.Registry] | |
clear [Context] |
Clear the current value.
|
clear [Wp.Wpo] | |
clear [Wp.VC] | |
clear [Hashtbl.S] | |
clear [Wp.WpContext.Generator] | |
clear [Wp.WpContext.Registry] | |
clear [Wp.Context] |
Clear the current value.
|
clear_results [Wpo] | |
clear_results [Wp.Wpo] | |
clear_scheduled [Register] | |
clear_session [Register] | |
cloc [Sigs.CodeSemantics] |
Interpret a value as a location.
|
cloc [Wp.Sigs.CodeSemantics] |
Interpret a value as a location.
|
close [Script] | |
close [Conditions] |
With free variables quantified.
|
close [Mcfg.S] | |
close [Wp.Conditions] |
With free variables quantified.
|
close [Wp.Mcfg.S] | |
cluster [MemLoader] | |
cluster [Cstring] |
The cluster where all strings are defined.
|
cluster [Definitions] | |
cluster [Region] | |
cluster [Wp.Cstring] |
The cluster where all strings are defined.
|
cluster [Wp.Definitions] | |
cluster_age [Definitions] | |
cluster_age [Wp.Definitions] | |
cluster_compare [Definitions] | |
cluster_compare [Wp.Definitions] | |
cluster_id [Definitions] |
Unique
|
cluster_id [Wp.Definitions] |
Unique
|
cluster_position [Definitions] | |
cluster_position [Wp.Definitions] | |
cluster_title [Definitions] | |
cluster_title [Wp.Definitions] | |
cmdline [Register] | |
cmdline_run [Register] | |
cmp_prover [VCS] | |
cmp_prover [Wp.VCS] | |
code_lit [Cfloat] | |
code_lit [Wp.Cfloat] | |
codomain [Letify.Sigma] | |
command [VC] |
Run the provers with the command-line interface.
|
command [Rformat] | |
command [Wp.VC] |
Run the provers with the command-line interface.
|
commit [ProofEngine] | |
comp [Lang] | |
comp [Wp.Lang] | |
comp_id [Lang] | |
comp_id [Wp.Lang] | |
compare [VCS] | |
compare [Sigs.Chunk] | |
compare [LogicBuiltins] | |
compare [Lang.F] | |
compare [RegionAnnot.Lpath] | |
compare [Layout.Value] | |
compare [Layout.Data] | |
compare [WpContext.Key] | |
compare [WpContext.Entries] | |
compare [WpContext.SCOPE] | |
compare [WpContext.MODEL] | |
compare [WpContext.S] | |
compare [Warning] | |
compare [Why3Provers] | |
compare [Clabels.T] | |
compare [Ctypes.AinfoComparable] | |
compare [Ctypes] | |
compare [Map.OrderedType] |
A total ordering function over the keys.
|
compare [Wp.VCS] | |
compare [Wp.Sigs.Chunk] | |
compare [Wp.LogicBuiltins] | |
compare [Wp.Lang.F] | |
compare [Wp.WpContext.Key] | |
compare [Wp.WpContext.Entries] | |
compare [Wp.WpContext.SCOPE] | |
compare [Wp.WpContext.MODEL] | |
compare [Wp.WpContext.S] | |
compare [Wp.Warning] | |
compare [Set.S] |
Total ordering between sets.
|
compare [Map.S] |
Total ordering between maps.
|
compare [Wp.Clabels.T] | |
compare [Wp.Ctypes.AinfoComparable] | |
compare [Wp.Ctypes] | |
compare_c_float [Ctypes] | |
compare_c_float [Wp.Ctypes] | |
compare_c_int [Ctypes] | |
compare_c_int [Wp.Ctypes] | |
compare_prop_id [WpPropId] | |
compare_prop_id [Wp.WpPropId] | |
compare_ptr_conflated [Ctypes] |
same as
Ctypes.compare but all PTR are considered the same
|
compare_ptr_conflated [Wp.Ctypes] |
same as
Wp.Ctypes.compare but all PTR are considered the same
|
comparep [Lang.F] | |
comparep [Wp.Lang.F] | |
compile [CfgCompiler.Cfg] | |
compile [WpContext.IData] | |
compile [WpContext.Data] | |
compile [WpContext.Registry] |
with circularity protection
|
compile [Wp.CfgCompiler.Cfg] | |
compile [Wp.WpContext.IData] | |
compile [Wp.WpContext.Data] | |
compile [Wp.WpContext.Registry] |
with circularity protection
|
compile_lemma [Definitions] | |
compile_lemma [Wp.Definitions] | |
compiler [Factory] | |
compiler [Wp.Factory] | |
compinfo [Definitions] | |
compinfo [Wp.Definitions] | |
complexity [TacInstance] | |
compose [Tactical] | |
compose [Wp.Tactical] | |
composer [Tactical] |
Unless specified, default is Empty selection.
|
composer [Wp.Tactical] |
Unless specified, default is Empty selection.
|
compound [Auto] | |
compound [Wp.Auto] | |
compute [Calculus.Cfg] | |
compute [Auto.Range] | |
compute [Wpo.GOAL] | |
compute [Wpo] | |
compute [Filtering] | |
compute [Letify.Ground] | |
compute [RefUsage] | |
compute [LogicUsage] |
To force computation
|
compute [Dyncall] |
Forces computation of dynamic calls.
|
compute [Wp.Wpo.GOAL] | |
compute [Wp.Wpo] | |
compute [Wp.Auto.Range] | |
compute [Wp.Filtering] | |
compute [Wp.RefUsage] | |
compute [Wp.LogicUsage] |
To force computation
|
compute_auto [Register] | |
compute_call [Generator] | |
compute_descr [Wpo.GOAL] | |
compute_descr [Wp.Wpo.GOAL] | |
compute_hypotheses [WpContext] | |
compute_hypotheses [Wp.WpContext] | |
compute_ip [Generator] | |
compute_kf [Generator] | |
compute_kf [StmtSemantics.Make] |
Full Compilation
|
compute_kf [Wp.StmtSemantics.Make] |
Full Compilation
|
compute_proof [Wpo.GOAL] | |
compute_proof [Wp.Wpo.GOAL] | |
compute_provers [Register] | |
compute_selection [Generator] | |
computer [Register] | |
computer [CfgWP] | |
computing [VCS] | |
computing [Wp.VCS] | |
concat [CfgCompiler.Cfg] |
The concatenation is the intersection of all
possible collection of traces from each cfg.
|
concat [Conditions] |
List conjunction
|
concat [Wp.CfgCompiler.Cfg] |
The concatenation is the intersection of all
possible collection of traces from each cfg.
|
concat [Wp.Conditions] |
List conjunction
|
concretize [Vset] | |
concretize [Wp.Vset] | |
cond [Sigs.CodeSemantics] |
Evaluate the conditional expression on the given memory state.
|
cond [Wp.Sigs.CodeSemantics] |
Evaluate the conditional expression on the given memory state.
|
condition [Conditions] |
With free variables kept.
|
condition [Wp.Conditions] |
With free variables kept.
|
conditions [Passive] | |
conditions [Wp.Passive] | |
config [Why3Provers] | |
configure [ProofScript] | |
configure [VCS] | |
configure [Sigs.Model] |
Initializers to be run before using the model.
|
configure [Cfloat] | |
configure [Cint] | |
configure [Context] |
Apply global configure hooks, once per project/ast.
|
configure [Why3Provers] | |
configure [Wp.VCS] | |
configure [Wp.Sigs.Model] |
Initializers to be run before using the model.
|
configure [Wp.Cfloat] | |
configure [Wp.Cint] | |
configure [Wp.Context] |
Apply global configure hooks, once per project/ast.
|
configure_driver [Factory] | |
configure_driver [Wp.Factory] | |
configure_ia [Sigs.Model] |
Given an automaton, return a vertex's binder.
|
configure_ia [Wp.Sigs.Model] |
Given an automaton, return a vertex's binder.
|
const [Mcfg.S] | |
const [Wp.Mcfg.S] | |
constant [Cvalues] | |
constant [LogicBuiltins] | |
constant [Lang.F] | |
constant [Ctypes] | |
constant [Wp.LogicBuiltins] | |
constant [Wp.Lang.F] | |
constant [Wp.Ctypes] | |
constant_exp [Cvalues] | |
constant_term [Cvalues] | |
context [Warning] | |
context [Wp.Warning] | |
context_pp [Lang.F] |
Context used by pp_term, pp_pred, pp_var, ppvars for printing
the term.
|
context_pp [Wp.Lang.F] |
Context used by pp_term, pp_pred, pp_var, ppvars for printing
the term.
|
continue [Clabels] | |
continue [Wp.Clabels] | |
contrapose [Auto] | |
contrapose [Wp.Auto] | |
convert [Cint] |
Independent from model
|
convert [Wp.Cint] |
Independent from model
|
copied [MemLoader.Make] | |
copied [Sigs.Model] |
Return a set of equations that express a copy between two memory state.
|
copied [Wp.Sigs.Model] |
Return a set of equations that express a copy between two memory state.
|
copy [Sigs.Sigma] |
Duplicate the environment.
|
copy [Letify.Ground] | |
copy [Hashtbl.S] | |
copy [Wp.Sigs.Sigma] |
Duplicate the environment.
|
copy [Datatype.S] |
Deep copy: no possible sharing between
x and copy x .
|
create [CfgDump] | |
create [Tactical.Fmap] | |
create [CfgCompiler.Cfg.E] |
Bundle an equation with the sigma sequence that created it
|
create [CfgCompiler.Cfg.T] |
Bundle a term with the sigma sequence that created it.
|
create [CfgCompiler.Cfg.P] |
Bundle an equation with the sigma sequence that created it.
|
create [CfgCompiler.Cfg.C] |
Bundle an equation with the sigma sequence that created it.
|
create [CfgCompiler.Cfg.Node] | |
create [Pcfg] | |
create [Mstate] | |
create [Sigs.Sigma] |
Initially empty environment.
|
create [Cleaning] | |
create [Letify.Split] | |
create [Cil2cfg.HEsig] | |
create [Region] | |
create [Warning] | |
create [Context] |
Creates a new context with name
|
create [Wp.Tactical.Fmap] | |
create [Wp.CfgCompiler.Cfg.E] |
Bundle an equation with the sigma sequence that created it
|
create [Wp.CfgCompiler.Cfg.T] |
Bundle a term with the sigma sequence that created it.
|
create [Wp.CfgCompiler.Cfg.P] |
Bundle an equation with the sigma sequence that created it.
|
create [Wp.CfgCompiler.Cfg.C] |
Bundle an equation with the sigma sequence that created it.
|
create [Hashtbl.S] | |
create [Wp.CfgCompiler.Cfg.Node] | |
create [Wp.Pcfg] | |
create [Wp.Mstate] | |
create [Wp.Sigs.Sigma] |
Initially empty environment.
|
create [Wp.Warning] | |
create [Wp.Context] |
Creates a new context with name
|
create_option [LogicBuiltins] | add_option_sanitizer ~driver_dir group name
add a sanitizer for group group and option name
|
create_option [Wp.LogicBuiltins] | add_option_sanitizer ~driver_dir group name
add a sanitizer for group group and option name
|
create_proof [WpAnnot] |
to be used only once for one of the related prop_id
|
create_tbl [WpStrategy] | |
ctor [LogicBuiltins] | |
ctor [Wp.LogicBuiltins] | |
ctor_id [Lang] | |
ctor_id [Wp.Lang] | |
current [ProofEngine] | |
current [VCS] |
Current parameters
|
current [LogicCompiler.Make] | |
current [Sigs.LogicSemantics] |
The current memory state.
|
current [Cint] | |
current [Wp.VCS] |
Current parameters
|
current [Wp.LogicCompiler.Make] | |
current [Wp.Sigs.LogicSemantics] |
The current memory state.
|
current [Wp.Cint] | |
cut [Auto] | |
cut [Wp.Auto] | |
cval [Sigs.CodeSemantics] |
Evaluate an abstract value.
|
cval [Wp.Sigs.CodeSemantics] |
Evaluate an abstract value.
|
cvar [Sigs.Model] |
Return the location of a C variable.
|
cvar [Wp.Sigs.Model] |
Return the location of a C variable.
|
D | |
datatype [MemVar.VarUsage] | |
datatype [Sigs.Model] |
For projectification.
|
datatype [Lang] | |
datatype [Wp.MemVar.VarUsage] | |
datatype [Wp.Sigs.Model] |
For projectification.
|
datatype [Wp.Lang] | |
debugp [Lang.F] | |
debugp [Wp.Lang.F] | |
decide [Lang.F] |
Return
true if and only the term is e_true .
|
decide [Wp.Lang.F] |
Return
true if and only the term is e_true .
|
decode [ProofScript] | |
def_into_axiom [Filter_axioms] | |
default [Factory] | "Var,Typed,Nat,Real" memory model.
|
default [Tactical] | |
default [VCS] |
all None
|
default [Layout.Pack] | |
default [Layout.Flat] | |
default [Layout.RW] | |
default [Clabels] | |
default [Wp.Tactical] | |
default [Wp.VCS] |
all None
|
default [Wp.Factory] | "Var,Typed,Nat,Real" memory model.
|
default [Wp.Clabels] | |
default_mode [Register] | |
define [Lang.F] | |
define [WpContext.Registry] |
no redefinition ; circularity protected
|
define [Wp.Lang.F] | |
define [Wp.WpContext.Registry] |
no redefinition ; circularity protected
|
define_lemma [Definitions] | |
define_lemma [Wp.Definitions] | |
define_symbol [Definitions] | |
define_symbol [Wp.Definitions] | |
define_type [Definitions] | |
define_type [Wp.Definitions] | |
defined [Context] |
The current value is defined.
|
defined [Wp.Context] |
The current value is defined.
|
definition [Auto] | |
definition [Wp.Auto] | |
defs [Lang.F] | |
defs [Wp.Lang.F] | |
delete_script_for [Proof] | delete_script ~gid remove known script for goal.
|
denv [Matrix] | |
dependencies [WpAnnot] | |
dependencies [LogicBuiltins] |
Of external theories.
|
dependencies [Wp.LogicBuiltins] |
Of external theories.
|
deprecated [Register] | |
deprecated_wp_clear [Register] | |
deprecated_wp_compute [Register] | |
deprecated_wp_compute_call [Register] | |
deprecated_wp_compute_ip [Register] | |
deprecated_wp_compute_kf [Register] | |
deref [Layout.Cluster] | |
descr [Factory] | |
descr [Vset] | |
descr [LogicBuiltins] | |
descr [WpContext.MODEL] | |
descr [Wp.Factory] | |
descr [Wp.Vset] | |
descr [Wp.LogicBuiltins] | |
descr [Wp.WpContext.MODEL] | |
destruct [Tactical] | |
destruct [Wp.Tactical] | |
diff [Set.S] |
Set difference.
|
dimension_of_object [Ctypes] |
Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells
|
dimension_of_object [Wp.Ctypes] |
Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells
|
directory [WpContext] |
Current model in
"-wp-out" directory
|
directory [Wp.WpContext] |
Current model in
"-wp-out" directory
|
disjoint [Vset] | |
disjoint [Layout.Chunk] | |
disjoint [Wp.Vset] | |
dkey_builtins [Register] | |
dkey_cluster [ProverErgo] | |
dkey_logicusage [Register] | |
dkey_main [Register] | |
dkey_no_cache_info [VCS] | |
dkey_no_cache_info [Wp.VCS] | |
dkey_no_goals_info [VCS] | |
dkey_no_goals_info [Wp.VCS] | |
dkey_no_step_info [VCS] | |
dkey_no_step_info [Wp.VCS] | |
dkey_no_time_info [VCS] | |
dkey_no_time_info [Wp.VCS] | |
dkey_prover [Register] | |
dkey_raised [Register] | |
dkey_refusage [Register] | |
dkey_shell [Register] | |
dkey_success_only [VCS] | |
dkey_success_only [Wp.VCS] | |
do_alias [Region] | |
do_cache_cleanup [Register] | |
do_list_scheduled [Register] | |
do_list_scheduled_result [Register] | |
do_progress [Register] | |
do_prover_detect [Register] | |
do_report_cache_usage [Register] | |
do_report_prover_stats [Register] | |
do_report_scheduled [Register] | |
do_report_steps [Register] | |
do_report_stopped [Register] | |
do_report_time [Register] | |
do_update_session [Register] | |
do_wp_print [Register] | |
do_wp_print_for [Register] | |
do_wp_proofs [Register] | |
do_wp_proofs_for [Register] | |
do_wp_proofs_iter [Register] | |
do_wp_report [Register] | |
do_wpo_display [Register] | |
do_wpo_failed [Register] | |
do_wpo_result [Register] | |
do_wpo_smoke [Register] | |
do_wpo_start [Register] | |
do_wpo_stat [Register] | |
do_wpo_success [Register] | |
do_wpo_wait [Register] | |
domain [MemLoader.Model] | |
domain [Conditions] |
Assumes a list of predicates in a
Type section on top of the bundle.
|
domain [Sigs.LogicAssigns] |
Memory footprint of a region.
|
domain [Sigs.Model] |
Compute the set of chunks that hold the value of an object with
the given C-type.
|
domain [Sigs.Sigma] |
Footprint of a memory environment.
|
domain [Letify.Defs] | |
domain [Letify.Sigma] | |
domain [Wp.Conditions] |
Assumes a list of predicates in a
Type section on top of the bundle.
|
domain [Wp.Sigs.LogicAssigns] |
Memory footprint of a region.
|
domain [Wp.Sigs.Model] |
Compute the set of chunks that hold the value of an object with
the given C-type.
|
domain [Wp.Sigs.Sigma] |
Footprint of a memory environment.
|
doomed_if_valid [WpPropId] |
Properties that are False-if-unreachable in case the PO is valid.
|
doomed_if_valid [Wp.WpPropId] |
Properties that are False-if-unreachable in case the PO is valid.
|
downcast [Cint] |
Dependent on model
|
downcast [Wp.Cint] |
Dependent on model
|
driver [LogicBuiltins] | |
driver [Wp.LogicBuiltins] | |
dummy [Wpo.GOAL] | |
dummy [Definitions] | |
dummy [Wp.Wpo.GOAL] | |
dummy [Wp.Definitions] | |
dump [WpReached] | |
dump [Pcond] | |
dump [LogicBuiltins] | |
dump [RegionDump] | |
dump [RefUsage] | |
dump [LogicUsage] |
Print on output
|
dump [Wp.Pcond] | |
dump [Wp.LogicBuiltins] | |
dump [Wp.RefUsage] | |
dump [Wp.LogicUsage] |
Print on output
|
dump_env [CfgCompiler.Cfg] | |
dump_env [Wp.CfgCompiler.Cfg] | |
dump_strategies [Register] | |
E | |
e_add [Lang.F] | |
e_add [Wp.Lang.F] | |
e_and [Lang.F] | |
e_and [Wp.Lang.F] | |
e_apply [Letify.Sigma] | |
e_apply [Letify.Ground] | |
e_bigint [Lang.F] | |
e_bigint [Wp.Lang.F] | |
e_bind [Lang.F] | |
e_bind [Wp.Lang.F] | |
e_bool [Lang.F] | |
e_bool [Wp.Lang.F] | |
e_close [Lang.F] |
Closes all specified binders
|
e_close [Wp.Lang.F] |
Closes all specified binders
|
e_cnf [WpTac] | |
e_const [Lang.F] | |
e_const [Wp.Lang.F] | |
e_div [Lang.F] | |
e_div [Wp.Lang.F] | |
e_dnf [WpTac] | |
e_eq [Lang.F] | |
e_eq [Wp.Lang.F] | |
e_equiv [Lang.F] | |
e_equiv [Wp.Lang.F] | |
e_expr [Lang.F] | |
e_expr [Wp.Lang.F] | |
e_fact [Lang.F] | |
e_fact [Wp.Lang.F] | |
e_false [Lang.F] | |
e_false [Wp.Lang.F] | |
e_float [Lang.F] | |
e_float [Wp.Lang.F] | |
e_fun [Lang.F] | |
e_fun [Wp.Lang.F] | |
e_get [Lang.F] | |
e_get [Wp.Lang.F] | |
e_getfield [Lang.F] | |
e_getfield [Wp.Lang.F] | |
e_if [Lang.F] | |
e_if [Wp.Lang.F] | |
e_imply [Lang.F] | |
e_imply [Wp.Lang.F] | |
e_int [Lang.F] | |
e_int [Wp.Lang.F] | |
e_int64 [Lang.F] | |
e_int64 [Wp.Lang.F] | |
e_leq [Lang.F] | |
e_leq [Wp.Lang.F] | |
e_literal [Lang.F] | |
e_literal [Wp.Lang.F] | |
e_lt [Lang.F] | |
e_lt [Wp.Lang.F] | |
e_minus_one [Lang.F] | |
e_minus_one [Wp.Lang.F] | |
e_minus_one_real [Lang.F] | |
e_minus_one_real [Wp.Lang.F] | |
e_mod [Lang.F] | |
e_mod [Wp.Lang.F] | |
e_mul [Lang.F] | |
e_mul [Wp.Lang.F] | |
e_neq [Lang.F] | |
e_neq [Wp.Lang.F] | |
e_not [Lang.F] | |
e_not [Wp.Lang.F] | |
e_one [Lang.F] | |
e_one [Wp.Lang.F] | |
e_one_real [Lang.F] | |
e_one_real [Wp.Lang.F] | |
e_open [Lang.F] |
Open all the specified binders (flags default to `true`, so all
consecutive top most binders are opened by default).
|
e_open [Wp.Lang.F] |
Open all the specified binders (flags default to `true`, so all
consecutive top most binders are opened by default).
|
e_opp [Lang.F] | |
e_opp [Wp.Lang.F] | |
e_or [Lang.F] | |
e_or [Wp.Lang.F] | |
e_prod [Lang.F] | |
e_prod [Wp.Lang.F] | |
e_prop [Lang.F] | |
e_prop [Wp.Lang.F] | |
e_props [Lang.F] | |
e_props [Wp.Lang.F] | |
e_range [Lang.F] |
e_range a b = b+1-a
|
e_range [Wp.Lang.F] |
e_range a b = b+1-a
|
e_real [Lang.F] | |
e_real [Wp.Lang.F] | |
e_record [Lang.F] | |
e_record [Wp.Lang.F] | |
e_set [Lang.F] | |
e_set [Wp.Lang.F] | |
e_setfield [Lang.F] | |
e_setfield [Wp.Lang.F] | |
e_sub [Lang.F] | |
e_sub [Wp.Lang.F] | |
e_subst [Lang.F] | |
e_subst [Lang] |
uses current pool
|
e_subst [Wp.Lang.F] | |
e_subst [Wp.Lang] |
uses current pool
|
e_sum [Lang.F] | |
e_sum [Wp.Lang.F] | |
e_times [Lang.F] | |
e_times [Wp.Lang.F] | |
e_true [Lang.F] | |
e_true [Wp.Lang.F] | |
e_var [Lang.F] | |
e_var [Wp.Lang.F] | |
e_vars [Lang.F] |
Sorted
|
e_vars [Wp.Lang.F] |
Sorted
|
e_zero [Lang.F] | |
e_zero [Wp.Lang.F] | |
e_zero_real [Lang.F] | |
e_zero_real [Wp.Lang.F] | |
e_zint [Lang.F] | |
e_zint [Wp.Lang.F] | |
eat [Script] | |
edge_dst [Cil2cfg] | |
edge_src [Cil2cfg] |
node and edges relations
|
effect [CfgCompiler.Cfg] |
Represents all execution trace
T such that, if T contains node a ,
then T also contains b with the given effect on corresponding
memory states.
|
effect [Wp.CfgCompiler.Cfg] |
Represents all execution trace
T such that, if T contains node a ,
then T also contains b with the given effect on corresponding
memory states.
|
either [CfgCompiler.Cfg] |
Structurally corresponds to an arbitrary choice among the different
possible executions.
|
either [Conditions] |
Construct a disjunction bundle, with merging of all common parts.
|
either [Wp.CfgCompiler.Cfg] |
Structurally corresponds to an arbitrary choice among the different
possible executions.
|
either [Wp.Conditions] |
Construct a disjunction bundle, with merging of all common parts.
|
elements [Vlist] | |
elements [Set.S] |
Return the list of all elements of the given set.
|
emit [Warning] |
Emit a warning in current context.
|
emit [Wp.Warning] |
Emit a warning in current context.
|
empty [Conditions] |
empty sequence, equivalent to true assumption
|
empty [Sigs.Sigma] |
Same as
Chunk.Set.empty
|
empty [Letify.Defs] | |
empty [Letify.Sigma] | |
empty [Vset] | |
empty [Splitter] | |
empty [Passive] | |
empty [Mcfg.S] | |
empty [Layout.Chunk] | |
empty [MemoryContext] | |
empty [Wp.Conditions] |
empty sequence, equivalent to true assumption
|
empty [Wp.Sigs.Sigma] |
Same as
Chunk.Set.empty
|
empty [Wp.Vset] | |
empty [Wp.Splitter] | |
empty [Wp.Passive] | |
empty [Wp.Mcfg.S] | |
empty [Wp.MemoryContext] | |
empty [Set.S] |
The empty set.
|
empty [Map.S] |
The empty map.
|
empty_acc [WpStrategy] | |
empty_assigns_info [WpPropId] | |
empty_assigns_info [Wp.WpPropId] | |
empty_env [StmtSemantics.Make] | |
empty_env [Wp.StmtSemantics.Make] | |
encode [ProofScript] | |
end_session [Register] | |
env [Lang.F] | |
env [Wp.Lang.F] | |
env_at [LogicCompiler.Make] | |
env_at [Sigs.LogicSemantics] |
Returns a new environment where the current memory state is
moved to to the corresponding label.
|
env_at [Wp.LogicCompiler.Make] | |
env_at [Wp.Sigs.LogicSemantics] |
Returns a new environment where the current memory state is
moved to to the corresponding label.
|
env_let [LogicCompiler.Make] | |
env_let [Wp.LogicCompiler.Make] | |
env_letp [LogicCompiler.Make] | |
env_letp [Wp.LogicCompiler.Make] | |
env_letval [LogicCompiler.Make] | |
env_letval [Wp.LogicCompiler.Make] | |
env_script_update [Register] | |
epsilon [Rformat] | |
eq_alias [Region] | |
eqmem [MemLoader.Model] | |
eqmem_forall [MemLoader.Model] | |
eqp [Lang.F] | |
eqp [Wp.Lang.F] | |
equal [CfgCompiler.Cfg.C] | |
equal [CfgCompiler.Cfg.Node] | |
equal [Mstate] | |
equal [Sigs.Chunk] | |
equal [Letify.Sigma] | |
equal [Vset] | |
equal [Lang.F] |
Same as
==
|
equal [RegionAnnot.Lpath] | |
equal [Layout.Value] | |
equal [Layout.Data] | |
equal [WpContext.SCOPE] | |
equal [WpContext.MODEL] | |
equal [WpContext.S] | |
equal [Clabels] | |
equal [Ctypes.AinfoComparable] | |
equal [Ctypes] | |
equal [Wp.CfgCompiler.Cfg.C] | |
equal [Wp.CfgCompiler.Cfg.Node] | |
equal [Wp.Mstate] | |
equal [Wp.Sigs.Chunk] | |
equal [Wp.Vset] | |
equal [Wp.Lang.F] |
Same as
==
|
equal [Wp.WpContext.SCOPE] | |
equal [Wp.WpContext.MODEL] | |
equal [Wp.WpContext.S] | |
equal [Set.S] | equal s1 s2 tests whether the sets s1 and s2 are
equal, that is, contain equal elements.
|
equal [Map.S] | equal cmp m1 m2 tests whether the maps m1 and m2 are
equal, that is, contain equal keys and associate them with
equal data.
|
equal [Wp.Clabels] | |
equal [Wp.Ctypes.AinfoComparable] | |
equal [Wp.Ctypes] | |
equal_array [Cvalues] | |
equal_comp [Cvalues] | |
equal_float [Ctypes] | |
equal_float [Wp.Ctypes] | |
equal_obj [Sigs.CodeSemantics] |
Same as
equal_typ with an object type.
|
equal_obj [Wp.Sigs.CodeSemantics] |
Same as
equal_typ with an object type.
|
equal_object [Cvalues] | |
equal_typ [Sigs.CodeSemantics] |
Computes the value of
(a==b) provided both a and b are values
with the given type.
|
equal_typ [Wp.Sigs.CodeSemantics] |
Computes the value of
(a==b) provided both a and b are values
with the given type.
|
equation [Cvalues] | |
error [Script] | |
error [Warning] | |
error [Wp.Warning] | |
eval_eq [Lang.F] |
Same as
are_equal is Yes
|
eval_eq [Wp.Lang.F] |
Same as
are_equal is Yes
|
eval_leq [Lang.F] |
Same as
e_leq is e_true
|
eval_leq [Wp.Lang.F] |
Same as
e_leq is e_true
|
eval_lt [Lang.F] |
Same as
e_lt is e_true
|
eval_lt [Wp.Lang.F] |
Same as
e_lt is e_true
|
eval_neq [Lang.F] |
Same as
are_equal is No
|
eval_neq [Wp.Lang.F] |
Same as
are_equal is No
|
exercised [Register] | |
exist_intro [Conditions] |
Introduce existential quantified formulae: head exist quantifiers
are instanciated to fresh variables, recursively.
|
exist_intro [Wp.Conditions] |
Introduce existential quantified formulae: head exist quantifiers
are instanciated to fresh variables, recursively.
|
exists [ProofSession] | |
exists [Splitter] | |
exists [Wp.Splitter] | |
exists [Set.S] | exists p s checks if at least one element of
the set satisfies the predicate p .
|
exists [Map.S] | exists p m checks if at least one binding of the map
satisfies the predicate p .
|
exists [Parameter_sig.Set] |
Is there some element satisfying the given predicate?
|
exp [Sigs.CodeSemantics] |
Evaluate the expression on the given memory state.
|
exp [Wp.Sigs.CodeSemantics] |
Evaluate the expression on the given memory state.
|
export [Strategy] | |
export [Tactical] |
Register and returns the tactical
|
export [WpReport] | |
export [Vlist] | |
export [Wp.Strategy] | |
export [Wp.Tactical] |
Register and returns the tactical
|
export_decl [Mcfg.Export] | |
export_decl [Wp.Mcfg.Export] | |
export_goal [Mcfg.Export] | |
export_goal [Wp.Mcfg.Export] | |
export_json [WpReport] | |
export_section [Mcfg.Export] | |
export_section [Wp.Mcfg.Export] | |
extern_f [Lang] |
balance just give a default when link is not specified
|
extern_f [Wp.Lang] |
balance just give a default when link is not specified
|
extern_fp [Lang] | |
extern_fp [Wp.Lang] | |
extern_p [Lang] | |
extern_p [Wp.Lang] | |
extern_s [Lang] | |
extern_s [Wp.Lang] | |
extern_t [Lang] | |
extern_t [Wp.Lang] | |
extract [Conditions] |
Computes a formulae equivalent to the bundle.
|
extract [Letify.Defs] | |
extract [Wp.Conditions] |
Computes a formulae equivalent to the bundle.
|
F | |
f32 [Cfloat] | |
f32 [Wp.Cfloat] | |
f64 [Cfloat] | |
f64 [Wp.Cfloat] | |
f_addr_of_int [MemMemory] |
Physical address
|
f_base [MemMemory] | |
f_bits [Cint] |
All bit-test functions
|
f_bits [Ctypes] |
size in bits
|
f_bits [Wp.Cint] |
All bit-test functions
|
f_bits [Wp.Ctypes] |
size in bits
|
f_bitwised [Cint] |
All except f_bit_positive
|
f_bitwised [Wp.Cint] |
All except f_bit_positive
|
f_bytes [Ctypes] |
size in bytes
|
f_bytes [Wp.Ctypes] |
size in bytes
|
f_concat [Vlist] | |
f_cons [Vlist] | |
f_convert [Ctypes] | |
f_convert [Wp.Ctypes] | |
f_delta [Cfloat] | |
f_delta [Wp.Cfloat] | |
f_elt [Vlist] | |
f_epsilon [Cfloat] | |
f_epsilon [Wp.Cfloat] | |
f_global [MemMemory] | |
f_havoc [MemMemory] | |
f_iabs [Cmath] | |
f_int_of_addr [MemMemory] |
Physical address
|
f_iter [Ctypes] | |
f_iter [Wp.Ctypes] | |
f_land [Cint] | |
f_land [Wp.Cint] | |
f_lnot [Cint] | |
f_lnot [Wp.Cint] | |
f_lor [Cint] | |
f_lor [Wp.Cint] | |
f_lsl [Cint] | |
f_lsl [Wp.Cint] | |
f_lsr [Cint] | |
f_lsr [Wp.Cint] | |
f_lxor [Cint] | |
f_lxor [Wp.Cint] | |
f_memo [Ctypes] |
memoized, not-projectified
|
f_memo [Wp.Ctypes] |
memoized, not-projectified
|
f_model [Cfloat] | |
f_model [Wp.Cfloat] | |
f_nil [Vlist] | |
f_nth [Vlist] | |
f_null [MemMemory] | |
f_offset [MemMemory] | |
f_rabs [Cmath] | |
f_real_of_int [Cmath] | |
f_region [MemMemory] | |
f_repeat [Vlist] | |
f_shift [MemMemory] | |
f_sqrt [Cmath] | |
fadd [Cfloat] | |
fadd [Wp.Cfloat] | |
failed [VCS] | |
failed [Wp.VCS] | |
fcstat [WpReport] | |
fdiv [Cfloat] | |
fdiv [Wp.Cfloat] | |
feq [Cfloat] | |
feq [Wp.Cfloat] | |
field [MemLoader.Model] | |
field [Mstate] | |
field [Sigs.Model] |
Return the memory location obtained by field access from a given
memory location.
|
field [Cvalues.Logic] | |
field [Repr] | |
field [Lang] | |
field [Layout.Offset] | |
field [Wp.Mstate] | |
field [Wp.Sigs.Model] |
Return the memory location obtained by field access from a given
memory location.
|
field [Wp.Repr] | |
field [Wp.Lang] | |
field_id [Lang] | |
field_id [Wp.Lang] | |
field_offset [Region] | |
field_offset [Layout.Offset] | |
field_offset [Ctypes] | |
field_offset [Wp.Ctypes] | |
fields [TacInstance] | |
fields_of_adt [Lang] | |
fields_of_adt [Wp.Lang] | |
fields_of_field [Lang] | |
fields_of_field [Wp.Lang] | |
fields_of_tau [Lang] | |
fields_of_tau [Wp.Lang] | |
file_goal [Wpo.DISK] | |
file_goal [Wp.Wpo.DISK] | |
file_kf [Wpo.DISK] | |
file_kf [Wp.Wpo.DISK] | |
file_logerr [Wpo.DISK] | |
file_logerr [Wp.Wpo.DISK] | |
file_logout [Wpo.DISK] | |
file_logout [Wp.Wpo.DISK] | |
filename_for_prover [VCS] | |
filename_for_prover [Wp.VCS] | |
filter [GuiProver] | |
filter [Auto] | |
filter [TacInstance] | |
filter [Script] | |
filter [Filtering] | |
filter [Conditions] | |
filter [Splitter] | |
filter [Wp.Auto] | |
filter [Wp.Filtering] | |
filter [Wp.Conditions] | |
filter [Wp.Splitter] | |
filter [Set.S] | filter p s returns the set of all elements in s
that satisfy predicate p .
|
filter [Map.S] | filter p m returns the map with all the bindings in m
that satisfy predicate p .
|
filter_hypotheses [Lang] | |
filter_hypotheses [Wp.Lang] | |
filter_map_inplace [Hashtbl.S] | |
filter_pred [Cleaning] | |
filter_status [WpAnnot] | |
filter_type [Cleaning] | |
find [TacLemma] | |
find [Pcfg] | |
find [Letify.Sigma] | |
find [Cfloat] | |
find [Cil2cfg.HEsig] | |
find [WpContext.Registry] | |
find [Hashtbl.S] | |
find [Wp.Pcfg] | |
find [Wp.Cfloat] | |
find [Wp.WpContext.Registry] | |
find [Set.S] | find x s returns the element of s equal to x (according
to Ord.compare ), or raise Not_found if no such element
exists.
|
find [Map.S] | find x m returns the current binding of x in m ,
or raises Not_found if no such binding exists.
|
find_all [Cil2cfg.HEsig] | |
find_all [Hashtbl.S] | |
find_fallback [Why3Provers] | |
find_first [Set.S] | find_first f s , where f is a monotonically increasing function,
returns the lowest element e of s such that f e ,
or raises Not_found if no such element exists.
|
find_first [Map.S] | find_first f m , where f is a monotonically increasing function,
returns the binding of m with the lowest key k such that f k ,
or raises Not_found if no such key exists.
|
find_first_opt [Set.S] | find_first_opt f s , where f is a monotonically increasing function,
returns an option containing the lowest element e of s such that
f e , or None if no such element exists.
|
find_first_opt [Map.S] | find_first_opt f m , where f is a monotonically increasing function,
returns an option containing the binding of m with the lowest key k
such that f k , or None if no such key exists.
|
find_last [Set.S] | find_last f s , where f is a monotonically decreasing function,
returns the highest element e of s such that f e ,
or raises Not_found if no such element exists.
|
find_last [Map.S] | find_last f m , where f is a monotonically decreasing function,
returns the binding of m with the highest key k such that f k ,
or raises Not_found if no such key exists.
|
find_last_opt [Set.S] | find_last_opt f s , where f is a monotonically decreasing function,
returns an option containing the highest element e of s such that
f e , or None if no such element exists.
|
find_last_opt [Map.S] | find_last_opt f m , where f is a monotonically decreasing function,
returns an option containing the binding of m with the highest key k
such that f k , or None if no such key exists.
|
find_lemma [Definitions] | |
find_lemma [Wp.Definitions] | |
find_lib [LogicBuiltins] |
find a file in the includes of the current drivers
|
find_lib [Wp.LogicBuiltins] |
find a file in the includes of the current drivers
|
find_name [Definitions] | |
find_name [Wp.Definitions] | |
find_opt [Why3Provers] | |
find_opt [Hashtbl.S] | |
find_opt [Set.S] | find_opt x s returns the element of s equal to x (according
to Ord.compare ), or None if no such element
exists.
|
find_opt [Map.S] | find_opt x m returns Some v if the current binding of x
in m is v , or None if no such binding exists.
|
find_symbol [Definitions] | |
find_symbol [Wp.Definitions] | |
first [ProverSearch] | |
fixpoint [Region] | |
fle [Cfloat] | |
fle [Wp.Cfloat] | |
float_lit [Cfloat] |
Returns a string literal in decimal notation (without suffix)
that reparses to the same value (when added suffix).
|
float_lit [Wp.Cfloat] |
Returns a string literal in decimal notation (without suffix)
that reparses to the same value (when added suffix).
|
float_of_int [Cfloat] | |
float_of_int [Wp.Cfloat] | |
float_of_real [Cfloat] | |
float_of_real [Wp.Cfloat] | |
floats [Lang] |
type of floats
|
floats [Wp.Lang] |
type of floats
|
flt [Cfloat] | |
flt [Wp.Cfloat] | |
flt_add [Cfloat] | |
flt_add [Wp.Cfloat] | |
flt_div [Cfloat] | |
flt_div [Wp.Cfloat] | |
flt_mul [Cfloat] | |
flt_mul [Wp.Cfloat] | |
flt_neg [Cfloat] | |
flt_neg [Wp.Cfloat] | |
flt_of_real [Cfloat] | |
flt_of_real [Wp.Cfloat] | |
flush [Warning] | |
flush [Wp.Warning] | |
fmode [TacCut] | |
fmul [Cfloat] | |
fmul [Wp.Cfloat] | |
fneq [Cfloat] | |
fneq [Wp.Cfloat] | |
fold [Splitter] | |
fold [Hashtbl.S] | |
fold [Wp.Splitter] | |
fold [Set.S] | fold f s a computes (f xN ... (f x2 (f x1 a))...) ,
where x1 ... xN are the elements of s , in increasing order.
|
fold [Map.S] | fold f m a computes (f kN dN ... (f k1 d1 a)...) ,
where k1 ... kN are the keys of all bindings in m
(in increasing order), and d1 ... dN are the associated data.
|
fold_bhv_post_cond [WpStrategy] |
apply
f_normal on the Normal postconditions,
f_exits on the Exits postconditions, and warn on the others.
|
fold_nodes [Cil2cfg] |
iterators
|
fopp [Cfloat] | |
fopp [Wp.Cfloat] | |
for_all [Splitter] | |
for_all [Wp.Splitter] | |
for_all [Set.S] | for_all p s checks if all elements of the set
satisfy the predicate p .
|
for_all [Map.S] | for_all p m checks if all the bindings of the map
satisfy the predicate p .
|
forall_intro [Conditions] |
Introduce universally quantified formulae: head forall quantifiers
are instanciated to fresh variables in current pool and left-implies are
extracted, recursively.
|
forall_intro [Wp.Conditions] |
Introduce universally quantified formulae: head forall quantifiers
are instanciated to fresh variables in current pool and left-implies are
extracted, recursively.
|
fork [ProofEngine] | |
formal [LogicCompiler.Make] | |
formal [Clabels] | |
formal [Wp.LogicCompiler.Make] | |
formal [Wp.Clabels] | |
forward [ProofEngine] | |
forward [Letify.Ground] | |
fq32 [Cfloat] | |
fq32 [Wp.Cfloat] | |
fq64 [Cfloat] | |
fq64 [Wp.Cfloat] | |
frame [LogicCompiler.Make] | |
frame [Sigs.LogicSemantics] |
Make a fresh frame with the given function.
|
frame [Sigs.Model] |
Assert the memory is a proper heap state preceeding the function
entry point.
|
frame [Wp.LogicCompiler.Make] | |
frame [Wp.Sigs.LogicSemantics] |
Make a fresh frame with the given function.
|
frame [Wp.Sigs.Model] |
Assert the memory is a proper heap state preceeding the function
entry point.
|
framed [Layout.Root] | |
frames [MemMemory] | |
frames [MemLoader.Model] | |
free [Context] |
Performs the job with local context cleared.
|
free [Wp.Context] |
Performs the job with local context cleared.
|
fresh [Lang.F] | |
fresh [Wp.Lang.F] | |
freshen [Lang] | |
freshen [Wp.Lang] | |
freshvar [Lang] | |
freshvar [Wp.Lang] | |
from [Layout.Root] | |
froms [StmtSemantics.Make] | |
froms [Wp.StmtSemantics.Make] | |
fsub [Cfloat] | |
fsub [Wp.Cfloat] | |
ftau [Cfloat] |
model independant
|
ftau [Wp.Cfloat] |
model independant
|
fusion [Region] | |
fusionned [Region] | |
G | |
garbled [Layout.Compound] | |
gcd [Layout.Matrix] | |
generate [WpRTE] | |
generate_call [VC] | |
generate_call [Wp.VC] | |
generate_ip [VC] | |
generate_ip [Wp.VC] | |
generate_kf [VC] | |
generate_kf [Wp.VC] | |
generated_f [Lang] | |
generated_f [Wp.Lang] | |
generated_p [Lang] | |
generated_p [Wp.Lang] | |
get [ProverScript] | |
get [ProofEngine] | |
get [ProofSession] | |
get [Tactical.Fmap] |
raises Not_found if absent
|
get [CfgCompiler.Cfg.E] | |
get [CfgCompiler.Cfg.T] | |
get [CfgCompiler.Cfg.P] | |
get [CfgCompiler.Cfg.C] | |
get [Sigs.Sigma] |
Lazily get the variable for a chunk.
|
get [Lang.F.Subst] | |
get [Cil2cfg] | |
get [RegionAnalysis] | |
get [RefUsage] | |
get [WpContext.Generator] | |
get [WpContext.Registry] | |
get [Context] |
Retrieves the current value of the context.
|
get [Dyncall] |
Returns
None if there is no specified dynamic call.
|
get [Wp.Tactical.Fmap] |
raises Not_found if absent
|
get [Wp.CfgCompiler.Cfg.E] | |
get [Wp.CfgCompiler.Cfg.T] | |
get [Wp.CfgCompiler.Cfg.P] | |
get [Wp.CfgCompiler.Cfg.C] | |
get [Wp.Sigs.Sigma] |
Lazily get the variable for a chunk.
|
get [Wp.Lang.F.Subst] | |
get [Wp.WpContext.Generator] | |
get [Wp.WpContext.Registry] | |
get [Wp.Context] |
Retrieves the current value of the context.
|
get [Wp.RefUsage] | |
get_addrof [Region] | |
get_alias [Region] | |
get_annots [WpStrategy] | |
get_array [Ctypes] | |
get_array [Wp.Ctypes] | |
get_array_dim [Ctypes] | |
get_array_dim [Wp.Ctypes] | |
get_array_size [Ctypes] | |
get_array_size [Wp.Ctypes] | |
get_asgn_goal [WpStrategy] | |
get_asgn_hyp [WpStrategy] | |
get_bhv [WpStrategy] | |
get_both_hyp_goals [WpStrategy] | |
get_builtin_type [Lang] | |
get_builtin_type [Wp.Lang] | |
get_call_asgn [WpStrategy] | |
get_call_hyp [WpStrategy] |
To be used as hypotheses around a call, (the pre are in
get_call_pre_goal )
|
get_call_out_edges [Cil2cfg] |
similar to
succ_e g v
but gives the edge to VcallOut first and the edge to Vexit second.
|
get_call_post [WpStrategy] |
Post-checks of a called function to be considered as goal only
|
get_call_pre [WpStrategy] |
Preconditions of a called function to be considered as hyp and goal
(similar to
get_both_hyp_goals ).
|
get_call_pre_strategies [WpAnnot] | |
get_call_type [Cil2cfg] | |
get_called_assigns [WpAnnot] |
Properties for assigns of kf
|
get_called_exit_conditions [WpAnnot] | |
get_called_post_conditions [WpAnnot] | |
get_called_preconditions_at [WpAnnot] | |
get_context [VC] | |
get_context [Wpo] | |
get_context [WpContext] | |
get_context [Wp.Wpo] | |
get_context [Wp.VC] | |
get_context [Wp.WpContext] | |
get_copies [Region] | |
get_cut [WpStrategy] |
the
bool in get_cut results says if the property has to be
considered as a both goal and hyp (goal=true , or hyp only (goal=false )
|
get_descr [Wpo.GOAL] | |
get_descr [WpContext] | |
get_descr [Wp.Wpo.GOAL] | |
get_descr [Wp.WpContext] | |
get_description [VC] | |
get_description [Wp.VC] | |
get_edge_labels [Cil2cfg] | |
get_edge_next_stmt [Cil2cfg] | |
get_edge_stmt [Cil2cfg] |
Complete get_edge_labels and returns the associated stmt, if any.
|
get_emitter [WpContext] | |
get_emitter [Wp.WpContext] | |
get_exit_edges [Cil2cfg] |
Find the edges
e that goes to the Vexit node inside the statement
beginning at node n
|
get_file_logerr [Wpo] |
only filename, might not exists
|
get_file_logerr [Wp.Wpo] |
only filename, might not exists
|
get_file_logout [Wpo] |
only filename, might not exists
|
get_file_logout [Wp.Wpo] |
only filename, might not exists
|
get_files [Wpo] | |
get_files [Wp.Wpo] | |
get_formula [VC] | |
get_formula [Wp.VC] | |
get_frame [LogicCompiler.Make] | |
get_frame [Sigs.LogicSemantics] |
Get the current frame, or raise a fatal error if none.
|
get_frame [Wp.LogicCompiler.Make] | |
get_frame [Wp.Sigs.LogicSemantics] |
Get the current frame, or raise a fatal error if none.
|
get_froms [Region] | |
get_function_name [Parameter_sig.String] |
returns the given argument only if it is a valid function name
(see
Parameter_customize.get_c_ified_functions for more information),
and abort otherwise.
|
get_function_strategies [WpAnnot] | |
get_gamma [Lang] | |
get_gamma [Wp.Lang] | |
get_gid [Wpo] |
Dynamically exported
|
get_gid [Wp.Wpo] |
Dynamically exported
|
get_goal_only [WpStrategy] | |
get_hits [ProverWhy3] | |
get_hyp_only [WpStrategy] | |
get_hypotheses [Lang] | |
get_hypotheses [Wp.Lang] | |
get_id [VC] | |
get_id [Wp.VC] | |
get_id_prop_strategies [WpAnnot] | |
get_index [Wpo] | |
get_index [Wp.Wpo] | |
get_induction [WpPropId] |
Quite don't understand what is going on here...
|
get_induction [Wp.WpPropId] | |
get_induction_labels [LogicUsage] |
Given an inductive
phi{...A...} .
|
get_induction_labels [Wp.LogicUsage] |
Given an inductive
phi{...A...} .
|
get_int [Tactical] | |
get_int [Ctypes] | |
get_int [Wp.Tactical] | |
get_int [Wp.Ctypes] | |
get_int64 [Ctypes] | |
get_int64 [Wp.Ctypes] | |
get_internal_edges [Cil2cfg] |
Find the edges
e of the statement node n postcondition
and the set of edges that are inside the statement (e excluded).
|
get_kf [WpStrategy] | |
get_kf [Wp_parameters] | |
get_kf [Wp.Wp_parameters] | |
get_label [Wpo] | |
get_label [Wp.Wpo] | |
get_legacy [WpPropId] |
Unique legacy identifier of
prop_id
|
get_legacy [Wp.WpPropId] |
Unique legacy identifier of
prop_id
|
get_logerr [VC] |
only file name, might not exists
|
get_logerr [Wp.VC] |
only file name, might not exists
|
get_logout [VC] |
only file name, might not exists
|
get_logout [Wp.VC] |
only file name, might not exists
|
get_merged [Region] | |
get_miss [ProverWhy3] | |
get_mode [ProverWhy3] | |
get_model [VC] | |
get_model [Wpo] | |
get_model [WpContext] | |
get_model [Wp.Wpo] | |
get_model [Wp.VC] | |
get_model [Wp.WpContext] | |
get_name [LogicUsage] | |
get_name [Wp.LogicUsage] | |
get_offset [Region] | |
get_opt [Context] |
Retrieves the current value of the context.
|
get_opt [Wp.Context] |
Retrieves the current value of the context.
|
get_option [LogicBuiltins] |
return the values of option (group, name),
return the empty list if not set
|
get_option [Wp.LogicBuiltins] |
return the values of option (group, name),
return the empty list if not set
|
get_output [Wp_parameters] | |
get_output [Wp.Wp_parameters] | |
get_output_dir [Wp_parameters] | |
get_output_dir [Wp.Wp_parameters] | |
get_overflows [Wp_parameters] | |
get_overflows [Wp.Wp_parameters] | |
get_plain_string [Parameter_sig.String] |
always return the argument, even if the argument is not a function name.
|
get_pointed [Region] | |
get_pool [Lang] | |
get_pool [Wp.Lang] | |
get_possible_values [Parameter_sig.String] |
What are the acceptable values for this parameter.
|
get_post_edges [Cil2cfg] |
Find the edges where the postconditions of the node statement have to be
checked.
|
get_post_label [Cil2cfg] |
Get the label to be used for the Post state of the node contract if any.
|
get_pre_edges [Cil2cfg] |
Find the edges where the precondition of the node statement have to be
checked.
|
get_proof [Wpo] | |
get_proof [Wp.Wpo] | |
get_property [VC] | |
get_property [Wpo] |
Dynamically exported
|
get_property [Wp.Wpo] |
Dynamically exported
|
get_property [Wp.VC] | |
get_propid [WpPropId] |
Unique identifier of
prop_id
|
get_propid [Wp.WpPropId] |
Unique identifier of
prop_id
|
get_prover_names [Register] | |
get_pstat [Register] | |
get_range [Parameter_sig.Int] |
What is the possible range of values for this parameter.
|
get_removed [ProverWhy3] | |
get_result [VC] | |
get_result [Wpo] | |
get_result [Wp.Wpo] | |
get_result [Wp.VC] | |
get_results [VC] | |
get_results [Wpo] | |
get_results [Wp.Wpo] | |
get_results [Wp.VC] | |
get_roots [Region] | |
get_scope [VC] | |
get_scope [Wpo] | |
get_scope [WpContext] | |
get_scope [Wp.Wpo] | |
get_scope [Wp.VC] | |
get_scope [Wp.WpContext] | |
get_sequent [VC] | |
get_sequent [Wp.VC] | |
get_session [Wp_parameters] | |
get_session [Wp.Wp_parameters] | |
get_session_dir [Wp_parameters] | |
get_session_dir [Wp.Wp_parameters] | |
get_stepout [VCS] |
0 means no-stepout
|
get_stepout [Wp.VCS] |
0 means no-stepout
|
get_steps [Wpo] | |
get_steps [Wp.Wpo] | |
get_strategies [ProofEngine] | |
get_switch_edges [Cil2cfg] |
similar to
succ_e g v
but give the switch cases and the default edge
|
get_target [Wpo] | |
get_target [Wp.Wpo] | |
get_test_edges [Cil2cfg] |
similar to
succ_e g v
but tests the branch to return (then-edge, else-edge)
|
get_time [Wpo] | |
get_time [Rformat] | get_time T t returns k such that T[k-1] <= t <= T[k] ,
T is extended with T[-1]=0 and T[N]=+oo .
|
get_time [Wp.Wpo] | |
get_timeout [VCS] |
0 means no-timeout
|
get_timeout [Wp.VCS] |
0 means no-timeout
|
get_wp [Wp_parameters] | |
get_wp [Wp.Wp_parameters] | |
global [Sigs.Model] |
Given a pointer value
p , assumes this pointer p (when valid)
is allocated outside the function frame under analysis.
|
global [Wp.Sigs.Model] |
Given a pointer value
p , assumes this pointer p (when valid)
is allocated outside the function frame under analysis.
|
global_axioms [WpStrategy] | |
goal [ProofEngine] | |
goals_nodes [StmtSemantics.Make] | |
goals_nodes [Wp.StmtSemantics.Make] | |
goals_of_property [Wpo] |
All POs related to a given property.
|
goals_of_property [Wp.Wpo] |
All POs related to a given property.
|
goto [ProofEngine] | |
goto [CfgCompiler.Cfg] |
Represents all execution traces
T such that, if T contains node a ,
T also contains node b and memory states at a and b are equal.
|
goto [Wp.CfgCompiler.Cfg] |
Represents all execution traces
T such that, if T contains node a ,
T also contains node b and memory states at a and b are equal.
|
group [Splitter] | |
group [Wp.Splitter] | |
guard [CfgCompiler.Cfg] |
Structurally corresponds to an assume control-flow.
|
guard [Wp.CfgCompiler.Cfg] |
Structurally corresponds to an assume control-flow.
|
guard' [CfgCompiler.Cfg] |
Same than guard but the condition is negated
|
guard' [Wp.CfgCompiler.Cfg] |
Same than guard but the condition is negated
|
guards [LogicCompiler.Make] | |
guards [Sigs.LogicSemantics] |
Returns the current gamma environment from the current frame.
|
guards [Wp.LogicCompiler.Make] | |
guards [Wp.Sigs.LogicSemantics] |
Returns the current gamma environment from the current frame.
|
H | |
hack [LogicBuiltins] |
Replace a logic definition or predicate by a built-in function.
|
hack [Wp.LogicBuiltins] |
Replace a logic definition or predicate by a built-in function.
|
hack_type [LogicBuiltins] |
Replace a logic type definition or predicate by a built-in type.
|
hack_type [Wp.LogicBuiltins] |
Replace a logic type definition or predicate by a built-in type.
|
handle [Warning] |
Handle the error and emit a warning with specified severity and effect
if a context has been set.
|
handle [Wp.Warning] |
Handle the error and emit a warning with specified severity and effect
if a context has been set.
|
has_copies [Region] | |
has_ctype [Cvalues] | |
has_deref [Region] | |
has_dkey [Wp_parameters] | |
has_dkey [Wp.Wp_parameters] | |
has_exit [Cil2cfg] |
whether an exit edge exists or not
|
has_gamma [Lang] | |
has_gamma [Wp.Lang] | |
has_init [Mcfg.S] | |
has_init [Wp.Mcfg.S] | |
has_layout [Region] | |
has_ltype [LogicCompiler.Make] | |
has_ltype [Wp.LogicCompiler.Make] | |
has_names [Region] | |
has_offset [Region] | |
has_out [Wp_parameters] | |
has_out [Wp.Wp_parameters] | |
has_pointed [Region] | |
has_print_generated [Wp_parameters] |
Debugging Categories
|
has_print_generated [Wp.Wp_parameters] |
Debugging Categories
|
has_proof [ProofScript] |
Has a tactical alternative
|
has_return [Region] | |
has_roots [Region] | |
has_session [Wp_parameters] | |
has_session [Wp.Wp_parameters] | |
has_shortcut [Why3Provers] | |
has_verdict [Wpo] | |
has_verdict [Wp.Wpo] | |
hash [Sigs.Chunk] | |
hash [Lang.F] |
Constant time
|
hash [WpContext.SCOPE] | |
hash [WpContext.MODEL] | |
hash [WpContext.S] | |
hash [Ctypes.AinfoComparable] | |
hash [Ctypes] | |
hash [Wp.Sigs.Chunk] | |
hash [Wp.Lang.F] |
Constant time
|
hash [Wp.WpContext.SCOPE] | |
hash [Wp.WpContext.MODEL] | |
hash [Wp.WpContext.S] | |
hash [Wp.Ctypes.AinfoComparable] | |
hash [Wp.Ctypes] | |
have [Conditions] |
Predicate for Have and such, True for any other
|
have [Wp.Conditions] |
Predicate for Have and such, True for any other
|
havoc [Auto] | |
havoc [CfgCompiler.Cfg] |
Inserts an assigns effect between nodes
a and b , correspondings
to all the written memory chunks accessible in execution paths delimited
by the effects sequence of nodes.
|
havoc [MemLoader.Model] | |
havoc [MemLoader.Make] | |
havoc [Sigs.Sigma] |
All the chunks in the provided footprint are generated and made fresh.
|
havoc [Wp.Auto] | |
havoc [Wp.CfgCompiler.Cfg] |
Inserts an assigns effect between nodes
a and b , correspondings
to all the written memory chunks accessible in execution paths delimited
by the effects sequence of nodes.
|
havoc [Wp.Sigs.Sigma] |
All the chunks in the provided footprint are generated and made fresh.
|
havoc_any [Sigs.Sigma] |
All the chunks are made fresh.
|
havoc_any [Wp.Sigs.Sigma] |
All the chunks are made fresh.
|
havoc_chunk [Sigs.Sigma] |
Generate a new fresh variable for the given chunk.
|
havoc_chunk [Wp.Sigs.Sigma] |
Generate a new fresh variable for the given chunk.
|
havoc_length [MemLoader.Make] | |
head [ProofEngine] | |
head [Tactical] | |
head [Footprint] |
Head only footprint
|
head [Conditions] |
Predicate for Have and such, Condition for Branch, True for Either
|
head [Wp.Tactical] | |
head [Wp.Conditions] |
Predicate for Have and such, Condition for Branch, True for Either
|
here [Clabels] | |
here [Wp.Clabels] | |
hints_for [Proof] | |
hypotheses [MemVar.VarUsage] | |
hypotheses [Sigs.Model] |
Computes the memory model hypotheses including separation and validity
clauses to be verified for this model.
|
hypotheses [Lang] | |
hypotheses [Wp.MemVar.VarUsage] | |
hypotheses [Wp.Sigs.Model] |
Computes the memory model hypotheses including separation and validity
clauses to be verified for this model.
|
hypotheses [Wp.Lang] | |
I | |
i_bits [Ctypes] |
size in bits
|
i_bits [Wp.Ctypes] |
size in bits
|
i_bytes [Ctypes] |
size in bytes
|
i_bytes [Wp.Ctypes] |
size in bytes
|
i_convert [Ctypes] | |
i_convert [Wp.Ctypes] | |
i_iter [Ctypes] | |
i_iter [Wp.Ctypes] | |
i_memo [Ctypes] |
memoized, not-projectified
|
i_memo [Wp.Ctypes] |
memoized, not-projectified
|
iadd [Cint] | |
iadd [Wp.Cint] | |
id [LogicBuiltins] | |
id [Matrix] |
unique w.r.t
equal
|
id [Region] | |
id [WpContext.Registry] | |
id [WpContext.SCOPE] | |
id [WpContext.MODEL] | |
id [WpContext.S] | |
id [Wp.LogicBuiltins] | |
id [Wp.WpContext.Registry] | |
id [Wp.WpContext.SCOPE] | |
id [Wp.WpContext.MODEL] | |
id [Wp.WpContext.S] | |
ident [Factory] | |
ident [Tactical] | |
ident [Script] | |
ident [Wp.Tactical] | |
ident [Wp.Factory] | |
idents [Script] | |
idiv [Cint] | |
idiv [Wp.Cint] | |
if_else [Splitter] | |
if_else [Wp.Splitter] | |
if_then [Splitter] | |
if_then [Wp.Splitter] | |
imod [Cint] | |
imod [Wp.Cint] | |
implies [CfgCompiler.Cfg] |
implies is the dual of either.
|
implies [Wp.CfgCompiler.Cfg] |
implies is the dual of either.
|
imul [Cint] | |
imul [Wp.Cint] | |
in_frame [LogicCompiler.Make] | |
in_frame [Sigs.LogicSemantics] |
Execute the given closure with the specified current frame.
|
in_frame [Wp.LogicCompiler.Make] | |
in_frame [Wp.Sigs.LogicSemantics] |
Execute the given closure with the specified current frame.
|
in_range [Vset] | |
in_range [Wp.Vset] | |
in_size [Vset] | |
in_size [Wp.Vset] | |
in_state [Lang.For_export] | |
in_state [Wp.Lang.For_export] | |
included [MemMemory] | |
included [Sigs.Model] |
Return the formula that tests if two segment are included
|
included [Cvalues.Logic] | |
included [Layout.Range] | |
included [Wp.Sigs.Model] |
Return the formula that tests if two segment are included
|
incr [Parameter_sig.Int] |
Increment the integer.
|
index [ProverSearch] | |
index [Conditions] |
Compute steps' id of sequent left hand-side.
|
index [Mstate] | |
index [Layout.Offset] | |
index [Wp.Conditions] |
Compute steps' id of sequent left hand-side.
|
index [Wp.Mstate] | |
indexed [Layout.Root] | |
infoprover [Lang] |
same information for all the provers
|
infoprover [Wp.Lang] |
same information for all the provers
|
init [StmtSemantics.Make] |
connect init to here.
|
init [CfgCompiler.Cfg.T] | |
init [Sigs.CodeSemantics] |
Express that some variable has some initial value at the
given memory state.
|
init [Mcfg.S] | |
init [Clabels] | |
init [Wp.StmtSemantics.Make] | |
init [Wp.CfgCompiler.Cfg.T] | |
init [Wp.Sigs.CodeSemantics] |
Express that some variable has some initial value at the
given memory state.
|
init [Wp.Mcfg.S] | |
init [Wp.Clabels] | |
init' [CfgCompiler.Cfg.T] | |
init' [Wp.CfgCompiler.Cfg.T] | |
insert [Tactical] | |
insert [Conditions] |
Insert a step in the sequent immediately
at the specified position.
|
insert [Wp.Tactical] | |
insert [Wp.Conditions] |
Insert a step in the sequent immediately
at the specified position.
|
instance [Factory] | |
instance [Auto] | |
instance [Wp.Auto] | |
instance [Wp.Factory] | |
instance_goal [TacInstance] | |
instance_have [TacInstance] | |
instance_of [Sigs.CodeSemantics] |
Check whether a function pointer is (an instance of)
some kernel function.
|
instance_of [Wp.Sigs.CodeSemantics] |
Check whether a function pointer is (an instance of)
some kernel function.
|
instr [StmtSemantics.Make] | |
instr [Wp.StmtSemantics.Make] | |
int [Tactical] | |
int [Wp.Tactical] | |
int_of_bool [Cmath] | |
int_of_loc [Sigs.Model] |
Cast a memory location into its absolute memory address,
given as an integer with the given C-type.
|
int_of_loc [Wp.Sigs.Model] |
Cast a memory location into its absolute memory address,
given as an integer with the given C-type.
|
int_of_real [Cmath] | |
inter [Cvalues.Logic] | |
inter [Vset] | |
inter [Wp.Vset] | |
inter [Set.S] |
Set intersection.
|
intersect [Conditions] |
Variables of predicate and the bundle intersects
|
intersect [Lang.F] | |
intersect [Wp.Conditions] |
Variables of predicate and the bundle intersects
|
intersect [Wp.Lang.F] | |
intersectp [Lang.F] | |
intersectp [Wp.Lang.F] | |
introduction [Conditions] |
Performs existential, universal and hypotheses introductions
|
introduction [Wp.Conditions] |
Performs existential, universal and hypotheses introductions
|
introduction_eq [Conditions] |
Same as
introduction but returns the same sequent is None
|
introduction_eq [Wp.Conditions] |
Same as
introduction but returns the same sequent is None
|
intros [Conditions] |
Assumes a list of predicates in a
Have section on top of the bundle.
|
intros [Wp.Conditions] |
Assumes a list of predicates in a
Have section on top of the bundle.
|
intuition [Auto] | |
intuition [Wp.Auto] | |
invalid [VCS] | |
invalid [Sigs.Model] |
Returns the formula that tests if the entire memory is invalid
for write access.
|
invalid [Cvalues.Logic] | |
invalid [Wp.VCS] | |
invalid [Wp.Sigs.Model] |
Returns the formula that tests if the entire memory is invalid
for write access.
|
iopp [Cint] | |
iopp [Wp.Cint] | |
ip_lemma [LogicUsage] | |
ip_lemma [Wp.LogicUsage] | |
isGlobalInitConst [WpStrategy] |
True if the variable is global, not extern, with a
"const" qualifier type.
|
isInitConst [WpStrategy] |
True if both options
-const-readonly and -wp-init are positioned,
and the variable is global, not extern, with a "const" type
(see hasConstAttribute ).
|
is_absorbant [Lang.F] | |
is_absorbant [Wp.Lang.F] | |
is_aliased [Region] | |
is_aliased [Layout.Usage] | |
is_aliased [Layout.Alias] | |
is_arith [Lang.F] |
Integer or Real sort
|
is_arith [Wp.Lang.F] |
Integer or Real sort
|
is_array [Ctypes] | |
is_array [Wp.Ctypes] | |
is_assigns [WpPropId] | |
is_assigns [Wp.WpPropId] | |
is_atomic [Lang.F] |
Constants and variables
|
is_atomic [Wp.Lang.F] |
Constants and variables
|
is_auto [VCS] | |
is_auto [Wp.VCS] | |
is_available [Why3Provers] | |
is_back_edge [Cil2cfg] | |
is_builtin [Lang] | |
is_builtin [Wp.Lang] | |
is_builtin_type [Lang] | |
is_builtin_type [Wp.Lang] | |
is_call_assigns [WpPropId] | |
is_call_assigns [Wp.WpPropId] | |
is_char [Ctypes] | |
is_char [Wp.Ctypes] | |
is_check [WpPropId] | |
is_check [Wp.WpPropId] | |
is_cint [Cint] |
Raises
Not_found if not.
|
is_cint [Wp.Cint] |
Raises
Not_found if not.
|
is_cint_simplifier [Cint] |
Remove the
is_cint in formulas that are
redundant with other conditions.
|
is_cint_simplifier [Wp.Cint] |
Remove the
is_cint in formulas that are
redundant with other conditions.
|
is_closed [Lang.F] |
No bound variables
|
is_closed [Wp.Lang.F] |
No bound variables
|
is_cnf [WpTac] | |
is_comp [Ctypes] | |
is_comp [Wp.Ctypes] | |
is_composed [WpAnnot] |
whether a proof needs several lemma to be complete
|
is_compound [Ctypes] | |
is_compound [Wp.Ctypes] | |
is_computing [VCS] | |
is_computing [Wp.VCS] | |
is_dead_annot [WpReached] |
False assertions and loop invariant.
|
is_dead_code [WpReached] |
Checks whether the stmt has a dead-code annotation.
|
is_default [LogicBuiltins] | |
is_default [Wp.LogicBuiltins] | |
is_default_behavior [WpStrategy] | |
is_defined [WpContext] | |
is_defined [Wp.WpContext] | |
is_dnf [WpTac] | |
is_empty [Tactical] | |
is_empty [Conditions] |
No step at all
|
is_empty [Vset] | |
is_empty [Passive] | |
is_empty [Region] | |
is_empty [Layout.Cluster] | |
is_empty [Wp.Tactical] | |
is_empty [Wp.Conditions] |
No step at all
|
is_empty [Wp.Vset] | |
is_empty [Wp.Passive] | |
is_empty [Set.S] |
Test whether a set is empty or not.
|
is_empty [Map.S] |
Test whether a map is empty or not.
|
is_empty_script [Proof] |
Check a proof script text for emptyness
|
is_equal [Lang.F] | |
is_equal [Wp.Lang.F] | |
is_exp_range [Sigs.CodeSemantics] |
Express that all objects in a range of locations have a given value.
|
is_exp_range [Wp.Sigs.CodeSemantics] |
Express that all objects in a range of locations have a given value.
|
is_false [Cvalues] | p ? 0 : 1
|
is_false [Lang.F] |
Constant time.
|
is_false [Wp.Lang.F] |
Constant time.
|
is_framed [Sigs.Chunk] |
Whether the chunk is local to a function call.
|
is_framed [Wp.Sigs.Chunk] |
Whether the chunk is local to a function call.
|
is_garbled [Region] | |
is_garbled [Layout.Cluster] | |
is_here [Clabels] | |
is_here [Wp.Clabels] | |
is_int [Lang.F] |
Integer sort
|
is_int [Wp.Lang.F] |
Integer sort
|
is_invalid [WpAnnot] |
whether an invalid proof result has been registered or not
|
is_literal [Lang] | |
is_literal [Wp.Lang] | |
is_loop_preservation [WpPropId] | |
is_loop_preservation [Wp.WpPropId] | |
is_main_init [WpStrategy] |
The function is the main entry point AND it is not a lib entry
|
is_neutral [Lang.F] | |
is_neutral [Wp.Lang.F] | |
is_null [Sigs.Model] |
Return the formula that check if a given location is null
|
is_null [Cvalues] | |
is_null [Wp.Sigs.Model] |
Return the formula that check if a given location is null
|
is_object [Cvalues] | |
is_pfalse [Lang.F] | |
is_pfalse [Wp.Lang.F] | |
is_pointer [Ctypes] | |
is_pointer [Wp.Ctypes] | |
is_positive_or_null [Cint] | |
is_positive_or_null [Wp.Cint] | |
is_predicate [WpReached] |
If returns
true the predicate has always the given boolean value.
|
is_primitive [Lang.F] |
Constants only
|
is_primitive [Wp.Lang.F] |
Constants only
|
is_prop [Lang.F] |
Boolean or Property
|
is_prop [Wp.Lang.F] |
Boolean or Property
|
is_proved [VC] | |
is_proved [Wpo] |
do not tries simplification, check prover results
|
is_proved [VCS] | |
is_proved [WpAnnot] |
whether all partial proofs have been accumulated or not
|
is_proved [Wp.Wpo] |
do not tries simplification, check prover results
|
is_proved [Wp.VC] | |
is_proved [Wp.VCS] | |
is_prover [ProofScript] | |
is_ptrue [Lang.F] | |
is_ptrue [Wp.Lang.F] | |
is_read [Region] | |
is_real [Lang.F] |
Real sort
|
is_real [Wp.Lang.F] |
Real sort
|
is_recursive [LogicUsage] | |
is_recursive [Wp.LogicUsage] | |
is_requires [WpPropId] | |
is_requires [Wp.WpPropId] | |
is_shifted [Region] | |
is_shifted [Layout.Usage] | |
is_simple [Lang.F] |
Constants, variables, functions of arity 0
|
is_simple [Wp.Lang.F] |
Constants, variables, functions of arity 0
|
is_smoke_test [Wpo] | |
is_smoke_test [WpPropId] | |
is_smoke_test [Wp.Wpo] | |
is_smoke_test [Wp.WpPropId] | |
is_subterm [Lang.F] | |
is_subterm [Wp.Lang.F] | |
is_tactic [ProofScript] | |
is_tactic [Wpo] | |
is_tactic [WpPropId] | |
is_tactic [Wp.Wpo] | |
is_tactic [Wp.WpPropId] | |
is_trivial [VC] | |
is_trivial [Wpo.VC_Annot] | |
is_trivial [Wpo.VC_Lemma] | |
is_trivial [Wpo.GOAL] | |
is_trivial [Wpo] |
do not tries simplification, do not check prover results
|
is_trivial [Conditions] |
Goal is true or hypotheses contains false.
|
is_trivial [Wp.Wpo.VC_Annot] | |
is_trivial [Wp.Wpo.VC_Lemma] | |
is_trivial [Wp.Wpo.GOAL] | |
is_trivial [Wp.Wpo] |
do not tries simplification, do not check prover results
|
is_trivial [Wp.VC] | |
is_trivial [Wp.Conditions] |
Goal is true or hypotheses contains false.
|
is_true [Conditions] |
Contains only true or empty steps
|
is_true [Cvalues] | p ? 1 : 0
|
is_true [Lang.F] |
Constant time.
|
is_true [Wp.Conditions] |
Contains only true or empty steps
|
is_true [Wp.Lang.F] |
Constant time.
|
is_unknown [Wpo] | |
is_unknown [Wp.Wpo] | |
is_valid [Wpo] | true if the result is valid.
|
is_valid [VCS] | |
is_valid [Wp.Wpo] | true if the result is valid.
|
is_valid [Wp.VCS] | |
is_verdict [VCS] | |
is_verdict [Wp.VCS] | |
is_well_formed [Sigs.Model] |
Provides the constraint corresponding to the kind of data stored by all
chunks in sigma.
|
is_well_formed [Wp.Sigs.Model] |
Provides the constraint corresponding to the kind of data stored by all
chunks in sigma.
|
is_written [Region] | |
is_zero [Sigs.CodeSemantics] |
Express that the object (of specified type) at the given location
is filled with zeroes.
|
is_zero [Lang.F] | |
is_zero [Wp.Sigs.CodeSemantics] |
Express that the object (of specified type) at the given location
is filled with zeroes.
|
is_zero [Wp.Lang.F] | |
isub [Cint] | |
isub [Wp.Cint] | |
iter [ProofEngine] | |
iter [Strategy] | |
iter [Tactical] | |
iter [Footprint] |
Width-first full iterator.
|
iter [Wpo] | |
iter [Pcfg] | |
iter [Conditions] |
Iterate only over the head steps of the sequence.
|
iter [Mstate] | |
iter [Sigs.Model] |
Debug
|
iter [Sigs.Sigma] |
Iterates over the chunks and associated variables already
accessed so far in the environment.
|
iter [Letify.Sigma] | |
iter [Definitions] | |
iter [Splitter] | |
iter [Passive] | |
iter [Region] | |
iter [RefUsage] | |
iter [WpContext.Registry] | |
iter [Wp.Wpo] | |
iter [Wp.Strategy] | |
iter [Wp.Tactical] | |
iter [Hashtbl.S] | |
iter [Wp.Pcfg] | |
iter [Wp.Conditions] |
Iterate only over the head steps of the sequence.
|
iter [Wp.Mstate] | |
iter [Wp.Sigs.Model] |
Debug
|
iter [Wp.Sigs.Sigma] |
Iterates over the chunks and associated variables already
accessed so far in the environment.
|
iter [Wp.Definitions] | |
iter [Wp.Splitter] | |
iter [Wp.Passive] | |
iter [Wp.WpContext.Registry] | |
iter [Wp.RefUsage] | |
iter [Set.S] | iter f s applies f in turn to all elements of s .
|
iter [Map.S] | iter f m applies f to all bindings in map m .
|
iter2 [Sigs.Sigma] |
Same as
iter for both environments.
|
iter2 [Wp.Sigs.Sigma] |
Same as
iter for both environments.
|
iter_composer [Tactical] | |
iter_composer [Wp.Tactical] | |
iter_consequence_literals [Lang] | iter_consequence_literals assume_from_litteral hypothesis applies
the function assume_from_litteral on literals that are a consequence of the hypothesis
(i.e.
|
iter_consequence_literals [Wp.Lang] | iter_consequence_literals assume_from_litteral hypothesis applies
the function assume_from_litteral on literals that are a consequence of the hypothesis
(i.e.
|
iter_copies [Region] | |
iter_deref [Region] | |
iter_edges [Cil2cfg] | |
iter_fct [Wp_parameters] | |
iter_fct [Wp.Wp_parameters] | |
iter_fusion [Region] | |
iter_ip [VC] | |
iter_ip [Wp.VC] | |
iter_kf [VC] | |
iter_kf [Wp_parameters] | |
iter_kf [Wp.VC] | |
iter_kf [Wp.Wp_parameters] | |
iter_lemmas [LogicUsage] | |
iter_lemmas [Wp.LogicUsage] | |
iter_names [Region] | |
iter_nodes [Cil2cfg] | |
iter_offset [Region] | |
iter_on_goals [Wpo] |
Dynamically exported.
|
iter_on_goals [Wp.Wpo] |
Dynamically exported.
|
iter_read [Region] | |
iter_session [Register] | |
iter_shift [Region] | |
iter_sorted [WpContext.Registry] | |
iter_sorted [Wp.WpContext.Registry] | |
iter_strings [Region] | |
iter_vars [Region] | |
iter_wp [Wp_parameters] | |
iter_wp [Wp.Wp_parameters] | |
iter_write [Region] | |
J | |
join [Sigs.Sigma] |
Make two environment pairwise equal via the passive form.
|
join [Passive] | |
join [Wp.Sigs.Sigma] |
Make two environment pairwise equal via the passive form.
|
join [Wp.Passive] | |
json_of_param [ProofScript] | |
json_of_parameters [ProofScript] | |
json_of_result [ProofScript] | |
json_of_selection [ProofScript] | |
json_of_tactic [ProofScript] | |
jtactic [ProofScript] | |
K | |
key [Script] | |
kf_context [Wpo] | |
kf_context [Wp.Wpo] | |
kfailed [VCS] | |
kfailed [Wp.VCS] | |
kind_of_id [WpPropId] |
get the 'kind' information.
|
kind_of_id [Wp.WpPropId] |
get the 'kind' information.
|
kind_of_tau [LogicBuiltins] | |
kind_of_tau [Wp.LogicBuiltins] | |
ko_status [GuiProver] | |
L | |
l_and [Cint] | |
l_and [Wp.Cint] | |
l_lsl [Cint] | |
l_lsl [Wp.Cint] | |
l_lsr [Cint] | |
l_lsr [Wp.Cint] | |
l_not [Cint] | |
l_not [Wp.Cint] | |
l_or [Cint] | |
l_or [Wp.Cint] | |
l_xor [Cint] | |
l_xor [Wp.Cint] | |
label [Mcfg.S] | |
label [Wp.Mcfg.S] | |
label_of_prop_id [WpPropId] |
Short description of the kind of PO
|
label_of_prop_id [Wp.WpPropId] |
Short description of the kind of PO
|
labels_assert_after [NormAtLabels] | |
labels_assert_after [Wp.NormAtLabels] | |
labels_assert_before [NormAtLabels] | |
labels_assert_before [Wp.NormAtLabels] | |
labels_axiom [NormAtLabels] | |
labels_axiom [Wp.NormAtLabels] | |
labels_empty [NormAtLabels] | |
labels_empty [Wp.NormAtLabels] | |
labels_fct_assigns [NormAtLabels] | |
labels_fct_assigns [Wp.NormAtLabels] | |
labels_fct_post [NormAtLabels] | |
labels_fct_post [Wp.NormAtLabels] | |
labels_fct_pre [NormAtLabels] | |
labels_fct_pre [Wp.NormAtLabels] | |
labels_loop [NormAtLabels] | |
labels_loop [Wp.NormAtLabels] | |
labels_predicate [NormAtLabels] | |
labels_predicate [Wp.NormAtLabels] | |
labels_stmt_assigns [NormAtLabels] | |
labels_stmt_assigns [Wp.NormAtLabels] | |
labels_stmt_post [NormAtLabels] | |
labels_stmt_post [Wp.NormAtLabels] | |
labels_stmt_pre [NormAtLabels] | |
labels_stmt_pre [Wp.NormAtLabels] | |
last [MemLoader.Model] | |
launch [Register] | |
lc_closed [Lang.F] | |
lc_closed [Wp.Lang.F] | |
lc_iter [Lang.F] | |
lc_iter [Wp.Lang.F] | |
ldomain [Cvalues] | |
lemma [Auto] | |
lemma [LogicCompiler.Make] | |
lemma [Conditions] |
Performs existential, universal and hypotheses introductions
|
lemma [Sigs.LogicSemantics] |
Compile a lemma definition.
|
lemma [Wp.Auto] | |
lemma [Wp.LogicCompiler.Make] | |
lemma [Wp.Conditions] |
Performs existential, universal and hypotheses introductions
|
lemma [Wp.Sigs.LogicSemantics] |
Compile a lemma definition.
|
lemma_id [Lang] | |
lemma_id [Wp.Lang] | |
length [Splitter] | |
length [Hashtbl.S] | |
length [Wp.Splitter] | |
lfun [Repr] | |
lfun [Wp.Repr] | |
lift [Vset] | |
lift [Lang.F] | |
lift [Wp.Vset] | |
lift [Wp.Lang.F] | |
lift_add [Vset] | |
lift_add [Wp.Vset] | |
lift_sub [Vset] | |
lift_sub [Wp.Vset] | |
list [Conditions] |
Same domain than
iter .
|
list [Wp.Conditions] |
Same domain than
iter .
|
literal [Sigs.Model] |
Return the memory location of a constant string,
the id is a unique identifier.
|
literal [Wp.Sigs.Model] |
Return the memory location of a constant string,
the id is a unique identifier.
|
load [ProofSession] | |
load [MemLoader.Make] | |
load [Sigs.Model] |
Return the value of the object of the given type at the given location in
the given memory state.
|
load [Cvalues.Logic] | |
load [Wp.Sigs.Model] |
Return the value of the object of the given type at the given location in
the given memory state.
|
load_driver [Driver] |
Memoized loading of drivers according to current
WP options.
|
load_driver [Wp.Driver] |
Memoized loading of drivers according to current
WP options.
|
load_float [MemLoader.Model] | |
load_int [MemLoader.Model] | |
load_pointer [MemLoader.Model] | |
loadvalue [MemLoader.Make] | |
loc [Cvalues.Logic] | |
loc [Splitter] | |
loc [Wp.Splitter] | |
loc_diff [Sigs.Model] |
Compute the length in bytes between two memory locations
|
loc_diff [Wp.Sigs.Model] |
Compute the length in bytes between two memory locations
|
loc_eq [Sigs.Model] | |
loc_eq [Wp.Sigs.Model] | |
loc_leq [Sigs.Model] |
Memory location comparisons
|
loc_leq [Wp.Sigs.Model] |
Memory location comparisons
|
loc_lt [Sigs.Model] | |
loc_lt [Wp.Sigs.Model] | |
loc_neq [Sigs.Model] | |
loc_neq [Wp.Sigs.Model] | |
loc_of_exp [Sigs.CodeSemantics] |
Compile an expression as a location.
|
loc_of_exp [Wp.Sigs.CodeSemantics] |
Compile an expression as a location.
|
loc_of_int [Sigs.Model] |
Cast a term representing an absolute memory address (to some c_object)
given as an integer, into an abstract memory location.
|
loc_of_int [Wp.Sigs.Model] |
Cast a term representing an absolute memory address (to some c_object)
given as an integer, into an abstract memory location.
|
loc_of_term [Sigs.LogicSemantics] |
Same as
term above but expects a single loc or a single
pointer value.
|
loc_of_term [Wp.Sigs.LogicSemantics] |
Same as
term above but expects a single loc or a single
pointer value.
|
local [LogicCompiler.Make] | |
local [Sigs.LogicSemantics] |
Make a local frame reusing the current pool and gamma.
|
local [Lang] | |
local [Wp.LogicCompiler.Make] | |
local [Wp.Sigs.LogicSemantics] |
Make a local frame reusing the current pool and gamma.
|
local [Wp.Lang] | |
locate [Footprint] |
Locate the occurrence of
select footprint inside a term.
|
location [ProverTask] | |
location [Wp.ProverTask] | |
logic [LogicCompiler.Make] | |
logic [LogicBuiltins] | |
logic [Wp.LogicCompiler.Make] | |
logic [Wp.LogicBuiltins] | |
logic_constant [Cvalues] | |
logic_id [Lang] | |
logic_id [Wp.Lang] | |
logic_info [LogicCompiler.Make] | |
logic_info [Wp.LogicCompiler.Make] | |
logic_lemma [LogicUsage] | |
logic_lemma [Wp.LogicUsage] | |
logic_var [LogicCompiler.Make] | |
logic_var [Wp.LogicCompiler.Make] | |
lookup [Strategy] | |
lookup [Tactical] | |
lookup [Footprint] |
Retrieve back the
k -th occurrence of a footprint inside a term.
|
lookup [Mstate] | |
lookup [Sigs.Model] |
Try to interpret a term as an in-memory operation
located at this program point.
|
lookup [LogicBuiltins] | |
lookup [Clabels] | lookup bindings lparam retrieves the actual label
for the label in bindings for label parameter lparam .
|
lookup [Wp.Strategy] | |
lookup [Wp.Tactical] | |
lookup [Wp.Mstate] | |
lookup [Wp.Sigs.Model] |
Try to interpret a term as an in-memory operation
located at this program point.
|
lookup [Wp.LogicBuiltins] | |
lookup [Wp.Clabels] | lookup bindings lparam retrieves the actual label
for the label in bindings for label parameter lparam .
|
loop_current [Clabels] | |
loop_current [Wp.Clabels] | |
loop_entry [Mcfg.S] | |
loop_entry [Clabels] | |
loop_entry [Wp.Mcfg.S] | |
loop_entry [Wp.Clabels] | |
loop_step [Mcfg.S] | |
loop_step [Wp.Mcfg.S] | |
loopcurrent [Clabels] | |
loopcurrent [Wp.Clabels] | |
loopentry [Clabels] | |
loopentry [Wp.Clabels] | |
lval [Sigs.LogicSemantics] |
Compile a term l-value into a (typed) abstract location
|
lval [Sigs.CodeSemantics] |
Evaluate the left-value on the given memory state.
|
lval [Wp.Sigs.LogicSemantics] |
Compile a term l-value into a (typed) abstract location
|
lval [Wp.Sigs.CodeSemantics] |
Evaluate the left-value on the given memory state.
|
M | |
main [Register] | |
main [ProofEngine] | |
make [GuiNavigator] | |
make [Strategy] | |
make [Wpo.GOAL] | |
make [Wp.Wpo.GOAL] | |
make [Wp.Strategy] | |
make_output_dir [Wp_parameters] | |
make_output_dir [Wp.Wp_parameters] | |
make_type [Datatype.Hashtbl] | |
map [Cvalues.Logic] | |
map [Vset] | |
map [Splitter] | |
map [Wp.Vset] | |
map [Wp.Splitter] | |
map [Set.S] | map f s is the set whose elements are f a0 ,f a1 ...
|
map [Map.S] | map f m returns a map with same domain as m , where the
associated value a of all bindings of m has been
replaced by the result of the application of f to a .
|
map_condition [Conditions] |
Rewrite all root predicates in condition
|
map_condition [Wp.Conditions] |
Rewrite all root predicates in condition
|
map_l2t [Cvalues.Logic] | |
map_loc [Cvalues.Logic] | |
map_logic [Cvalues] | |
map_opp [Cvalues.Logic] | |
map_opp [Vset] | |
map_opp [Wp.Vset] | |
map_sequence [Conditions] |
Rewrite all root predicates in sequence
|
map_sequence [Wp.Conditions] |
Rewrite all root predicates in sequence
|
map_sequent [Conditions] |
Rewrite all root predocates in hypotheses and goal
|
map_sequent [Wp.Conditions] |
Rewrite all root predocates in hypotheses and goal
|
map_sloc [Cvalues] | |
map_step [Conditions] |
Rewrite all root predicates in step
|
map_step [Wp.Conditions] |
Rewrite all root predicates in step
|
map_t2l [Cvalues.Logic] | |
map_value [Cvalues] | |
mapi [Tactical] | |
mapi [Wp.Tactical] | |
mapi [Map.S] |
Same as
Map.S.map , but the function receives as arguments both the
key and the associated value for each binding of the map.
|
mark_e [Lang.F] | |
mark_e [Wp.Lang.F] | |
mark_p [Lang.F] |
Returns a list of terms to be shared among all shared or marked subterms.
|
mark_p [Wp.Lang.F] |
Returns a list of terms to be shared among all shared or marked subterms.
|
marker [Lang.F] | |
marker [Wp.Lang.F] | |
mask_simplifier [Cint] | |
mask_simplifier [Wp.Cint] | |
matches [Footprint] |
Head match
|
matrix [Definitions] | |
matrix [Wp.Definitions] | |
max_binding [Map.S] |
Same as
Map.S.min_binding , but returns the largest binding
of the given map.
|
max_binding_opt [Map.S] |
Same as
Map.S.min_binding_opt , but returns the largest binding
of the given map.
|
max_elt [Set.S] |
Same as
Set.S.min_elt , but returns the largest element of the
given set.
|
max_elt_opt [Set.S] |
Same as
Set.S.min_elt_opt , but returns the largest element of the
given set.
|
mem [Sigs.Sigma] |
Whether a chunk has been assigned.
|
mem [Layout.Chunk] | |
mem [WpContext.Generator] | |
mem [WpContext.Registry] | |
mem [Clabels] | |
mem [Wprop.Indexed2] | |
mem [Wprop.Indexed] | |
mem [Hashtbl.S] | |
mem [Wp.Sigs.Sigma] |
Whether a chunk has been assigned.
|
mem [Wp.WpContext.Generator] | |
mem [Wp.WpContext.Registry] | |
mem [Set.S] | mem x s tests whether x belongs to the set s .
|
mem [Map.S] | mem x m returns true if m contains a binding for x ,
and false otherwise.
|
mem [Wp.Clabels] | |
mem [Parameter_sig.Set] |
Does the given element belong to the set?
|
mem_at [LogicCompiler.Make] | |
mem_at [Sigs.LogicSemantics] |
Returns the memory state at the requested label.
|
mem_at [Wp.LogicCompiler.Make] | |
mem_at [Wp.Sigs.LogicSemantics] |
Returns the memory state at the requested label.
|
mem_at_frame [LogicCompiler.Make] | |
mem_at_frame [Sigs.LogicSemantics] |
Get the memory environment at the given label.
|
mem_at_frame [Wp.LogicCompiler.Make] | |
mem_at_frame [Wp.Sigs.LogicSemantics] |
Get the memory environment at the given label.
|
mem_builtin_type [Lang] | |
mem_builtin_type [Wp.Lang] | |
mem_frame [LogicCompiler.Make] | |
mem_frame [Sigs.LogicSemantics] |
Same as
mem_at_frame but for the current frame.
|
mem_frame [Wp.LogicCompiler.Make] | |
mem_frame [Wp.Sigs.LogicSemantics] |
Same as
mem_at_frame but for the current frame.
|
member [Vset] | |
member [Wp.Vset] | |
memoize [WpContext.Registry] |
with circularity protection
|
memoize [Wp.WpContext.Registry] |
with circularity protection
|
merge [VCS] | |
merge [Conditions] |
Performs a diff-based disjunction, introducing If-Then-Else or Either
branches when possible.
|
merge [Sigs.Sigma] |
Make the union of each sigma, choosing a new variable for
each conflict, and returns the corresponding joins.
|
merge [Letify.Defs] | |
merge [Splitter] | |
merge [Matrix] | |
merge [Mcfg.S] | |
merge [Layout.Pack] | |
merge [Layout.Flat] | |
merge [Layout.RW] | |
merge [Layout.Root] | |
merge [Layout.Cluster] | |
merge [Layout.Overlay] | |
merge [Layout.Matrix] | |
merge [Layout.Value] | |
merge [Layout.Usage] | |
merge [Layout.Alias] | |
merge [Wp.VCS] | |
merge [Wp.Conditions] |
Performs a diff-based disjunction, introducing If-Then-Else or Either
branches when possible.
|
merge [Wp.Sigs.Sigma] |
Make the union of each sigma, choosing a new variable for
each conflict, and returns the corresponding joins.
|
merge [Wp.Splitter] | |
merge [Wp.Mcfg.S] | |
merge [Map.S] | merge f m1 m2 computes a map whose keys is a subset of keys of m1
and of m2 .
|
merge_all [Splitter] | |
merge_all [Wp.Splitter] | |
merge_assign_info [WpPropId] | |
merge_assign_info [Wp.WpPropId] | |
merge_list [Sigs.Sigma] |
Same than
Sigs.Sigma.merge but for a list of sigmas.
|
merge_list [Wp.Sigs.Sigma] |
Same than
Wp.Sigs.Sigma.merge but for a list of sigmas.
|
meta [CfgCompiler.Cfg] |
Attach meta informations to a node.
|
meta [Wp.CfgCompiler.Cfg] |
Attach meta informations to a node.
|
min_binding [Map.S] |
Return the smallest binding of the given map
(with respect to the
Ord.compare ordering), or raise
Not_found if the map is empty.
|
min_binding_opt [Map.S] |
Return the smallest binding of the given map
(with respect to the
Ord.compare ordering), or None
if the map is empty.
|
min_elt [Set.S] |
Return the smallest element of the given set
(with respect to the
Ord.compare ordering), or raise
Not_found if the set is empty.
|
min_elt_opt [Set.S] |
Return the smallest element of the given set
(with respect to the
Ord.compare ordering), or None
if the set is empty.
|
missing_guards [WpRTE] |
Returns
true if RTE annotations should be generated for
the given function and model (and are not generated yet).
|
mk_asm_assigns_desc [WpPropId] | |
mk_asm_assigns_desc [Wp.WpPropId] | |
mk_assert_id [WpPropId] | |
mk_assert_id [Wp.WpPropId] | |
mk_assigns_info [WpPropId] | |
mk_assigns_info [Wp.WpPropId] | |
mk_axiom_info [WpPropId] | |
mk_axiom_info [Wp.WpPropId] | |
mk_bhv_from_id [WpPropId] |
\from property of function or statement behavior assigns.
|
mk_bhv_from_id [Wp.WpPropId] |
\from property of function or statement behavior assigns.
|
mk_call_pre_id [WpPropId] | mk_call_pre_id called_kf s_call called_pre
|
mk_call_pre_id [Wp.WpPropId] | mk_call_pre_id called_kf s_call called_pre
|
mk_check [WpPropId] | |
mk_check [Wp.WpPropId] | |
mk_code_annot_ids [WpPropId] | |
mk_code_annot_ids [Wp.WpPropId] | |
mk_compl_bhv_id [WpPropId] |
complete behaviors property.
|
mk_compl_bhv_id [Wp.WpPropId] |
complete behaviors property.
|
mk_decrease_id [WpPropId] | |
mk_decrease_id [Wp.WpPropId] | |
mk_disj_bhv_id [WpPropId] |
disjoint behaviors property.
|
mk_disj_bhv_id [Wp.WpPropId] |
disjoint behaviors property.
|
mk_env [LogicCompiler.Make] | |
mk_env [Sigs.LogicSemantics] |
Create a new environment.
|
mk_env [Wp.LogicCompiler.Make] | |
mk_env [Wp.Sigs.LogicSemantics] |
Create a new environment.
|
mk_fct_assigns_id [WpPropId] |
function assigns
|
mk_fct_assigns_id [Wp.WpPropId] |
function assigns
|
mk_fct_from_id [WpPropId] |
\from property of function behavior assigns.
|
mk_fct_from_id [Wp.WpPropId] |
\from property of function behavior assigns.
|
mk_fct_post_id [WpPropId] | |
mk_fct_post_id [Wp.WpPropId] | |
mk_frame [LogicCompiler.Make] | |
mk_frame [Sigs.LogicSemantics] |
Full featured constructor for frames, with fresh pool and gamma.
|
mk_frame [Wp.LogicCompiler.Make] | |
mk_frame [Wp.Sigs.LogicSemantics] |
Full featured constructor for frames, with fresh pool and gamma.
|
mk_init_assigns [WpPropId] | |
mk_init_assigns [Wp.WpPropId] | |
mk_inv_hyp_id [WpPropId] |
Invariant used as hypothesis
|
mk_inv_hyp_id [Wp.WpPropId] |
Invariant used as hypothesis
|
mk_kf_any_assigns_info [WpPropId] | |
mk_kf_any_assigns_info [Wp.WpPropId] | |
mk_kf_assigns_desc [WpPropId] | |
mk_kf_assigns_desc [Wp.WpPropId] | |
mk_lemma_id [WpPropId] |
axiom identification
|
mk_lemma_id [Wp.WpPropId] |
axiom identification
|
mk_loop_any_assigns_info [WpPropId] | |
mk_loop_any_assigns_info [Wp.WpPropId] | |
mk_loop_assigns_desc [WpPropId] | |
mk_loop_assigns_desc [Wp.WpPropId] | |
mk_loop_assigns_id [WpPropId] | |
mk_loop_assigns_id [Wp.WpPropId] | |
mk_loop_from_id [WpPropId] |
\from property of loop assigns.
|
mk_loop_from_id [Wp.WpPropId] |
\from property of loop assigns.
|
mk_loop_inv_id [WpPropId] |
Invariant establishment and preservation
|
mk_loop_inv_id [Wp.WpPropId] |
Invariant establishment and preservation
|
mk_part [WpPropId] | mk_part pid (k, n) build the identification for the k/n part of pid .
|
mk_part [Wp.WpPropId] | mk_part pid (k, n) build the identification for the k/n part of pid .
|
mk_pre_id [WpPropId] | |
mk_pre_id [Wp.WpPropId] | |
mk_pred_info [WpPropId] | |
mk_pred_info [Wp.WpPropId] | |
mk_property [WpPropId] | |
mk_property [Wp.WpPropId] | |
mk_smoke [WpPropId] | |
mk_smoke [Wp.WpPropId] | |
mk_stmt_any_assigns_info [WpPropId] | |
mk_stmt_any_assigns_info [Wp.WpPropId] | |
mk_stmt_assigns_desc [WpPropId] | |
mk_stmt_assigns_desc [Wp.WpPropId] | |
mk_stmt_assigns_id [WpPropId] | |
mk_stmt_assigns_id [Wp.WpPropId] | |
mk_stmt_post_id [WpPropId] | |
mk_stmt_post_id [Wp.WpPropId] | |
mk_strategy [WpStrategy] | |
mk_var_decr_id [WpPropId] |
Variant decrease
|
mk_var_decr_id [Wp.WpPropId] |
Variant decrease
|
mk_var_pos_id [WpPropId] |
Variant positive
|
mk_var_pos_id [Wp.WpPropId] |
Variant positive
|
mk_variant_properties [WpStrategy] | |
mode_of_prover_name [VCS] | |
mode_of_prover_name [Wp.VCS] | |
move_at [LogicCompiler.Make] | |
move_at [Sigs.LogicSemantics] |
Move the compilation environment to the specified
Here memory state.
|
move_at [Wp.LogicCompiler.Make] | |
move_at [Wp.Sigs.LogicSemantics] |
Move the compilation environment to the specified
Here memory state.
|
N | |
name [MemLoader.Model] | |
name [WpContext.IData] | |
name [WpContext.Data] | |
name [WpContext.Entries] | |
name [Context] | |
name [Why3Provers] | |
name [Clabels] | |
name [Wp_error] | |
name [Wp.WpContext.IData] | |
name [Wp.WpContext.Data] | |
name [Wp.WpContext.Entries] | |
name [Wp.Context] | |
name [Wp.Clabels] | |
name_of_field [Lang] | |
name_of_field [Wp.Lang] | |
name_of_lfun [Lang] | |
name_of_lfun [Wp.Lang] | |
name_of_prover [VCS] | |
name_of_prover [Wp.VCS] | |
named [TacLemma] | |
natural_id [Matrix] |
name for elements in NATURAL
|
nearest_elt_ge [Datatype.Set] | |
nearest_elt_le [Datatype.Set] | |
negate [Cvalues] | |
new_driver [LogicBuiltins] |
Creates a configured driver from an existing one.
|
new_driver [Wp.LogicBuiltins] |
Creates a configured driver from an existing one.
|
new_env [Mcfg.S] |
optionally init env with user logic variables
|
new_env [Wp.Mcfg.S] |
optionally init env with user logic variables
|
new_gamma [Lang] | |
new_gamma [Wp.Lang] | |
new_pool [Lang] | |
new_pool [Wp.Lang] | |
next [Pcfg] | |
next [Clabels] | |
next [Wp.Pcfg] | |
next [Wp.Clabels] | |
nil [Conditions] |
Same as empty
|
nil [Wp.Conditions] |
Same as empty
|
no_infinite_array [Ctypes] | |
no_infinite_array [Wp.Ctypes] | |
no_result [VCS] | |
no_result [Wp.VCS] | |
no_status [GuiProver] | |
node [CfgCompiler.Cfg] |
fresh node
|
node [Wp.CfgCompiler.Cfg] |
fresh node
|
node_context [ProofEngine] | |
node_stmt_opt [Cil2cfg] | |
node_type [Cil2cfg] | |
nodes [CfgCompiler.Cfg.P] | |
nodes [Wp.CfgCompiler.Cfg.P] | |
noid [Region] | |
nop [CfgCompiler.Cfg] |
Structurally,
nop is an empty execution trace.
|
nop [Wp.CfgCompiler.Cfg] |
Structurally,
nop is an empty execution trace.
|
normalize [WpStrategy] | |
not [Lang.N] | |
not [Wp.Lang.N] | |
not_equal_obj [Sigs.CodeSemantics] |
Same as
not_equal_typ with an object type.
|
not_equal_obj [Wp.Sigs.CodeSemantics] |
Same as
not_equal_typ with an object type.
|
not_equal_typ [Sigs.CodeSemantics] |
Computes the value of
(a==b) provided both a and b are values
with the given type.
|
not_equal_typ [Wp.Sigs.CodeSemantics] |
Computes the value of
(a==b) provided both a and b are values
with the given type.
|
not_yet_implemented [Wp_error] | |
null [Sigs.Model] |
Return the location of the null pointer
|
null [Cvalues] |
test for null pointer value
|
null [Wp.Sigs.Model] |
Return the location of the null pointer
|
num_of_bhv_from [WpPropId] | |
num_of_bhv_from [Wp.WpPropId] | |
O | |
object_of [Ctypes] | |
object_of [Wp.Ctypes] | |
object_of_array_elem [Ctypes] | |
object_of_array_elem [Wp.Ctypes] | |
object_of_logic_pointed [Ctypes] | |
object_of_logic_pointed [Wp.Ctypes] | |
object_of_logic_type [Ctypes] | |
object_of_logic_type [Wp.Ctypes] | |
object_of_pointed [Ctypes] | |
object_of_pointed [Wp.Ctypes] | |
occurs [Conditions] | |
occurs [Sigs.LogicSemantics] |
Member of vars.
|
occurs [Sigs.Model] |
Test if a location depend on a given logic variable
|
occurs [Vset] | |
occurs [Lang.F] | |
occurs [Wp.Conditions] | |
occurs [Wp.Sigs.LogicSemantics] |
Member of vars.
|
occurs [Wp.Sigs.Model] |
Test if a location depend on a given logic variable
|
occurs [Wp.Vset] | |
occurs [Wp.Lang.F] | |
occurs_e [Strategy] | |
occurs_e [Wp.Strategy] | |
occurs_p [Strategy] | |
occurs_p [Wp.Strategy] | |
occurs_q [Strategy] | |
occurs_q [Wp.Strategy] | |
occurs_x [Strategy] | |
occurs_x [Wp.Strategy] | |
occurs_y [Strategy] | |
occurs_y [Wp.Strategy] | |
occursp [Lang.F] | |
occursp [Wp.Lang.F] | |
of_array [Matrix] | |
of_behavior [RegionAnnot] | |
of_class [Region] | |
of_cstring [Region] | |
of_cvar [Region] | |
of_extension [RegionAnnot] | |
of_integer [Cint] | |
of_integer [Wp.Cint] | |
of_list [Set.S] | of_list l creates a set from a list of elements.
|
of_logic [Clabels] |
Assumes the logic label only comes from normalized or non-ambiguous
labels.
|
of_logic [Wp.Clabels] |
Assumes the logic label only comes from normalized or non-ambiguous
labels.
|
of_name [Region] | |
of_null [Region] | |
of_pred [Definitions.Trigger] | |
of_pred [Wp.Definitions.Trigger] | |
of_real [Cint] | |
of_real [Wp.Cint] | |
of_region_pointer [MemLoader.Model] | |
of_return [Region] | |
of_term [Definitions.Trigger] | |
of_term [Wp.Definitions.Trigger] | |
off [Parameter_sig.Bool] |
Set the boolean to
false .
|
ok_status [GuiProver] | |
old [Clabels] | |
old [Wp.Clabels] | |
on [Parameter_sig.Bool] |
Set the boolean to
true .
|
on_context [WpContext] | |
on_context [Wp.WpContext] | |
on_reload [GuiPanel] | |
on_remove [Wpo] | |
on_remove [Wp.Wpo] | |
on_update [GuiPanel] | |
once [Footprint] |
Width-first once iterator.
|
once [Layout.Overlay] | |
open_file [Script] | |
ordered [Vset] |
-
limit : result when either parameter is None strict : if true , comparison is < instead of <=
|
ordered [Wp.Vset] |
-
limit : result when either parameter is None strict : if true , comparison is < instead of <=
|
output_dot [CfgCompiler.Cfg] | |
output_dot [Wp.CfgCompiler.Cfg] | |
overflow [TacOverflow] | |
overlap [Layout.Range] | |
P | |
p_addr_le [MemMemory] | |
p_addr_lt [MemMemory] | |
p_all [Lang.F] | |
p_all [Wp.Lang.F] | |
p_and [Lang.F] | |
p_and [Wp.Lang.F] | |
p_any [Lang.F] | |
p_any [Wp.Lang.F] | |
p_apply [Letify.Sigma] | |
p_apply [Letify.Ground] | |
p_bind [Lang.F] | |
p_bind [Wp.Lang.F] | |
p_bits [Ctypes] |
pointer size in bits
|
p_bits [Wp.Ctypes] |
pointer size in bits
|
p_bool [Lang.F] | |
p_bool [Wp.Lang.F] | |
p_bools [Lang.F] | |
p_bools [Wp.Lang.F] | |
p_bytes [Ctypes] |
pointer size in bits
|
p_bytes [Wp.Ctypes] |
pointer size in bits
|
p_call [Lang.F] | |
p_call [Wp.Lang.F] | |
p_close [Lang.F] |
Quantify over (sorted) free variables
|
p_close [Wp.Lang.F] |
Quantify over (sorted) free variables
|
p_conj [Lang.F] | |
p_conj [Wp.Lang.F] | |
p_disj [Lang.F] | |
p_disj [Wp.Lang.F] | |
p_eqmem [MemMemory] | |
p_equal [Lang.F] | |
p_equal [Wp.Lang.F] | |
p_equals [Lang.F] | |
p_equals [Wp.Lang.F] | |
p_equiv [Lang.F] | |
p_equiv [Wp.Lang.F] | |
p_exists [Lang.F] | |
p_exists [Wp.Lang.F] | |
p_expr [Lang.F] | |
p_expr [Wp.Lang.F] | |
p_false [Lang.F] | |
p_false [Wp.Lang.F] | |
p_float [ProverTask] |
Float group pattern
\([0-9.]+\)
|
p_float [Wp.ProverTask] |
Float group pattern
\([0-9.]+\)
|
p_forall [Lang.F] | |
p_forall [Wp.Lang.F] | |
p_framed [MemMemory] | |
p_group [ProverTask] |
Put pattern in group
\(p\)
|
p_group [Wp.ProverTask] |
Put pattern in group
\(p\)
|
p_hyps [Lang.F] | |
p_hyps [Wp.Lang.F] | |
p_if [Lang.F] | |
p_if [Wp.Lang.F] | |
p_imply [Lang.F] | |
p_imply [Wp.Lang.F] | |
p_included [MemMemory] | |
p_int [ProverTask] |
Int group pattern
\([0-9]+\)
|
p_int [Wp.ProverTask] |
Int group pattern
\([0-9]+\)
|
p_invalid [MemMemory] | |
p_leq [Lang.F] | |
p_leq [Wp.Lang.F] | |
p_linked [MemMemory] | |
p_lt [Lang.F] | |
p_lt [Wp.Lang.F] | |
p_name [RegionAnnot] | |
p_neq [Lang.F] | |
p_neq [Wp.Lang.F] | |
p_not [Lang.F] | |
p_not [Wp.Lang.F] | |
p_or [Lang.F] | |
p_or [Wp.Lang.F] | |
p_positive [Lang.F] | |
p_positive [Wp.Lang.F] | |
p_sconst [MemMemory] | |
p_separated [MemMemory] | |
p_string [ProverTask] |
String group pattern
"\(...\)"
|
p_string [Wp.ProverTask] |
String group pattern
"\(...\)"
|
p_subst [Lang.F] | |
p_subst [Lang] |
uses current pool
|
p_subst [Wp.Lang.F] | |
p_subst [Wp.Lang] |
uses current pool
|
p_subst_var [Lang.F] | |
p_subst_var [Wp.Lang.F] | |
p_true [Lang.F] | |
p_true [Wp.Lang.F] | |
p_until_space [ProverTask] |
No space group pattern "\\(
^ \t\n *\\)"
|
p_until_space [Wp.ProverTask] |
No space group pattern "\\(
^ \t\n *\\)"
|
p_valid_obj [MemMemory] | |
p_valid_rd [MemMemory] | |
p_valid_rw [MemMemory] | |
p_vars [Lang.F] |
Sorted
|
p_vars [Wp.Lang.F] |
Sorted
|
parallel [StmtSemantics.Make] |
Chain compiler in parallel, between labels
~pre and ~post , which
defaults to resp.
|
parallel [Wp.StmtSemantics.Make] |
Chain compiler in parallel, between labels
~pre and ~post , which
defaults to resp.
|
param [MemVar.VarUsage] |
Memory Model Hypotheses
|
param [Wp.MemVar.VarUsage] |
Memory Model Hypotheses
|
param_of_json [ProofScript] | |
parameters [Lang] |
definitions
|
parameters [Wp.Lang] |
definitions
|
parameters_of_json [ProofScript] | |
params [TacInstance] | |
parasite [Conditions] | |
parasite [Wp.Conditions] | |
parent [ProofEngine] | |
parse [Factory] |
Apply specifications to default setup.
|
parse [Wp.Factory] |
Apply specifications to default setup.
|
parse_coqproof [Proof] | parse_coqproof f parses a coq-file f and fetch the first proof.
|
partition [Set.S] | partition p s returns a pair of sets (s1, s2) , where
s1 is the set of all the elements of s that satisfy the
predicate p , and s2 is the set of all the elements of
s that do not satisfy p .
|
partition [Map.S] | partition p m returns a pair of maps (m1, m2) , where
m1 contains all the bindings of s that satisfy the
predicate p , and m2 is the map with all the bindings of
s that do not satisfy p .
|
parts_of_id [WpPropId] |
get the 'part' information.
|
parts_of_id [Wp.WpPropId] |
get the 'part' information.
|
pattern [Footprint] |
Generate head footprint up to size
|
pending [ProofEngine] |
0 means proved
|
pending [ProofScript] |
pending goals
|
pending_any [ProofScript] |
minimum of pending goals
|
plain [Cvalues] | |
pointed [Layout.Value] | |
pointer [MemTyped] | |
pointer [Lang] |
type of pointers
|
pointer [Wp.MemTyped] | |
pointer [Wp.Lang] |
type of pointers
|
pointer_loc [Sigs.Model] |
Interpret an address value (a pointer) as an abstract location.
|
pointer_loc [Wp.Sigs.Model] |
Interpret an address value (a pointer) as an abstract location.
|
pointer_val [Sigs.Model] |
Return the adress value (a pointer) of an abstract location.
|
pointer_val [Wp.Sigs.Model] |
Return the adress value (a pointer) of an abstract location.
|
poly [Lang] |
polymorphism
|
poly [Wp.Lang] |
polymorphism
|
pool [ProofEngine] | |
pool [Plang] | |
pool [Lang.F] | |
pool [Wp.Plang] | |
pool [Wp.Lang.F] | |
pop [Context] | |
pop [Wp.Context] | |
post [Clabels] | |
post [Wp.Clabels] | |
pp [CfgCompiler.Cfg.Node] | |
pp [Wp.CfgCompiler.Cfg.Node] | |
pp_acs [Cvalues] | |
pp_annots [WpStrategy] | |
pp_assign_info [WpPropId] | |
pp_assign_info [Wp.WpPropId] | |
pp_assigns [Wp_error] | |
pp_assigns_desc [WpPropId] | |
pp_assigns_desc [Wp.WpPropId] | |
pp_axiom_info [WpPropId] | |
pp_axiom_info [Wp.WpPropId] | |
pp_axiomatics [Wpo] | |
pp_axiomatics [Wp.Wpo] | |
pp_bound [Cvalues] | |
pp_bound [Vset] | |
pp_bound [Wp.Vset] | |
pp_call_type [Cil2cfg] | |
pp_calls [Dyncall] | |
pp_chain [Layout.Offset] | |
pp_clause [Tactical] |
Debug only
|
pp_clause [MemoryContext] | |
pp_clause [Wp.Tactical] |
Debug only
|
pp_clause [Wp.MemoryContext] | |
pp_cluster [Definitions] | |
pp_cluster [Wp.Definitions] | |
pp_depend [Wpo] | |
pp_depend [Wp.Wpo] | |
pp_dependencies [Wpo] | |
pp_dependencies [Wp.Wpo] | |
pp_dependency [Wpo] | |
pp_dependency [Wp.Wpo] | |
pp_edge [Cil2cfg] | |
pp_epred [Lang.F] | |
pp_epred [Wp.Lang.F] | |
pp_eterm [Lang.F] | |
pp_eterm [Wp.Lang.F] | |
pp_file [ProverTask] | |
pp_file [Wp.ProverTask] | |
pp_float [Ctypes] | |
pp_float [Wp.Ctypes] | |
pp_frame [LogicCompiler.Make] | |
pp_frame [Sigs.LogicSemantics] | |
pp_frame [Wp.LogicCompiler.Make] | |
pp_frame [Wp.Sigs.LogicSemantics] | |
pp_function [Wpo] | |
pp_function [Wp.Wpo] | |
pp_goal [Wpo] | |
pp_goal [Wp.Wpo] | |
pp_goal_flow [Wpo] | |
pp_goal_flow [Wp.Wpo] | |
pp_index [Wpo] | |
pp_index [Wp.Wpo] | |
pp_info_of_strategy [WpStrategy] | |
pp_int [Ctypes] | |
pp_int [Wp.Ctypes] | |
pp_logfile [Wpo] | |
pp_logfile [Wp.Wpo] | |
pp_logic [Cvalues] | |
pp_logic_label [Wp_error] | |
pp_mode [VCS] | |
pp_mode [Wp.VCS] | |
pp_node [Cil2cfg] | |
pp_node_type [Cil2cfg] | |
pp_object [Ctypes] | |
pp_object [Wp.Ctypes] | |
pp_param [MemoryContext] | |
pp_param [Wp.MemoryContext] | |
pp_pred [Lang.F] | |
pp_pred [Wp.Lang.F] | |
pp_pred_info [WpPropId] | |
pp_pred_info [Wp.WpPropId] | |
pp_pred_of_pred_info [WpPropId] | |
pp_pred_of_pred_info [Wp.WpPropId] | |
pp_profile [LogicUsage] | |
pp_profile [Wp.LogicUsage] | |
pp_propid [WpPropId] |
Print unique id of
prop_id
|
pp_propid [Wp.WpPropId] |
Print unique id of
prop_id
|
pp_prover [VCS] | |
pp_prover [Wp.VCS] | |
pp_region [Cvalues] | |
pp_result [VCS] | |
pp_result [Wp.VCS] | |
pp_result_perf [VCS] | |
pp_result_perf [Wp.VCS] | |
pp_rloc [Cvalues] | |
pp_script [ProofSession] | |
pp_script_for [ProofSession] | |
pp_selection [Tactical] |
Debug only
|
pp_selection [Wp.Tactical] |
Debug only
|
pp_sloc [Cvalues] | |
pp_string_list [Wp_error] | |
pp_tau [Lang.F] | |
pp_tau [Wp.Lang.F] | |
pp_term [Lang.F] | |
pp_term [Wp.Lang.F] | |
pp_time [Rformat] |
Pretty print time in hour, minutes, seconds, or milliseconds, as appropriate
|
pp_time_range [Rformat] | |
pp_title [Wpo] | |
pp_title [Wp.Wpo] | |
pp_value [Sigs.CodeSemantics] | |
pp_value [Cvalues] | |
pp_value [Wp.Sigs.CodeSemantics] | |
pp_var [Lang.F] | |
pp_var [Wp.Lang.F] | |
pp_vars [Lang.F] | |
pp_vars [Wp.Lang.F] | |
pp_vset [Vset] | |
pp_vset [Wp.Vset] | |
pp_warnings [Register] | |
pp_warnings [Wpo] | |
pp_warnings [Wp.Wpo] | |
pp_wp_parameters [Register] | |
pp_zone [MemoryContext] | |
pp_zone [Wp.MemoryContext] | |
pprepeat [Vlist] | |
pre [Clabels] | |
pre [Wp.Clabels] | |
pred [LogicCompiler.Make] | |
pred [Sigs.LogicSemantics] |
Compile a predicate.
|
pred [Repr] | |
pred [Wp.LogicCompiler.Make] | |
pred [Wp.Sigs.LogicSemantics] |
Compile a predicate.
|
pred [Wp.Repr] | |
pred_e [Cil2cfg] | |
pred_info_id [WpPropId] | |
pred_info_id [Wp.WpPropId] | |
preproc_annot [NormAtLabels] | |
preproc_annot [Wp.NormAtLabels] | |
preproc_assigns [NormAtLabels] | |
preproc_assigns [Wp.NormAtLabels] | |
pretty [ProofEngine] | |
pretty [Wpo.DISK] | |
pretty [CfgCompiler.Cfg.E] | |
pretty [CfgCompiler.Cfg.T] | |
pretty [CfgCompiler.Cfg.P] | |
pretty [Pcond] | |
pretty [Conditions] | |
pretty [Sigs.Model] |
pretty printing of memory location
|
pretty [Sigs.Sigma] |
For debugging purpose
|
pretty [Sigs.Chunk] | |
pretty [Letify.Sigma] | |
pretty [Letify.Ground] | |
pretty [Cstring] | |
pretty [Vlist] | |
pretty [Vset] | |
pretty [Splitter] | |
pretty [Passive] | |
pretty [Mcfg.S] | |
pretty [WpPropId] | |
pretty [RegionAnnot.Lpath] | |
pretty [Layout.Chunk] | |
pretty [Layout.Root] | |
pretty [Layout.Cluster] | |
pretty [Layout.Overlay] | |
pretty [Layout.Range] | |
pretty [Layout.Matrix] | |
pretty [Layout.Value] | |
pretty [Layout.Usage] | |
pretty [Layout.Alias] | |
pretty [Layout.Data] | |
pretty [WpContext.Key] | |
pretty [WpContext.Entries] | |
pretty [Warning] | |
pretty [Clabels] | |
pretty [Ctypes] | |
pretty [Rformat] | |
pretty [Wp.Wpo.DISK] | |
pretty [Wp.CfgCompiler.Cfg.E] | |
pretty [Wp.CfgCompiler.Cfg.T] | |
pretty [Wp.CfgCompiler.Cfg.P] | |
pretty [Wp.Pcond] | |
pretty [Wp.Conditions] | |
pretty [Wp.Sigs.Model] |
pretty printing of memory location
|
pretty [Wp.Sigs.Sigma] |
For debugging purpose
|
pretty [Wp.Sigs.Chunk] | |
pretty [Wp.Cstring] | |
pretty [Wp.Vset] | |
pretty [Wp.Splitter] | |
pretty [Wp.Passive] | |
pretty [Wp.WpContext.Key] | |
pretty [Wp.WpContext.Entries] | |
pretty [Wp.Warning] | |
pretty [Wp.Mcfg.S] | |
pretty [Wp.WpPropId] | |
pretty [Wp.Clabels] | |
pretty [Wp.Ctypes] | |
pretty_context [WpPropId] | |
pretty_context [Wp.WpPropId] | |
pretty_local [WpPropId] | |
pretty_local [Wp.WpPropId] | |
prev [Pcfg] | |
prev [Wp.Pcfg] | |
print [RefUsage] | |
print [Wp.RefUsage] | |
print_generated [Wp_parameters] |
print the given file if the debugging category
"print-generated" is set
|
print_generated [Wp.Wp_parameters] |
print the given file if the debugging category
"print-generated" is set
|
print_why3 [Why3Provers] | |
print_wp [Why3Provers] | |
promote [Ctypes] | |
promote [Wp.Ctypes] | |
proof [VC] |
List of proof obligations computed for a given property.
|
proof [ProofEngine] | |
proof [Wp.VC] |
List of proof obligations computed for a given property.
|
proof_context [LogicUsage] |
Lemmas that are not in an axiomatic.
|
proof_context [Wp.LogicUsage] |
Lemmas that are not in an axiomatic.
|
prop_id_keys [WpPropId] | |
prop_id_keys [Wp.WpPropId] | |
property [Wprop.Info] | |
property [Wprop.Indexed2] | |
property [Wprop.Indexed] | |
property_of_id [WpPropId] |
returns the annotation which lead to the given PO.
|
property_of_id [Wp.WpPropId] |
returns the annotation which lead to the given PO.
|
prove [VC] |
Returns a ready-to-schedule task.
|
prove [ProverScript] | |
prove [Prover] | |
prove [ProverWhy3] |
Return NoResult if it is already proved by Qed
|
prove [ProverCoq] | |
prove [ProverErgo] | |
prove [Wp.Prover] | |
prove [Wp.VC] |
Returns a ready-to-schedule task.
|
proved [Register] | |
proved [ProofEngine] | |
prover_of_json [ProofScript] | |
prover_of_name [Wpo] |
Dynamically exported.
|
prover_of_name [VCS] | |
prover_of_name [Wp.Wpo] |
Dynamically exported.
|
prover_of_name [Wp.VCS] | |
provers [Register] | |
provers [Why3Provers] | |
provers_set [Why3Provers] | |
pruning [Conditions] | |
pruning [Wp.Conditions] | |
push [Context] | |
push [Wp.Context] | |
Q | |
qed_time [Wpo.GOAL] | |
qed_time [Wpo] | |
qed_time [Wp.Wpo.GOAL] | |
qed_time [Wp.Wpo] | |
R | |
range [Auto] | |
range [Tactical] | |
range [Vset] | |
range [Cint] |
Dependent on model
|
range [Layout.Offset] | |
range [Wp.Auto] | |
range [Wp.Tactical] | |
range [Wp.Vset] | |
range [Wp.Cint] |
Dependent on model
|
ranges [Auto.Range] | |
ranges [Wp.Auto.Range] | |
rdescr [Cvalues.Logic] | |
reached [WpReached] |
memoized reached cfg for function
|
reads [CfgCompiler.Cfg.E] | |
reads [CfgCompiler.Cfg.T] | |
reads [CfgCompiler.Cfg.P] | |
reads [CfgCompiler.Cfg.C] | |
reads [Wp.CfgCompiler.Cfg.E] | |
reads [Wp.CfgCompiler.Cfg.T] | |
reads [Wp.CfgCompiler.Cfg.P] | |
reads [Wp.CfgCompiler.Cfg.C] | |
real_of_float [Cfloat] | |
real_of_float [Wp.Cfloat] | |
real_of_flt [Cfloat] | |
real_of_flt [Wp.Cfloat] | |
real_of_int [Cmath] | |
rebuild [Lang.For_export] | |
rebuild [Wp.Lang.For_export] | |
record [Lang] | |
record [Wp.Lang] | |
record_with [Lang.F] | |
record_with [Wp.Lang.F] | |
reduce [Wpo] |
tries simplification
|
reduce [Wp.Wpo] |
tries simplification
|
region [LogicCompiler.Make] |
When
~unfold:true , decompose compound regions field by field
|
region [Sigs.LogicSemantics] |
Compile a term representing a set of memory locations into an abstract
region.
|
region [Cvalues.Logic] | |
region [Region] | |
region [Wp.LogicCompiler.Make] |
When
~unfold:true , decompose compound regions field by field
|
region [Wp.Sigs.LogicSemantics] |
Compile a term representing a set of memory locations into an abstract
region.
|
register [GuiPanel] | |
register [Register] | |
register [Strategy] | |
register [Tactical] | |
register [MemMemory] | |
register [Pcfg] | |
register [RegionAnnot] |
Auto when `-wp-region`
|
register [WpContext] |
Model registration.
|
register [Context] |
Register a global configure, to be executed once per project/ast.
|
register [Wp.Strategy] | |
register [Wp.Tactical] | |
register [Wp.Pcfg] | |
register [Wp.WpContext] |
Model registration.
|
register [Wp.Context] |
Register a global configure, to be executed once per project/ast.
|
release [Lang.F] |
Empty local caches
|
release [Wp.Lang.F] |
Empty local caches
|
reload [GuiPanel] | |
relocate [CfgCompiler.Cfg.E] | |
relocate [CfgCompiler.Cfg.T] | |
relocate [CfgCompiler.Cfg.P] | | relocate m' (create m p) | = | p{ } |
|
relocate [CfgCompiler.Cfg.C] | |
relocate [Wp.CfgCompiler.Cfg.E] | |
relocate [Wp.CfgCompiler.Cfg.T] | |
relocate [Wp.CfgCompiler.Cfg.P] | | relocate m' (create m p) | = | p{ } |
|
relocate [Wp.CfgCompiler.Cfg.C] | |
remove [VC] | |
remove [ProofEngine] | |
remove [ProofSession] | |
remove [Wpo] | |
remove [Cil2cfg.HEsig] | |
remove [WpContext.Generator] | |
remove [WpContext.Registry] | |
remove [Wp.Wpo] | |
remove [Wp.VC] | |
remove [Hashtbl.S] | |
remove [Wp.WpContext.Generator] | |
remove [Wp.WpContext.Registry] | |
remove [Set.S] | remove x s returns a set containing all elements of s ,
except x .
|
remove [Map.S] | remove x m returns a map containing the same bindings as
m , except for x which is unbound in the returned map.
|
remove_chunks [Sigs.Sigma] |
Return a copy of the environment where chunks in the footprint
have been removed.
|
remove_chunks [Wp.Sigs.Sigma] |
Return a copy of the environment where chunks in the footprint
have been removed.
|
remove_for_altergo [Filter_axioms] | |
remove_for_why3 [Filter_axioms] | |
replace [Tactical] | |
replace [Conditions] |
replace a step in the sequent, the one
at the specified position.
|
replace [Cil2cfg.HEsig] | |
replace [Wp.Tactical] | |
replace [Hashtbl.S] | |
replace [Wp.Conditions] |
replace a step in the sequent, the one
at the specified position.
|
repr [Lang.F] |
Constant time
|
repr [WpContext.MODEL] | |
repr [Wp.Lang.F] |
Constant time
|
repr [Wp.WpContext.MODEL] | |
requires [MemoryContext] |
Build the separation clause from a partition,
including the clauses related to the pointer validity
|
requires [Wp.MemoryContext] |
Build the separation clause from a partition,
including the clauses related to the pointer validity
|
reset [ProofEngine] | |
reset [Wp_parameters] | |
reset [Hashtbl.S] | |
reset [Wp.Wp_parameters] | |
reshape [Layout.Cluster] | |
reshape [Layout.Compound] | |
resolve [Wpo.VC_Annot] | |
resolve [Wpo] |
tries simplification and set result if valid
|
resolve [Wp.Wpo.VC_Annot] | |
resolve [Wp.Wpo] |
tries simplification and set result if valid
|
result [VCS] | |
result [StmtSemantics.Make] | |
result [LogicCompiler.Make] | |
result [Sigs.LogicSemantics] |
Result location of the current function in the current frame.
|
result [Sigs.CodeSemantics] |
Value of an abstract result container.
|
result [Wp.VCS] | |
result [Wp.StmtSemantics.Make] | |
result [Wp.LogicCompiler.Make] | |
result [Wp.Sigs.LogicSemantics] |
Result location of the current function in the current frame.
|
result [Wp.Sigs.CodeSemantics] |
Value of an abstract result container.
|
result_of_json [ProofScript] | |
results [Register] | |
return [StmtSemantics.Make] | |
return [LogicCompiler.Make] | |
return [Sigs.LogicSemantics] |
Result type of the current function in the current frame.
|
return [Sigs.CodeSemantics] |
Return an expression with a given type.
|
return [Mcfg.S] | |
return [Wp.StmtSemantics.Make] | |
return [Wp.LogicCompiler.Make] | |
return [Wp.Sigs.LogicSemantics] |
Result type of the current function in the current frame.
|
return [Wp.Sigs.CodeSemantics] |
Return an expression with a given type.
|
return [Wp.Mcfg.S] | |
rewrite [Tactical] |
For each pattern
(descr,guard,src,tgt) replace src with tgt
under condition guard , inserted in position at .
|
rewrite [Wp.Tactical] |
For each pattern
(descr,guard,src,tgt) replace src with tgt
under condition guard , inserted in position at .
|
run [Register] | |
run_and_prove [GuiPanel] | |
S | |
s_bool [WpTac] | |
s_cnf_iff [WpTac] | |
s_cnf_ite [WpTac] | |
s_cnf_xor [WpTac] | |
s_dnf_iff [WpTac] | |
s_dnf_ite [WpTac] | |
s_dnf_xor [WpTac] | |
same_edge [Cil2cfg] | |
same_node [Cil2cfg] | |
sanitizer [Plang] | |
sanitizer [Wp.Plang] | |
save [ProverScript] | |
save [ProofSession] | |
saved [ProofEngine] | |
savescripts [Proof] |
If necessary, dump the scripts database into the file
specified by
-wp-script f .
|
schedule [ProverTask] | |
schedule [Wp.ProverTask] | |
scheduled [Register] | |
scope [StmtSemantics.Make] | |
scope [Sigs.Model] |
Manage the scope of variables.
|
scope [Mcfg.S] | |
scope [Wp.StmtSemantics.Make] | |
scope [Wp.Sigs.Model] |
Manage the scope of variables.
|
scope [Wp.Mcfg.S] | |
script [ProofEngine] | |
script_for [Proof] | |
script_for_ide [Proof] | |
search [ProverScript] | |
search [ProverSearch] | |
search [TacLemma] | |
search [Tactical] |
Search field.
|
search [Wp.Tactical] |
Search field.
|
section [Definitions] | |
section [Wp.Definitions] | |
section_of_lemma [LogicUsage] | |
section_of_lemma [Wp.LogicUsage] | |
section_of_logic [LogicUsage] | |
section_of_logic [Wp.LogicUsage] | |
section_of_type [LogicUsage] | |
section_of_type [Wp.LogicUsage] | |
select [Letify.Split] | |
select_by_name [WpPropId] |
test if the prop_id has to be selected for the asked name.
|
select_by_name [Wp.WpPropId] |
test if the prop_id has to be selected for the asked name.
|
select_call_pre [WpPropId] |
test if the prop_id has to be selected when we want to select the call
precondition the the
stmt call (None means all the call preconditions).
|
select_call_pre [Wp.WpPropId] |
test if the prop_id has to be selected when we want to select the call
precondition the the
stmt call (None means all the call preconditions).
|
select_default [WpPropId] |
test if the prop_id does not have a
no_wp: in its name(s).
|
select_default [Wp.WpPropId] |
test if the prop_id does not have a
no_wp: in its name(s).
|
select_e [Strategy] |
Lookup the first occurrence of term in the sequent and returns
the associated selection.
|
select_e [Wp.Strategy] |
Lookup the first occurrence of term in the sequent and returns
the associated selection.
|
select_p [Strategy] |
Same as
select_e but for a predicate.
|
select_p [Wp.Strategy] |
Same as
select_e but for a predicate.
|
selected [Tactical] | |
selected [Wp.Tactical] | |
selection_of_json [ProofScript] | |
selection_target [ProofScript] | |
selector [Tactical] |
Unless specified, default is head option.
|
selector [Wp.Tactical] |
Unless specified, default is head option.
|
self [Sigs.Chunk] |
Chunk names, for pretty-printing.
|
self [Wp.Sigs.Chunk] |
Chunk names, for pretty-printing.
|
separated [Auto] | |
separated [MemMemory] | |
separated [Sigs.Model] |
Return the formula that tests if two segment are separated
|
separated [Cvalues.Logic] | |
separated [Wp.Auto] | |
separated [Wp.Sigs.Model] |
Return the formula that tests if two segment are separated
|
seq_branch [Conditions] |
Creates an If-Then-Else branch located at the provided stmt, if any.
|
seq_branch [Wp.Conditions] |
Creates an If-Then-Else branch located at the provided stmt, if any.
|
sequence [Register] | |
sequence [StmtSemantics.Make] |
Chain compiler by introducing fresh nodes between each element
of the list.
|
sequence [Pcond] | |
sequence [Conditions] | |
sequence [Wp.StmtSemantics.Make] |
Chain compiler by introducing fresh nodes between each element
of the list.
|
sequence [Wp.Pcond] | |
sequence [Wp.Conditions] | |
server [VC] |
Default number of parallel tasks is given by
-wp-par command-line option.
|
server [ProverTask] | |
server [Wp.ProverTask] | |
server [Wp.VC] |
Default number of parallel tasks is given by
-wp-par command-line option.
|
session [Register] | |
set [Tactical.Fmap] | |
set [StmtSemantics.Make] | |
set [MemoryContext] | |
set [Context] |
Define the current value.
|
set [Wp.Tactical.Fmap] | |
set [Wp.StmtSemantics.Make] | |
set [Wp.Context] |
Define the current value.
|
set [Wp.MemoryContext] | |
set_at_frame [LogicCompiler.Make] | |
set_at_frame [Sigs.LogicSemantics] |
Update a frame with a specific environment for the given label.
|
set_at_frame [Wp.LogicCompiler.Make] | |
set_at_frame [Wp.Sigs.LogicSemantics] |
Update a frame with a specific environment for the given label.
|
set_builtin [Lang.For_export] | |
set_builtin [Lang.F] | |
set_builtin [Wp.Lang.For_export] | |
set_builtin [Wp.Lang.F] | |
set_builtin' [Lang.For_export] | |
set_builtin' [Wp.Lang.For_export] | |
set_builtin_1 [Lang.F] | |
set_builtin_1 [Wp.Lang.F] | |
set_builtin_2 [Lang.F] | |
set_builtin_2 [Wp.Lang.F] | |
set_builtin_2' [Lang.F] | |
set_builtin_2' [Wp.Lang.F] | |
set_builtin_eq [Lang.For_export] | |
set_builtin_eq [Lang.F] | |
set_builtin_eq [Wp.Lang.For_export] | |
set_builtin_eq [Wp.Lang.F] | |
set_builtin_eqp [Lang.F] | |
set_builtin_eqp [Wp.Lang.F] | |
set_builtin_get [Lang.F] | |
set_builtin_get [Wp.Lang.F] | |
set_builtin_leq [Lang.For_export] | |
set_builtin_leq [Lang.F] | |
set_builtin_leq [Wp.Lang.For_export] | |
set_builtin_leq [Wp.Lang.F] | |
set_mode [ProverWhy3] | |
set_model [Register] | |
set_model [Wp_error] | |
set_option [LogicBuiltins] |
reset and add a value to an option (group, name)
|
set_option [Wp.LogicBuiltins] |
reset and add a value to an option (group, name)
|
set_possible_values [Parameter_sig.String] |
Set what are the acceptable values for this parameter.
|
set_procs [Why3Provers] | |
set_range [Parameter_sig.Int] |
Set what is the possible range of values for this parameter.
|
set_result [Wpo] | |
set_result [Wp.Wpo] | |
set_saved [ProofEngine] | |
set_strategies [ProofEngine] | |
severe [Warning] | |
severe [Wp.Warning] | |
shareable [Vlist] | |
shift [MemLoader.Model] | |
shift [Sigs.Model] |
Return the memory location obtained by array access at an index
represented by the given
term .
|
shift [Cvalues.Logic] | |
shift [Layout.Cluster] | |
shift [Wp.Sigs.Model] |
Return the memory location obtained by array access at an index
represented by the given
term .
|
sigma [Lang] |
uses current pool
|
sigma [Wp.Lang] |
uses current pool
|
signature [Tactical] | |
signature [Wp.Tactical] | |
signed [Ctypes] | true if signed
|
signed [Wp.Ctypes] | true if signed
|
simplify [Conditions] | |
simplify [Mcfg.Splitter] | |
simplify [Wp.Conditions] | |
simplify [Wp.Mcfg.Splitter] | |
singleton [Letify.Ground] | |
singleton [Vset] | |
singleton [Splitter] | |
singleton [Layout.Chunk] | |
singleton [Wp.Vset] | |
singleton [Wp.Splitter] | |
singleton [Set.S] | singleton x returns the one-element set containing only x .
|
singleton [Map.S] | singleton x y returns the one-element map that contains a binding y
for x .
|
size [Conditions] |
Compute the total number of steps in the sequence, including
nested sequences from branches and disjunctions.
|
size [Matrix] | |
size [Wp.Conditions] |
Compute the total number of steps in the sequence, including
nested sequences from branches and disjunctions.
|
sizeof [MemLoader.Model] | |
sizeof [Layout.Matrix] | |
sizeof [Layout.Value] | |
sizeof [Layout.Offset] | |
sizeof_defined [Ctypes] | |
sizeof_defined [Wp.Ctypes] | |
sizeof_object [Ctypes] | |
sizeof_object [Wp.Ctypes] | |
skip [Script] | |
smoked [VCS] | |
smoked [Wp.VCS] | |
smoking [WpReached] |
Returns whether a stmt need a smoke tests to avoid being unreachable.
|
sort [Lang.F] |
Constant time
|
sort [Wp.Lang.F] |
Constant time
|
source_of_id [WpPropId] | |
source_of_id [Wp.WpPropId] | |
spawn [VC] |
Same as
prove but schedule the tasks into the global server returned
by server function below.
|
spawn [ProverScript] | |
spawn [Prover] | |
spawn [ProverTask] | |
spawn [Wp.Prover] | |
spawn [Wp.ProverTask] | |
spawn [Wp.VC] |
Same as
prove but schedule the tasks into the global server returned
by server function below.
|
spawn_wp_proofs_iter [Register] | |
spec [StmtSemantics.Make] | |
spec [Wp.StmtSemantics.Make] | |
specialize_eq_list [Vlist] | |
spinner [Tactical] |
Unless specified, default is
vmin or 0 or vmax , whichever fits.
|
spinner [Wp.Tactical] |
Unless specified, default is
vmin or 0 or vmax , whichever fits.
|
split [Auto] | |
split [Tactical] | |
split [Mcfg.Splitter] | |
split [Wp.Auto] | |
split [Wp.Tactical] | |
split [Wp.Mcfg.Splitter] | |
split [Set.S] | split x s returns a triple (l, present, r) , where
l is the set of elements of s that are
strictly less than x ;
r is the set of elements of s that are
strictly greater than x ;
present is false if s contains no element equal to x ,
or true if s contains an element equal to x .
|
split [Map.S] | split x m returns a triple (l, data, r) , where
l is the map with all the bindings of m whose key
is strictly less than x ;
r is the map with all the bindings of m whose key
is strictly greater than x ;
data is None if m contains no binding for x ,
or Some v if m binds v to x .
|
split_bag [WpPropId] | |
split_bag [Wp.WpPropId] | |
split_map [WpPropId] | |
split_map [Wp.WpPropId] | |
spy [Register] | |
start_edge [Cil2cfg] |
get the starting edges
|
start_stmt_of_node [Cil2cfg] | |
startof [Cvalues] |
Shift a location with 0-indices wrt to its array type
|
state [Conditions] |
Stack a memory model state on top of the bundle.
|
state [Mstate] | |
state [Sigs.Model] |
Returns a memory state description from a memory environement.
|
state [Wp.Conditions] |
Stack a memory model state on top of the bundle.
|
state [Wp.Mstate] | |
state [Wp.Sigs.Model] |
Returns a memory state description from a memory environement.
|
stats [Hashtbl.S] | |
status [ProofEngine] | |
status [WpAnnot] | |
status [LogicCompiler.Make] | |
status [Sigs.LogicSemantics] |
Exit status for the current frame.
|
status [Wp.LogicCompiler.Make] | |
status [Wp.Sigs.LogicSemantics] |
Exit status for the current frame.
|
step [Conditions] |
Creates a single step
|
step [Wp.Conditions] |
Creates a single step
|
step_at [Conditions] |
Retrieve a step by
id in the sequence.
|
step_at [Wp.Conditions] |
Retrieve a step by
id in the sequence.
|
stepout [ProverTask] | |
stepout [VCS] | |
stepout [Wp.ProverTask] | |
stepout [Wp.VCS] | |
steps [Conditions] |
Attributes unique indices to every
step.id in the sequence,
starting from zero.
|
steps [Wp.Conditions] |
Attributes unique indices to every
step.id in the sequence,
starting from zero.
|
stmt [Clabels] | |
stmt [Wp.Clabels] | |
store_float [MemLoader.Model] | |
store_int [MemLoader.Model] | |
store_pointer [MemLoader.Model] | |
stored [MemLoader.Make] | |
stored [Sigs.Model] |
Return a set of formula that express a modification between two memory
state.
|
stored [Wp.Sigs.Model] |
Return a set of formula that express a modification between two memory
state.
|
str_id [Cstring] |
Non-zero integer, unique for each different string literal
|
str_id [Wp.Cstring] |
Non-zero integer, unique for each different string literal
|
str_len [Cstring] |
Property defining the size of the string in bytes,
with
\0 terminator included.
|
str_len [Wp.Cstring] |
Property defining the size of the string in bytes,
with
\0 terminator included.
|
str_val [Cstring] |
The array containing the
char of the constant
|
str_val [Wp.Cstring] |
The array containing the
char of the constant
|
strange_loops [Cil2cfg] |
detect is there are non natural loops or natural loops where we didn't
manage to compute back edges (see
mark_loops ).
|
strategy [TacCongruence] | |
strategy [TacShift] | |
strategy [TacBitrange] | |
strategy [TacBitwised] | |
strategy [TacRewrite] | |
strategy [TacNormalForm] | |
strategy [TacCut] | |
strategy [TacFilter] | |
strategy [TacLemma] | |
strategy [TacInstance] | |
strategy [TacHavoc.Validity] | |
strategy [TacHavoc.Separated] | |
strategy [TacHavoc.Havoc] | |
strategy [TacUnfold] | |
strategy [TacCompound] | |
strategy [TacArray] | |
strategy [TacRange] | |
strategy [TacChoice.Contrapose] | |
strategy [TacChoice.Absurd] | |
strategy [TacChoice.Choice] | |
strategy [TacSplit] | |
strategy_has_asgn_goal [WpStrategy] | |
strategy_has_prop_goal [WpStrategy] | |
strategy_kind [WpStrategy] | |
string_of_termination_kind [WpPropId] |
TODO: should probably be somewhere else
|
string_of_termination_kind [Wp.WpPropId] |
TODO: should probably be somewhere else
|
sub_c_int [Ctypes] | |
sub_c_int [Wp.Ctypes] | |
sub_range [Vset] | |
sub_range [Wp.Vset] | |
subclause [Tactical] |
When
subclause clause p , we have clause = Step H and H -> p ,
or clause = Goal G and p -> G .
|
subclause [Wp.Tactical] |
When
subclause clause p , we have clause = Step H and H -> p ,
or clause = Goal G and p -> G .
|
subproof_idx [WpPropId] |
subproof index of this propr_id
|
subproof_idx [Wp.WpPropId] |
subproof index of this propr_id
|
subproofs [WpPropId] |
How many subproofs
|
subproofs [Wp.WpPropId] |
How many subproofs
|
subset [Cvalues.Logic] | |
subset [Vset] | |
subset [Wp.Vset] | |
subset [Set.S] | subset s1 s2 tests whether the set s1 is a subset of
the set s2 .
|
subst [Conditions] |
Apply the atomic substitution recursively using
Lang.F.p_subst f .
|
subst [Lang] |
replace variables
|
subst [Wp.Conditions] |
Apply the atomic substitution recursively using
Lang.F.p_subst f .
|
subst [Wp.Lang] |
replace variables
|
subterms [Pcfg] | |
subterms [Wp.Pcfg] | |
succ_e [Cil2cfg] | |
switch [Mcfg.S] | |
switch [Wp.Mcfg.S] | |
switch_cases [Splitter] | |
switch_cases [Wp.Splitter] | |
switch_default [Splitter] | |
switch_default [Wp.Splitter] | |
T | |
t32 [Cfloat] | |
t32 [Wp.Cfloat] | |
t64 [Cfloat] | |
t64 [Wp.Cfloat] | |
t_absurd [Auto] |
Find a contradiction.
|
t_absurd [Wp.Auto] |
Find a contradiction.
|
t_addr [MemMemory] | |
t_addr [Lang] |
pointer on Void
|
t_addr [Wp.Lang] |
pointer on Void
|
t_array [Lang] | |
t_array [Wp.Lang] | |
t_bool [Lang] | |
t_bool [Wp.Lang] | |
t_case [Auto] |
Case analysis:
t_case p a b applies process a under hypothesis p
and process b under hypothesis not p .
|
t_case [Wp.Auto] |
Case analysis:
t_case p a b applies process a under hypothesis p
and process b under hypothesis not p .
|
t_cases [Auto] |
Complete analysis: applies each process under its guard, and proves that
all guards are complete.
|
t_cases [Wp.Auto] |
Complete analysis: applies each process under its guard, and proves that
all guards are complete.
|
t_chain [Auto] |
Apply second process to every goal generated by the first one.
|
t_chain [Wp.Auto] |
Apply second process to every goal generated by the first one.
|
t_cut [Auto] |
Prove condition
p and use-it as a forward hypothesis.
|
t_cut [Wp.Auto] |
Prove condition
p and use-it as a forward hypothesis.
|
t_datatype [Lang] | |
t_datatype [Wp.Lang] | |
t_descr [Auto] |
Apply a description to each sub-goal
|
t_descr [Wp.Auto] |
Apply a description to each sub-goal
|
t_farray [Lang] | |
t_farray [Wp.Lang] | |
t_finally [Auto] |
Apply a description to a leaf goal.
|
t_finally [Wp.Auto] |
Apply a description to a leaf goal.
|
t_id [Auto] |
Keep goal unchanged.
|
t_id [Wp.Auto] |
Keep goal unchanged.
|
t_int [Lang] | |
t_int [Wp.Lang] | |
t_malloc [MemMemory] |
allocation tables
|
t_mem [MemMemory] |
t_addr indexed array
|
t_prop [Lang] | |
t_prop [Wp.Lang] | |
t_range [Auto] | |
t_range [Wp.Auto] | |
t_real [Lang] | |
t_real [Wp.Lang] | |
t_replace [Auto] |
Prove
src=tgt then replace src by tgt .
|
t_replace [Wp.Auto] |
Prove
src=tgt then replace src by tgt .
|
t_split [Auto] |
Split with
p and not p .
|
t_split [Wp.Auto] |
Split with
p and not p .
|
tactical [ProofEngine] | |
tactical [TacCongruence] | |
tactical [TacShift] | |
tactical [TacBitrange] | |
tactical [TacBitwised] | |
tactical [TacRewrite] | |
tactical [TacNormalForm] | |
tactical [TacCut] | |
tactical [TacFilter] | |
tactical [TacLemma] | |
tactical [TacInstance] | |
tactical [TacHavoc.Validity] | |
tactical [TacHavoc.Separated] | |
tactical [TacHavoc.Havoc] | |
tactical [TacUnfold] | |
tactical [TacCompound] | |
tactical [TacArray] | |
tactical [TacRange] | |
tactical [TacChoice.Contrapose] | |
tactical [TacChoice.Absurd] | |
tactical [TacChoice.Choice] | |
tactical [TacSplit] | |
tactical [WpPropId] | |
tactical [Wp.WpPropId] | |
target [WpAnnot] | |
tau [Matrix] | |
tau_of_chunk [Sigs.Chunk] |
The type of data hold in a chunk.
|
tau_of_chunk [Wp.Sigs.Chunk] |
The type of data hold in a chunk.
|
tau_of_comp [Lang] | |
tau_of_comp [Wp.Lang] | |
tau_of_ctype [Lang] | |
tau_of_ctype [Wp.Lang] | |
tau_of_field [Lang] | |
tau_of_field [Wp.Lang] | |
tau_of_float [Cfloat] |
with respect to model
|
tau_of_float [Wp.Cfloat] |
with respect to model
|
tau_of_lfun [Lang] | |
tau_of_lfun [Wp.Lang] | |
tau_of_ltype [Lang] | |
tau_of_ltype [Wp.Lang] | |
tau_of_object [Lang] | |
tau_of_object [Wp.Lang] | |
tau_of_record [Lang] | |
tau_of_record [Wp.Lang] | |
tau_of_return [Lang] | |
tau_of_return [Wp.Lang] | |
tau_of_set [Vset] | |
tau_of_set [Wp.Vset] | |
tau_of_var [Lang.F] | |
tau_of_var [Wp.Lang.F] | |
term [LogicCompiler.Make] | |
term [Sigs.LogicSemantics] |
Compile a term expression.
|
term [Repr] | |
term [Wp.LogicCompiler.Make] | |
term [Wp.Sigs.LogicSemantics] |
Compile a term expression.
|
term [Wp.Repr] | |
test [Mcfg.S] | |
test [Wp.Mcfg.S] | |
timeout [ProverTask] | |
timeout [VCS] | |
timeout [Wp.ProverTask] | |
timeout [Wp.VCS] | |
title [ProofEngine] | |
title [Why3Provers] | |
title_of_mode [VCS] | |
title_of_mode [Wp.VCS] | |
title_of_prover [VCS] | |
title_of_prover [Wp.VCS] | |
to_addr [MemLoader.Model] | |
to_cint [Cint] |
Raises
Not_found if not.
|
to_cint [Wp.Cint] |
Raises
Not_found if not.
|
to_condition [CfgCompiler.Cfg.P] | |
to_condition [Wp.CfgCompiler.Cfg.P] | |
to_integer [Cint] | |
to_integer [Wp.Cint] | |
to_logic [Clabels] | |
to_logic [Wp.Clabels] | |
to_region_pointer [MemLoader.Model] | |
token [Script] | |
top [Letify.Ground] | |
tracelog [Register] | |
trans [Filter_axioms] | |
tree_context [ProofEngine] | |
trigger [LogicCompiler.Make] | |
trigger [Wp.LogicCompiler.Make] | |
trivial [Wpo.GOAL] | |
trivial [Conditions] |
empty implies true
|
trivial [Wp.Wpo.GOAL] | |
trivial [Wp.Conditions] |
empty implies true
|
try_sequence [Register] | |
type_id [Lang] | |
type_id [Wp.Lang] | |
typeof [Lang.F] |
Try to extract a type of term.
|
typeof [Layout.Offset] | |
typeof [Wp.Lang.F] |
Try to extract a type of term.
|
typeof_chain [Layout.Offset] | |
U | |
unchanged [Sigs.CodeSemantics] |
Express that a given variable has the same value in two memory states.
|
unchanged [Wp.Sigs.CodeSemantics] |
Express that a given variable has the same value in two memory states.
|
union [Sigs.Sigma] |
Same as
Chunk.Set.union
|
union [Cvalues.Logic] | |
union [Vset] | |
union [Splitter] | |
union [Passive] | |
union [Layout.Chunk] | |
union [Wp.Sigs.Sigma] |
Same as
Chunk.Set.union
|
union [Wp.Vset] | |
union [Wp.Splitter] | |
union [Wp.Passive] | |
union [Set.S] |
Set union.
|
union [Map.S] | union f m1 m2 computes a map whose keys is the union of keys
of m1 and of m2 .
|
union_map [Layout.Chunk] | |
unknown [VCS] | |
unknown [Wp.VCS] | |
unmark [Splitter] |
erase all tags
|
unmark [Wp.Splitter] |
erase all tags
|
unreachable_if_valid [WpPropId] |
Stmt that is unreachable in case the PO is valid.
|
unreachable_if_valid [Wp.WpPropId] |
Stmt that is unreachable in case the PO is valid.
|
unreachable_nodes [Cil2cfg] | |
unsupported [Wp_error] | |
update [GuiPanel] | |
update [WpContext.Registry] |
set current value, with no protection
|
update [Context] |
Modification of the current value
|
update [Wp.WpContext.Registry] |
set current value, with no protection
|
update [Wp.Context] |
Modification of the current value
|
update_cond [Conditions] |
Updates the condition of a step and merges
descr , deps and warn
|
update_cond [Wp.Conditions] |
Updates the condition of a step and merges
descr , deps and warn
|
update_symbol [Definitions] | |
update_symbol [Wp.Definitions] | |
updates [Pcfg] | |
updates [Mstate] | |
updates [Sigs.Model] |
Try to interpret a sequence of states into updates.
|
updates [Wp.Pcfg] | |
updates [Wp.Mstate] | |
updates [Wp.Sigs.Model] |
Try to interpret a sequence of states into updates.
|
use [Layout.Alias] | |
use_assigns [Mcfg.S] | use_assigns env hid kind assgn goal performs the havoc on the goal.
|
use_assigns [Wp.Mcfg.S] | use_assigns env hid kind assgn goal performs the havoc on the goal.
|
V | |
val_of_exp [Sigs.CodeSemantics] |
Compile an expression as a term.
|
val_of_exp [Wp.Sigs.CodeSemantics] |
Compile an expression as a term.
|
val_of_term [Sigs.LogicSemantics] |
Same as
term above but reject any set of locations.
|
val_of_term [Wp.Sigs.LogicSemantics] |
Same as
term above but reject any set of locations.
|
valid [VCS] | |
valid [Sigs.Model] |
Return the formula that tests if a memory state is valid
(according to
Sigs.acs ) in the given memory state at the given
segment.
|
valid [Cvalues.Logic] | |
valid [Wp.VCS] | |
valid [Wp.Sigs.Model] |
Return the formula that tests if a memory state is valid
(according to
Wp.Sigs.acs ) in the given memory state at the given
segment.
|
validate [ProofEngine] | |
value [Sigs.Sigma] |
Same as
Lang.F.e_var of get .
|
value [Cvalues.Logic] | |
value [Wp.Sigs.Sigma] |
Same as
Lang.F.e_var of get .
|
vanti [TacFilter] | |
vars [Sigs.LogicSemantics] |
Qed variables appearing in a region expression.
|
vars [Sigs.Model] |
Return the logic variables from which the given location depend on.
|
vars [Vset] | |
vars [Definitions.Trigger] | |
vars [Lang.F] |
Constant time
|
vars [Wp.Sigs.LogicSemantics] |
Qed variables appearing in a region expression.
|
vars [Wp.Sigs.Model] |
Return the logic variables from which the given location depend on.
|
vars [Wp.Vset] | |
vars [Wp.Definitions.Trigger] | |
vars [Wp.Lang.F] |
Constant time
|
vars_hyp [Conditions] |
Pre-computed and available in constant time.
|
vars_hyp [Wp.Conditions] |
Pre-computed and available in constant time.
|
vars_seq [Conditions] |
At the cost of the union of hypotheses and goal.
|
vars_seq [Wp.Conditions] |
At the cost of the union of hypotheses and goal.
|
varsp [Lang.F] |
Constant time
|
varsp [Wp.Lang.F] |
Constant time
|
verdict [VCS] | |
verdict [Wp.VCS] | |
version [Why3Provers] | |
very_strange_loops [Cil2cfg] |
detect is there are natural loops where we didn't manage to compute
back edges (see
mark_loops ).
|
visible [Pcfg] | |
visible [Wp.Pcfg] | |
vmax [TacRange] | |
vmin [TacRange] | |
volatile [Cvalues] |
Check if a volatile access must be properly modelled or ignored.
|
vset [Cvalues.Logic] | |
W | |
warnings [Wpo] | |
warnings [Wp.Wpo] | |
wg_status [GuiProver] | |
with_current_loc [Context] | |
with_current_loc [Wp.Context] | |
without_assume [Lang] | |
without_assume [Wp.Lang] | |
wkey_smoke [Register] | |
wp_iter_model [Register] | |
wp_print_memory_context [Register] | |
wp_warn_memory_context [Register] | |
wrap [TacInstance] | |
writes [CfgCompiler.Cfg.E] |
as defined by S.writes
|
writes [Sigs.Sigma] | writes s indicates which chunks are new in s.post compared
to s.pre .
|
writes [Wp.CfgCompiler.Cfg.E] |
as defined by S.writes
|
writes [Wp.Sigs.Sigma] | writes s indicates which chunks are new in s.post compared
to s.pre .
|