|
( * ) [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] |
|
(>) [Wp.Lang.N] |
|
(>=) [Lang.N] |
|
(>=) [Wp.Lang.N] |
|
(@-) [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 [Map.S] |
add x y m returns a map containing the same bindings as
m , plus a binding of x to y .
|
add [Set.S] |
add x s returns a set containing all elements of s ,
plus x .
|
add [Hashtbl.S] |
|
add [Wp.Lang.F.Subst] |
|
add [Wp.Warning] |
|
add [FCMap.S] |
add x y m returns a map containing the same bindings as
m , plus a binding of x to y .
|
add_alias [LogicBuiltins] |
|
add_alias [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_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_fct_bhv_pre [WpStrategy] |
Add the preconditions of the behavior :
if impl_assumes , add b_assumes => b_requires
else add both the b_requires and the b_assumes
|
add_prop_fct_post [WpStrategy] |
|
add_prop_fct_pre [WpStrategy] |
Add the predicate as a function precondition.
|
add_prop_fct_pre_bhv [WpStrategy] |
|
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] |
|
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] |
|
append [Wp.Conditions] |
|
append_after [Parameter_sig.List] |
append a list at the end of the current state
|
append_before [Parameter_sig.List] |
append a list in front of the current state
|
apply [Mstate] |
|
apply [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.
|
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] |
|
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] |
|
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.
|
bindings [FCMap.S] |
Return the list of all bindings of the given map.
|
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.
|
blocks_closed_by_edge [Cil2cfg] |
|
blsl [Cint] |
|
blsl [Wp.Cint] |
|
blsr [Cint] |
|
blsr [Wp.Cint] |
|
bnot [Cint] |
|
bnot [Wp.Cint] |
|
bool_and [Cvalues] |
|
bool_eq [Cvalues] |
|
bool_leq [Cvalues] |
|
bool_lt [Cvalues] |
|
bool_neq [Cvalues] |
|
bool_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] |
|
branch [Letify.Ground] |
|
branch [Wp.CfgCompiler.Cfg] |
Structurally corresponds to an if-then-else control-flow.
|
branch [Wp.Conditions] |
|
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.
|
bundle [Pcond] |
|
bundle [Conditions] |
|
bundle [Wp.Pcond] |
|
bundle [Wp.Conditions] |
|
bxor [Cint] |
|
bxor [Wp.Cint] |
|
C |
c_bool [Ctypes] |
Returns the type of int
|
c_bool [Wp.Ctypes] |
Returns the type of int
|
c_char [Ctypes] |
Returns the type of char
|
c_char [Wp.Ctypes] |
Returns the type of char
|
c_float [Ctypes] |
Conforms to
|
c_float [Wp.Ctypes] |
Conforms to
|
c_int [Ctypes] |
Conforms to
|
c_int [Wp.Ctypes] |
Conforms to
|
c_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 [Map.S] |
Return the number of bindings of a map.
|
cardinal [Set.S] |
Return the number of elements of a set.
|
cardinal [FCMap.S] |
Return the number of bindings of a map.
|
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 .
|
checked [VCS] |
|
checked [Wp.VCS] |
|
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 [Map.S] |
Return one binding of the given map, or raise Not_found if
the map is empty.
|
choose [Set.S] |
Return one element of the given set, or raise Not_found if
the set is empty.
|
choose [Wp.VCS] |
|
choose [Wp.Sigs.Sigma] |
Make the union of each sigma, choosing the minimal variable
in case of conflict.
|
choose [FCMap.S] |
Return one binding of the given map, or raise Not_found if
the map is empty.
|
choose_opt [Map.S] |
Return one binding of the given map, or None if
the map is empty.
|
choose_opt [Set.S] |
Return one element of the given set, or None if
the set 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 [Map.S] |
Total ordering between maps.
|
compare [Set.S] |
Total ordering between sets.
|
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 [FCMap.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] |
|
compare_ptr_conflated [Wp.Ctypes] |
|
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] |
|
concat [Wp.CfgCompiler.Cfg] |
The concatenation is the intersection of all
possible collection of traces from each cfg.
|
concat [Wp.Conditions] |
|
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 [Factory] |
|
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.Factory] |
|
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_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 [LogicBuiltins] |
Create a new driver.
|
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.LogicBuiltins] |
Create a new driver.
|
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_result [Register] |
|
do_wpo_start [Register] |
|
do_wpo_stat [Register] |
|
do_wpo_success [Register] |
|
do_wpo_wait [Register] |
|
domain [MemLoader.Model] |
|
domain [Conditions] |
|
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] |
|
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.
|
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 [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] |
|
either [Wp.CfgCompiler.Cfg] |
Structurally corresponds to an arbitrary choice among the different
possible executions.
|
either [Wp.Conditions] |
|
elements [Vlist] |
|
elements [Set.S] |
Return the list of all elements of the given set.
|
emit [Warning] |
Emit a warning in current context.
|
emit [Wp.Warning] |
Emit a warning in current context.
|
empty [Conditions] |
|
empty [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 [Map.S] |
The empty map.
|
empty [Set.S] |
The empty set.
|
empty [Wp.Conditions] |
|
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 [FCMap.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] |
|
epsilon [Lang] |
|
epsilon [Rformat] |
|
epsilon [Wp.Lang] |
|
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 [Map.S] |
equal cmp m1 m2 tests whether the maps m1 and m2 are
equal, that is, contain equal keys and associate them with
equal data.
|
equal [Set.S] |
equal s1 s2 tests whether the sets s1 and s2 are
equal, that is, contain equal elements.
|
equal [Wp.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 [FCMap.S] |
equal cmp m1 m2 tests whether the maps m1 and m2 are
equal, that is, contain equal keys and associate them with
equal data.
|
equal [Wp.Clabels] |
|
equal [Wp.Ctypes.AinfoComparable] |
|
equal [Wp.Ctypes] |
|
equal_array [Cvalues] |
|
equal_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] |
|
exist_intro [Wp.Conditions] |
|
exists [ProofSession] |
|
exists [Splitter] |
|
exists [Map.S] |
exists p m checks if at least one binding of the map
satisfies the predicate p .
|
exists [Set.S] |
exists p s checks if at least one element of
the set satisfies the predicate p .
|
exists [Wp.Splitter] |
|
exists [FCMap.S] |
exists p m checks if at least one binding of the map
satisfy the predicate p .
|
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] |
|
extract [Conditions] |
|
extract [Letify.Defs] |
|
extract [Wp.Conditions] |
|
F |
f32 [Cfloat] |
|
f32 [Wp.Cfloat] |
|
f64 [Cfloat] |
|
f64 [Wp.Cfloat] |
|
f_addr_of_int [MemMemory] |
Physical address
|
f_base [MemMemory] |
|
f_bits [Ctypes] |
size in bits
|
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 [Map.S] |
filter p m returns the map with all the bindings in m
that satisfy predicate p .
|
filter [Set.S] |
filter p s returns the set of all elements in s
that satisfy predicate p .
|
filter [Wp.Filtering] |
|
filter [Wp.Conditions] |
|
filter [Wp.Splitter] |
|
filter [FCMap.S] |
filter p m returns the map with all the bindings in m
that satisfy predicate p .
|
filter_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 [Why3Provers] |
|
find [Map.S] |
find x m returns the current binding of x in m ,
or raises Not_found if no such binding exists.
|
find [Set.S] |
find x s returns the element of s equal to x (according
to Ord.compare ), or raise Not_found if no such element
exists.
|
find [Hashtbl.S] |
|
find [Wp.Pcfg] |
|
find [Wp.Cfloat] |
|
find [Wp.WpContext.Registry] |
|
find [FCMap.S] |
find x m returns the current binding of x in m ,
or raises Not_found if no such binding exists.
|
find_all [Cil2cfg.HEsig] |
|
find_all [Hashtbl.S] |
|
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 [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_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_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_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 [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_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_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_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 [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_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 [Hashtbl.S] |
|
find_opt [FCMap.S] |
find x m returns the current binding of x in m ,
or return 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 [Map.S] |
fold f m a computes (f kN dN ... (f k1 d1 a)...) ,
where k1 ... kN are the keys of all bindings in m
(in increasing order), and d1 ... dN are the associated data.
|
fold [Set.S] |
fold f s a computes (f xN ... (f x2 (f x1 a))...) ,
where x1 ... xN are the elements of s , in increasing order.
|
fold [Hashtbl.S] |
|
fold [Wp.Splitter] |
|
fold [FCMap.S] |
fold f m a computes (f kN dN ... (f k1 d1 a)...) ,
where k1 ... kN are the keys of all bindings in m
(in increasing order), and d1 ... dN are the associated data.
|
fold_bhv_post_cond [WpStrategy] |
apply f_normal on the Normal postconditions,
f_exits on the Exits postconditions, and warn on the others.
|
fold_nodes [Cil2cfg] |
iterators
|
fopp [Cfloat] |
|
fopp [Wp.Cfloat] |
|
for_all [Splitter] |
|
for_all [Map.S] |
for_all p m checks if all the bindings of the map
satisfy the predicate p .
|
for_all [Set.S] |
for_all p s checks if all elements of the set
satisfy the predicate p .
|
for_all [Wp.Splitter] |
|
for_all [FCMap.S] |
for_all p m checks if all the bindings of the map
satisfy the predicate p .
|
forall_intro [Conditions] |
Predicates
|
forall_intro [Wp.Conditions] |
Predicates
|
fork [ProofEngine] |
|
formal [LogicCompiler.Make] |
|
formal [Clabels] |
|
formal [Wp.LogicCompiler.Make] |
|
formal [Wp.Clabels] |
|
forward [ProofEngine] |
|
forward [Letify.Ground] |
|
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 [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_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] |
|
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_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_variables [Lang] |
|
get_variables [Wp.Lang] |
|
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.
|
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 [Cvalues] |
|
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_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 [LogicBuiltins] |
Reset the context to a newly created driver
|
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.LogicBuiltins] |
Reset the context to a newly created driver
|
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 [Set.S] |
Set intersection.
|
inter [Wp.Vset] |
|
intersect [Conditions] |
|
intersect [Lang.F] |
|
intersect [Wp.Conditions] |
|
intersect [Wp.Lang.F] |
|
intersectp [Lang.F] |
|
intersectp [Wp.Lang.F] |
|
introduction [Conditions] |
Performs existential, universal and hypotheses introductions
|
introduction [Wp.Conditions] |
Performs existential, universal and hypotheses introductions
|
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] |
|
intros [Wp.Conditions] |
|
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_computing [VCS] |
|
is_computing [Wp.VCS] |
|
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 [Map.S] |
Test whether a map is empty or not.
|
is_empty [Set.S] |
Test whether a set is empty or not.
|
is_empty [Wp.Conditions] |
No step at all
|
is_empty [Wp.Vset] |
|
is_empty [Wp.Passive] |
|
is_empty [FCMap.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_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_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 [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_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_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] |
|
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] |
|
is_true [Conditions] |
Only true or empty steps
|
is_true [Cvalues] |
p ? 1 : 0
|
is_true [Lang.F] |
Constant time.
|
is_true [Wp.Conditions] |
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_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 [Map.S] |
iter f m applies f to all bindings in map m .
|
iter [Set.S] |
iter f s applies f in turn to all elements of s .
|
iter [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 [FCMap.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_assigns [NormAtLabels] |
|
labels_loop_assigns [Wp.NormAtLabels] |
|
labels_loop_inv [NormAtLabels] |
|
labels_loop_inv [Wp.NormAtLabels] |
|
labels_predicate [NormAtLabels] |
|
labels_predicate [Wp.NormAtLabels] |
|
labels_stmt_assigns [NormAtLabels] |
|
labels_stmt_assigns [Wp.NormAtLabels] |
|
labels_stmt_post [NormAtLabels] |
|
labels_stmt_post [Wp.NormAtLabels] |
|
labels_stmt_pre [NormAtLabels] |
|
labels_stmt_pre [Wp.NormAtLabels] |
|
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] |
The internal list of steps
|
list [Wp.Conditions] |
The internal list of steps
|
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 [Map.S] |
map f m returns a map with same domain as m , where the
associated value a of all bindings of m has been
replaced by the result of the application of f to a .
|
map [Set.S] |
map f s is the set whose elements are f a0 ,f a1 ...
|
map [Wp.Vset] |
|
map [Wp.Splitter] |
|
map [FCMap.S] |
map f m returns a map with same domain as m , where the
associated value a of all bindings of m has been
replaced by the result of the application of f to a .
|
map_condition [Conditions] |
|
map_condition [Wp.Conditions] |
|
map_l2t [Cvalues.Logic] |
|
map_loc [Cvalues.Logic] |
|
map_logic [Cvalues] |
|
map_opp [Cvalues.Logic] |
|
map_opp [Vset] |
|
map_opp [Wp.Vset] |
|
map_sequence [Conditions] |
|
map_sequence [Wp.Conditions] |
|
map_sequent [Conditions] |
|
map_sequent [Wp.Conditions] |
|
map_sloc [Cvalues] |
|
map_step [Conditions] |
|
map_step [Wp.Conditions] |
|
map_t2l [Cvalues.Logic] |
|
map_value [Cvalues] |
|
mapi [Tactical] |
|
mapi [Wp.Tactical] |
|
mapi [Map.S] |
Same as Map.S.map , but the function receives as arguments both the
key and the associated value for each binding of the map.
|
mapi [FCMap.S] |
Same as FCMap.S.map , but the function receives as arguments both the
key and the associated value for each binding of the map.
|
mark [Splitter] |
|
mark [Wp.Splitter] |
|
mark_e [Lang.F] |
|
mark_e [Wp.Lang.F] |
|
mark_p [Lang.F] |
Returns a list of terms to be shared among all shared or marked subterms.
|
mark_p [Wp.Lang.F] |
Returns a list of terms to be shared among all shared or marked subterms.
|
marker [Lang.F] |
|
marker [Wp.Lang.F] |
|
mask_simplifier [Cint] |
|
mask_simplifier [Wp.Cint] |
|
matches [Footprint] |
Head match
|
matrix [Definitions] |
|
matrix [Wp.Definitions] |
|
max_binding [Map.S] |
|
max_binding [FCMap.S] |
|
max_binding_opt [Map.S] |
|
max_elt [Set.S] |
Same as Set.S.min_elt , but returns the largest element of the
given set.
|
max_elt [FCSet.S] |
Same as , but returns the largest element of the
given set.
|
max_elt_opt [Set.S] |
|
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 [Map.S] |
mem x m returns true if m contains a binding for x ,
and false otherwise.
|
mem [Set.S] |
mem x s tests whether x belongs to the set s .
|
mem [Hashtbl.S] |
|
mem [Wp.Sigs.Sigma] |
Whether a chunk has been assigned.
|
mem [Wp.WpContext.Generator] |
|
mem [Wp.WpContext.Registry] |
|
mem [FCMap.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] |
|
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 [Map.S] |
merge f m1 m2 computes a map whose keys is a subset of keys of m1
and of m2 .
|
merge [Wp.VCS] |
|
merge [Wp.Conditions] |
|
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 [FCMap.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] |
|
merge_list [Wp.Sigs.Sigma] |
|
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 [FCMap.S] |
Return the smallest binding of the given map
(with respect to the Ord.compare ordering), or raise
Not_found if the map is empty.
|
min_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 [FCSet.S] |
Return the smallest element of the given set
(with respect to the Ord.compare ordering), or raise
Not_found if the set is empty.
|
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_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 [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 [FCSet.S] |
nearest_elt_ge v s returns the smallest element of s that is
bigger or equal to v .
|
nearest_elt_le [FCSet.S] |
nearest_elt_le v s returns the largest element of s that is
smaller or equal to v .
|
negate [Cvalues] |
|
new_env [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] |
|
nil [Wp.Conditions] |
|
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] |
|
opened [ProofEngine] |
not proved
|
ordered [Vset] |
- limit : result when either parameter is None strict : if true , comparison is < instead of <=
|
ordered [Wp.Vset] |
- limit : result when either parameter is None strict : if true , comparison is < instead of <=
|
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_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 [Map.S] |
partition p m returns a pair of maps (m1, m2) , where
m1 contains all the bindings of s that satisfy the
predicate p , and m2 is the map with all the bindings of
s that do not satisfy p .
|
partition [Set.S] |
partition p s returns a pair of sets (s1, s2) , where
s1 is the set of all the elements of s that satisfy the
predicate p , and s2 is the set of all the elements of
s that do not satisfy p .
|
partition [FCMap.S] |
partition p m returns a pair of maps (m1, m2) , where
m1 contains all the bindings of s that satisfy the
predicate p , and m2 is the map with all the bindings of
s that do not satisfy p .
|
parts_of_id [WpPropId] |
get the 'part' information.
|
parts_of_id [Wp.WpPropId] |
get the 'part' information.
|
pattern [Footprint] |
Generate head footprint up to size
|
pending [ProofEngine] |
|
pending [ProofScript] |
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_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 [ProofSession] |
|
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_selection [Tactical] |
Debug only
|
pp_selection [Wp.Tactical] |
Debug only
|
pp_sloc [Cvalues] |
|
pp_status [ProofSession] |
|
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 [Why3Provers] |
|
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
|
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] |
not opened
|
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] |
|
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] |
|
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] |
|
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 [Map.S] |
remove x m returns a map containing the same bindings as
m , except for x which is unbound in the returned map.
|
remove [Set.S] |
remove x s returns a set containing all elements of s ,
except x .
|
remove [Hashtbl.S] |
|
remove [Wp.WpContext.Generator] |
|
remove [Wp.WpContext.Registry] |
|
remove [FCMap.S] |
remove x m returns a map containing the same bindings as
m , except for x which is unbound in the returned map.
|
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] |
|
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] |
|
seq_branch [Wp.Conditions] |
|
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_builtin_type [Lang] |
|
set_builtin_type [Wp.Lang] |
|
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 [Map.S] |
singleton x y returns the one-element map that contains a binding y
for x .
|
singleton [Set.S] |
singleton x returns the one-element set containing only x .
|
singleton [Wp.Vset] |
|
singleton [Wp.Splitter] |
|
singleton [FCMap.S] |
singleton x y returns the one-element map that contains a binding y
for x .
|
size [Conditions] |
|
size [Matrix] |
|
size [Wp.Conditions] |
|
sizeof [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] |
|
sort [Lang.F] |
Constant time
|
sort [Wp.Lang.F] |
Constant time
|
source_of_id [WpPropId] |
|
source_of_id [Wp.WpPropId] |
|
spawn [VC] |
Same as prove but schedule the tasks into the global server returned
by server function below.
|
spawn [ProverScript] |
|
spawn [Prover] |
|
spawn [ProverTask] |
Spawn all the tasks over the server and retain the first 'validated' one.
|
spawn [Wp.Prover] |
|
spawn [Wp.ProverTask] |
Spawn all the tasks over the server and retain the first 'validated' one.
|
spawn [Wp.VC] |
Same as prove but schedule the tasks into the global server returned
by server function below.
|
spawn_wp_proofs_iter [Register] |
|
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 [WpAnnot] |
splits a prop_id goals into prop_id parts for each sub-goals
|
split [Mcfg.Splitter] |
|
split [Wp.Auto] |
|
split [Wp.Tactical] |
|
split [Map.S] |
split x m returns a triple (l, data, r) , where
l is the map with all the bindings of m whose key
is strictly less than x ;
r is the map with all the bindings of m whose key
is strictly greater than x ;
data is None if m contains no binding for x ,
or Some v if m binds v to x .
|
split [Set.S] |
split x s returns a triple (l, present, r) , where
l is the set of elements of s that are
strictly less than x ;
r is the set of elements of s that are
strictly greater than x ;
present is false if s contains no element equal to x ,
or true if s contains an element equal to x .
|
split [Wp.Mcfg.Splitter] |
|
split [FCSet.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 [FCMap.S] |
split x m returns a triple (l, data, r) , where
l is the map with all the bindings of m whose key
is strictly less than x ;
r is the map with all the bindings of m whose key
is strictly greater than x ;
data is None if m contains no binding for x ,
or Some v if m binds v to x .
|
spy [Register] |
|
start_edge [Cil2cfg] |
get the starting edges
|
start_stmt_of_node [Cil2cfg] |
|
startof [Cvalues] |
Shift a location with 0-indices wrt to its array type
|
state [ProofEngine] |
|
state [Conditions] |
|
state [Mstate] |
|
state [Sigs.Model] |
Returns a memory state description from a memory environement.
|
state [Wp.Conditions] |
|
state [Wp.Mstate] |
|
state [Wp.Sigs.Model] |
Returns a memory state description from a memory environement.
|
stats [Hashtbl.S] |
|
status [ProofEngine] |
|
status [ProofScript] |
minimum of pending goals
|
status [ProofSession] |
|
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] |
|
step [Wp.Conditions] |
|
step_at [Conditions] |
Retrieve a step by id in the sequence.
|
step_at [Wp.Conditions] |
Retrieve a step by id in the sequence.
|
stepout [ProverTask] |
|
stepout [VCS] |
|
stepout [Wp.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 [Set.S] |
subset s1 s2 tests whether the set s1 is a subset of
the set s2 .
|
subset [Wp.Vset] |
|
subst [Conditions] |
Apply the atomic substitution recursively using Lang.F.p_subst f .
|
subst [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] |
|
trivial [Wp.Wpo.GOAL] |
|
trivial [Wp.Conditions] |
|
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 [Map.S] |
union f m1 m2 computes a map whose keys is the union of keys
of m1 and of m2 .
|
union [Set.S] |
Set union.
|
union [Wp.Sigs.Sigma] |
Same as Chunk.Set.union
|
union [Wp.Vset] |
|
union [Wp.Splitter] |
|
union [Wp.Passive] |
|
union_map [Layout.Chunk] |
|
unknown [VCS] |
|
unknown [Wp.VCS] |
|
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] |
|
variables [Lang] |
|
variables [Wp.Lang] |
|
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] |
|
vars_hyp [Wp.Conditions] |
|
vars_seq [Conditions] |
|
vars_seq [Wp.Conditions] |
|
varsp [Lang.F] |
Constant time
|
varsp [Wp.Lang.F] |
Constant time
|
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] |
|
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 .
|