( * ) [Lang.N] |
|
( * ) [Wp.Lang.N] |
|
( @* ) [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] |
|
(+) [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] | |
(=) [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 |
(@^) [Wp.StmtSemantics.Make] | Same as |
(mod) [Lang.N] |
|
(mod) [Wp.Lang.N] |
|
(||) [Lang.N] | |
(||) [Wp.Lang.N] | |
(~-) [Lang.N] |
|
(~-) [Wp.Lang.N] |
|
A | |
a_addr [MemMemory] | Constructor for |
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_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 [Wp.Lang.F.Subst] | |
add [Hashtbl.S] | |
add [Wp.Warning] | |
add [Set.S] |
|
add [Map.S] |
|
add_alias [LogicBuiltins] | |
add_alias [Region] | |
add_alias [Wp.LogicBuiltins] | |
add_all_axioms [WpStrategy] | |
add_assigns [Mcfg.S] | |
add_assigns [WpStrategy] | generic function to add an assigns property. |
add_assigns [Wp.Mcfg.S] | |
add_assigns_any [WpStrategy] | generic function to add a WriteAny assigns property. |
add_axiom [Mcfg.S] | |
add_axiom [WpStrategy] | |
add_axiom [Wp.Mcfg.S] | |
add_behavior [MemoryContext] | |
add_behavior [Wp.MemoryContext] | |
add_builtin [LogicBuiltins] | Add a new builtin. |
add_builtin [Wp.LogicBuiltins] | Add a new builtin. |
add_call_assigns_any [WpStrategy] | short cut to add a dynamic call |
add_call_assigns_hyp [WpStrategy] | shortcut to add a call assigns property as an hypothesis. |
add_composer [Tactical] | |
add_composer [Wp.Tactical] | |
add_ctor [LogicBuiltins] | |
add_ctor [Wp.LogicBuiltins] | |
add_definitions [Letify] |
|
add_fct_bhv_assigns_hyp [WpStrategy] | |
add_filter [Lang.F.Subst] | |
add_filter [Wp.Lang.F.Subst] | |
add_fun [Lang.F.Subst] | |
add_fun [Wp.Lang.F.Subst] | |
add_goal [Mcfg.S] | |
add_goal [Wp.Mcfg.S] | |
add_hook [Wprop.Indexed2] | Hooks are executed once at property creation |
add_hook [Wprop.Indexed] | Hooks are executed once at property creation |
add_hyp [Mcfg.S] | |
add_hyp [Wp.Mcfg.S] | |
add_invalid_proof [WpPropId] | add an invalid proof result ; can not revert a complete proof |
add_invalid_proof [Wp.WpPropId] | add an invalid proof result ; can not revert a complete proof |
add_library [LogicBuiltins] | Add a new library or update the dependencies of an existing one |
add_library [Wp.LogicBuiltins] | Add a new library or update the dependencies of an existing one |
add_logic [LogicBuiltins] | |
add_logic [Wp.LogicBuiltins] | |
add_loop_annots [WpStrategy] | |
add_loop_assigns_hyp [WpStrategy] | shortcut to add a loop assigns property as an hypothesis. |
add_map [Lang.F.Subst] | |
add_map [Wp.Lang.F.Subst] | |
add_node_annots [WpStrategy] |
|
add_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 [WpPropId] | accumulate in the proof the partial proof for this prop_id |
add_proof [Wp.WpPropId] | accumulate in the proof the partial proof for this prop_id |
add_prop [WpStrategy] | generic function to add a predicate property after normalisation. |
add_prop_assert [WpStrategy] | |
add_prop_call_post [WpStrategy] | Add a postcondition of a called function. |
add_prop_call_pre [WpStrategy] | |
add_prop_dead_call [WpStrategy] | Add Smoke Test for possibly dead call : (posts,exits) |
add_prop_dead_code [WpStrategy] | Add Smoke Test for possibly dead code |
add_prop_dead_loop [WpStrategy] | Add Smoke Test for loop |
add_prop_fct_bhv_pre [WpStrategy] | Add the preconditions of the behavior |
add_prop_fct_post [WpStrategy] | |
add_prop_fct_pre [WpStrategy] | Add the predicate as a function precondition. |
add_prop_fct_pre_bhv [WpStrategy] | |
add_prop_fct_smoke [WpStrategy] | Add Smoke Test behavior |
add_prop_loop_inv [WpStrategy] | |
add_prop_stmt_bhv_requires [WpStrategy] | Add all the |
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] |
|
add_seq [Hashtbl.S] | |
add_seq [Set.S] | Add the given elements to the set, in order. |
add_seq [Map.S] | Add the given bindings to the map, in order. |
add_specific_equality [ProverWhy3] | Equality used in the goal, simpler to prove than polymorphic equality |
add_step [Register] | |
add_stmt_spec_assigns_hyp [WpStrategy] | shortcut to add a stmt spec assigns property as an hypothesis. |
add_time [Register] | |
add_tmpnode [CfgCompiler.Cfg] | Set a node as temporary. |
add_tmpnode [Wp.CfgCompiler.Cfg] | Set a node as temporary. |
add_type [LogicBuiltins] | |
add_type [Wp.LogicBuiltins] | |
add_var [Lang.F] | |
add_var [Wp.Lang.F] | |
add_vars [Lang.F] | |
add_vars [Wp.Lang.F] | |
adt [Lang] | Must not be a builtin |
adt [Wp.Lang] | Must not be a builtin |
age [Wpo] | |
age [Wp.Wpo] | |
ainf [Cvalues] | Array lower-bound, ie `Some(0)` |
alias [Region] | |
alias [Layout.Alias] | |
alloc [Sigs.Model] | Allocates new chunk for the validity of variables. |
alloc [Wp.Sigs.Model] | Allocates new chunk for the validity of variables. |
alloc_domain [Plang] | |
alloc_domain [Wp.Plang] | |
alloc_e [Plang] | |
alloc_e [Wp.Plang] | |
alloc_hyp [Pcond] | |
alloc_hyp [Wp.Pcond] | |
alloc_p [Plang] | |
alloc_p [Wp.Plang] | |
alloc_seq [Pcond] | |
alloc_seq [Wp.Pcond] | |
alloc_xs [Plang] | |
alloc_xs [Wp.Plang] | |
alpha [Lang.F] | |
alpha [Lang] | freshen all variables |
alpha [Wp.Lang.F] | |
alpha [Wp.Lang] | freshen all variables |
always_initialized [Cvalues] | |
anchor [ProofEngine] | |
annots [CfgInfos] | |
append [Conditions] | Conjunction |
append [Wp.Conditions] | Conjunction |
append_after [Parameter_sig.List] | append a list at the end of the current state |
append_before [Parameter_sig.List] | append a list in front of the current state |
apply [Mstate] | |
apply [Sigs.Model] | Propagate a sequent substitution inside the memory state. |
apply [Cvalues.Logic] | |
apply [Passive] | |
apply [Wp.Mstate] | |
apply [Wp.Sigs.Model] | Propagate a sequent substitution inside the memory state. |
apply [Wp.Passive] | |
apply_add [Cvalues.Logic] | |
apply_assigns [Sigs.LogicAssigns] | Relates two memory states corresponding to an assigns clause with the specified set of locations. |
apply_assigns [Wp.Sigs.LogicAssigns] | Relates two memory states corresponding to an assigns clause with the specified set of locations. |
apply_sub [Cvalues.Logic] | |
are_equal [Lang.F] | Computes equality |
are_equal [Wp.Lang.F] | Computes equality |
are_selected_names [WpPropId] |
|
are_selected_names [Wp.WpPropId] |
|
arg [Strategy] | |
arg [Wp.Strategy] | |
array [Auto] | |
array [Wp.Auto] | |
array_dimensions [Ctypes] | Returns the list of dimensions the array consists of. |
array_dimensions [Wp.Ctypes] | Returns the list of dimensions the array consists of. |
array_size [Ctypes] | |
array_size [Wp.Ctypes] | |
as_atom [Cleaning] | |
as_have [Cleaning] | |
as_init [Cleaning] | |
as_type [Cleaning] | |
assign [Mcfg.S] | |
assign [Wp.Mcfg.S] | |
assigned [MemLoader.Make] | |
assigned [Sigs.Model] | Return a set of formula that express that two memory state are the same except at the given set of memory location. |
assigned [Sigs.Sigma] | Make chunks equal outside of some domain. |
assigned [Wp.Sigs.Model] | Return a set of formula that express that two memory state are the same except at the given set of memory location. |
assigned [Wp.Sigs.Sigma] | Make chunks equal outside of some domain. |
assigned_of_assigns [Sigs.LogicSemantics] | Computes the region assigned by an assigns clause. |
assigned_of_assigns [Wp.Sigs.LogicSemantics] | Computes the region assigned by an assigns clause. |
assigned_of_froms [Sigs.LogicSemantics] | Computes the region assigned by a list of froms. |
assigned_of_froms [Wp.Sigs.LogicSemantics] | Computes the region assigned by a list of froms. |
assigned_of_lval [Sigs.LogicSemantics] | Computes the region assigned by a list of froms. |
assigned_of_lval [Wp.Sigs.LogicSemantics] | Computes the region assigned by a list of froms. |
assigns [StmtSemantics.Make] | |
assigns [Wp.StmtSemantics.Make] | |
assigns_info_id [WpPropId] | |
assigns_info_id [Wp.WpPropId] | |
assigns_upper_bound [WpStrategy] | |
assume [StmtSemantics.Make] | |
assume [CfgCompiler.Cfg] | Represents execution traces |
assume [Conditions] | Assumes a predicate in the specified section, with the specified decorations. |
assume [Letify.Sigma] | |
assume [Lang] | |
assume [Wp.StmtSemantics.Make] | |
assume [Wp.CfgCompiler.Cfg] | Represents execution traces |
assume [Wp.Conditions] | Assumes a predicate in the specified section, with the specified decorations. |
assume [Wp.Lang] | |
assume_ [StmtSemantics.Make] | |
assume_ [Wp.StmtSemantics.Make] | |
asup [Cvalues] | Array upper-bound, ie `Some(n-1)` |
at [Tactical] | |
at [Pcfg] | |
at [Wp.Tactical] | |
at [Wp.Pcfg] | |
at_closure [Conditions] | register a transformation applied just before close |
at_closure [Wp.Conditions] | register a transformation applied just before close |
atype [Lang] | |
atype [Wp.Lang] | |
auto_range [Auto] | |
auto_range [Wp.Auto] | |
auto_split [Auto] | |
auto_split [Wp.Auto] | |
autofit [VCS] | Result that fits the default configuration |
autofit [Wp.VCS] | Result that fits the default configuration |
automaton [StmtSemantics.Make] | |
automaton [Wp.StmtSemantics.Make] | |
axiomatic [Definitions] | |
axiomatic [LogicUsage] | |
axiomatic [Wp.Definitions] | |
axiomatic [Wp.LogicUsage] | |
B | |
backtrack [ProverSearch] | |
backward [Letify.Ground] | |
band [Cint] | |
band [Wp.Cint] | |
bar [Wpo] | |
bar [Wp.Wpo] | |
base_addr [Sigs.Model] | Return the memory location of the base address of a given memory location. |
base_addr [Wp.Sigs.Model] | Return the memory location of the base address of a given memory location. |
base_offset [Sigs.Model] | Return the offset of the location, in bytes, from its base_addr. |
base_offset [Wp.Sigs.Model] | Return the offset of the location, in bytes, from its base_addr. |
basename [Lang.F] | |
basename [LogicUsage] | Trims the original name |
basename [WpContext.IData] | |
basename [Ctypes] | |
basename [Wp.Lang.F] | |
basename [Wp.WpContext.IData] | |
basename [Wp.LogicUsage] | Trims the original name |
basename [Wp.Ctypes] | |
basename_of_chunk [Sigs.Chunk] | Used when generating fresh variables for a chunk. |
basename_of_chunk [Wp.Sigs.Chunk] | Used when generating fresh variables for a chunk. |
behavior_name_of_strategy [WpStrategy] | |
best [VCS] | |
best [Wp.VCS] | |
bind [ProofEngine] | |
bind [StmtSemantics.Make] | |
bind [Letify] |
|
bind [Passive] | |
bind [Context] | Performs the job with local context bound to local value. |
bind [Wp.StmtSemantics.Make] | |
bind [Wp.Passive] | |
bind [Wp.Context] | Performs the job with local context bound to local value. |
bindings [Map.S] | Return the list of all bindings of the given map. |
bit_test [Cint] | |
bit_test [Wp.Cint] | |
bits_sizeof_array [Ctypes] | |
bits_sizeof_array [Wp.Ctypes] | |
bits_sizeof_comp [Ctypes] | |
bits_sizeof_comp [Wp.Ctypes] | |
bits_sizeof_object [Ctypes] | |
bits_sizeof_object [Wp.Ctypes] | |
block_length [Sigs.Model] | Returns the length (in bytes) of the allocated block containing the given location. |
block_length [Wp.Sigs.Model] | Returns the length (in bytes) of the allocated block containing the given location. |
block_scope_for_edge [Cil2cfg] | |
blsl [Cint] | |
blsl [Wp.Cint] | |
blsr [Cint] | |
blsr [Wp.Cint] | |
bnot [Cint] | |
bnot [Wp.Cint] | |
body [CfgInfos] | |
bool_and [Cvalues] | |
bool_eq [Cvalues] | |
bool_leq [Cvalues] | |
bool_lt [Cvalues] | |
bool_neq [Cvalues] | |
bool_of_int [Cmath] | |
bool_or [Cvalues] | |
bool_val [Cvalues] | |
bootstrap_logic [LogicCompiler.Make] | |
bootstrap_logic [Wp.LogicCompiler.Make] | |
bootstrap_pred [LogicCompiler.Make] | |
bootstrap_pred [Wp.LogicCompiler.Make] | |
bootstrap_region [LogicCompiler.Make] | |
bootstrap_region [Wp.LogicCompiler.Make] | |
bootstrap_term [LogicCompiler.Make] | |
bootstrap_term [Wp.LogicCompiler.Make] | |
bor [Cint] | |
bor [Wp.Cint] | |
bound [ProofEngine] | |
bound_add [Vset] | |
bound_add [Wp.Vset] | |
bound_shift [Vset] | |
bound_shift [Wp.Vset] | |
bound_sub [Vset] | |
bound_sub [Wp.Vset] | |
bounds [Auto.Range] | |
bounds [Ctypes] | domain, bounds included |
bounds [Wp.Auto.Range] | |
bounds [Wp.Ctypes] | domain, bounds included |
branch [CfgCompiler.Cfg] | Structurally corresponds to an if-then-else control-flow. |
branch [Conditions] | Construct a branch bundle, with merging of all common parts. |
branch [Letify.Ground] | |
branch [Wp.CfgCompiler.Cfg] | Structurally corresponds to an if-then-else control-flow. |
branch [Wp.Conditions] | Construct a branch bundle, with merging of all common parts. |
branching [Pcfg] | |
branching [Wp.Pcfg] | |
break [Clabels] | |
break [Wp.Clabels] | |
build_prop_of_from [Mcfg.S] | build |
build_prop_of_from [Wp.Mcfg.S] | build |
build_wto [Interpreted_automata.Compute] | Extract an exit strategy from a component, i.e. |
build_wto_index_table [Interpreted_automata.Compute] | Compute the index table from a wto |
builtin_types [Lang] | |
builtin_types [Wp.Lang] | |
bundle [Conditions] | Closes the bundle and promote it into a well-formed sequence. |
bundle [Wp.Conditions] | Closes the bundle and promote it into a well-formed sequence. |
bxor [Cint] | |
bxor [Wp.Cint] | |
bytes_length_of_opaque_comp [Cvalues] | |
C | |
c_bool [Ctypes] | Returns the type of |
c_bool [Wp.Ctypes] | Returns the type of |
c_char [Ctypes] | Returns the type of |
c_char [Wp.Ctypes] | Returns the type of |
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] | |
calls [CfgInfos] | |
cancel [ProofEngine] | |
cardinal [TacInstance] | less than limit |
cardinal [Set.S] | Return the number of elements of a set. |
cardinal [Map.S] | Return the number of bindings of a map. |
case [Clabels] | |
case [Wp.Clabels] | |
cases [Splitter] | |
cases [Wp.Splitter] | |
cast [Sigs.CodeSemantics] | Applies a pointer cast or a conversion. |
cast [Sigs.Model] | Cast a memory location into another memory location. |
cast [Wp.Sigs.CodeSemantics] | Applies a pointer cast or a conversion. |
cast [Wp.Sigs.Model] | Cast a memory location into another memory location. |
cat_print_generated [Wp_parameters] | |
cat_print_generated [Wp.Wp_parameters] | |
catch [Warning] | Set up a context for the job. |
catch [Wp.Warning] | Set up a context for the job. |
catch_label_error [NormAtLabels] | |
catch_label_error [Wp.NormAtLabels] | |
cc_assign [RegionAccess] | |
cc_dims [Matrix] | Value of size variables |
cc_env [Matrix] | Dimension environment |
cc_fundec [RegionAccess] | |
cc_init [RegionAccess] | |
cc_instr [RegionAccess] | |
cc_lval [RegionAccess] | |
cc_pred [RegionAccess] | |
cc_read [RegionAccess] | |
cc_region [RegionAccess] | |
cc_spec [RegionAccess] | |
cc_tau [Matrix] | Type of matrix |
cc_term [RegionAccess] | |
cdomain [Cvalues] | |
cfg_kf [Cil2cfg] | |
cfg_of_strategy [WpStrategy] | |
cfg_spec_only [Cil2cfg] | returns |
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 |
checkbox [Wp.Tactical] | Unless specified, default is |
children [ProofEngine] | |
choice [Auto] | |
choice [StmtSemantics.Make] | Chain compiler in parallel, between labels |
choice [Wp.Auto] | |
choice [Wp.StmtSemantics.Make] | Chain compiler in parallel, between labels |
choose [VCS] | |
choose [Sigs.Sigma] | Make the union of each sigma, choosing the minimal variable in case of conflict. |
choose [Wp.VCS] | |
choose [Wp.Sigs.Sigma] | Make the union of each sigma, choosing the minimal variable in case of conflict. |
choose [Set.S] | Return one element of the given set, or raise |
choose [Map.S] | Return one binding of the given map, or raise |
choose_opt [Set.S] | Return one element of the given set, or |
choose_opt [Map.S] | Return one binding of the given map, or |
chunk [Region] | |
chunks [Region] | |
cint [Tactical] | |
cint [Wp.Tactical] | |
clean [Conditions] | |
clean [Wp.Conditions] | |
cleanup_cache [Cache] | |
clear [VC] | |
clear [CfgInfos] | |
clear [CfgAnnot] | |
clear [Wpo] | |
clear [Cil2cfg.HEsig] | |
clear [WpContext.Generator] | |
clear [WpContext.Registry] | |
clear [Context] | Clear the current value. |
clear [Wp.Wpo] | |
clear [Wp.VC] | |
clear [Wp.WpContext.Generator] | |
clear [Wp.WpContext.Registry] | |
clear [Hashtbl.S] | |
clear [Wp.Context] | Clear the current value. |
clear_result [Cache] | |
clear_results [Wpo] | |
clear_results [Wp.Wpo] | |
clear_scheduled [Register] | |
cloc [Sigs.CodeSemantics] | Interpret a value as a location. |
cloc [Wp.Sigs.CodeSemantics] | Interpret a value as a location. |
close [Script] | |
close [Conditions] | With free variables quantified. |
close [Mcfg.S] | |
close [Wp.Conditions] | With free variables quantified. |
close [Wp.Mcfg.S] | |
cluster [MemLoader] | |
cluster [Cstring] | The cluster where all strings are defined. |
cluster [Definitions] | |
cluster [Region] | |
cluster [Wp.Cstring] | The cluster where all strings are defined. |
cluster [Wp.Definitions] | |
cluster_age [Definitions] | |
cluster_age [Wp.Definitions] | |
cluster_compare [Definitions] | |
cluster_compare [Wp.Definitions] | |
cluster_id [Definitions] | Unique |
cluster_id [Wp.Definitions] | Unique |
cluster_position [Definitions] | |
cluster_position [Wp.Definitions] | |
cluster_title [Definitions] | |
cluster_title [Wp.Definitions] | |
cmdline_run [Register] | |
cmp_prover [VCS] | |
cmp_prover [Wp.VCS] | |
code_lit [Cfloat] | |
code_lit [Wp.Cfloat] | |
codomain [Letify.Sigma] | |
command [VC] | Run the provers with the command-line interface. |
command [Rformat] | |
command [Wp.VC] | Run the provers with the command-line interface. |
commit [ProofEngine] | |
comp [Lang] | |
comp [Wp.Lang] | |
comp_id [Lang] | |
comp_id [Wp.Lang] | |
comp_init [Lang] | |
comp_init [Wp.Lang] | |
comp_init_id [Lang] | |
comp_init_id [Wp.Lang] | |
compare [VCS] | |
compare [Sigs.Chunk] | |
compare [LogicBuiltins] | |
compare [Matrix] | |
compare [Lang.F] | |
compare [RegionAnnot.Lpath] | |
compare [Layout.Value] | |
compare [Layout.Data] | |
compare [WpContext.Key] | |
compare [WpContext.Entries] | |
compare [WpContext.SCOPE] | |
compare [WpContext.MODEL] | |
compare [WpContext.S] | |
compare [Clabels.T] | |
compare [Ctypes.AinfoComparable] | |
compare [Ctypes] | |
compare [Warning] | |
compare [Why3Provers] | |
compare [Map.OrderedType] | A total ordering function over the keys. |
compare [Wp.VCS] | |
compare [Wp.Sigs.Chunk] | |
compare [Wp.LogicBuiltins] | |
compare [Wp.Lang.F] | |
compare [Wp.WpContext.Key] | |
compare [Wp.WpContext.Entries] | |
compare [Wp.WpContext.SCOPE] | |
compare [Wp.WpContext.MODEL] | |
compare [Wp.WpContext.S] | |
compare [Wp.Warning] | |
compare [Set.S] | Total ordering between sets. |
compare [Map.S] | Total ordering between maps. |
compare [Wp.Clabels.T] | |
compare [Wp.Ctypes.AinfoComparable] | |
compare [Wp.Ctypes] | |
compare_c_float [Ctypes] | |
compare_c_float [Wp.Ctypes] | |
compare_c_int [Ctypes] | |
compare_c_int [Wp.Ctypes] | |
compare_prop_id [WpPropId] | |
compare_prop_id [Wp.WpPropId] | |
compare_ptr_conflated [Ctypes] | same as |
compare_ptr_conflated [Wp.Ctypes] | same as |
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 [CfgWP.VCgen] | |
compile_lemma [Definitions] | |
compile_lemma [Wp.Definitions] | |
compile_wp [CfgWP.VCgen] | |
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 [CfgCalculus.Make] | |
compute [Auto.Range] | |
compute [Wpo.GOAL] | |
compute [Wpo] | |
compute [WpTarget] | |
compute [Filtering] | |
compute [Letify.Ground] | |
compute [RefUsage] | |
compute [LogicUsage] | To force computation |
compute [MemoryContext] | |
compute [AssignsCompleteness] | |
compute [Dyncall] | Forces computation of dynamic calls. |
compute [Wp.Wpo.GOAL] | |
compute [Wp.Wpo] | |
compute [Wp.Auto.Range] | |
compute [Wp.Filtering] | |
compute [Wp.AssignsCompleteness] | |
compute [Wp.RefUsage] | |
compute [Wp.LogicUsage] | To force computation |
compute [Wp.MemoryContext] | |
compute_auto [Register] | |
compute_call [WpGenerator] | |
compute_descr [Wpo.GOAL] | |
compute_descr [Wp.Wpo.GOAL] | |
compute_hypotheses [WpContext] | |
compute_hypotheses [Wp.WpContext] | |
compute_ip [WpGenerator] | |
compute_kf [WpGenerator] | |
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 [WpGenerator] | |
computer [WpGenerator] | |
computing [VCS] | |
computing [Wp.VCS] | |
concat [CfgCompiler.Cfg] | The concatenation is the intersection of all possible collection of traces from each cfg. |
concat [Conditions] | List conjunction |
concat [Wp.CfgCompiler.Cfg] | The concatenation is the intersection of all possible collection of traces from each cfg. |
concat [Wp.Conditions] | List conjunction |
concretize [Vset] | |
concretize [Wp.Vset] | |
cond [Sigs.CodeSemantics] | Evaluate the conditional expression on the given memory state. |
cond [Wp.Sigs.CodeSemantics] | Evaluate the conditional expression on the given memory state. |
condition [Tactical] | Apply process, but only after proving some condition |
condition [Conditions] | With free variables kept. |
condition [Wp.Tactical] | Apply process, but only after proving some condition |
condition [Wp.Conditions] | With free variables kept. |
conditions [Passive] | |
conditions [Wp.Passive] | |
config [Why3Provers] | |
configure [ProofScript] | |
configure [VCS] | |
configure [Sigs.Model] | Initializers to be run before using the model. |
configure [Cfloat] | |
configure [Cint] | |
configure [Context] | Apply global configure hooks, once per project/ast. |
configure [Why3Provers] | |
configure [Wp.VCS] | |
configure [Wp.Sigs.Model] | Initializers to be run before using the model. |
configure [Wp.Cfloat] | |
configure [Wp.Cint] | |
configure [Wp.Context] | Apply global configure hooks, once per project/ast. |
configure_driver [Factory] | |
configure_driver [Wp.Factory] | |
configure_ia [Sigs.Model] | Given an automaton, return a vertex's binder. |
configure_ia [Wp.Sigs.Model] | Given an automaton, return a vertex's binder. |
const [Mcfg.S] | |
const [Wp.Mcfg.S] | |
constant [Cvalues] | |
constant [LogicBuiltins] | |
constant [Lang.F] | |
constant [Ctypes] | |
constant [Wp.LogicBuiltins] | |
constant [Wp.Lang.F] | |
constant [Wp.Ctypes] | |
constant_exp [Cvalues] | |
constant_term [Cvalues] | |
context [Warning] | |
context [Wp.Warning] | |
context_pp [Lang.F] | Context used by pp_term, pp_pred, pp_var, ppvars for printing the term. |
context_pp [Wp.Lang.F] | Context used by pp_term, pp_pred, pp_var, ppvars for printing the term. |
continue [Clabels] | |
continue [Wp.Clabels] | |
contrapose [Auto] | |
contrapose [Wp.Auto] | |
convert [Cint] | Independent from model |
convert [Wp.Cint] | Independent from model |
copied [MemLoader.Make] | |
copied [Sigs.Model] | Return a set of equations that express a copy between two memory state. |
copied [Wp.Sigs.Model] | Return a set of equations that express a copy between two memory state. |
copied_init [MemLoader.Make] | |
copied_init [Sigs.Model] | Return a set of equations that express a copy of an initialized state between two memory state. |
copied_init [Wp.Sigs.Model] | Return a set of equations that express a copy of an initialized state between two memory state. |
copy [Sigs.Sigma] | Duplicate the environment. |
copy [Letify.Ground] | |
copy [Wp.Sigs.Sigma] | Duplicate the environment. |
copy [Hashtbl.S] | |
copy [Datatype.S] | Deep copy: no possible sharing between |
create [Generator] | |
create [Tactical.Fmap] | |
create [CfgCompiler.Cfg.E] | Bundle an equation with the sigma sequence that created it |
create [CfgCompiler.Cfg.T] | Bundle a term with the sigma sequence that created it. |
create [CfgCompiler.Cfg.P] | Bundle an equation with the sigma sequence that created it. |
create [CfgCompiler.Cfg.C] | Bundle an equation with the sigma sequence that created it. |
create [CfgCompiler.Cfg.Node] | |
create [Pcfg] | |
create [Mstate] | |
create [Sigs.Sigma] | Initially empty environment. |
create [Cleaning] | |
create [Letify.Split] | |
create [Cil2cfg.HEsig] | |
create [Region] | |
create [Warning] | |
create [Context] | Creates a new context with name |
create [Wp.Tactical.Fmap] | |
create [Wp.CfgCompiler.Cfg.E] | Bundle an equation with the sigma sequence that created it |
create [Wp.CfgCompiler.Cfg.T] | Bundle a term with the sigma sequence that created it. |
create [Wp.CfgCompiler.Cfg.P] | Bundle an equation with the sigma sequence that created it. |
create [Wp.CfgCompiler.Cfg.C] | Bundle an equation with the sigma sequence that created it. |
create [Wp.CfgCompiler.Cfg.Node] | |
create [Wp.Pcfg] | |
create [Wp.Mstate] | |
create [Wp.Sigs.Sigma] | Initially empty environment. |
create [Hashtbl.S] | |
create [Wp.Warning] | |
create [Wp.Context] | Creates a new context with name |
create_option [LogicBuiltins] |
|
create_option [Wp.LogicBuiltins] |
|
create_proof [WpPropId] | to be used only once for one of the related prop_id |
create_proof [Wp.WpPropId] | 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 |
decide [Wp.Lang.F] | Return |
decode [ProofScript] | |
def_into_axiom [Filter_axioms] | |
default [Factory] |
|
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] |
|
default [Wp.Clabels] | |
default_script_mode [Register] | |
define [Lang.F] | |
define [WpContext.Registry] | no redefinition ; circularity protected |
define [Wp.Lang.F] | |
define [Wp.WpContext.Registry] | no redefinition ; circularity protected |
define_lemma [Definitions] | |
define_lemma [Wp.Definitions] | |
define_symbol [Definitions] | |
define_symbol [Wp.Definitions] | |
define_type [Definitions] | |
define_type [Wp.Definitions] | |
defined [Context] | The current value is defined. |
defined [Wp.Context] | The current value is defined. |
definition [Auto] | |
definition [Wp.Auto] | |
defs [Lang.F] | |
defs [Wp.Lang.F] | |
delete_script_for [Proof] |
|
dependencies [LogicBuiltins] | Of external theories. |
dependencies [WpPropId] | |
dependencies [Wp.LogicBuiltins] | Of external theories. |
dependencies [Wp.WpPropId] | |
deprecated [Register] | |
deref [Layout.Cluster] | |
descr [Factory] | |
descr [Vset] | |
descr [LogicBuiltins] | |
descr [WpContext.MODEL] | |
descr [Wp.Factory] | |
descr [Wp.Vset] | |
descr [Wp.LogicBuiltins] | |
descr [Wp.WpContext.MODEL] | |
destruct [Tactical] | |
destruct [Wp.Tactical] | |
diff [Set.S] | Set difference: |
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 |
directory [Wp.WpContext] | Current model in |
disjoint [Vset] | |
disjoint [Layout.Chunk] | |
disjoint [Wp.Vset] | |
disjoint [Set.S] | Test if two sets are disjoint. |
dkey_builtins [Register] | |
dkey_cluster [ProverErgo] | |
dkey_logicusage [Register] | |
dkey_main [Register] | |
dkey_prover [Register] | |
dkey_raised [Register] | |
dkey_refusage [Register] | |
dkey_shell [VCS] | |
dkey_shell [Wp.VCS] | |
do_alias [Region] | |
do_cache_cleanup [Register] | |
do_list_scheduled [Register] | |
do_list_scheduled_result [Register] | |
do_progress [Register] | |
do_prover_detect [Register] | |
do_report_cache_usage [Register] | |
do_report_prover_stats [Register] | |
do_report_scheduled [Register] | |
do_report_steps [Register] | |
do_report_stopped [Register] | |
do_report_time [Register] | |
do_update_session [Register] | |
do_wp_print [Register] | |
do_wp_print_for [Register] | |
do_wp_proofs [Register] | |
do_wp_report [Register] | |
do_wpo_display [Register] | |
do_wpo_failed [Register] | |
do_wpo_result [Register] | |
do_wpo_smoke [Register] | |
do_wpo_start [Register] | |
do_wpo_stat [Register] | |
do_wpo_success [Register] | |
do_wpo_wait [Register] | |
domain [MemLoader.Make] | |
domain [Conditions] | Assumes a list of predicates in a |
domain [Sigs.LogicAssigns] | Memory footprint of a region. |
domain [Sigs.Model] | Compute the set of chunks that hold the value of an object with the given C-type. |
domain [Sigs.Sigma] | Footprint of a memory environment. |
domain [Letify.Defs] | |
domain [Letify.Sigma] | |
domain [Wp.Conditions] | Assumes a list of predicates in a |
domain [Wp.Sigs.LogicAssigns] | Memory footprint of a region. |
domain [Wp.Sigs.Model] | Compute the set of chunks that hold the value of an object with the given C-type. |
domain [Wp.Sigs.Sigma] | Footprint of a memory environment. |
doomed [CfgInfos] | |
doomed_if_valid [WpPropId] | Properties that are False-if-unreachable in case the PO is valid. |
doomed_if_valid [Wp.WpPropId] | Properties that are False-if-unreachable in case the PO is valid. |
downcast [Cint] | Dependent on model |
downcast [Wp.Cint] | Dependent on model |
driver [LogicBuiltins] | |
driver [Wp.LogicBuiltins] | |
dummy [Wpo.GOAL] | |
dummy [Definitions] | |
dummy [Wp.Wpo.GOAL] | |
dummy [Wp.Definitions] | |
dump [WpReached] | |
dump [Pcond] | |
dump [LogicBuiltins] | |
dump [RegionDump] | |
dump [RefUsage] | |
dump [LogicUsage] | Print on output |
dump [Wp.Pcond] | |
dump [Wp.LogicBuiltins] | |
dump [Wp.RefUsage] | |
dump [Wp.LogicUsage] | Print on output |
dump_bundle [Pcond] | |
dump_bundle [Wp.Pcond] | |
dump_env [CfgCompiler.Cfg] | |
dump_env [Wp.CfgCompiler.Cfg] | |
dump_sequence [Pcond] | |
dump_sequence [Wp.Pcond] | |
dump_strategies [Register] | |
dumper [CfgGenerator] | |
dumper [WpGenerator] | |
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 |
effect [Wp.CfgCompiler.Cfg] | Represents all execution trace |
either [CfgCompiler.Cfg] | Structurally corresponds to an arbitrary choice among the different possible executions. |
either [Conditions] | Construct a disjunction bundle, with merging of all common parts. |
either [Wp.CfgCompiler.Cfg] | Structurally corresponds to an arbitrary choice among the different possible executions. |
either [Wp.Conditions] | Construct a disjunction bundle, with merging of all common parts. |
elements [Vlist] | |
elements [Set.S] | Return the list of all elements of the given set. |
emit [Warning] | Emit a warning in current context. |
emit [Wp.Warning] | Emit a warning in current context. |
empty [Conditions] | empty sequence, equivalent to true assumption |
empty [Sigs.Sigma] | Same as |
empty [Letify.Defs] | |
empty [Letify.Sigma] | |
empty [Vset] | |
empty [Splitter] | |
empty [Passive] | |
empty [Mcfg.S] | |
empty [Layout.Chunk] | |
empty [MemoryContext] | |
empty [Wp.Conditions] | empty sequence, equivalent to true assumption |
empty [Wp.Sigs.Sigma] | Same as |
empty [Wp.Vset] | |
empty [Wp.Splitter] | |
empty [Wp.Passive] | |
empty [Wp.Mcfg.S] | |
empty [Wp.MemoryContext] | |
empty [Set.S] | The empty set. |
empty [Map.S] | The empty map. |
empty_acc [WpStrategy] | |
empty_assigns_info [WpPropId] | |
empty_assigns_info [Wp.WpPropId] | |
empty_env [StmtSemantics.Make] | |
empty_env [Wp.StmtSemantics.Make] | |
encode [ProofScript] | |
env [Lang.F] | |
env [Wp.Lang.F] | |
env_at [LogicCompiler.Make] | |
env_at [Sigs.LogicSemantics] | Returns a new environment where the current memory state is moved to to the corresponding label. |
env_at [Wp.LogicCompiler.Make] | |
env_at [Wp.Sigs.LogicSemantics] | Returns a new environment where the current memory state is moved to to the corresponding label. |
env_let [LogicCompiler.Make] | |
env_let [Wp.LogicCompiler.Make] | |
env_letp [LogicCompiler.Make] | |
env_letp [Wp.LogicCompiler.Make] | |
env_letval [LogicCompiler.Make] | |
env_letval [Wp.LogicCompiler.Make] | |
env_script_update [Register] | |
epsilon [Rformat] | |
eq_alias [Region] | |
eqmem [MemLoader.Model] | |
eqmem_forall [MemLoader.Model] | |
eqp [Lang.F] | |
eqp [Wp.Lang.F] | |
equal [CfgCompiler.Cfg.C] | |
equal [CfgCompiler.Cfg.Node] | |
equal [Mstate] | |
equal [Sigs.Chunk] | |
equal [Letify.Sigma] | |
equal [Vset] | |
equal [Lang.F] | Same as |
equal [RegionAnnot.Lpath] | |
equal [Layout.Value] | |
equal [Layout.Data] | |
equal [WpContext.SCOPE] | |
equal [WpContext.MODEL] | |
equal [WpContext.S] | |
equal [Clabels] | |
equal [Ctypes.AinfoComparable] | |
equal [Ctypes] | |
equal [Wp.CfgCompiler.Cfg.C] | |
equal [Wp.CfgCompiler.Cfg.Node] | |
equal [Wp.Mstate] | |
equal [Wp.Sigs.Chunk] | |
equal [Wp.Vset] | |
equal [Wp.Lang.F] | Same as |
equal [Wp.WpContext.SCOPE] | |
equal [Wp.WpContext.MODEL] | |
equal [Wp.WpContext.S] | |
equal [Set.S] |
|
equal [Map.S] |
|
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_obj [Wp.Sigs.CodeSemantics] | Same as |
equal_object [Cvalues] | |
equal_typ [Sigs.CodeSemantics] | Computes the value of |
equal_typ [Wp.Sigs.CodeSemantics] | Computes the value of |
equation [Cvalues] | |
error [Script] | |
error [Warning] | |
error [Wp.Warning] | |
eval_eq [Lang.F] | Same as |
eval_eq [Wp.Lang.F] | Same as |
eval_leq [Lang.F] | Same as |
eval_leq [Wp.Lang.F] | Same as |
eval_lt [Lang.F] | Same as |
eval_lt [Wp.Lang.F] | Same as |
eval_neq [Lang.F] | Same as |
eval_neq [Wp.Lang.F] | Same as |
exercised [Register] | |
exist_intro [Conditions] | Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively. |
exist_intro [Wp.Conditions] | Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively. |
exists [ProofSession] | |
exists [Splitter] | |
exists [Wp.Splitter] | |
exists [Set.S] |
|
exists [Map.S] |
|
exists [Parameter_sig.Set] | Is there some element satisfying the given predicate? |
exit [Clabels] | |
exit [Wp.Clabels] | |
exit_strategy [Interpreted_automata.Compute] | Output the automaton in dot format |
exit_strategy [Interpreted_automata] | Output the automaton in dot format |
exp [Sigs.CodeSemantics] | Evaluate the expression on the given memory state. |
exp [Wp.Sigs.CodeSemantics] | Evaluate the expression on the given memory state. |
export [Strategy] | |
export [Tactical] | Register and returns the tactical |
export [WpReport] | |
export [Vlist] | |
export [Wp.Strategy] | |
export [Wp.Tactical] | Register and returns the tactical |
export_decl [Mcfg.Export] | |
export_decl [Wp.Mcfg.Export] | |
export_goal [Mcfg.Export] | |
export_goal [Wp.Mcfg.Export] | |
export_json [WpReport] | |
export_section [Mcfg.Export] | |
export_section [Wp.Mcfg.Export] | |
extern_f [Lang] | balance just give a default when link is not specified |
extern_f [Wp.Lang] | balance just give a default when link is not specified |
extern_fp [Lang] | |
extern_fp [Wp.Lang] | |
extern_p [Lang] | |
extern_p [Wp.Lang] | |
extern_s [Lang] | |
extern_s [Wp.Lang] | |
extern_t [Lang] | |
extern_t [Wp.Lang] | |
extract [Conditions] | Computes a formulae equivalent to the bundle. |
extract [Letify.Defs] | |
extract [Wp.Conditions] | Computes a formulae equivalent to the bundle. |
F | |
f32 [Cfloat] | |
f32 [Wp.Cfloat] | |
f64 [Cfloat] | |
f64 [Wp.Cfloat] | |
f_addr_of_int [MemMemory] | Physical address |
f_base [MemMemory] | |
f_bits [Cint] | All bit-test functions |
f_bits [Ctypes] | size in bits |
f_bits [Wp.Cint] | All bit-test functions |
f_bits [Wp.Ctypes] | size in bits |
f_bitwised [Cint] | All except f_bit_positive |
f_bitwised [Wp.Cint] | All except f_bit_positive |
f_bytes [Ctypes] | size in bytes |
f_bytes [Wp.Ctypes] | size in bytes |
f_concat [Vlist] | |
f_cons [Vlist] | |
f_convert [Ctypes] | |
f_convert [Wp.Ctypes] | |
f_delta [Cfloat] | |
f_delta [Wp.Cfloat] | |
f_elt [Vlist] | |
f_epsilon [Cfloat] | |
f_epsilon [Wp.Cfloat] | |
f_global [MemMemory] | |
f_havoc [MemMemory] | |
f_iabs [Cmath] | |
f_int_of_addr [MemMemory] | Physical address |
f_iter [Ctypes] | |
f_iter [Wp.Ctypes] | |
f_land [Cint] | |
f_land [Wp.Cint] | |
f_lnot [Cint] | |
f_lnot [Wp.Cint] | |
f_lor [Cint] | |
f_lor [Wp.Cint] | |
f_lsl [Cint] | |
f_lsl [Wp.Cint] | |
f_lsr [Cint] | |
f_lsr [Wp.Cint] | |
f_lxor [Cint] | |
f_lxor [Wp.Cint] | |
f_memo [Ctypes] | memoized, not-projectified |
f_memo [Wp.Ctypes] | memoized, not-projectified |
f_model [Cfloat] | |
f_model [Wp.Cfloat] | |
f_name [Ctypes] | |
f_name [Wp.Ctypes] | |
f_nil [Vlist] | |
f_nth [Vlist] | |
f_null [MemMemory] | |
f_offset [MemMemory] | |
f_rabs [Cmath] | |
f_real_of_int [Cmath] | |
f_region [MemMemory] | |
f_repeat [Vlist] | |
f_set_init [MemMemory] | |
f_shift [MemMemory] | |
f_sqrt [Cmath] | |
fadd [Cfloat] | |
fadd [Wp.Cfloat] | |
failed [VCS] | |
failed [Wp.VCS] | |
fcstat [WpReport] | |
fdiv [Cfloat] | |
fdiv [Wp.Cfloat] | |
feq [Cfloat] | |
feq [Wp.Cfloat] | |
field [MemLoader.Model] | |
field [Mstate] | |
field [Sigs.Model] | Return the memory location obtained by field access from a given memory location. |
field [Cvalues.Logic] | |
field [Repr] | |
field [Lang] | |
field [Layout.Offset] | |
field [Wp.Mstate] | |
field [Wp.Sigs.Model] | Return the memory location obtained by field access from a given memory location. |
field [Wp.Repr] | |
field [Wp.Lang] | |
field_id [Lang] | |
field_id [Wp.Lang] | |
field_init_id [Lang] | |
field_init_id [Wp.Lang] | |
field_offset [Region] | |
field_offset [Layout.Offset] | |
field_offset [Ctypes] | |
field_offset [Wp.Ctypes] | |
fields [TacInstance] | |
fields_of_adt [Lang] | |
fields_of_adt [Wp.Lang] | |
fields_of_field [Lang] | |
fields_of_field [Wp.Lang] | |
fields_of_tau [Lang] | |
fields_of_tau [Wp.Lang] | |
file_goal [Wpo.DISK] | |
file_goal [Wp.Wpo.DISK] | |
file_kf [Wpo.DISK] | |
file_kf [Wp.Wpo.DISK] | |
file_logerr [Wpo.DISK] | |
file_logerr [Wp.Wpo.DISK] | |
file_logout [Wpo.DISK] | |
file_logout [Wp.Wpo.DISK] | |
filename_for_prover [VCS] | |
filename_for_prover [Wp.VCS] | |
filter [GuiProver] | |
filter [Auto] | |
filter [TacInstance] | |
filter [Script] | |
filter [Filtering] | |
filter [Conditions] | |
filter [Splitter] | |
filter [Wp.Auto] | |
filter [Wp.Filtering] | |
filter [Wp.Conditions] | |
filter [Wp.Splitter] | |
filter [Set.S] |
|
filter [Map.S] |
|
filter_hypotheses [Lang] | |
filter_hypotheses [Wp.Lang] | |
filter_map [Set.S] |
|
filter_map [Map.S] |
|
filter_map_inplace [Hashtbl.S] | |
filter_pred [Cleaning] | |
filter_status [WpPropId] | |
filter_status [Wp.WpPropId] | |
filter_type [Cleaning] | |
find [TacLemma] | |
find [Pcfg] | |
find [Letify.Sigma] | |
find [Cfloat] | |
find [Cil2cfg.HEsig] | |
find [WpContext.Registry] | |
find [Wp.Pcfg] | |
find [Wp.Cfloat] | |
find [Wp.WpContext.Registry] | |
find [Hashtbl.S] | |
find [Set.S] |
|
find [Map.S] |
|
find_all [Cil2cfg.HEsig] | |
find_all [Hashtbl.S] | |
find_fallback [Why3Provers] | |
find_first [Set.S] |
|
find_first [Map.S] |
|
find_first_opt [Set.S] |
|
find_first_opt [Map.S] |
|
find_last [Set.S] |
|
find_last [Map.S] |
|
find_last_opt [Set.S] |
|
find_last_opt [Map.S] |
|
find_lemma [Definitions] | |
find_lemma [Wp.Definitions] | |
find_lib [LogicBuiltins] | find a file in the includes of the current drivers |
find_lib [Wp.LogicBuiltins] | find a file in the includes of the current drivers |
find_name [Definitions] | |
find_name [Wp.Definitions] | |
find_opt [Why3Provers] | |
find_opt [Hashtbl.S] | |
find_opt [Set.S] |
|
find_opt [Map.S] |
|
find_symbol [Definitions] | |
find_symbol [Wp.Definitions] | |
first [ProverSearch] | |
fixpoint [Interpreted_automata.Dataflow] | |
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 [CfgDump] | |
flush [Warning] | |
flush [Wp.Warning] | |
fmode [TacCut] | |
fmul [Cfloat] | |
fmul [Wp.Cfloat] | |
fneq [Cfloat] | |
fneq [Wp.Cfloat] | |
fold [Splitter] | |
fold [Wp.Splitter] | |
fold [Hashtbl.S] | |
fold [Set.S] |
|
fold [Map.S] |
|
fold_bhv_post_cond [WpStrategy] | apply |
fold_lemmas [LogicUsage] | |
fold_lemmas [Wp.LogicUsage] | |
fold_nodes [Cil2cfg] | iterators |
fopen [CfgDump] | |
fopp [Cfloat] | |
fopp [Wp.Cfloat] | |
for_all [Splitter] | |
for_all [Wp.Splitter] | |
for_all [Set.S] |
|
for_all [Map.S] |
|
forall_intro [Conditions] | Introduce universally quantified formulae: head forall quantifiers are instanciated to fresh variables in current pool and left-implies are extracted, recursively. |
forall_intro [Wp.Conditions] | Introduce universally quantified formulae: head forall quantifiers are instanciated to fresh variables in current pool and left-implies are extracted, recursively. |
fork [ProofEngine] | |
formal [LogicCompiler.Make] | |
formal [Clabels] | |
formal [Wp.LogicCompiler.Make] | |
formal [Wp.Clabels] | |
forward [ProofEngine] | |
forward [Letify.Ground] | |
fq32 [Cfloat] | |
fq32 [Wp.Cfloat] | |
fq64 [Cfloat] | |
fq64 [Wp.Cfloat] | |
frame [LogicCompiler.Make] | |
frame [Sigs.LogicSemantics] | Make a fresh frame with the given function. |
frame [Sigs.Model] | Assert the memory is a proper heap state preceeding the function entry point. |
frame [Wp.LogicCompiler.Make] | |
frame [Wp.Sigs.LogicSemantics] | Make a fresh frame with the given function. |
frame [Wp.Sigs.Model] | Assert the memory is a proper heap state preceeding the function entry point. |
framed [Layout.Root] | |
frames [MemMemory] | |
frames [MemLoader.Model] | |
free [Context] | Performs the job with local context cleared. |
free [Wp.Context] | Performs the job with local context cleared. |
fresh [Lang.F] | |
fresh [Wp.Lang.F] | |
freshen [Lang] | |
freshen [Wp.Lang] | |
freshvar [Lang] | |
freshvar [Wp.Lang] | |
from [Layout.Root] | |
froms [StmtSemantics.Make] | |
froms [Wp.StmtSemantics.Make] | |
fsub [Cfloat] | |
fsub [Wp.Cfloat] | |
ftau [Cfloat] | model independant |
ftau [Wp.Cfloat] | model independant |
fusion [Region] | |
fusionned [Region] | |
G | |
garbled [Layout.Compound] | |
gcd [Layout.Matrix] | |
generate [WpRTE] | |
generate_all [WpRTE] | Invoke RTE on all selected functions |
generate_call [VC] | |
generate_call [Wp.VC] | |
generate_ip [VC] | |
generate_ip [Wp.VC] | |
generate_kf [VC] | |
generate_kf [Wp.VC] | |
generated_f [Lang] | |
generated_f [Wp.Lang] | |
generated_p [Lang] | |
generated_p [Wp.Lang] | |
generator [CfgGenerator] | |
get [CfgInfos] | Memoized |
get [ProverScript] | |
get [ProofEngine] | |
get [ProofSession] | |
get [Tactical.Fmap] | raises Not_found if absent |
get [CfgCompiler.Cfg.E] | |
get [CfgCompiler.Cfg.T] | |
get [CfgCompiler.Cfg.P] | |
get [CfgCompiler.Cfg.C] | |
get [Sigs.Sigma] | Lazily get the variable for a chunk. |
get [Lang.F.Subst] | |
get [Cil2cfg] | |
get [RegionAnalysis] | |
get [RefUsage] | |
get [WpContext.Generator] | |
get [WpContext.Registry] | |
get [Dyncall] | Returns |
get [Context] | Retrieves the current value of the context. |
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_automaton [Interpreted_automata.Compute] | Get the interpreted automaton for the given kernel_function. |
get_automaton [Interpreted_automata] | Get the automaton for the given kernel_function without annotations |
get_behavior_goals [CfgAnnot] | |
get_bhv [WpStrategy] | |
get_both_hyp_goals [WpStrategy] | |
get_builtin_type [Lang] | |
get_builtin_type [Wp.Lang] | |
get_call_asgn [WpStrategy] | |
get_call_contract [CfgAnnot] | |
get_call_hyp [WpStrategy] | To be used as hypotheses around a call, (the pre are in
|
get_call_out_edges [Cil2cfg] | similar to |
get_call_post [WpStrategy] | Post-checks of a called function to be considered as goal only |
get_call_pre [WpStrategy] | Preconditions of a called function to be considered as hyp and goal
(similar to |
get_call_pre_strategies [WpAnnot] | |
get_call_type [Cil2cfg] | |
get_code_assertions [CfgAnnot] | |
get_complete_behaviors [CfgAnnot] | |
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 |
get_descr [Wpo.GOAL] | |
get_descr [WpContext] | |
get_descr [Wp.Wpo.GOAL] | |
get_descr [Wp.WpContext] | |
get_description [VC] | |
get_description [Wp.VC] | |
get_dir [Cache] | |
get_disjoint_behaviors [CfgAnnot] | |
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 |
get_fct [Wp_parameters] | |
get_fct [Wp.Wp_parameters] | |
get_file_logerr [Wpo] | only filename, might not exists |
get_file_logerr [Wp.Wpo] | only filename, might not exists |
get_file_logout [Wpo] | only filename, might not exists |
get_file_logout [Wp.Wpo] | only filename, might not exists |
get_files [Wpo] | |
get_files [Wp.Wpo] | |
get_formula [VC] | |
get_formula [Wp.VC] | |
get_frame [LogicCompiler.Make] | |
get_frame [Sigs.LogicSemantics] | Get the current frame, or raise a fatal error if none. |
get_frame [Wp.LogicCompiler.Make] | |
get_frame [Wp.Sigs.LogicSemantics] | Get the current frame, or raise a fatal error if none. |
get_froms [Region] | |
get_function_name [Parameter_sig.String] | returns the given argument only if it is a valid function name
(see |
get_function_strategies [WpAnnot] | |
get_gamma [Lang] | |
get_gamma [Wp.Lang] | |
get_gid [Wpo] | Dynamically exported |
get_gid [Wp.Wpo] | Dynamically exported |
get_goal_only [WpStrategy] | |
get_hits [Cache] | |
get_hyp_only [WpStrategy] | |
get_hypotheses [Lang] | |
get_hypotheses [Wp.Lang] | |
get_id [VC] | |
get_id [Wp.VC] | |
get_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 |
get_induction_labels [Wp.LogicUsage] | Given an inductive |
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 |
get_kf [WpStrategy] | |
get_label [Wpo] | |
get_label [Wp.Wpo] | |
get_legacy [WpPropId] | Unique legacy identifier of |
get_legacy [Wp.WpPropId] | Unique legacy identifier of |
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_loop_contract [CfgAnnot] | |
get_merged [Region] | |
get_miss [Cache] | |
get_mode [Cache] | |
get_model [VC] | |
get_model [Wpo] | |
get_model [WpContext] | |
get_model [Wp.Wpo] | |
get_model [Wp.VC] | |
get_model [Wp.WpContext] | |
get_name [LogicUsage] | |
get_name [Wp.LogicUsage] | |
get_offset [Region] | |
get_opt [Context] | Retrieves the current value of the context. |
get_opt [Wp.Context] | Retrieves the current value of the context. |
get_option [LogicBuiltins] | return the values of option (group, name), return the empty list if not set |
get_option [Wp.LogicBuiltins] | return the values of option (group, name), return the empty list if not set |
get_output [Wp_parameters] | |
get_output [Wp.Wp_parameters] | |
get_output_dir [Wp_parameters] | |
get_output_dir [Wp.Wp_parameters] | |
get_overflows [Wp_parameters] | |
get_overflows [Wp.Wp_parameters] | |
get_plain_string [Parameter_sig.String] | always return the argument, even if the argument is not a function name. |
get_pointed [Region] | |
get_pool [Lang] | |
get_pool [Wp.Lang] | |
get_possible_values [Parameter_sig.String] | What are the acceptable values for this parameter. |
get_post_edges [Cil2cfg] | Find the edges where the postconditions of the node statement have to be checked. |
get_post_label [Cil2cfg] | Get the label to be used for the Post state of the node contract if any. |
get_pre_edges [Cil2cfg] | Find the edges where the precondition of the node statement have to be checked. |
get_preconditions [CfgAnnot] | |
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_property_strategies [WpAnnot] | |
get_propid [WpPropId] | Unique identifier of |
get_propid [Wp.WpPropId] | Unique identifier of |
get_prover_names [Register] | |
get_pstat [Register] | |
get_range [Parameter_sig.Int] | What is the possible range of values for this parameter. |
get_removed [Cache] | |
get_requires [CfgAnnot] | |
get_result [VC] | |
get_result [Cache] | |
get_result [Wpo] | |
get_result [Wp.Wpo] | |
get_result [Wp.VC] | |
get_results [VC] | |
get_results [Wpo] | |
get_results [Wp.Wpo] | |
get_results [Wp.VC] | |
get_roots [Region] | |
get_scope [VC] | |
get_scope [Wpo] | |
get_scope [WpContext] | |
get_scope [Wp.Wpo] | |
get_scope [Wp.VC] | |
get_scope [Wp.WpContext] | |
get_sequent [VC] | |
get_sequent [Wp.VC] | |
get_session [Wp_parameters] | |
get_session [Wp.Wp_parameters] | |
get_session_dir [Wp_parameters] | |
get_session_dir [Wp.Wp_parameters] | |
get_stepout [VCS] | 0 means no-stepout |
get_stepout [Wp.VCS] | 0 means no-stepout |
get_steps [Wpo] | |
get_steps [Wp.Wpo] | |
get_stmt_assigns [CfgAnnot] | |
get_strategies [ProofEngine] | |
get_switch_edges [Cil2cfg] | similar to |
get_target [Wpo] | |
get_target [Wp.Wpo] | |
get_test_edges [Cil2cfg] | similar to |
get_time [Wpo] | |
get_time [Rformat] |
|
get_time [Wp.Wpo] | |
get_timeout [VCS] | 0 means no-timeout |
get_timeout [Wp.VCS] | 0 means no-timeout |
get_unreachable [CfgAnnot] | |
get_wto [Interpreted_automata] | Extract an exit strategy from a component, i.e. |
get_wto_index [Interpreted_automata.Compute] | |
get_wto_index [Interpreted_automata] | |
get_wto_index_diff [Interpreted_automata.Compute] | |
get_wto_index_diff [Interpreted_automata] | |
global [Sigs.Model] | Given a pointer value |
global [Wp.Sigs.Model] | Given a pointer value |
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 |
goto [Wp.CfgCompiler.Cfg] | Represents all execution traces |
group [Splitter] | |
group [Wp.Splitter] | |
guard [CfgCompiler.Cfg] | Structurally corresponds to an assume control-flow. |
guard [Wp.CfgCompiler.Cfg] | Structurally corresponds to an assume control-flow. |
guard' [CfgCompiler.Cfg] | Same than guard but the condition is negated |
guard' [Wp.CfgCompiler.Cfg] | Same than guard but the condition is negated |
guards [LogicCompiler.Make] | |
guards [Sigs.LogicSemantics] | Returns the current gamma environment from the current frame. |
guards [Wp.LogicCompiler.Make] | |
guards [Wp.Sigs.LogicSemantics] | Returns the current gamma environment from the current frame. |
H | |
hack [LogicBuiltins] | Replace a logic definition or predicate by a built-in function. |
hack [Wp.LogicBuiltins] | Replace a logic definition or predicate by a built-in function. |
hack_type [LogicBuiltins] | Replace a logic type definition or predicate by a built-in type. |
hack_type [Wp.LogicBuiltins] | Replace a logic type definition or predicate by a built-in type. |
handle [Warning] | Handle the error and emit a warning with specified severity and effect if a context has been set. |
handle [Wp.Warning] | Handle the error and emit a warning with specified severity and effect if a context has been set. |
has_at_frame [LogicCompiler.Make] | |
has_at_frame [Sigs.LogicSemantics] | Chek if a frame already has a specific envioronement for the given label. |
has_at_frame [Wp.LogicCompiler.Make] | |
has_at_frame [Wp.Sigs.LogicSemantics] | Chek if a frame already has a specific envioronement for the given label. |
has_copies [Region] | |
has_ctype [Cvalues] | |
has_deref [Region] | |
has_dkey [Wp_parameters] | |
has_dkey [Wp.Wp_parameters] | |
has_exit [Cil2cfg] | whether an exit edge exists or not |
has_gamma [Lang] | |
has_gamma [Wp.Lang] | |
has_init [Mcfg.S] | |
has_init [Wp.Mcfg.S] | |
has_layout [Region] | |
has_ltype [LogicCompiler.Make] | |
has_ltype [Wp.LogicCompiler.Make] | |
has_names [Region] | |
has_nullable [RefUsage] |
|
has_nullable [Wp.RefUsage] |
|
has_offset [Region] | |
has_out [Wp_parameters] | |
has_out [Wp.Wp_parameters] | |
has_pointed [Region] | |
has_postassigns [NormAtLabels] | |
has_postassigns [Wp.NormAtLabels] | |
has_print_generated [Wp_parameters] | Debugging Categories |
has_print_generated [Wp.Wp_parameters] | Debugging Categories |
has_proof [ProofScript] | Has a tactical alternative |
has_return [Region] | |
has_roots [Region] | |
has_session [Wp_parameters] | |
has_session [Wp.Wp_parameters] | |
has_shortcut [Why3Provers] | |
has_verdict [Wpo] | |
has_verdict [Wp.Wpo] | |
hash [Sigs.Chunk] | |
hash [Lang.F] | Constant time |
hash [WpContext.SCOPE] | |
hash [WpContext.MODEL] | |
hash [WpContext.S] | |
hash [Ctypes.AinfoComparable] | |
hash [Ctypes] | |
hash [Wp.Sigs.Chunk] | |
hash [Wp.Lang.F] | Constant time |
hash [Wp.WpContext.SCOPE] | |
hash [Wp.WpContext.MODEL] | |
hash [Wp.WpContext.S] | |
hash [Wp.Ctypes.AinfoComparable] | |
hash [Wp.Ctypes] | |
have [Conditions] | Predicate for Have and such, True for any other |
have [Wp.Conditions] | Predicate for Have and such, True for any other |
havoc [Auto] | |
havoc [CfgCompiler.Cfg] | Inserts an assigns effect between nodes |
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 |
havoc [Wp.Sigs.Sigma] | All the chunks in the provided footprint are generated and made fresh. |
havoc_any [Sigs.Sigma] | All the chunks are made fresh. |
havoc_any [Wp.Sigs.Sigma] | All the chunks are made fresh. |
havoc_chunk [Sigs.Sigma] | Generate a new fresh variable for the given chunk. |
havoc_chunk [Wp.Sigs.Sigma] | Generate a new fresh variable for the given chunk. |
havoc_length [MemLoader.Make] | |
head [ProofEngine] | |
head [Tactical] | |
head [Footprint] | Head only footprint |
head [Conditions] | Predicate for Have and such, Condition for Branch, True for Either |
head [Wp.Tactical] | |
head [Wp.Conditions] | Predicate for Have and such, Condition for Branch, True for Either |
here [Clabels] | |
here [Wp.Clabels] | |
hints_for [Proof] | |
hypotheses [Sigs.Model] | Computes the memory model partitionning of the memory locations. |
hypotheses [Lang] | |
hypotheses [Wp.Sigs.Model] | Computes the memory model partitionning of the memory locations. |
hypotheses [Wp.Lang] | |
I | |
i_bits [Ctypes] | size in bits |
i_bits [Wp.Ctypes] | size in bits |
i_bytes [Ctypes] | size in bytes |
i_bytes [Wp.Ctypes] | size in bytes |
i_convert [Ctypes] | |
i_convert [Wp.Ctypes] | |
i_iter [Ctypes] | |
i_iter [Wp.Ctypes] | |
i_memo [Ctypes] | memoized, not-projectified |
i_memo [Wp.Ctypes] | memoized, not-projectified |
i_name [Ctypes] | |
i_name [Wp.Ctypes] | |
iadd [Cint] | |
iadd [Wp.Cint] | |
id [LogicBuiltins] | |
id [Region] | |
id [WpContext.Registry] | |
id [WpContext.SCOPE] | |
id [WpContext.MODEL] | |
id [WpContext.S] | |
id [Wp.LogicBuiltins] | |
id [Wp.WpContext.Registry] | |
id [Wp.WpContext.SCOPE] | |
id [Wp.WpContext.MODEL] | |
id [Wp.WpContext.S] | |
ident [Factory] | |
ident [Tactical] | |
ident [Script] | |
ident [Wp.Tactical] | |
ident [Wp.Factory] | |
ident_names [WpPropId] | From a list of names (of an identified terms), returns usable names. |
ident_names [Wp.WpPropId] | From a list of names (of an identified terms), returns usable names. |
idents [Script] | |
idiv [Cint] | |
idiv [Wp.Cint] | |
if_else [Splitter] | |
if_else [Wp.Splitter] | |
if_then [Splitter] | |
if_then [Wp.Splitter] | |
imod [Cint] | |
imod [Wp.Cint] | |
implies [CfgCompiler.Cfg] | implies is the dual of either. |
implies [Wp.CfgCompiler.Cfg] | implies is the dual of either. |
imul [Cint] | |
imul [Wp.Cint] | |
in_frame [LogicCompiler.Make] | |
in_frame [Sigs.LogicSemantics] | Execute the given closure with the specified current frame. |
in_frame [Wp.LogicCompiler.Make] | |
in_frame [Wp.Sigs.LogicSemantics] | Execute the given closure with the specified current frame. |
in_range [Vset] | |
in_range [Wp.Vset] | |
in_size [Vset] | |
in_size [Wp.Vset] | |
in_state [Lang.For_export] | |
in_state [Wp.Lang.For_export] | |
included [MemMemory] | |
included [Sigs.Model] | Return the formula that tests if two segment are included |
included [Cvalues.Logic] | |
included [Layout.Range] | |
included [Wp.Sigs.Model] | Return the formula that tests if two segment are included |
incr [Parameter_sig.Int] | Increment the integer. |
index [ProverSearch] | |
index [Conditions] | Compute steps' id of sequent left hand-side. |
index [Mstate] | |
index [Layout.Offset] | |
index [Wp.Conditions] | Compute steps' id of sequent left hand-side. |
index [Wp.Mstate] | |
indexed [Layout.Root] | |
infoprover [Lang] | same information for all the provers |
infoprover [Wp.Lang] | same information for all the provers |
init [StmtSemantics.Make] | connect init to here. |
init [CfgCompiler.Cfg.T] | |
init [Sigs.CodeSemantics] | Express that some variable has some initial value at the given memory state. |
init [Mcfg.S] | |
init [Clabels] | |
init [Wp.StmtSemantics.Make] | |
init [Wp.CfgCompiler.Cfg.T] | |
init [Wp.Sigs.CodeSemantics] | Express that some variable has some initial value at the given memory state. |
init [Wp.Mcfg.S] | |
init [Wp.Clabels] | |
init' [CfgCompiler.Cfg.T] | |
init' [Wp.CfgCompiler.Cfg.T] | |
init_filter [Conditions] | |
init_filter [Wp.Conditions] | |
init_footprint [MemLoader.Model] | |
init_of_ctype [Lang] | |
init_of_ctype [Wp.Lang] | |
init_of_object [Lang] | |
init_of_object [Wp.Lang] | |
initialized [MemLoader.Make] | |
initialized [Sigs.Model] | Return the formula that tests if a memory state is initialized
(according to |
initialized [Cvalues.Logic] | |
initialized [Wp.Sigs.Model] | Return the formula that tests if a memory state is initialized
(according to |
initialized_obj [Cvalues] | |
insert [Tactical] | |
insert [Conditions] | Insert a step in the sequent immediately |
insert [Wp.Tactical] | |
insert [Wp.Conditions] | Insert a step in the sequent immediately |
instance [Factory] | |
instance [Auto] | |
instance [Wp.Auto] | |
instance [Wp.Factory] | |
instance_goal [TacInstance] | |
instance_have [TacInstance] | |
instance_of [Sigs.CodeSemantics] | Check whether a function pointer is (an instance of) some kernel function. |
instance_of [Wp.Sigs.CodeSemantics] | Check whether a function pointer is (an instance of) some kernel function. |
instr [StmtSemantics.Make] | |
instr [Wp.StmtSemantics.Make] | |
int [Tactical] | |
int [Wp.Tactical] | |
int_of_bool [Cmath] | |
int_of_loc [Sigs.Model] | Cast a memory location into its absolute memory address, given as an integer with the given C-type. |
int_of_loc [Wp.Sigs.Model] | Cast a memory location into its absolute memory address, given as an integer with the given C-type. |
int_of_real [Cmath] | |
inter [Cvalues.Logic] | |
inter [Vset] | |
inter [Wp.Vset] | |
inter [Set.S] | Set intersection. |
intersect [Conditions] | Variables of predicate and the bundle intersects |
intersect [Lang.F] | |
intersect [Wp.Conditions] | Variables of predicate and the bundle intersects |
intersect [Wp.Lang.F] | |
intersectp [Lang.F] | |
intersectp [Wp.Lang.F] | |
introduction [Conditions] | Performs existential, universal and hypotheses introductions |
introduction [Wp.Conditions] | Performs existential, universal and hypotheses introductions |
introduction_eq [Conditions] | Same as |
introduction_eq [Wp.Conditions] | Same as |
intros [Conditions] | Assumes a list of predicates in a |
intros [Wp.Conditions] | Assumes a list of predicates in a |
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 |
isInitConst [WpStrategy] | True if both options |
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 [Interpreted_automata.Compute] | |
is_back_edge [Interpreted_automata] | |
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 |
is_cint [Wp.Cint] | Raises |
is_cint_simplifier [Cint] | Remove the |
is_cint_simplifier [Wp.Cint] | Remove the |
is_closed [Lang.F] | No bound variables |
is_closed [Wp.Lang.F] | No bound variables |
is_cnf [WpTac] | |
is_comp [Ctypes] | |
is_comp [Wp.Ctypes] | |
is_complete [AssignsCompleteness] | |
is_complete [Wp.AssignsCompleteness] | |
is_composed [WpPropId] | whether a proof needs several lemma to be complete |
is_composed [Wp.WpPropId] | whether a proof needs several lemma to be complete |
is_compound [Ctypes] | |
is_compound [Wp.Ctypes] | |
is_computed [RefUsage] | |
is_computed [Wp.RefUsage] | |
is_computing [VCS] | |
is_computing [Wp.VCS] | |
is_dead_annot [WpReached] | False assertions and loop invariant. |
is_dead_code [WpReached] | Checks whether the stmt has a dead-code annotation. |
is_default [LogicBuiltins] | |
is_default [Wp.LogicBuiltins] | |
is_default_behavior [WpStrategy] | |
is_defined [WpContext] | |
is_defined [Wp.WpContext] | |
is_dnf [WpTac] | |
is_empty [Tactical] | |
is_empty [Conditions] | No step at all |
is_empty [Vset] | |
is_empty [Passive] | |
is_empty [Region] | |
is_empty [Layout.Cluster] | |
is_empty [Wp.Tactical] | |
is_empty [Wp.Conditions] | No step at all |
is_empty [Wp.Vset] | |
is_empty [Wp.Passive] | |
is_empty [Set.S] | Test whether a set is empty or not. |
is_empty [Map.S] | Test whether a map is empty or not. |
is_empty_script [Proof] | Check a proof script text for emptyness |
is_equal [Lang.F] | |
is_equal [Wp.Lang.F] | |
is_exp_range [Sigs.CodeSemantics] | Express that all objects in a range of locations have a given value. |
is_exp_range [Wp.Sigs.CodeSemantics] | Express that all objects in a range of locations have a given value. |
is_false [Cvalues] |
|
is_false [Lang.F] | Constant time. |
is_false [Wp.Lang.F] | Constant time. |
is_framed [Sigs.Chunk] | Whether the chunk is local to a function call. |
is_framed [Wp.Sigs.Chunk] | Whether the chunk is local to a function call. |
is_garbled [Region] | |
is_garbled [Layout.Cluster] | |
is_here [Clabels] | |
is_here [Wp.Clabels] | |
is_init_atom [MemLoader.Model] | |
is_init_range [MemLoader.Model] | |
is_int [Lang.F] | Integer sort |
is_int [Wp.Lang.F] | Integer sort |
is_invalid [WpPropId] | whether an invalid proof result has been registered or not |
is_invalid [Wp.WpPropId] | whether an invalid proof result has been registered or not |
is_literal [Lang] | |
is_literal [Wp.Lang] | |
is_loop_preservation [WpPropId] | |
is_loop_preservation [Wp.WpPropId] | |
is_main_init [WpStrategy] | The function is the main entry point AND it is not a lib entry |
is_mainstream [Why3Provers] | |
is_neutral [Lang.F] | |
is_neutral [Wp.Lang.F] | |
is_null [Sigs.Model] | Return the formula that check if a given location is null |
is_null [Cvalues] | |
is_null [Wp.Sigs.Model] | Return the formula that check if a given location is null |
is_nullable [RefUsage] |
|
is_nullable [Wp.RefUsage] |
|
is_object [Cvalues] | |
is_passed [Wpo] | proved, or unknown for smoke tests |
is_passed [Wp.Wpo] | proved, or unknown for smoke tests |
is_pfalse [Lang.F] | |
is_pfalse [Wp.Lang.F] | |
is_pointer [Ctypes] | |
is_pointer [Wp.Ctypes] | |
is_positive_or_null [Cint] | |
is_positive_or_null [Wp.Cint] | |
is_post [Clabels] | Checks whether the logic-label is |
is_post [Wp.Clabels] | Checks whether the logic-label is |
is_predicate [WpReached] | If returns |
is_primitive [Lang.F] | Constants only |
is_primitive [Wp.Lang.F] | Constants only |
is_prop [Lang.F] | Boolean or Property |
is_prop [Wp.Lang.F] | Boolean or Property |
is_proved [VC] | |
is_proved [Wpo] | do not tries simplification, check prover results |
is_proved [VCS] | |
is_proved [WpPropId] | whether all partial proofs have been accumulated or not |
is_proved [Wp.Wpo] | do not tries simplification, check prover results |
is_proved [Wp.VC] | |
is_proved [Wp.VCS] | |
is_proved [Wp.WpPropId] | whether all partial proofs have been accumulated or not |
is_prover [ProofScript] | |
is_ptrue [Lang.F] | |
is_ptrue [Wp.Lang.F] | |
is_read [Region] | |
is_real [Lang.F] | Real sort |
is_real [Wp.Lang.F] | Real sort |
is_recursive [LogicUsage] | |
is_recursive [Wp.LogicUsage] | |
is_requires [WpPropId] | |
is_requires [Wp.WpPropId] | |
is_shifted [Region] | |
is_shifted [Layout.Usage] | |
is_simple [Lang.F] | Constants, variables, functions of arity 0 |
is_simple [Wp.Lang.F] | Constants, variables, functions of arity 0 |
is_smoke_test [Wpo] | |
is_smoke_test [WpPropId] | |
is_smoke_test [Wp.Wpo] | |
is_smoke_test [Wp.WpPropId] | |
is_subterm [Lang.F] | |
is_subterm [Wp.Lang.F] | |
is_tactic [ProofScript] | |
is_tactic [Wpo] | |
is_tactic [WpPropId] | |
is_tactic [Wp.Wpo] | |
is_tactic [Wp.WpPropId] | |
is_trivial [VC] | |
is_trivial [Wpo.VC_Annot] | |
is_trivial [Wpo.VC_Lemma] | |
is_trivial [Wpo.GOAL] | |
is_trivial [Wpo] | do not tries simplification, do not check prover results |
is_trivial [Conditions] | Goal is true or hypotheses contains false. |
is_trivial [Wp.Wpo.VC_Annot] | |
is_trivial [Wp.Wpo.VC_Lemma] | |
is_trivial [Wp.Wpo.GOAL] | |
is_trivial [Wp.Wpo] | do not tries simplification, do not check prover results |
is_trivial [Wp.VC] | |
is_trivial [Wp.Conditions] | Goal is true or hypotheses contains false. |
is_true [Conditions] | Contains only true or empty steps |
is_true [Cvalues] |
|
is_true [Lang.F] | Constant time. |
is_true [Wp.Conditions] | Contains only true or empty steps |
is_true [Wp.Lang.F] | Constant time. |
is_unknown [Wpo] | at least one prover returns « Unknown » |
is_unknown [Wp.Wpo] | at least one prover returns « Unknown » |
is_updating [Cache] | |
is_valid [Wpo] |
|
is_valid [VCS] | |
is_valid [Wp.Wpo] |
|
is_valid [Wp.VCS] | |
is_verdict [VCS] | |
is_verdict [Wp.VCS] | |
is_well_formed [Sigs.Model] | Provides the constraint corresponding to the kind of data stored by all chunks in sigma. |
is_well_formed [Wp.Sigs.Model] | Provides the constraint corresponding to the kind of data stored by all chunks in sigma. |
is_written [Region] | |
is_wto_head [Interpreted_automata.Compute] | |
is_wto_head [Interpreted_automata] | |
is_zero [Sigs.CodeSemantics] | Express that the object (of specified type) at the given location is filled with zeroes. |
is_zero [Lang.F] | |
is_zero [Wp.Sigs.CodeSemantics] | Express that the object (of specified type) at the given location is filled with zeroes. |
is_zero [Wp.Lang.F] | |
isub [Cint] | |
isub [Wp.Cint] | |
iter [ProofEngine] | |
iter [Strategy] | |
iter [Tactical] | |
iter [Footprint] | Width-first full iterator. |
iter [Wpo] | |
iter [WpTarget] | |
iter [MemVar.VarUsage] | |
iter [Pcfg] | |
iter [Conditions] | Iterate only over the head steps of the sequence. |
iter [Mstate] | |
iter [Sigs.Model] | Debug |
iter [Sigs.Sigma] | Iterates over the chunks and associated variables already accessed so far in the environment. |
iter [Letify.Sigma] | |
iter [Definitions] | |
iter [Splitter] | |
iter [Passive] | |
iter [Region] | |
iter [RefUsage] | |
iter [WpContext.Registry] | |
iter [Wp.Wpo] | |
iter [Wp.Strategy] | |
iter [Wp.Tactical] | |
iter [Wp.MemVar.VarUsage] | |
iter [Wp.Pcfg] | |
iter [Wp.Conditions] | Iterate only over the head steps of the sequence. |
iter [Wp.Mstate] | |
iter [Wp.Sigs.Model] | Debug |
iter [Wp.Sigs.Sigma] | Iterates over the chunks and associated variables already accessed so far in the environment. |
iter [Wp.Definitions] | |
iter [Wp.Splitter] | |
iter [Wp.Passive] | |
iter [Wp.WpContext.Registry] | |
iter [Hashtbl.S] | |
iter [Wp.RefUsage] | |
iter [Set.S] |
|
iter [Map.S] |
|
iter2 [Sigs.Sigma] | Same as |
iter2 [Wp.Sigs.Sigma] | Same as |
iter_composer [Tactical] | |
iter_composer [Wp.Tactical] | |
iter_consequence_literals [Lang] |
|
iter_consequence_literals [Wp.Lang] |
|
iter_copies [Region] | |
iter_deref [Region] | |
iter_edges [Cil2cfg] | |
iter_fct [Wp_parameters] | |
iter_fct [Wp.Wp_parameters] | |
iter_fusion [Region] | |
iter_ip [VC] | |
iter_ip [Wp.VC] | |
iter_kf [VC] | |
iter_kf [Wp_parameters] | |
iter_kf [Wp.VC] | |
iter_kf [Wp.Wp_parameters] | |
iter_lemmas [LogicUsage] | |
iter_lemmas [Wp.LogicUsage] | |
iter_names [Region] | |
iter_nodes [Cil2cfg] | |
iter_offset [Region] | |
iter_on_goals [Wpo] | Dynamically exported. |
iter_on_goals [Wp.Wpo] | Dynamically exported. |
iter_read [Region] | |
iter_shift [Region] | |
iter_sorted [WpContext.Registry] | |
iter_sorted [Wp.WpContext.Registry] | |
iter_strings [Region] | |
iter_vars [Region] | |
iter_write [Region] | |
J | |
join [Interpreted_automata.Domain] | Merges two states coming from different paths. |
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 [NormAtLabels] | |
labels_assert [Wp.NormAtLabels] | |
labels_axiom [NormAtLabels] | |
labels_axiom [Wp.NormAtLabels] | |
labels_empty [NormAtLabels] | |
labels_empty [Wp.NormAtLabels] | |
labels_fct_assigns [NormAtLabels] | |
labels_fct_assigns [Wp.NormAtLabels] | |
labels_fct_post [NormAtLabels] | |
labels_fct_post [Wp.NormAtLabels] | |
labels_fct_pre [NormAtLabels] | |
labels_fct_pre [Wp.NormAtLabels] | |
labels_loop [NormAtLabels] | |
labels_loop [Wp.NormAtLabels] | |
labels_predicate [NormAtLabels] | |
labels_predicate [Wp.NormAtLabels] | |
labels_stmt_assigns [NormAtLabels] | |
labels_stmt_assigns [Wp.NormAtLabels] | |
labels_stmt_assigns_l [NormAtLabels] | |
labels_stmt_assigns_l [Wp.NormAtLabels] | |
labels_stmt_post [NormAtLabels] | |
labels_stmt_post [Wp.NormAtLabels] | |
labels_stmt_post_l [NormAtLabels] | |
labels_stmt_post_l [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 [Wp.Splitter] | |
length [Hashtbl.S] | |
lfun [Repr] | |
lfun [Wp.Repr] | |
lift [Vset] | |
lift [Lang.F] | |
lift [Wp.Vset] | |
lift [Wp.Lang.F] | |
lift_add [Vset] | |
lift_add [Wp.Vset] | |
lift_sub [Vset] | |
lift_sub [Wp.Vset] | |
list [Conditions] | Same domain than |
list [Wp.Conditions] | Same domain than |
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_init [MemLoader.Make] | |
load_init [Sigs.Model] | Return the initialization status at the given location in the given memory state. |
load_init [Wp.Sigs.Model] | Return the initialization status at the given location in the given memory state. |
load_int [MemLoader.Model] | |
load_pointer [MemLoader.Model] | |
load_value [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 |
loc_of_term [Wp.Sigs.LogicSemantics] | Same as |
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 |
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 |
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 [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] |
|
loop_current [Clabels] | |
loop_current [Wp.Clabels] | |
loop_entry [Mcfg.S] | |
loop_entry [Clabels] | |
loop_entry [Wp.Mcfg.S] | |
loop_entry [Wp.Clabels] | |
loop_step [Mcfg.S] | |
loop_step [Wp.Mcfg.S] | |
loopcurrent [Clabels] | |
loopcurrent [Wp.Clabels] | |
loopentry [Clabels] | |
loopentry [Wp.Clabels] | |
lval [Sigs.LogicSemantics] | Compile a term l-value into a (typed) abstract location |
lval [Sigs.CodeSemantics] | Evaluate the left-value on the given memory state. |
lval [Wp.Sigs.LogicSemantics] | Compile a term l-value into a (typed) abstract location |
lval [Wp.Sigs.CodeSemantics] | Evaluate the left-value on the given memory state. |
M | |
main [Register] | |
main [ProofEngine] | |
make [GuiNavigator] | |
make [Strategy] | |
make [Wpo.GOAL] | |
make [Wp.Wpo.GOAL] | |
make [Wp.Strategy] | |
make_output_dir [Wp_parameters] | |
make_output_dir [Wp.Wp_parameters] | |
make_type [Datatype.Hashtbl] | |
map [Cvalues.Logic] | |
map [Vset] | |
map [Splitter] | |
map [Wp.Vset] | |
map [Wp.Splitter] | |
map [Set.S] |
|
map [Map.S] |
|
map_condition [Conditions] | Rewrite all root predicates in condition |
map_condition [Wp.Conditions] | Rewrite all root predicates in condition |
map_l2t [Cvalues.Logic] | |
map_loc [Cvalues.Logic] | |
map_logic [Cvalues] | |
map_opp [Cvalues.Logic] | |
map_opp [Vset] | |
map_opp [Wp.Vset] | |
map_sequence [Conditions] | Rewrite all root predicates in sequence |
map_sequence [Wp.Conditions] | Rewrite all root predicates in sequence |
map_sequent [Conditions] | Rewrite all root predicates in hypotheses and goal |
map_sequent [Wp.Conditions] | Rewrite all root predicates in hypotheses and goal |
map_sloc [Cvalues] | |
map_step [Conditions] | Rewrite all root predicates in step |
map_step [Wp.Conditions] | Rewrite all root predicates in step |
map_t2l [Cvalues.Logic] | |
map_value [Cvalues] | |
mapi [Tactical] | |
mapi [Wp.Tactical] | |
mapi [Map.S] | Same as |
mark_e [Lang.F] | |
mark_e [Wp.Lang.F] | |
mark_p [Lang.F] | Returns a list of terms to be shared among all shared or marked subterms. |
mark_p [Wp.Lang.F] | Returns a list of terms to be shared among all shared or marked subterms. |
marker [Lang.F] | |
marker [Wp.Lang.F] | |
mask_simplifier [Cint] | |
mask_simplifier [Wp.Cint] | |
matches [Footprint] | Head match |
matrix [Definitions] | |
matrix [Wp.Definitions] | |
max_binding [Map.S] | Same as |
max_binding_opt [Map.S] | Same as |
max_elt [Set.S] | Same as |
max_elt_opt [Set.S] | Same as |
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 [Wp.Sigs.Sigma] | Whether a chunk has been assigned. |
mem [Wp.WpContext.Generator] | |
mem [Wp.WpContext.Registry] | |
mem [Hashtbl.S] | |
mem [Set.S] |
|
mem [Map.S] |
|
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_frame [Wp.LogicCompiler.Make] | |
mem_frame [Wp.Sigs.LogicSemantics] | Same as |
member [Vset] | |
member [Wp.Vset] | |
memoize [WpContext.Registry] | with circularity protection |
memoize [Wp.WpContext.Registry] | with circularity protection |
merge [VCS] | |
merge [Conditions] | Performs a diff-based disjunction, introducing If-Then-Else or Either branches when possible. |
merge [Sigs.Sigma] | Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins. |
merge [Letify.Defs] | |
merge [Splitter] | |
merge [Matrix] | |
merge [Mcfg.S] | |
merge [Layout.Pack] | |
merge [Layout.Flat] | |
merge [Layout.RW] | |
merge [Layout.Root] | |
merge [Layout.Cluster] | |
merge [Layout.Overlay] | |
merge [Layout.Matrix] | |
merge [Layout.Value] | |
merge [Layout.Usage] | |
merge [Layout.Alias] | |
merge [Wp.VCS] | |
merge [Wp.Conditions] | Performs a diff-based disjunction, introducing If-Then-Else or Either branches when possible. |
merge [Wp.Sigs.Sigma] | Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins. |
merge [Wp.Splitter] | |
merge [Wp.Mcfg.S] | |
merge [Map.S] |
|
merge_all [Splitter] | |
merge_all [Wp.Splitter] | |
merge_assign_info [WpPropId] | |
merge_assign_info [Wp.WpPropId] | |
merge_list [Sigs.Sigma] | Same than |
merge_list [Wp.Sigs.Sigma] | Same than |
meta [CfgCompiler.Cfg] | Attach meta informations to a node. |
meta [Wp.CfgCompiler.Cfg] | Attach meta informations to a node. |
min_binding [Map.S] | Return the binding with the smallest key in a given map
(with respect to the |
min_binding_opt [Map.S] | Return the binding with the smallest key in the given map
(with respect to the |
min_elt [Set.S] | Return the smallest element of the given set
(with respect to the |
min_elt_opt [Set.S] | Return the smallest element of the given set
(with respect to the |
missing_guards [WpRTE] | Returns |
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 [Wp.WpPropId] |
|
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 The boolean indicate whether the function has exit node or not. |
mk_fct_assigns_id [Wp.WpPropId] | function assigns The boolean indicate whether the function has exit node or not. |
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 [WpPropId] | Invariant establishment and preservation, in this order |
mk_loop_inv [Wp.WpPropId] | Invariant establishment and preservation, in this order |
mk_loop_inv_id [WpPropId] | Invariant establishment and preservation |
mk_loop_inv_id [Wp.WpPropId] | Invariant establishment and preservation |
mk_part [WpPropId] |
|
mk_part [Wp.WpPropId] |
|
mk_post_id [WpPropId] | |
mk_post_id [Wp.WpPropId] | |
mk_pre_id [WpPropId] | |
mk_pre_id [Wp.WpPropId] | |
mk_pred_info [WpPropId] | |
mk_pred_info [Wp.WpPropId] | |
mk_property [WpPropId] | |
mk_property [Wp.WpPropId] | |
mk_smoke [WpPropId] | |
mk_smoke [Wp.WpPropId] | |
mk_stmt_any_assigns_info [WpPropId] | |
mk_stmt_any_assigns_info [Wp.WpPropId] | |
mk_stmt_assigns_any_desc [WpPropId] | |
mk_stmt_assigns_any_desc [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] | |
move_at [LogicCompiler.Make] | |
move_at [Sigs.LogicSemantics] | Move the compilation environment to the specified |
move_at [Wp.LogicCompiler.Make] | |
move_at [Wp.Sigs.LogicSemantics] | Move the compilation environment to the specified |
N | |
name [MemLoader.Model] | |
name [WpContext.IData] | |
name [WpContext.Data] | |
name [WpContext.Entries] | |
name [Clabels] | |
name [Context] | |
name [Why3Provers] | |
name [Wp_error] | |
name [Wp.WpContext.IData] | |
name [Wp.WpContext.Data] | |
name [Wp.WpContext.Entries] | |
name [Wp.Context] | |
name [Wp.Clabels] | |
name_of_field [Lang] | |
name_of_field [Wp.Lang] | |
name_of_lfun [Lang] | |
name_of_lfun [Wp.Lang] | |
name_of_prover [VCS] | |
name_of_prover [Wp.VCS] | |
named [TacLemma] | |
nearest_elt_ge [Datatype.Set] | |
nearest_elt_le [Datatype.Set] | |
negate [Cvalues] | |
new_driver [LogicBuiltins] | Creates a configured driver from an existing one. |
new_driver [Wp.LogicBuiltins] | Creates a configured driver from an existing one. |
new_env [Mcfg.S] | optionally init env with user logic variables |
new_env [Wp.Mcfg.S] | optionally init env with user logic variables |
new_gamma [Lang] | |
new_gamma [Wp.Lang] | |
new_pool [Lang] | |
new_pool [Wp.Lang] | |
next [Pcfg] | |
next [Clabels] | |
next [Wp.Pcfg] | |
next [Wp.Clabels] | |
nil [Conditions] | Same as empty |
nil [Wp.Conditions] | Same as empty |
no_infinite_array [Ctypes] | |
no_infinite_array [Wp.Ctypes] | |
no_result [VCS] | |
no_result [Wp.VCS] | |
no_status [GuiProver] | |
node [CfgCompiler.Cfg] | fresh node |
node [Wp.CfgCompiler.Cfg] | fresh node |
node_context [ProofEngine] | |
node_stmt_opt [Cil2cfg] | |
node_type [Cil2cfg] | |
nodes [CfgCompiler.Cfg.P] | |
nodes [Wp.CfgCompiler.Cfg.P] | |
noid [Region] | |
nop [CfgCompiler.Cfg] | Structurally, |
nop [Wp.CfgCompiler.Cfg] | Structurally, |
normalize [WpStrategy] | |
not [Lang.N] | |
not [Wp.Lang.N] | |
not_equal_obj [Sigs.CodeSemantics] | Same as |
not_equal_obj [Wp.Sigs.CodeSemantics] | Same as |
not_equal_typ [Sigs.CodeSemantics] | Computes the value of |
not_equal_typ [Wp.Sigs.CodeSemantics] | Computes the value of |
not_yet_implemented [Wp_error] | |
null [Sigs.Model] | Return the location of the null pointer |
null [Cvalues] | test for null pointer value |
null [Wp.Sigs.Model] | Return the location of the null pointer |
num_of_bhv_from [WpPropId] | |
num_of_bhv_from [Wp.WpPropId] | |
O | |
object_of [Ctypes] | |
object_of [Wp.Ctypes] | |
object_of_array_elem [Ctypes] | |
object_of_array_elem [Wp.Ctypes] | |
object_of_logic_pointed [Ctypes] | |
object_of_logic_pointed [Wp.Ctypes] | |
object_of_logic_type [Ctypes] | |
object_of_logic_type [Wp.Ctypes] | |
object_of_pointed [Ctypes] | |
object_of_pointed [Wp.Ctypes] | |
occurs [Conditions] | |
occurs [Sigs.LogicSemantics] | Member of vars. |
occurs [Sigs.Model] | Test if a location depend on a given logic variable |
occurs [Vset] | |
occurs [Lang.F] | |
occurs [Wp.Conditions] | |
occurs [Wp.Sigs.LogicSemantics] | Member of vars. |
occurs [Wp.Sigs.Model] | Test if a location depend on a given logic variable |
occurs [Wp.Vset] | |
occurs [Wp.Lang.F] | |
occurs_e [Strategy] | |
occurs_e [Wp.Strategy] | |
occurs_p [Strategy] | |
occurs_p [Wp.Strategy] | |
occurs_q [Strategy] | |
occurs_q [Wp.Strategy] | |
occurs_x [Strategy] | |
occurs_x [Wp.Strategy] | |
occurs_y [Strategy] | |
occurs_y [Wp.Strategy] | |
occursp [Lang.F] | |
occursp [Wp.Lang.F] | |
of_behavior [RegionAnnot] | |
of_class [Region] | |
of_cstring [Region] | |
of_cvar [Region] | |
of_dims [Matrix] | |
of_extension [RegionAnnot] | |
of_integer [Cint] | |
of_integer [Wp.Cint] | |
of_list [Set.S] |
|
of_logic [Clabels] | Assumes the logic label only comes from normalized or non-ambiguous labels. |
of_logic [Wp.Clabels] | Assumes the logic label only comes from normalized or non-ambiguous labels. |
of_name [Region] | |
of_null [Region] | |
of_pred [Definitions.Trigger] | |
of_pred [Wp.Definitions.Trigger] | |
of_real [Cint] | |
of_real [Wp.Cint] | |
of_region_pointer [MemLoader.Model] | |
of_return [Region] | |
of_seq [Hashtbl.S] | |
of_seq [Set.S] | Build a set from the given bindings |
of_seq [Map.S] | Build a map from the given bindings |
of_term [Definitions.Trigger] | |
of_term [Wp.Definitions.Trigger] | |
off [Parameter_sig.Bool] | Set the boolean to |
ok_status [GuiProver] | |
on [Parameter_sig.Bool] | Set the boolean to |
on_context [WpContext] | |
on_context [Wp.WpContext] | |
on_reload [GuiPanel] | |
on_remove [Wpo] | |
on_remove [Wp.Wpo] | |
on_update [GuiPanel] | |
once [Footprint] | Width-first once iterator. |
once [Layout.Overlay] | |
open_file [Script] | |
ordered [Vset] | - |
ordered [Wp.Vset] | - |
output_dot [CfgCompiler.Cfg] | |
output_dot [Wp.CfgCompiler.Cfg] | |
output_to_dot [Interpreted_automata.UnrollUnnatural] | |
output_to_dot [Interpreted_automata.Compute] | |
output_to_dot [Interpreted_automata] | |
overflow [TacOverflow] | |
overlap [Layout.Range] | |
P | |
p_addr_le [MemMemory] | |
p_addr_lt [MemMemory] | |
p_all [Lang.F] | |
p_all [Wp.Lang.F] | |
p_and [Lang.F] | |
p_and [Wp.Lang.F] | |
p_any [Lang.F] | |
p_any [Wp.Lang.F] | |
p_apply [Letify.Sigma] | |
p_apply [Letify.Ground] | |
p_bind [Lang.F] | |
p_bind [Wp.Lang.F] | |
p_bits [Ctypes] | pointer size in bits |
p_bits [Wp.Ctypes] | pointer size in bits |
p_bool [Lang.F] | |
p_bool [Wp.Lang.F] | |
p_bools [Lang.F] | |
p_bools [Wp.Lang.F] | |
p_bytes [Ctypes] | pointer size in bits |
p_bytes [Wp.Ctypes] | pointer size in bits |
p_call [Lang.F] | |
p_call [Wp.Lang.F] | |
p_cinits [MemMemory] | |
p_close [Lang.F] | Quantify over (sorted) free variables |
p_close [Wp.Lang.F] | Quantify over (sorted) free variables |
p_conj [Lang.F] | |
p_conj [Wp.Lang.F] | |
p_disj [Lang.F] | |
p_disj [Wp.Lang.F] | |
p_eqmem [MemMemory] | |
p_equal [Lang.F] | |
p_equal [Wp.Lang.F] | |
p_equals [Lang.F] | |
p_equals [Wp.Lang.F] | |
p_equiv [Lang.F] | |
p_equiv [Wp.Lang.F] | |
p_exists [Lang.F] | |
p_exists [Wp.Lang.F] | |
p_expr [Lang.F] | |
p_expr [Wp.Lang.F] | |
p_false [Lang.F] | |
p_false [Wp.Lang.F] | |
p_float [ProverTask] | Float group pattern |
p_float [Wp.ProverTask] | Float group pattern |
p_forall [Lang.F] | |
p_forall [Wp.Lang.F] | |
p_framed [MemMemory] | |
p_group [ProverTask] | Put pattern in group |
p_group [Wp.ProverTask] | Put pattern in group |
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 |
p_int [Wp.ProverTask] | Int group pattern |
p_invalid [MemMemory] | |
p_is_init_r [MemMemory] | |
p_leq [Lang.F] | |
p_leq [Wp.Lang.F] | |
p_linked [MemMemory] | |
p_lt [Lang.F] | |
p_lt [Wp.Lang.F] | |
p_monotonic [MemMemory] | |
p_name [RegionAnnot] | |
p_neq [Lang.F] | |
p_neq [Wp.Lang.F] | |
p_not [Lang.F] | |
p_not [Wp.Lang.F] | |
p_or [Lang.F] | |
p_or [Wp.Lang.F] | |
p_positive [Lang.F] | |
p_positive [Wp.Lang.F] | |
p_sconst [MemMemory] | |
p_separated [MemMemory] | |
p_string [ProverTask] | String group pattern |
p_string [Wp.ProverTask] | String group pattern |
p_subst [Lang.F] | |
p_subst [Lang] | uses current pool |
p_subst [Wp.Lang.F] | |
p_subst [Wp.Lang] | uses current pool |
p_subst_var [Lang.F] | |
p_subst_var [Wp.Lang.F] | |
p_true [Lang.F] | |
p_true [Wp.Lang.F] | |
p_until_space [ProverTask] | No space group pattern "\\( |
p_until_space [Wp.ProverTask] | No space group pattern "\\( |
p_valid_obj [MemMemory] | |
p_valid_rd [MemMemory] | |
p_valid_rw [MemMemory] | |
p_vars [Lang.F] | Sorted |
p_vars [Wp.Lang.F] | Sorted |
parallel [StmtSemantics.Make] | Chain compiler in parallel, between labels |
parallel [Wp.StmtSemantics.Make] | Chain compiler in parallel, between labels |
param [MemVar.VarUsage] | |
param [Wp.MemVar.VarUsage] | |
param_of_json [ProofScript] | |
parameters [Lang] | definitions |
parameters [Wp.Lang] | definitions |
parameters_of_json [ProofScript] | |
params [TacInstance] | |
parasite [Conditions] | |
parasite [Wp.Conditions] | |
parent [ProofEngine] | |
parse [Factory] | Apply specifications to default setup. |
parse [Wp.Factory] | Apply specifications to default setup. |
parse_coqproof [Proof] |
|
parse_mode [VCS] | |
parse_mode [Wp.VCS] | |
parse_prover [VCS] | |
parse_prover [Wp.VCS] | |
partition [Set.S] |
|
partition [Map.S] |
|
parts_of_id [WpPropId] | get the 'part' information. |
parts_of_id [Wp.WpPropId] | get the 'part' information. |
pattern [Footprint] | Generate head footprint up to size |
pending [ProofEngine] | 0 means proved |
pending [ProofScript] | pending goals |
pending_any [ProofScript] | minimum of pending goals |
plain [Cvalues] | |
pointed [Layout.Value] | |
pointer [MemTyped] | |
pointer [Lang] | type of pointers |
pointer [Wp.MemTyped] | |
pointer [Wp.Lang] | type of pointers |
pointer_loc [Sigs.Model] | Interpret an address value (a pointer) as an abstract location. |
pointer_loc [Wp.Sigs.Model] | Interpret an address value (a pointer) as an abstract location. |
pointer_val [Sigs.Model] | Return the adress value (a pointer) of an abstract location. |
pointer_val [Wp.Sigs.Model] | Return the adress value (a pointer) of an abstract location. |
poly [Lang] | polymorphism |
poly [Wp.Lang] | polymorphism |
pool [ProofEngine] | |
pool [Plang] | |
pool [Lang.F] | |
pool [Wp.Plang] | |
pool [Wp.Lang.F] | |
pop [Context] | |
pop [Wp.Context] | |
post [Clabels] | |
post [Wp.Clabels] | |
pp [CfgCompiler.Cfg.Node] | |
pp [Wp.CfgCompiler.Cfg.Node] | |
pp_acs [Cvalues] | |
pp_annots [WpStrategy] | |
pp_assign_info [WpPropId] | |
pp_assign_info [Wp.WpPropId] | |
pp_assigns [Wp_error] | |
pp_assigns_desc [WpPropId] | |
pp_assigns_desc [Wp.WpPropId] | |
pp_axiom_info [WpPropId] | |
pp_axiom_info [Wp.WpPropId] | |
pp_axiomatics [Wpo] | |
pp_axiomatics [Wp.Wpo] | |
pp_bound [Cvalues] | |
pp_bound [Vset] | |
pp_bound [Wp.Vset] | |
pp_call_type [Cil2cfg] | |
pp_calls [Dyncall] | |
pp_chain [Layout.Offset] | |
pp_clause [Tactical] | Debug only |
pp_clause [Wp.Tactical] | Debug only |
pp_cluster [Definitions] | |
pp_cluster [Wp.Definitions] | |
pp_depend [Wpo] | |
pp_depend [Wp.Wpo] | |
pp_dependencies [Wpo] | |
pp_dependencies [Wp.Wpo] | |
pp_dependency [Wpo] | |
pp_dependency [Wp.Wpo] | |
pp_edge [Cil2cfg] | |
pp_epred [Lang.F] | |
pp_epred [Wp.Lang.F] | |
pp_eterm [Lang.F] | |
pp_eterm [Wp.Lang.F] | |
pp_file [ProverTask] | |
pp_file [Wp.ProverTask] | |
pp_float [Ctypes] | |
pp_float [Wp.Ctypes] | |
pp_frame [LogicCompiler.Make] | |
pp_frame [Sigs.LogicSemantics] | |
pp_frame [Wp.LogicCompiler.Make] | |
pp_frame [Wp.Sigs.LogicSemantics] | |
pp_function [Wpo] | |
pp_function [Wp.Wpo] | |
pp_goal [Wpo] | |
pp_goal [Wp.Wpo] | |
pp_goal_flow [Wpo] | |
pp_goal_flow [Wp.Wpo] | |
pp_index [Wpo] | |
pp_index [Wp.Wpo] | |
pp_info_of_strategy [WpStrategy] | |
pp_int [Ctypes] | |
pp_int [Wp.Ctypes] | |
pp_logfile [Wpo] | |
pp_logfile [Wp.Wpo] | |
pp_logic [Cvalues] | |
pp_logic_label [Wp_error] | |
pp_mode [VCS] | |
pp_mode [Wp.VCS] | |
pp_node [Cil2cfg] | |
pp_node_type [Cil2cfg] | |
pp_object [Ctypes] | |
pp_object [Wp.Ctypes] | |
pp_param [MemoryContext] | |
pp_param [Wp.MemoryContext] | |
pp_pred [Lang.F] | |
pp_pred [Wp.Lang.F] | |
pp_pred_info [WpPropId] | |
pp_pred_info [Wp.WpPropId] | |
pp_pred_of_pred_info [WpPropId] | |
pp_pred_of_pred_info [Wp.WpPropId] | |
pp_profile [LogicUsage] | |
pp_profile [Wp.LogicUsage] | |
pp_propid [WpPropId] | Print unique id of |
pp_propid [Wp.WpPropId] | Print unique id of |
pp_prover [VCS] | |
pp_prover [Wp.VCS] | |
pp_region [Cvalues] | |
pp_result [VCS] | |
pp_result [Wp.VCS] | |
pp_result_qualif [VCS] | |
pp_result_qualif [Wp.VCS] | |
pp_rloc [Cvalues] | |
pp_script [ProofSession] | |
pp_script_for [ProofSession] | |
pp_selection [Tactical] | Debug only |
pp_selection [Wp.Tactical] | Debug only |
pp_sloc [Cvalues] | |
pp_string_list [Wp_error] | |
pp_suffix_id [Matrix] | |
pp_tau [Lang.F] | |
pp_tau [Wp.Lang.F] | |
pp_term [Lang.F] | |
pp_term [Wp.Lang.F] | |
pp_time [Rformat] | Pretty print time in hour, minutes, seconds, or milliseconds, as appropriate |
pp_time_range [Rformat] | |
pp_title [Wpo] | |
pp_title [Wp.Wpo] | |
pp_value [Sigs.CodeSemantics] | |
pp_value [Cvalues] | |
pp_value [Wp.Sigs.CodeSemantics] | |
pp_var [Lang.F] | |
pp_var [Wp.Lang.F] | |
pp_vars [Lang.F] | |
pp_vars [Wp.Lang.F] | |
pp_vset [Vset] | |
pp_vset [Wp.Vset] | |
pp_warnings [Register] | |
pp_warnings [Wpo] | |
pp_warnings [Wp.Wpo] | |
pp_wp_parameters [Register] | |
pprepeat [Vlist] | |
pre [Clabels] | |
pre [Wp.Clabels] | |
pred [LogicCompiler.Make] | |
pred [Sigs.LogicSemantics] | Compile a predicate. |
pred [Repr] | |
pred [Wp.LogicCompiler.Make] | |
pred [Wp.Sigs.LogicSemantics] | Compile a predicate. |
pred [Wp.Repr] | |
pred_e [Cil2cfg] | |
pred_info_id [WpPropId] | |
pred_info_id [Wp.WpPropId] | |
preproc_annot [NormAtLabels] | |
preproc_annot [Wp.NormAtLabels] | |
preproc_assigns [NormAtLabels] | |
preproc_assigns [Wp.NormAtLabels] | |
pretty [Interpreted_automata.UnrollUnnatural.G] | |
pretty [ProofEngine] | |
pretty [Wpo.DISK] | |
pretty [CfgCompiler.Cfg.E] | |
pretty [CfgCompiler.Cfg.T] | |
pretty [CfgCompiler.Cfg.P] | |
pretty [Pcond] | |
pretty [Conditions] | |
pretty [Sigs.Model] | pretty printing of memory location |
pretty [Sigs.Sigma] | For debugging purpose |
pretty [Sigs.Chunk] | |
pretty [Letify.Sigma] | |
pretty [Letify.Ground] | |
pretty [Cstring] | |
pretty [Vlist] | |
pretty [Vset] | |
pretty [Splitter] | |
pretty [Passive] | |
pretty [Matrix] | |
pretty [Mcfg.S] | |
pretty [WpPropId] | |
pretty [RegionAnnot.Lpath] | |
pretty [Layout.Chunk] | |
pretty [Layout.Root] | |
pretty [Layout.Cluster] | |
pretty [Layout.Overlay] | |
pretty [Layout.Range] | |
pretty [Layout.Matrix] | |
pretty [Layout.Value] | |
pretty [Layout.Usage] | |
pretty [Layout.Alias] | |
pretty [Layout.Data] | |
pretty [WpContext.Key] | |
pretty [WpContext.Entries] | |
pretty [Clabels] | |
pretty [Ctypes] | |
pretty [Warning] | |
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_edge [Interpreted_automata] | |
pretty_local [WpPropId] | |
pretty_local [Wp.WpPropId] | |
pretty_transition [Interpreted_automata] | |
prev [Pcfg] | |
prev [Wp.Pcfg] | |
print [RefUsage] | |
print [Wp.RefUsage] | |
print_generated [Wp_parameters] | print the given file if the debugging category "print-generated" is set |
print_generated [Wp.Wp_parameters] | print the given file if the debugging category "print-generated" is set |
print_why3 [Why3Provers] | |
print_wp [Why3Provers] | |
process [Cil2cfg.Dump] | |
process_global_init [CfgInit.Make] | |
promote [Ctypes] | |
promote [Wp.Ctypes] | |
proof [VC] | List of proof obligations computed for a given property. |
proof [ProofEngine] | |
proof [Wp.VC] | List of proof obligations computed for a given property. |
proof_context [LogicUsage] | Lemmas that are not in an axiomatic. |
proof_context [Wp.LogicUsage] | Lemmas that are not in an axiomatic. |
prop_id_keys [WpPropId] | |
prop_id_keys [Wp.WpPropId] | |
property [Wprop.Info] | |
property [Wprop.Indexed2] | |
property [Wprop.Indexed] | |
property_of_id [WpPropId] | returns the annotation which lead to the given PO. |
property_of_id [Wp.WpPropId] | returns the annotation which lead to the given PO. |
protect [Wp_parameters] | |
protect [Wp.Wp_parameters] | |
prove [VC] | Returns a ready-to-schedule task. |
prove [ProverScript] | |
prove [Prover] | |
prove [ProverWhy3] | Return NoResult if it is already proved by Qed |
prove [ProverCoq] | |
prove [ProverErgo] | |
prove [Wp.Prover] | |
prove [Wp.VC] | Returns a ready-to-schedule task. |
proved [ProofEngine] | |
prover_of_json [ProofScript] | |
prover_of_name [Wpo] | Dynamically exported. |
prover_of_name [Wp.Wpo] | Dynamically exported. |
provers [Register] | |
provers [Why3Provers] | |
provers_set [Why3Provers] | |
pruning [Conditions] | |
pruning [Wp.Conditions] | |
push [Context] | |
push [Wp.Context] | |
Q | |
qed_time [Wpo.GOAL] | |
qed_time [Wpo] | |
qed_time [Wp.Wpo.GOAL] | |
qed_time [Wp.Wpo] | |
R | |
range [Auto] | |
range [Tactical] | |
range [Vset] | |
range [Cint] | Dependent on model |
range [Layout.Offset] | |
range [Wp.Auto] | |
range [Wp.Tactical] | |
range [Wp.Vset] | |
range [Wp.Cint] | Dependent on model |
ranges [Auto.Range] | |
ranges [Wp.Auto.Range] | |
rdescr [Cvalues.Logic] | |
reachability [WpReached] | memoized reached cfg for function |
reads [CfgCompiler.Cfg.E] | |
reads [CfgCompiler.Cfg.T] | |
reads [CfgCompiler.Cfg.P] | |
reads [CfgCompiler.Cfg.C] | |
reads [Wp.CfgCompiler.Cfg.E] | |
reads [Wp.CfgCompiler.Cfg.T] | |
reads [Wp.CfgCompiler.Cfg.P] | |
reads [Wp.CfgCompiler.Cfg.C] | |
real_of_float [Cfloat] | |
real_of_float [Wp.Cfloat] | |
real_of_flt [Cfloat] | |
real_of_flt [Wp.Cfloat] | |
real_of_int [Cmath] | |
rebuild [Lang.For_export] | |
rebuild [Wp.Lang.For_export] | |
record [Lang] | |
record [Wp.Lang] | |
record_with [Lang.F] | |
record_with [Wp.Lang.F] | |
reduce [Wpo] | tries simplification |
reduce [Wp.Wpo] | tries simplification |
region [LogicCompiler.Make] | |
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] | |
region [Wp.Sigs.LogicSemantics] | Compile a term representing a set of memory locations into an abstract region. |
register [GuiPanel] | |
register [Register] | |
register [Strategy] | |
register [Tactical] | |
register [MemMemory] | |
register [Pcfg] | |
register [RegionAnnot] | Auto when `-wp-region` |
register [WpContext] | Model registration. |
register [Context] | Register a global configure, to be executed once per project/ast. |
register [Wp.Strategy] | |
register [Wp.Tactical] | |
register [Wp.Pcfg] | |
register [Wp.WpContext] | Model registration. |
register [Wp.Context] | Register a global configure, to be executed once per project/ast. |
register_lemma [CfgWP.VCgen] | |
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 [CfgCompiler.Cfg.C] | |
relocate [Wp.CfgCompiler.Cfg.E] | |
relocate [Wp.CfgCompiler.Cfg.T] | |
relocate [Wp.CfgCompiler.Cfg.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 [Wp.WpContext.Generator] | |
remove [Wp.WpContext.Registry] | |
remove [Hashtbl.S] | |
remove [Set.S] |
|
remove [Map.S] |
|
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 |
replace [Cil2cfg.HEsig] | |
replace [Wp.Tactical] | |
replace [Wp.Conditions] | replace a step in the sequent, the one |
replace [Hashtbl.S] | |
replace_seq [Hashtbl.S] | |
repr [Lang.F] | Constant time |
repr [WpContext.MODEL] | |
repr [Wp.Lang.F] | Constant time |
repr [Wp.WpContext.MODEL] | |
reset [ProofEngine] | |
reset [Wp_parameters] | |
reset [Hashtbl.S] | |
reset [Wp.Wp_parameters] | |
reshape [Layout.Cluster] | |
reshape [Layout.Compound] | |
resolve [Wpo.VC_Annot] | |
resolve [Wpo] | tries simplification and set result if valid |
resolve [Wp.Wpo.VC_Annot] | |
resolve [Wp.Wpo] | tries simplification and set result if valid |
result [VCS] | |
result [StmtSemantics.Make] | |
result [LogicCompiler.Make] | |
result [Sigs.LogicSemantics] | Result location of the current function in the current frame. |
result [Sigs.CodeSemantics] | Value of an abstract result container. |
result [Wp.VCS] | |
result [Wp.StmtSemantics.Make] | |
result [Wp.LogicCompiler.Make] | |
result [Wp.Sigs.LogicSemantics] | Result location of the current function in the current frame. |
result [Wp.Sigs.CodeSemantics] | Value of an abstract result container. |
result_of_json [ProofScript] | |
results [Register] | |
return [StmtSemantics.Make] | |
return [LogicCompiler.Make] | |
return [Sigs.LogicSemantics] | Result type of the current function in the current frame. |
return [Sigs.CodeSemantics] | Return an expression with a given type. |
return [Mcfg.S] | |
return [Wp.StmtSemantics.Make] | |
return [Wp.LogicCompiler.Make] | |
return [Wp.Sigs.LogicSemantics] | Result type of the current function in the current frame. |
return [Wp.Sigs.CodeSemantics] | Return an expression with a given type. |
return [Wp.Mcfg.S] | |
rewrite [Tactical] | For each pattern |
rewrite [Wp.Tactical] | For each pattern |
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 |
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 names. |
select_by_name [Wp.WpPropId] | test if the prop_id has to be selected for the asked names. |
select_call_pre [WpPropId] | test if the prop_id has to be selected when we want to select the call. |
select_call_pre [Wp.WpPropId] | test if the prop_id has to be selected when we want to select the call. |
select_default [WpPropId] | test if the prop_id does not have a |
select_default [Wp.WpPropId] | test if the prop_id does not have a |
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_for_behaviors [WpPropId] | test if the prop_id has to be selected for the asked behavior names. |
select_for_behaviors [Wp.WpPropId] | test if the prop_id has to be selected for the asked behavior names. |
select_p [Strategy] | Same as |
select_p [Wp.Strategy] | Same as |
selected [Tactical] | |
selected [Wp.Tactical] | |
selection_of_json [ProofScript] | |
selection_target [ProofScript] | |
selector [Tactical] | Unless specified, default is head option. |
selector [Wp.Tactical] | Unless specified, default is head option. |
self [Sigs.Chunk] | Chunk names, for pretty-printing. |
self [Wp.Sigs.Chunk] | Chunk names, for pretty-printing. |
separated [Auto] | |
separated [MemMemory] | |
separated [Sigs.Model] | Return the formula that tests if two segment are separated |
separated [Cvalues.Logic] | |
separated [Wp.Auto] | |
separated [Wp.Sigs.Model] | Return the formula that tests if two segment are separated |
seq_branch [Conditions] | Creates an If-Then-Else branch located at the provided stmt, if any. |
seq_branch [Wp.Conditions] | Creates an If-Then-Else branch located at the provided stmt, if any. |
sequence [Register] | |
sequence [StmtSemantics.Make] | Chain compiler by introducing fresh nodes between each element of the list. |
sequence [Conditions] | |
sequence [Wp.StmtSemantics.Make] | Chain compiler by introducing fresh nodes between each element of the list. |
sequence [Wp.Conditions] | |
server [VC] | Default number of parallel tasks is given by |
server [ProverTask] | |
server [Wp.ProverTask] | |
server [Wp.VC] | Default number of parallel tasks is given by |
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_doomed [WpReached] | |
set_init [MemLoader.Model] | |
set_init_atom [MemLoader.Model] | |
set_mode [Cache] | |
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] | |
set_unreachable [WpAnnot] | |
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 |
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 |
sigma [Lang] | uses current pool |
sigma [Wp.Lang] | uses current pool |
signature [Tactical] | |
signature [Wp.Tactical] | |
signed [Ctypes] |
|
signed [Wp.Ctypes] |
|
simplify [Prover] | |
simplify [Conditions] | |
simplify [Mcfg.Splitter] | |
simplify [Wp.Prover] | |
simplify [Wp.Conditions] | |
simplify [Wp.Mcfg.Splitter] | |
singleton [Letify.Ground] | |
singleton [Vset] | |
singleton [Splitter] | |
singleton [Layout.Chunk] | |
singleton [Wp.Vset] | |
singleton [Wp.Splitter] | |
singleton [Set.S] |
|
singleton [Map.S] |
|
size [Conditions] | Compute the total number of steps in the sequence, including nested sequences from branches and disjunctions. |
size [Wp.Conditions] | Compute the total number of steps in the sequence, including nested sequences from branches and disjunctions. |
sizeof [MemLoader.Model] | |
sizeof [Layout.Matrix] | |
sizeof [Layout.Value] | |
sizeof [Layout.Offset] | |
sizeof_defined [Ctypes] | |
sizeof_defined [Wp.Ctypes] | |
sizeof_object [Ctypes] | |
sizeof_object [Wp.Ctypes] | |
skip [Script] | |
smoke_status [GuiProver] | |
smoked [VCS] | |
smoked [Wp.VCS] | |
smoking [CfgInfos] | |
smoking [WpReached] | Returns whether a stmt need a smoke tests to avoid being unreachable. |
sort [Lang.F] | Constant time |
sort [Wp.Lang.F] | Constant time |
source_of_id [WpPropId] | |
source_of_id [Wp.WpPropId] | |
spawn [VC] | Same as |
spawn [ProverScript] | |
spawn [Prover] | |
spawn [ProverTask] | |
spawn [Wp.Prover] | |
spawn [Wp.ProverTask] | |
spawn [Wp.VC] | Same as |
spawn_wp_proofs [Register] | |
spec [StmtSemantics.Make] | |
spec [Wp.StmtSemantics.Make] | |
specialize_eq_list [Vlist] | |
spinner [Tactical] | Unless specified, default is |
spinner [Wp.Tactical] | Unless specified, default is |
split [Auto] | |
split [Tactical] | |
split [Mcfg.Splitter] | |
split [Wp.Auto] | |
split [Wp.Tactical] | |
split [Wp.Mcfg.Splitter] | |
split [Set.S] |
|
split [Map.S] |
|
split_bag [WpPropId] | |
split_bag [Wp.WpPropId] | |
split_map [WpPropId] | |
split_map [Wp.WpPropId] | |
start_edge [Cil2cfg] | get the starting edges |
start_stmt_of_node [Cil2cfg] | |
startof [Cvalues] | Shift a location with 0-indices wrt to its array type |
state [Conditions] | Stack a memory model state on top of the bundle. |
state [Mstate] | |
state [Sigs.Model] | Returns a memory state description from a memory environement. |
state [Wp.Conditions] | Stack a memory model state on top of the bundle. |
state [Wp.Mstate] | |
state [Wp.Sigs.Model] | Returns a memory state description from a memory environement. |
stats [Hashtbl.S] | |
status [ProofEngine] | |
status [LogicCompiler.Make] | |
status [Sigs.LogicSemantics] | Exit status for the current frame. |
status [Wp.LogicCompiler.Make] | |
status [Wp.Sigs.LogicSemantics] | Exit status for the current frame. |
step [Conditions] | Creates a single step |
step [Wp.Conditions] | Creates a single step |
step_at [Conditions] | Retrieve a step by |
step_at [Wp.Conditions] | Retrieve a step by |
stepout [ProverTask] | |
stepout [VCS] | |
stepout [Wp.ProverTask] | |
stepout [Wp.VCS] | |
steps [Conditions] | Attributes unique indices to every |
steps [Wp.Conditions] | Attributes unique indices to every |
stmt [Clabels] | |
stmt [Wp.Clabels] | |
stmt_post [Clabels] | |
stmt_post [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. |
stored_init [MemLoader.Make] | |
stored_init [Sigs.Model] | Return a set of formula that express a modification of the initialization status between two memory state. |
stored_init [Wp.Sigs.Model] | Return a set of formula that express a modification of the initialization status 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 |
str_len [Wp.Cstring] | Property defining the size of the string in bytes,
with |
str_val [Cstring] | The array containing the |
str_val [Wp.Cstring] | The array containing the |
strange_loops [Cil2cfg] | detect is there are non natural loops or natural loops where we didn't
manage to compute back edges (see |
strategy [TacCongruence] | |
strategy [TacShift] | |
strategy [TacBittest] | |
strategy [TacBitrange] | |
strategy [TacBitwised] | |
strategy [TacRewrite] | |
strategy [TacNormalForm] | |
strategy [TacCut] | |
strategy [TacFilter] | |
strategy [TacLemma] | |
strategy [TacInstance] | |
strategy [TacHavoc.Validity] | |
strategy [TacHavoc.Separated] | |
strategy [TacHavoc.Havoc] | |
strategy [TacUnfold] | |
strategy [TacCompound] | |
strategy [TacArray] | |
strategy [TacRange] | |
strategy [TacChoice.Contrapose] | |
strategy [TacChoice.Absurd] | |
strategy [TacChoice.Choice] | |
strategy [TacSplit] | |
strategy_has_asgn_goal [WpStrategy] | |
strategy_has_prop_goal [WpStrategy] | |
strategy_kind [WpStrategy] | |
string_of_termination_kind [WpPropId] | TODO: should probably be somewhere else |
string_of_termination_kind [Wp.WpPropId] | TODO: should probably be somewhere else |
sub_c_int [Ctypes] | |
sub_c_int [Wp.Ctypes] | |
sub_range [Vset] | |
sub_range [Wp.Vset] | |
subclause [Tactical] | When |
subclause [Wp.Tactical] | When |
subproof_idx [WpPropId] | subproof index of this propr_id |
subproof_idx [Wp.WpPropId] | subproof index of this propr_id |
subproofs [WpPropId] | How many subproofs |
subproofs [Wp.WpPropId] | How many subproofs |
subset [Cvalues.Logic] | |
subset [Vset] | |
subset [Wp.Vset] | |
subset [Set.S] |
|
subst [Conditions] | Apply the atomic substitution recursively using |
subst [Lang] | replace variables |
subst [Wp.Conditions] | Apply the atomic substitution recursively using |
subst [Wp.Lang] | replace variables |
subterms [Pcfg] | |
subterms [Wp.Pcfg] | |
succ_e [Cil2cfg] | |
switch [Mcfg.S] | |
switch [Wp.Mcfg.S] | |
switch_cases [Splitter] | |
switch_cases [Wp.Splitter] | |
switch_default [Splitter] | |
switch_default [Wp.Splitter] | |
T | |
t32 [Cfloat] | |
t32 [Wp.Cfloat] | |
t64 [Cfloat] | |
t64 [Wp.Cfloat] | |
t_absurd [Auto] | Find a contradiction. |
t_absurd [Wp.Auto] | Find a contradiction. |
t_addr [MemMemory] | |
t_addr [Lang] | |
t_addr [Wp.Lang] | |
t_array [Lang] | |
t_array [Wp.Lang] | |
t_bool [Lang] | |
t_bool [Wp.Lang] | |
t_case [Auto] | Case analysis: |
t_case [Wp.Auto] | Case analysis: |
t_cases [Auto] | Complete analysis: applies each process under its guard, and proves that all guards are complete. |
t_cases [Wp.Auto] | Complete analysis: applies each process under its guard, and proves that all guards are complete. |
t_chain [Auto] | Apply second process to every goal generated by the first one. |
t_chain [Wp.Auto] | Apply second process to every goal generated by the first one. |
t_comp [Lang] | |
t_comp [Wp.Lang] | |
t_cut [Auto] | Prove condition |
t_cut [Wp.Auto] | Prove condition |
t_datatype [Lang] | |
t_datatype [Wp.Lang] | |
t_descr [Auto] | Apply a description to each sub-goal |
t_descr [Wp.Auto] | Apply a description to each sub-goal |
t_farray [Lang] | |
t_farray [Wp.Lang] | |
t_finally [Auto] | Apply a description to a leaf goal. |
t_finally [Wp.Auto] | Apply a description to a leaf goal. |
t_float [Lang] | |
t_float [Wp.Lang] | |
t_id [Auto] | Keep goal unchanged. |
t_id [Wp.Auto] | Keep goal unchanged. |
t_init [MemMemory] | initialization tables |
t_init [Lang] | |
t_init [Wp.Lang] | |
t_int [Lang] | |
t_int [Wp.Lang] | |
t_malloc [MemMemory] | allocation tables |
t_matrix [Lang] | |
t_matrix [Wp.Lang] | |
t_mem [MemMemory] | t_addr indexed array |
t_prop [Lang] | |
t_prop [Wp.Lang] | |
t_range [Auto] | |
t_range [Wp.Auto] | |
t_real [Lang] | |
t_real [Wp.Lang] | |
t_replace [Auto] | Prove |
t_replace [Wp.Auto] | Prove |
t_split [Auto] | Split with |
t_split [Wp.Auto] | Split with |
tactical [ProofEngine] | |
tactical [TacCongruence] | |
tactical [TacSequence] | |
tactical [TacShift] | |
tactical [TacBittest] | |
tactical [TacBitrange] | |
tactical [TacBitwised] | |
tactical [TacRewrite] | |
tactical [TacNormalForm] | |
tactical [TacCut] | |
tactical [TacFilter] | |
tactical [TacLemma] | |
tactical [TacInstance] | |
tactical [TacHavoc.Validity] | |
tactical [TacHavoc.Separated] | |
tactical [TacHavoc.Havoc] | |
tactical [TacUnfold] | |
tactical [TacCompound] | |
tactical [TacArray] | |
tactical [TacInduction] | |
tactical [TacRange] | |
tactical [TacChoice.Contrapose] | |
tactical [TacChoice.Absurd] | |
tactical [TacChoice.Choice] | |
tactical [TacSplit] | |
tactical [WpPropId] | |
tactical [Wp.WpPropId] | |
target [WpPropId] | |
target [Wp.WpPropId] | |
tau_of_chunk [Sigs.Chunk] | The type of data hold in a chunk. |
tau_of_chunk [Wp.Sigs.Chunk] | The type of data hold in a chunk. |
tau_of_ctype [Lang] | |
tau_of_ctype [Wp.Lang] | |
tau_of_field [Lang] | |
tau_of_field [Wp.Lang] | |
tau_of_float [Cfloat] | with respect to model |
tau_of_float [Wp.Cfloat] | with respect to model |
tau_of_lfun [Lang] | |
tau_of_lfun [Wp.Lang] | |
tau_of_ltype [Lang] | |
tau_of_ltype [Wp.Lang] | |
tau_of_object [Lang] | |
tau_of_object [Wp.Lang] | |
tau_of_record [Lang] | |
tau_of_record [Wp.Lang] | |
tau_of_return [Lang] | |
tau_of_return [Wp.Lang] | |
tau_of_set [Vset] | |
tau_of_set [Wp.Vset] | |
tau_of_var [Lang.F] | |
tau_of_var [Wp.Lang.F] | |
term [LogicCompiler.Make] | |
term [Sigs.LogicSemantics] | Compile a term expression. |
term [Repr] | |
term [Wp.LogicCompiler.Make] | |
term [Wp.Sigs.LogicSemantics] | Compile a term expression. |
term [Wp.Repr] | |
test [Mcfg.S] | |
test [Wp.Mcfg.S] | |
timeout [ProverTask] | |
timeout [VCS] | |
timeout [Wp.ProverTask] | |
timeout [Wp.VCS] | |
title [ProofEngine] | |
title [Why3Provers] | |
title_of_mode [VCS] | |
title_of_mode [Wp.VCS] | |
title_of_prover [VCS] | |
title_of_prover [Wp.VCS] | |
to_addr [MemLoader.Model] | |
to_cint [Cint] | Raises |
to_cint [Wp.Cint] | Raises |
to_condition [CfgCompiler.Cfg.P] | |
to_condition [Wp.CfgCompiler.Cfg.P] | |
to_integer [Cint] | |
to_integer [Wp.Cint] | |
to_logic [Clabels] | |
to_logic [Wp.Clabels] | |
to_region_pointer [MemLoader.Model] | |
to_seq [Hashtbl.S] | |
to_seq [Set.S] | Iterate on the whole set, in ascending order |
to_seq [Map.S] | Iterate on the whole map, in ascending order of keys |
to_seq_from [Set.S] |
|
to_seq_from [Map.S] |
|
to_seq_keys [Hashtbl.S] | |
to_seq_values [Hashtbl.S] | |
token [Script] | |
top [Letify.Ground] | |
tracelog [Register] | |
trans [Filter_axioms] | |
transfer [Interpreted_automata.Domain] | Transfer function for transitions: computes the state after the transition from the state before. |
tree_context [ProofEngine] | |
trigger [LogicCompiler.Make] | |
trigger [Wp.LogicCompiler.Make] | |
trivial [Wpo.GOAL] | |
trivial [Conditions] | empty implies true |
trivial [Wp.Wpo.GOAL] | |
trivial [Wp.Conditions] | empty implies true |
try_sequence [Register] | |
type_id [Lang] | |
type_id [Wp.Lang] | |
typeof [Lang.F] | Try to extract a type of term. |
typeof [Layout.Offset] | |
typeof [Wp.Lang.F] | Try to extract a type of term. |
typeof_chain [Layout.Offset] | |
U | |
unchanged [Sigs.CodeSemantics] | Express that a given variable has the same value in two memory states. |
unchanged [Wp.Sigs.CodeSemantics] | Express that a given variable has the same value in two memory states. |
uninitialized_obj [Cvalues] | |
union [Sigs.Sigma] | Same as |
union [Cvalues.Logic] | |
union [Vset] | |
union [Splitter] | |
union [Passive] | |
union [Layout.Chunk] | |
union [Wp.Sigs.Sigma] | Same as |
union [Wp.Vset] | |
union [Wp.Splitter] | |
union [Wp.Passive] | |
union [Set.S] | Set union. |
union [Map.S] |
|
union_map [Layout.Chunk] | |
unknown [VCS] | |
unknown [Wp.VCS] | |
unmark [Splitter] | erase all tags |
unmark [Wp.Splitter] | erase all tags |
unreachable [CfgInfos] | |
unreachable_failed [WpAnnot] | |
unreachable_if_valid [WpPropId] | Stmt that is unreachable in case the PO is valid. |
unreachable_if_valid [Wp.WpPropId] | Stmt that is unreachable in case the PO is valid. |
unreachable_nodes [Cil2cfg] | |
unreachable_proved [WpAnnot] | |
unroll_unnatural_loop [Interpreted_automata.UnrollUnnatural] | |
unsupported [Wp_error] | |
update [GuiPanel] | |
update [WpContext.Registry] | set current value, with no protection |
update [Context] | Modification of the current value |
update [Wp.WpContext.Registry] | set current value, with no protection |
update [Wp.Context] | Modification of the current value |
update [Map.S] |
|
update_cond [Conditions] | Updates the condition of a step and merges |
update_cond [Wp.Conditions] | Updates the condition of a step and merges |
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 [Wp.Mcfg.S] |
|
user_bhv_names [WpPropId] | |
user_bhv_names [Wp.WpPropId] | |
user_pred_names [WpPropId] | |
user_pred_names [Wp.WpPropId] | |
user_prop_names [WpPropId] | This is used to give the name of the property that the user can give to select it from the command line (-wp-prop option) |
user_prop_names [Wp.WpPropId] | |
user_setup [Generator] | |
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 |
val_of_term [Wp.Sigs.LogicSemantics] | Same as |
valid [VCS] | |
valid [Sigs.Model] | Return the formula that tests if a memory state is valid
(according to |
valid [Cvalues.Logic] | |
valid [Wp.VCS] | |
valid [Wp.Sigs.Model] | Return the formula that tests if a memory state is valid
(according to |
validate [ProofEngine] | |
value [Sigs.Sigma] | Same as |
value [Cvalues.Logic] | |
value [Wp.Sigs.Sigma] | Same as |
value_footprint [MemLoader.Model] | |
vanti [TacFilter] | |
vars [Sigs.LogicSemantics] | Qed variables appearing in a region expression. |
vars [Sigs.Model] | Return the logic variables from which the given location depend on. |
vars [Vset] | |
vars [Definitions.Trigger] | |
vars [Lang.F] | Constant time |
vars [Wp.Sigs.LogicSemantics] | Qed variables appearing in a region expression. |
vars [Wp.Sigs.Model] | Return the logic variables from which the given location depend on. |
vars [Wp.Vset] | |
vars [Wp.Definitions.Trigger] | |
vars [Wp.Lang.F] | Constant time |
vars_hyp [Conditions] | Pre-computed and available in constant time. |
vars_hyp [Wp.Conditions] | Pre-computed and available in constant time. |
vars_seq [Conditions] | At the cost of the union of hypotheses and goal. |
vars_seq [Wp.Conditions] | At the cost of the union of hypotheses and goal. |
varsp [Lang.F] | Constant time |
varsp [Wp.Lang.F] | Constant time |
vcgen [CfgWP] | |
verdict [VCS] | |
verdict [Wp.VCS] | |
version [Why3Provers] | |
very_strange_loops [Cil2cfg] | detect is there are natural loops where we didn't manage to compute
back edges (see |
visible [Pcfg] | |
visible [Wp.Pcfg] | |
vmax [TacRange] | |
vmin [TacRange] | |
volatile [Cvalues] | Check if a volatile access must be properly modelled or ignored. |
vset [Cvalues.Logic] | |
W | |
warn [MemoryContext] | |
warn [AssignsCompleteness] | Displays a warning if the given kernel function has incomplete assigns. |
warn [Wp.AssignsCompleteness] | Displays a warning if the given kernel function has incomplete assigns. |
warn [Wp.MemoryContext] | |
warnings [Wpo] | |
warnings [Wp.Wpo] | |
wg_status [GuiProver] | |
widen [Interpreted_automata.Domain] |
|
with_callees [WpTarget] | |
with_current_loc [Context] | |
with_current_loc [Wp.Context] | |
without_assume [Lang] | |
without_assume [Wp.Lang] | |
wkey_pedantic [AssignsCompleteness] | |
wkey_pedantic [Wp.AssignsCompleteness] | |
wkey_smoke [Register] | |
wp_compute_memory_context [Register] | |
wp_insert_memory_context [Register] | |
wp_iter_model [Register] | |
wp_warn_memory_context [Register] | |
wrap [TacInstance] | |
writes [CfgCompiler.Cfg.E] | as defined by S.writes |
writes [Sigs.Sigma] |
|
writes [Wp.CfgCompiler.Cfg.E] | as defined by S.writes |
writes [Wp.Sigs.Sigma] |
|
wto_index_diff [Interpreted_automata.Compute] | |
wto_index_diff [Interpreted_automata] |