( * ) [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_base [MemTyped] | |
a_base [Wp.MemTyped] | |
a_offset [MemTyped] | |
a_offset [Wp.MemTyped] | |
a_prover [ProofScript] | |
a_tactic [ProofScript] | |
absurd [Auto] | |
absurd [Wp.Auto] | |
access [Region] | |
acsl_lit [Cfloat] | |
acsl_lit [Wp.Cfloat] | |
add [Wpo] | |
add [Letify.Split] | |
add [Letify.Defs] | |
add [Letify.Sigma] | |
add [Warning] | |
add [Cil2cfg.HEsig] | |
add [Wp.Wpo] | |
add [Map.S] |
|
add [Set.S] |
|
add [Hashtbl.S] | |
add [Wp.Warning] | |
add [FCMap.S] |
|
add_alias [LogicBuiltins] | |
add_alias [Wp.LogicBuiltins] | |
add_all_axioms [WpStrategy] | |
add_assigns [WpStrategy] | generic function to add an assigns property. |
add_assigns [Mcfg.S] | |
add_assigns [Wp.Mcfg.S] | |
add_assigns_any [WpStrategy] | generic function to add a WriteAny assigns property. |
add_axiom [WpStrategy] | |
add_axiom [Mcfg.S] | |
add_axiom [Wp.Mcfg.S] | |
add_builtin [LogicBuiltins] | Add a new builtin. |
add_builtin [Wp.LogicBuiltins] | Add a new builtin. |
add_call_assigns_any [WpStrategy] | short cut to add a dynamic call |
add_call_assigns_hyp [WpStrategy] | shortcut to add a call assigns property as an hypothesis. |
add_composer [Tactical] | |
add_composer [Wp.Tactical] | |
add_ctor [LogicBuiltins] | |
add_ctor [Wp.LogicBuiltins] | |
add_definitions [Letify] |
|
add_fct_bhv_assigns_hyp [WpStrategy] | |
add_goal [Mcfg.S] | |
add_goal [Wp.Mcfg.S] | |
add_hook [Wprop.Indexed2] | Hooks are executed once at property creation |
add_hook [Wprop.Indexed] | Hooks are executed once at property creation |
add_hyp [Mcfg.S] | |
add_hyp [Wp.Mcfg.S] | |
add_library [LogicBuiltins] | Add a new library or update the dependencies of an existing one |
add_library [Wp.LogicBuiltins] | Add a new library or update the dependencies of an existing one |
add_logic [LogicBuiltins] | |
add_logic [Wp.LogicBuiltins] | |
add_loop_annots [WpStrategy] | |
add_loop_assigns_hyp [WpStrategy] | shortcut to add a loop assigns property as an hypothesis. |
add_node_annots [WpStrategy] |
|
add_on_edges [WpStrategy] | |
add_option [LogicBuiltins] | add a value to an option (group, name) |
add_option [Wp.LogicBuiltins] | add a value to an option (group, name) |
add_predicate [LogicBuiltins] | |
add_predicate [Wp.LogicBuiltins] | |
add_proof [WpAnnot] | accumulate in the proof the partial proof for this prop_id |
add_prop [WpStrategy] | generic function to add a predicate property after normalisation. |
add_prop_assert [WpStrategy] | |
add_prop_call_post [WpStrategy] | Add a postcondition of a called function. |
add_prop_call_pre [WpStrategy] | |
add_prop_fct_bhv_pre [WpStrategy] | Add the preconditions of the behavior :
if |
add_prop_fct_post [WpStrategy] | |
add_prop_fct_pre [WpStrategy] | Add the predicate as a function precondition. |
add_prop_loop_inv [WpStrategy] | |
add_prop_stmt_bhv_requires [WpStrategy] | Add all the |
add_prop_stmt_post [WpStrategy] | Add the predicate as a stmt precondition. |
add_prop_stmt_pre [WpStrategy] | Add the predicate as a stmt precondition. |
add_prop_stmt_spec_pre [WpStrategy] | Process the stmt spec precondition as an hypothesis for external properties. |
add_script [Proof] |
|
add_step [Register] | |
add_stmt_spec_assigns_hyp [WpStrategy] | shortcut to add a stmt spec assigns property as an hypothesis. |
add_time [Register] | |
add_tmpnode [CfgCompiler.Cfg] | Set a node as temporary. |
add_tmpnode [Wp.CfgCompiler.Cfg] | Set a node as temporary. |
add_type [LogicBuiltins] | |
add_type [Wp.LogicBuiltins] | |
add_var [Lang.F] | |
add_var [Wp.Lang.F] | |
add_vars [Lang.F] | |
add_vars [Wp.Lang.F] | |
age [Wpo] | |
age [Wp.Wpo] | |
ainf [Cvalues] | Array lower-bound, ie `Some(0)` |
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] | |
anchor [ProofEngine] | |
append [Conditions] | |
append [Wp.Conditions] | |
append_after [Parameter_sig.List] | append a list at the end of the current state |
append_before [Parameter_sig.List] | append a list in front of the current state |
apply [Mstate] | |
apply [Sigs.Model] | Propagate a sequent substitution inside the memory state. |
apply [Cvalues.Logic] | |
apply [Passive] | |
apply [Wp.Mstate] | |
apply [Wp.Sigs.Model] | Propagate a sequent substitution inside the memory state. |
apply [Wp.Passive] | |
apply_add [Cvalues.Logic] | |
apply_assigns [Sigs.LogicAssigns] | Relates two memory states corresponding to an assigns clause with the specified set of locations. |
apply_assigns [Wp.Sigs.LogicAssigns] | Relates two memory states corresponding to an assigns clause with the specified set of locations. |
apply_sub [Cvalues.Logic] | |
are_equal [Lang.F] | Computes equality |
are_equal [Wp.Lang.F] | Computes equality |
arg [Strategy] | |
arg [Wp.Strategy] | |
array [Auto] | |
array [Wp.Auto] | |
array_dimensions [Ctypes] | Returns the list of dimensions the array consists of. |
array_dimensions [Wp.Ctypes] | Returns the list of dimensions the array consists of. |
array_size [Ctypes] | |
array_size [Wp.Ctypes] | |
as_atom [Cleaning] | |
as_have [Cleaning] | |
as_init [Cleaning] | |
as_type [Cleaning] | |
assemble_goal [ProverWhy3] | None if the po is trivial |
assign [Mcfg.S] | |
assign [Wp.Mcfg.S] | |
assigned [Sigs.Model] | Return a set of formula that express that two memory state are the same except at the given set of memory location. |
assigned [Sigs.Sigma] | Make chunks equal outside of some domain. |
assigned [Wp.Sigs.Model] | Return a set of formula that express that two memory state are the same except at the given set of memory location. |
assigned [Wp.Sigs.Sigma] | Make chunks equal outside of some domain. |
assigned_of_assigns [Sigs.LogicSemantics] | Computes the region assigned by an assigns clause. |
assigned_of_assigns [Wp.Sigs.LogicSemantics] | Computes the region assigned by an assigns clause. |
assigned_of_froms [Sigs.LogicSemantics] | Computes the region assigned by a list of froms. |
assigned_of_froms [Wp.Sigs.LogicSemantics] | Computes the region assigned by a list of froms. |
assigns [StmtSemantics.Make] | |
assigns [Wp.StmtSemantics.Make] | |
assigns_info_id [WpPropId] | |
assigns_info_id [Wp.WpPropId] | |
assigns_upper_bound [WpStrategy] | |
assume [StmtSemantics.Make] | |
assume [CfgCompiler.Cfg] | Represents execution traces |
assume [Conditions] | |
assume [Letify.Sigma] | |
assume [Lang] | |
assume [Wp.StmtSemantics.Make] | |
assume [Wp.CfgCompiler.Cfg] | Represents execution traces |
assume [Wp.Conditions] | |
assume [Wp.Lang] | |
assume_ [StmtSemantics.Make] | |
assume_ [Wp.StmtSemantics.Make] | |
asup [Cvalues] | Array upper-bound, ie `Some(n-1)` |
at [Tactical] | |
at [Pcfg] | |
at [Wp.Tactical] | |
at [Wp.Pcfg] | |
at_closure [Conditions] | register a transformation applied just before close |
at_closure [Wp.Conditions] | register a transformation applied just before close |
at_exit [Clabels] | |
at_exit [Wp.Clabels] | |
atype [Lang] | |
atype [Wp.Lang] | |
auto_check [Register] | |
auto_range [Auto] | |
auto_range [Wp.Auto] | |
auto_split [Auto] | |
auto_split [Wp.Auto] | |
autofit [VCS] | Result that fits the default configuration |
autofit [Wp.VCS] | Result that fits the default configuration |
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. |
basename [Lang.F] | |
basename [LogicUsage] | Trims the original name |
basename [Ctypes] | |
basename [Wp.Lang.F] | |
basename [Wp.LogicUsage] | Trims the original name |
basename [Wp.Ctypes] | |
basename_of_chunk [Sigs.Chunk] | Used when generating fresh variables for a chunk. |
basename_of_chunk [Wp.Sigs.Chunk] | Used when generating fresh variables for a chunk. |
begin_session [Register] | |
behavior_name_of_strategy [WpStrategy] | |
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. |
bindings [FCMap.S] | Return the list of all bindings of the given map. |
block_length [Sigs.Model] | Returns the length (in bytes) of the allocated block containing the given location. |
block_length [Wp.Sigs.Model] | Returns the length (in bytes) of the allocated block containing the given location. |
blocks_closed_by_edge [Cil2cfg] | |
blsl [Cint] | |
blsl [Wp.Cint] | |
blsr [Cint] | |
blsr [Wp.Cint] | |
bnot [Cint] | |
bnot [Wp.Cint] | |
bool_and [Cvalues] | |
bool_eq [Cvalues] | |
bool_leq [Cvalues] | |
bool_lt [Cvalues] | |
bool_neq [Cvalues] | |
bool_or [Cvalues] | |
bool_val [Cvalues] | |
bootstrap_logic [LogicCompiler.Make] | |
bootstrap_logic [Wp.LogicCompiler.Make] | |
bootstrap_pred [LogicCompiler.Make] | |
bootstrap_pred [Wp.LogicCompiler.Make] | |
bootstrap_region [LogicCompiler.Make] | |
bootstrap_region [Wp.LogicCompiler.Make] | |
bootstrap_term [LogicCompiler.Make] | |
bootstrap_term [Wp.LogicCompiler.Make] | |
bor [Cint] | |
bor [Wp.Cint] | |
bound [ProofEngine] | |
bound_add [Vset] | |
bound_add [Wp.Vset] | |
bound_shift [Vset] | |
bound_shift [Wp.Vset] | |
bound_sub [Vset] | |
bound_sub [Wp.Vset] | |
bounds [Auto.Range] | |
bounds [Ctypes] | domain, bounds included |
bounds [Wp.Auto.Range] | |
bounds [Wp.Ctypes] | domain, bounds included |
branch [CfgCompiler.Cfg] | Structurally corresponds to an if-then-else control-flow. |
branch [Conditions] | |
branch [Letify.Ground] | |
branch [Wp.CfgCompiler.Cfg] | Structurally corresponds to an if-then-else control-flow. |
branch [Wp.Conditions] | |
branching [Pcfg] | |
branching [Wp.Pcfg] | |
break [Clabels] | |
break [Wp.Clabels] | |
build_prop_of_from [Mcfg.S] | build |
build_prop_of_from [Wp.Mcfg.S] | build |
bundle [Pcond] | |
bundle [Conditions] | |
bundle [Wp.Pcond] | |
bundle [Wp.Conditions] | |
bxor [Cint] | |
bxor [Wp.Cint] | |
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_int_all [Ctypes] | |
c_int_all [Wp.Ctypes] | |
c_ptr [Ctypes] | Returns the type of pointers |
c_ptr [Wp.Ctypes] | Returns the type of pointers |
cache_descr [Wpo.VC_Annot] | |
cache_descr [Wpo.VC_Lemma] | |
cache_descr [Wp.Wpo.VC_Annot] | |
cache_descr [Wp.Wpo.VC_Lemma] | |
cache_log [Wpo.DISK] | |
cache_log [Wp.Wpo.DISK] | |
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 [Model.Registry] | |
callback [Wp.Model.Registry] | |
cancel [ProofEngine] | |
cardinal [TacInstance] | less than limit |
cardinal [Map.S] | Return the number of bindings of a map. |
cardinal [Set.S] | Return the number of elements of a set. |
cardinal [FCMap.S] | Return the number of bindings of a map. |
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. |
catch [Warning] | Set up a context for the job. |
catch [Wp.Warning] | Set up a context for the job. |
catch_label_error [NormAtLabels] | |
catch_label_error [Wp.NormAtLabels] | |
cdomain [Cvalues] | |
cfg_kf [Cil2cfg] | |
cfg_of_strategy [WpStrategy] | |
cfg_spec_only [Cil2cfg] | returns |
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 |
checked [VCS] | |
checked [Wp.VCS] | |
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 [Sigs.Sigma] | Make the union of each sigma, choosing the minimal variable in case of conflict. |
choose [Map.S] | Return one binding of the given map, or raise |
choose [Set.S] | Return one element of the given set, or raise |
choose [Wp.Sigs.Sigma] | Make the union of each sigma, choosing the minimal variable in case of conflict. |
choose [FCMap.S] | Return one binding of the given map, or raise |
choose_opt [Map.S] | Return one binding of the given map, or |
choose_opt [Set.S] | Return one element of the given set, or |
cint [Tactical] | |
cint [Wp.Tactical] | |
clean [Conditions] | |
clean [Wp.Conditions] | |
clear [VC] | |
clear [Wpo] | |
clear [Proof] | |
clear [Model.Generator] | |
clear [Model.Registry] | |
clear [Context] | Clear the current value. |
clear [Cil2cfg.HEsig] | |
clear [Wp.Wpo] | |
clear [Wp.VC] | |
clear [Hashtbl.S] | |
clear [Wp.Model.Generator] | |
clear [Wp.Model.Registry] | |
clear [Wp.Context] | Clear the current value. |
clear_results [Wpo] | |
clear_results [Wp.Wpo] | |
clear_scheduled [Register] | |
clear_session [Register] | |
cloc [Sigs.CodeSemantics] | Interpret a value as a location. |
cloc [Wp.Sigs.CodeSemantics] | Interpret a value as a location. |
close [Script] | |
close [Conditions] | With free variables quantified. |
close [Mcfg.S] | |
close [Wp.Conditions] | With free variables quantified. |
close [Wp.Mcfg.S] | |
cluster [Cstring] | The cluster where all strings are defined. |
cluster [Definitions] | |
cluster [Wp.Cstring] | The cluster where all strings are defined. |
cluster [Wp.Definitions] | |
cluster_age [Definitions] | |
cluster_age [Wp.Definitions] | |
cluster_compare [Definitions] | |
cluster_compare [Wp.Definitions] | |
cluster_id [Definitions] | Unique |
cluster_id [Wp.Definitions] | Unique |
cluster_position [Definitions] | |
cluster_position [Wp.Definitions] | |
cluster_title [Definitions] | |
cluster_title [Wp.Definitions] | |
cmdline [Register] | |
cmdline_run [Register] | |
cmp_prover [VCS] | |
cmp_prover [Wp.VCS] | |
code_lit [Cfloat] | |
code_lit [Wp.Cfloat] | |
codomain [Letify.Sigma] | |
command [VC] | Run the provers with the command-line interface |
command [Rformat] | |
command [Wp.VC] | Run the provers with the command-line interface |
commit [ProofEngine] | |
comp [Lang] | |
comp [Wp.Lang] | |
comp_id [Lang] | |
comp_id [Wp.Lang] | |
compare [ProverWhy3.Goal] | |
compare [VCS] | |
compare [Sigs.Chunk] | |
compare [LogicBuiltins] | |
compare [Lang.F] | |
compare [Model.Key] | |
compare [Model.Entries] | |
compare [Warning] | |
compare [Clabels.T] | |
compare [Ctypes.AinfoComparable] | |
compare [Ctypes] | |
compare [Map.OrderedType] | A total ordering function over the keys. |
compare [Map.S] | Total ordering between maps. |
compare [Set.S] | Total ordering between sets. |
compare [Wp.VCS] | |
compare [Wp.Sigs.Chunk] | |
compare [Wp.LogicBuiltins] | |
compare [Wp.Lang.F] | |
compare [Wp.Model.Key] | |
compare [Wp.Model.Entries] | |
compare [Wp.Warning] | |
compare [FCMap.S] | Total ordering between maps. |
compare [Wp.Clabels.T] | |
compare [Wp.Ctypes.AinfoComparable] | |
compare [Wp.Ctypes] | |
compare_prop_id [WpPropId] | |
compare_prop_id [Wp.WpPropId] | |
compare_ptr_conflated [Ctypes] | same as |
compare_ptr_conflated [Wp.Ctypes] | same as |
comparep [Lang.F] | |
comparep [Wp.Lang.F] | |
compile [CfgCompiler.Cfg] | |
compile [Model.Data] | |
compile [Model.Registry] | with circularity protection |
compile [Wp.CfgCompiler.Cfg] | |
compile [Wp.Model.Data] | |
compile [Wp.Model.Registry] | with circularity protection |
compile_lemma [Definitions] | |
compile_lemma [Wp.Definitions] | |
compiler [Factory] | |
compiler [Wp.Factory] | |
compinfo [Definitions] | |
compinfo [Wp.Definitions] | |
complexity [TacInstance] | |
compose [Tactical] | |
compose [Wp.Tactical] | |
composer [Tactical] | Unless specified, default is Empty selection. |
composer [Wp.Tactical] | Unless specified, default is Empty selection. |
compound [Auto] | |
compound [Wp.Auto] | |
compute [Calculus.Cfg] | |
compute [Auto.Range] | |
compute [Wpo.GOAL] | |
compute [Wpo] | |
compute [Filtering] | |
compute [Letify.Ground] | |
compute [RefUsage] | |
compute [LogicUsage] | To force computation |
compute [Dyncall] | Forces computation of dynamic calls. |
compute [Wp.Wpo.GOAL] | |
compute [Wp.Wpo] | |
compute [Wp.Auto.Range] | |
compute [Wp.Filtering] | |
compute [Wp.RefUsage] | |
compute [Wp.LogicUsage] | To force computation |
compute_auto [Register] | |
compute_call [Generator] | |
compute_descr [Wpo.GOAL] | |
compute_descr [Wp.Wpo.GOAL] | |
compute_ip [Generator] | |
compute_kf [Generator] | |
compute_kf [StmtSemantics.Make] | Full Compilation |
compute_kf [Wp.StmtSemantics.Make] | Full Compilation |
compute_proof [Wpo.GOAL] | |
compute_proof [Wp.Wpo.GOAL] | |
compute_provers [Register] | |
compute_selection [Generator] | |
computer [Register] | |
computer [CfgWP] | |
computing [VCS] | |
computing [Wp.VCS] | |
concat [CfgCompiler.Cfg] | The concatenation is the intersection of all possible collection of traces from each cfg. |
concat [Conditions] | |
concat [Wp.CfgCompiler.Cfg] | The concatenation is the intersection of all possible collection of traces from each cfg. |
concat [Wp.Conditions] | |
concretize [Vset] | |
concretize [Wp.Vset] | |
cond [Sigs.CodeSemantics] | Evaluate the conditional expression on the given memory state. |
cond [Wp.Sigs.CodeSemantics] | Evaluate the conditional expression on the given memory state. |
condition [Conditions] | With free variables kept. |
condition [Wp.Conditions] | With free variables kept. |
conditions [Passive] | |
conditions [Wp.Passive] | |
configure [Factory] | |
configure [ProofScript] | |
configure [VCS] | |
configure [Sigs.Model] | Initializers to be run before using the model. |
configure [Cfloat] | |
configure [Cint] | |
configure [Context] | Apply global configure hooks, once per project/ast. |
configure [Wp.VCS] | |
configure [Wp.Factory] | |
configure [Wp.Sigs.Model] | Initializers to be run before using the model. |
configure [Wp.Cfloat] | |
configure [Wp.Cint] | |
configure [Wp.Context] | Apply global configure hooks, once per project/ast. |
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 [Lang.Alpha] | |
convert [Wp.Cint] | Independent from model |
convert [Wp.Lang.Alpha] | |
convertp [Lang.Alpha] | |
convertp [Wp.Lang.Alpha] | |
copied [Sigs.Model] | Return a set of equations that express a copy between two memory state. |
copied [Wp.Sigs.Model] | Return a set of equations that express a copy between two memory state. |
copy [Sigs.Sigma] | Duplicate the environment. |
copy [Letify.Ground] | |
copy [Hashtbl.S] | |
copy [Wp.Sigs.Sigma] | Duplicate the environment. |
copy [Datatype.S] | Deep copy: no possible sharing between |
create [CfgDump] | |
create [Tactical.Fmap] | |
create [CfgCompiler.Cfg.E] | Bundle an equation with the sigma sequence that created it |
create [CfgCompiler.Cfg.T] | Bundle a term with the sigma sequence that created it. |
create [CfgCompiler.Cfg.P] | Bundle an equation with the sigma sequence that created it. |
create [CfgCompiler.Cfg.C] | Bundle an equation with the sigma sequence that created it. |
create [CfgCompiler.Cfg.Node] | |
create [Pcfg] | |
create [Mstate] | |
create [Sigs.Sigma] | Initially empty environment. |
create [Cleaning] | |
create [Letify.Split] | |
create [LogicBuiltins] | Create a new driver. |
create [Lang.Alpha] | |
create [Warning] | |
create [Context] | Creates a new context with name |
create [Cil2cfg.HEsig] | |
create [Wp.Tactical.Fmap] | |
create [Wp.CfgCompiler.Cfg.E] | Bundle an equation with the sigma sequence that created it |
create [Wp.CfgCompiler.Cfg.T] | Bundle a term with the sigma sequence that created it. |
create [Wp.CfgCompiler.Cfg.P] | Bundle an equation with the sigma sequence that created it. |
create [Wp.CfgCompiler.Cfg.C] | Bundle an equation with the sigma sequence that created it. |
create [Hashtbl.S] | |
create [Wp.CfgCompiler.Cfg.Node] | |
create [Wp.Pcfg] | |
create [Wp.Mstate] | |
create [Wp.Sigs.Sigma] | Initially empty environment. |
create [Wp.LogicBuiltins] | Create a new driver. |
create [Wp.Lang.Alpha] | |
create [Wp.Warning] | |
create [Wp.Context] | Creates a new context with name |
create_option [LogicBuiltins] |
|
create_option [Wp.LogicBuiltins] |
|
create_proof [WpAnnot] | to be used only once for one of the related prop_id |
create_tbl [WpStrategy] | |
ctor [LogicBuiltins] | |
ctor [Wp.LogicBuiltins] | |
current [ProofEngine] | |
current [VCS] | Current parameters |
current [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] | |
default [Factory] |
|
default [Tactical] | |
default [VCS] | all None |
default [Clabels] | |
default [Wp.Tactical] | |
default [Wp.VCS] | all None |
default [Wp.Factory] |
|
default [Wp.Clabels] | |
default_mode [Register] | |
define [Lang.F] | |
define [Model.Registry] | no redefinition ; circularity protected |
define [Wp.Lang.F] | |
define [Wp.Model.Registry] | no redefinition ; circularity protected |
define_lemma [Definitions] | |
define_lemma [Wp.Definitions] | |
define_symbol [Definitions] | |
define_symbol [Wp.Definitions] | |
define_type [Definitions] | |
define_type [Wp.Definitions] | |
defined [Context] | The current value is defined. |
defined [Wp.Context] | The current value is defined. |
definition [Auto] | |
definition [Wp.Auto] | |
defs [Lang.F] | |
defs [Wp.Lang.F] | |
delete_script [Proof] | |
denv [Matrix] | |
dependencies [WpAnnot] | |
dependencies [LogicBuiltins] | Of external theories. |
dependencies [Wp.LogicBuiltins] | Of external theories. |
deprecated [Register] | |
deprecated_wp_clear [Register] | |
deprecated_wp_compute [Register] | |
deprecated_wp_compute_call [Register] | |
deprecated_wp_compute_ip [Register] | |
deprecated_wp_compute_kf [Register] | |
depth [ProverTask] | |
depth [Wp.ProverTask] | |
descr [Factory] | |
descr [Vset] | |
descr [LogicBuiltins] | |
descr [Wp.Factory] | |
descr [Wp.Vset] | |
descr [Wp.LogicBuiltins] | |
destruct [Tactical] | |
destruct [Wp.Tactical] | |
detect_provers [ProverWhy3] | |
detect_why3 [ProverWhy3] | |
diff [Set.S] | Set difference. |
dimension_of_object [Ctypes] | Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells |
dimension_of_object [Wp.Ctypes] | Returns None for 1-dimension objects, and Some(d,N) for d-matrix with N cells |
directory [Model] | Current model in |
directory [Wp.Model] | Current model in |
disjoint [Region] | |
disjoint [Vset] | |
disjoint [Wp.Vset] | |
dkey_builtins [Register] | |
dkey_logicusage [Register] | |
dkey_no_goals_info [VCS] | |
dkey_no_goals_info [Wp.VCS] | |
dkey_no_step_info [VCS] | |
dkey_no_step_info [Wp.VCS] | |
dkey_no_time_info [VCS] | |
dkey_no_time_info [Wp.VCS] | |
dkey_prover [Register] | |
dkey_raised [Register] | |
dkey_refusage [Register] | |
dkey_shell [Register] | |
do_list_scheduled [Register] | |
do_list_scheduled_result [Register] | |
do_progress [Register] | |
do_prover_detect [Register] | |
do_report_prover_stats [Register] | |
do_report_scheduled [Register] | |
do_update_session [Register] | |
do_why3_result [Register] | |
do_wp_print [Register] | |
do_wp_print_for [Register] | |
do_wp_proofs [Register] | |
do_wp_proofs_for [Register] | |
do_wp_proofs_iter [Register] | |
do_wp_report [Register] | |
do_wpo_display [Register] | |
do_wpo_result [Register] | |
do_wpo_start [Register] | |
do_wpo_stat [Register] | |
do_wpo_success [Register] | |
do_wpo_wait [Register] | |
domain [Conditions] | |
domain [Sigs.LogicAssigns] | Memory footprint of a region. |
domain [Sigs.Model] | Compute the set of chunks that hold the value of an object with the given C-type. |
domain [Sigs.Sigma] | Footprint of a memory environment. |
domain [Letify.Defs] | |
domain [Letify.Sigma] | |
domain [Wp.Conditions] | |
domain [Wp.Sigs.LogicAssigns] | Memory footprint of a region. |
domain [Wp.Sigs.Model] | Compute the set of chunks that hold the value of an object with the given C-type. |
domain [Wp.Sigs.Sigma] | Footprint of a memory environment. |
downcast [Cint] | Dependent on model |
downcast [Wp.Cint] | Dependent on model |
driver [LogicBuiltins] | |
driver [Wp.LogicBuiltins] | |
dummy [Wpo.GOAL] | |
dummy [Wp.Wpo.GOAL] | |
dump [Pcond] | |
dump [LogicBuiltins] | |
dump [RefUsage] | |
dump [LogicUsage] | Print on output |
dump [Wp.Pcond] | |
dump [Wp.LogicBuiltins] | |
dump [Wp.RefUsage] | |
dump [Wp.LogicUsage] | Print on output |
dump_env [CfgCompiler.Cfg] | |
dump_env [Wp.CfgCompiler.Cfg] | |
dump_scripts [Proof] |
|
dump_strategies [Register] | |
E | |
e_add [Lang.F] | |
e_add [Wp.Lang.F] | |
e_and [Lang.F] | |
e_and [Wp.Lang.F] | |
e_apply [Letify.Sigma] | |
e_apply [Letify.Ground] | |
e_apply [Lang.Subst] | |
e_apply [Wp.Lang.Subst] | |
e_bigint [Lang.F] | |
e_bigint [Wp.Lang.F] | |
e_bind [Lang.F] | |
e_bind [Wp.Lang.F] | |
e_bool [Lang.F] | |
e_bool [Wp.Lang.F] | |
e_cnf [WpTac] | |
e_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_opp [Lang.F] | |
e_opp [Wp.Lang.F] | |
e_or [Lang.F] | |
e_or [Wp.Lang.F] | |
e_prod [Lang.F] | |
e_prod [Wp.Lang.F] | |
e_prop [Lang.F] | |
e_prop [Wp.Lang.F] | |
e_props [Lang.F] | |
e_props [Wp.Lang.F] | |
e_range [Lang.F] | e_range a b = b+1-a |
e_range [Wp.Lang.F] | e_range a b = b+1-a |
e_real [Lang.F] | |
e_real [Wp.Lang.F] | |
e_record [Lang.F] | |
e_record [Wp.Lang.F] | |
e_set [Lang.F] | |
e_set [Wp.Lang.F] | |
e_setfield [Lang.F] | |
e_setfield [Wp.Lang.F] | |
e_sub [Lang.F] | |
e_sub [Wp.Lang.F] | |
e_subst [Lang.F] | |
e_subst [Wp.Lang.F] | |
e_sum [Lang.F] | |
e_sum [Wp.Lang.F] | |
e_times [Lang.F] | |
e_times [Wp.Lang.F] | |
e_true [Lang.F] | |
e_true [Wp.Lang.F] | |
e_var [Lang.F] | |
e_var [Wp.Lang.F] | |
e_vars [Lang.F] | Sorted |
e_vars [Wp.Lang.F] | Sorted |
e_zero [Lang.F] | |
e_zero [Wp.Lang.F] | |
e_zero_real [Lang.F] | |
e_zero_real [Wp.Lang.F] | |
e_zint [Lang.F] | |
e_zint [Wp.Lang.F] | |
eat [Script] | |
edge_dst [Cil2cfg] | |
edge_src [Cil2cfg] | node and edges relations |
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] | |
either [Wp.CfgCompiler.Cfg] | Structurally corresponds to an arbitrary choice among the different possible executions. |
either [Wp.Conditions] | |
elements [Vlist] | |
elements [Set.S] | Return the list of all elements of the given set. |
emit [Warning] | Emit a warning in current context. |
emit [Wp.Warning] | Emit a warning in current context. |
empty [Conditions] | |
empty [Sigs.Sigma] | Same as |
empty [Letify.Defs] | |
empty [Letify.Sigma] | |
empty [Region] | |
empty [Vset] | |
empty [Splitter] | |
empty [Passive] | |
empty [Mcfg.S] | |
empty [Separation] | |
empty [Map.S] | The empty map. |
empty [Set.S] | The empty set. |
empty [Wp.Conditions] | |
empty [Wp.Sigs.Sigma] | Same as |
empty [Wp.Vset] | |
empty [Wp.Splitter] | |
empty [Wp.Passive] | |
empty [Wp.Mcfg.S] | |
empty [Wp.Separation] | |
empty [FCMap.S] | The empty map. |
empty_acc [WpStrategy] | |
empty_assigns_info [WpPropId] | |
empty_assigns_info [Wp.WpPropId] | |
empty_env [StmtSemantics.Make] | |
empty_env [Wp.StmtSemantics.Make] | |
encode [ProofScript] | |
end_session [Register] | |
env [Strategy] | |
env [Repr] | Create environment from a set of free variables |
env [Lang.F] | |
env [Wp.Strategy] | |
env [Wp.Repr] | Create environment from a set of free variables |
env [Wp.Lang.F] | |
env_at [LogicCompiler.Make] | |
env_at [Sigs.LogicSemantics] | Returns a new environment where the current memory state is moved to to the corresponding label. |
env_at [Wp.LogicCompiler.Make] | |
env_at [Wp.Sigs.LogicSemantics] | Returns a new environment where the current memory state is moved to to the corresponding label. |
env_let [LogicCompiler.Make] | |
env_let [Wp.LogicCompiler.Make] | |
env_letp [LogicCompiler.Make] | |
env_letp [Wp.LogicCompiler.Make] | |
env_letval [LogicCompiler.Make] | |
env_letval [Wp.LogicCompiler.Make] | |
epsilon [Lang] | |
epsilon [Rformat] | |
epsilon [Wp.Lang] | |
eqp [Lang.F] | |
eqp [Wp.Lang.F] | |
equal [CfgCompiler.Cfg.C] | |
equal [CfgCompiler.Cfg.Node] | |
equal [Mstate] | |
equal [Letify.Sigma] | |
equal [Vset] | |
equal [Lang.F] | Same as |
equal [Clabels] | |
equal [Ctypes.AinfoComparable] | |
equal [Ctypes] | |
equal [Map.S] |
|
equal [Set.S] |
|
equal [Wp.CfgCompiler.Cfg.C] | |
equal [Wp.CfgCompiler.Cfg.Node] | |
equal [Wp.Mstate] | |
equal [Wp.Vset] | |
equal [Wp.Lang.F] | Same as |
equal [FCMap.S] |
|
equal [Wp.Clabels] | |
equal [Wp.Ctypes.AinfoComparable] | |
equal [Wp.Ctypes] | |
equal_array [Cvalues] | |
equal_but [Region] | |
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] | |
exists [ProofSession] | |
exists [Splitter] | |
exists [Map.S] |
|
exists [Set.S] |
|
exists [Wp.Splitter] | |
exists [FCMap.S] |
|
exists [Parameter_sig.Set] | Is there some element satisfying the given predicate? |
exp [Sigs.CodeSemantics] | Evaluate the expression on the given memory state. |
exp [Wp.Sigs.CodeSemantics] | Evaluate the expression on the given memory state. |
export [Strategy] | |
export [Tactical] | Register and returns the tactical |
export [WpReport] | |
export [Vlist] | |
export [Wp.Strategy] | |
export [Wp.Tactical] | Register and returns the tactical |
export_decl [Mcfg.Export] | |
export_decl [Wp.Mcfg.Export] | |
export_goal [Mcfg.Export] | |
export_goal [Wp.Mcfg.Export] | |
export_json [WpReport] | |
export_section [Mcfg.Export] | |
export_section [Wp.Mcfg.Export] | |
extern_f [Lang] | balance just give a default when link is not specified |
extern_f [Wp.Lang] | balance just give a default when link is not specified |
extern_fp [Lang] | |
extern_fp [Wp.Lang] | |
extern_p [Lang] | |
extern_p [Wp.Lang] | |
extern_s [Lang] | |
extern_s [Wp.Lang] | |
extract [Conditions] | |
extract [Letify.Defs] | |
extract [Wp.Conditions] | |
F | |
f_bit [Cint] | |
f_bit [Wp.Cint] | |
f_bitwised [Cint] | All except f_bit |
f_bitwised [Wp.Cint] | All except f_bit |
f_concat [Vlist] | |
f_cons [Vlist] | |
f_convert [Ctypes] | |
f_convert [Wp.Ctypes] | |
f_delta [Cfloat] | |
f_delta [Wp.Cfloat] | |
f_elt [Vlist] | |
f_epsilon [Cfloat] | |
f_epsilon [Wp.Cfloat] | |
f_iabs [Cmath] | |
f_iter [Ctypes] | |
f_iter [Wp.Ctypes] | |
f_land [Cint] | |
f_land [Wp.Cint] | |
f_lnot [Cint] | |
f_lnot [Wp.Cint] | |
f_lor [Cint] | |
f_lor [Wp.Cint] | |
f_lsl [Cint] | |
f_lsl [Wp.Cint] | |
f_lsr [Cint] | |
f_lsr [Wp.Cint] | |
f_lxor [Cint] | |
f_lxor [Wp.Cint] | |
f_memo [Ctypes] | memoized, not-projectified |
f_memo [Wp.Ctypes] | memoized, not-projectified |
f_model [Cfloat] | |
f_model [Wp.Cfloat] | |
f_nil [Vlist] | |
f_nth [Vlist] | |
f_rabs [Cmath] | |
f_real_of_int [Cmath] | |
f_repeat [Vlist] | |
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 [TacHavoc.Havoc] | |
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 [Wp.Mstate] | |
field [Wp.Sigs.Model] | Return the memory location obtained by field access from a given memory location. |
field [Wp.Repr] | |
field [Wp.Lang] | |
field_id [Lang] | |
field_id [Wp.Lang] | |
field_offset [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 [ProofSession] | |
filename_for_prover [VCS] | |
filename_for_prover [Wp.VCS] | |
filter [GuiProver] | |
filter [Auto] | |
filter [TacInstance] | |
filter [Script] | |
filter [Filtering] | |
filter [Conditions] | |
filter [Splitter] | |
filter [Separation] | Only non-trivial clauses |
filter [Wp.Auto] | |
filter [Map.S] |
|
filter [Set.S] |
|
filter [Wp.Filtering] | |
filter [Wp.Conditions] | |
filter [Wp.Splitter] | |
filter [Wp.Separation] | Only non-trivial clauses |
filter [FCMap.S] |
|
filter_map_inplace [Hashtbl.S] | |
filter_pred [Cleaning] | |
filter_status [WpAnnot] | |
filter_type [Cleaning] | |
find [ProverWhy3] | |
find [TacLemma] | |
find [Pcfg] | |
find [Letify.Sigma] | |
find [Model.Registry] | |
find [Model] | |
find [Cil2cfg.HEsig] | |
find [Map.S] |
|
find [Set.S] |
|
find [Hashtbl.S] | |
find [Wp.Pcfg] | |
find [Wp.Model.Registry] | |
find [Wp.Model] | |
find [FCMap.S] |
|
find_all [Cil2cfg.HEsig] | |
find_all [Hashtbl.S] | |
find_first [Map.S] |
|
find_first [Set.S] |
|
find_first_opt [Map.S] |
|
find_first_opt [Set.S] |
|
find_last [Map.S] |
|
find_last [Set.S] |
|
find_last_opt [Map.S] |
|
find_last_opt [Set.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 [Map.S] |
|
find_opt [Set.S] |
|
find_opt [Hashtbl.S] | |
find_opt [FCMap.S] |
|
find_script_for_goal [Proof] | Retrieve script file for one specific goal. |
find_script_with_hints [Proof] | Retrieve matchable script files for w.r.t provided required and hints keywords. |
find_symbol [Definitions] | |
find_symbol [Wp.Definitions] | |
first [ProverSearch] | |
fle [Cfloat] | |
fle [Wp.Cfloat] | |
float_of_int [Cfloat] | |
float_of_int [Wp.Cfloat] | |
float_of_real [Cfloat] | |
float_of_real [Wp.Cfloat] | |
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_rnd [Cfloat] | |
flt_rnd [Wp.Cfloat] | |
flush [Warning] | |
flush [Wp.Warning] | |
fmode [TacCut] | |
fmul [Cfloat] | |
fmul [Wp.Cfloat] | |
fneq [Cfloat] | |
fneq [Wp.Cfloat] | |
fold [Splitter] | |
fold [Map.S] |
|
fold [Set.S] |
|
fold [Hashtbl.S] | |
fold [Wp.Splitter] | |
fold [FCMap.S] |
|
fold_bhv_post_cond [WpStrategy] | apply |
fold_nodes [Cil2cfg] | iterators |
fopp [Cfloat] | |
fopp [Wp.Cfloat] | |
for_all [Splitter] | |
for_all [Map.S] |
|
for_all [Set.S] |
|
for_all [Wp.Splitter] | |
for_all [FCMap.S] |
|
fork [ProofEngine] | |
formal [LogicCompiler.Make] | |
formal [Clabels] | |
formal [Wp.LogicCompiler.Make] | |
formal [Wp.Clabels] | |
forward [ProofEngine] | |
forward [Letify.Ground] | |
frame [LogicCompiler.Make] | |
frame [Sigs.LogicSemantics] | Make a fresh frame with the given function. |
frame [Sigs.Model] | Assert the memory is a proper heap state preceeding the function entry point. |
frame [Wp.LogicCompiler.Make] | |
frame [Wp.Sigs.LogicSemantics] | Make a fresh frame with the given function. |
frame [Wp.Sigs.Model] | Assert the memory is a proper heap state preceeding the function entry point. |
free [Context] | Performs the job with local context cleared. |
free [Wp.Context] | Performs the job with local context cleared. |
fresh [Lang.F] | |
fresh [Wp.Lang.F] | |
freshen [Lang] | |
freshen [Wp.Lang] | |
freshvar [Lang] | |
freshvar [Wp.Lang] | |
from_file [Why3_xml] | returns the list of XML elements from the given file. |
froms [StmtSemantics.Make] | |
froms [Wp.StmtSemantics.Make] | |
fsub [Cfloat] | |
fsub [Wp.Cfloat] | |
full [Region] | |
G | |
generate [WpRTE] | Invoke RTE to generate missing annotations for the given function and model. |
generate_call [VC] | |
generate_call [Wp.VC] | |
generate_ip [VC] | |
generate_ip [Wp.VC] | |
generate_kf [VC] | |
generate_kf [Wp.VC] | |
generated_f [Lang] | |
generated_f [Wp.Lang] | |
generated_p [Lang] | |
generated_p [Wp.Lang] | |
get [ProverScript] | |
get [ProofEngine] | |
get [Tactical.Fmap] | raises Not_found if absent |
get [CfgCompiler.Cfg.E] | |
get [CfgCompiler.Cfg.T] | |
get [CfgCompiler.Cfg.P] | |
get [CfgCompiler.Cfg.C] | |
get [Sigs.Sigma] | Lazily get the variable for a chunk. |
get [Lang.Alpha] | |
get [Model.Generator] | |
get [Model.Registry] | |
get [Context] | Retrieves the current value of the context. |
get [Cil2cfg] | |
get [RefUsage] | |
get [Dyncall] | Returns empty list if there is no specified dynamic call. |
get [Wp.Tactical.Fmap] | raises Not_found if absent |
get [Wp.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.Alpha] | |
get [Wp.Model.Generator] | |
get [Wp.Model.Registry] | |
get [Wp.Context] | Retrieves the current value of the context. |
get [Wp.RefUsage] | |
get_annots [WpStrategy] | |
get_array [Ctypes] | |
get_array [Wp.Ctypes] | |
get_array_dim [Ctypes] | |
get_array_dim [Wp.Ctypes] | |
get_array_size [Ctypes] | |
get_array_size [Wp.Ctypes] | |
get_asgn_goal [WpStrategy] | |
get_asgn_hyp [WpStrategy] | |
get_bhv [WpStrategy] | |
get_both_hyp_goals [WpStrategy] | |
get_builtin_type [Lang] | |
get_builtin_type [Wp.Lang] | |
get_call_asgn [WpStrategy] | |
get_call_hyp [WpStrategy] | To be used as hypotheses around a call, (the pre are in
|
get_call_out_edges [Cil2cfg] | similar to |
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_called_assigns [WpAnnot] | Properties for assigns of kf |
get_called_exit_conditions [WpAnnot] | |
get_called_post_conditions [WpAnnot] | |
get_called_preconditions_at [WpAnnot] | |
get_cut [WpStrategy] | the |
get_depth [VCS] | 0 means prover default |
get_depth [Wp.VCS] | 0 means prover default |
get_descr [Wpo.GOAL] | |
get_descr [Model] | |
get_descr [Wp.Wpo.GOAL] | |
get_descr [Wp.Model] | |
get_description [VC] | |
get_description [Wp.VC] | |
get_edge_labels [Cil2cfg] | |
get_edge_next_stmt [Cil2cfg] | |
get_edge_stmt [Cil2cfg] | Complete get_edge_labels and returns the associated stmt, if any. |
get_emitter [Model] | |
get_emitter [Wp.Model] | |
get_env [Wp_parameters] | |
get_env [Wp.Wp_parameters] | |
get_exit_edges [Cil2cfg] | Find the edges |
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_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_hyp_only [WpStrategy] | |
get_hypotheses [Lang] | |
get_hypotheses [Wp.Lang] | |
get_id [VC] | |
get_id [Model] | |
get_id [Wp.VC] | |
get_id [Wp.Model] | |
get_id_prop_strategies [WpAnnot] | |
get_includes [Wp_parameters] | |
get_includes [Wp.Wp_parameters] | |
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 [Ctypes] | |
get_int [Wp.Ctypes] | |
get_internal_edges [Cil2cfg] | Find the edges |
get_kf [WpStrategy] | |
get_label [Wpo] | |
get_label [Wp.Wpo] | |
get_logerr [VC] | only file name, might not exists |
get_logerr [Wp.VC] | only file name, might not exists |
get_logout [VC] | only file name, might not exists |
get_logout [Wp.VC] | only file name, might not exists |
get_model [VC] | |
get_model [Wpo] | |
get_model [Model] | Current model |
get_model [Wp.Wpo] | |
get_model [Wp.VC] | |
get_model [Wp.Model] | Current model |
get_model_id [Wpo] | |
get_model_id [Wp.Wpo] | |
get_model_name [Wpo] | |
get_model_name [Wp.Wpo] | |
get_name [LogicUsage] | |
get_name [Wp.LogicUsage] | |
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_plain_string [Parameter_sig.String] | always return the argument, even if the argument is not a function name. |
get_pool [Lang] | |
get_pool [Wp.Lang] | |
get_possible_values [Parameter_sig.String] | What are the acceptable values for this parameter. |
get_post_edges [Cil2cfg] | Find the edges where the postconditions of the node statement have to be checked. |
get_post_label [Cil2cfg] | Get the label to be used for the Post state of the node contract if any. |
get_pre_edges [Cil2cfg] | Find the edges where the precondition of the node statement have to be checked. |
get_proof [Wpo] | |
get_proof [Wp.Wpo] | |
get_property [VC] | |
get_property [Wpo] | Dynamically exported |
get_property [Wp.Wpo] | Dynamically exported |
get_property [Wp.VC] | |
get_propid [WpPropId] | Unique identifier of |
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_result [VC] | |
get_result [Wpo] | |
get_result [Wp.Wpo] | |
get_result [Wp.VC] | |
get_results [VC] | |
get_results [Wpo] | |
get_results [Wp.Wpo] | |
get_results [Wp.VC] | |
get_scope [Model] | |
get_scope [Wp.Model] | |
get_separation [Model] | |
get_separation [Wp.Model] | |
get_sequent [VC] | |
get_sequent [Wp.VC] | |
get_session [Wp_parameters] | |
get_session [Wp.Wp_parameters] | |
get_session_dir [Wp_parameters] | |
get_session_dir [Wp.Wp_parameters] | |
get_stepout [VCS] | 0 means no-stepout |
get_stepout [Wp.VCS] | 0 means no-stepout |
get_steps [Wpo] | |
get_steps [Wp.Wpo] | |
get_strategies [ProofEngine] | |
get_switch_edges [Cil2cfg] | similar to |
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_variables [Lang] | |
get_variables [Wp.Lang] | |
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. |
handle [Warning] | Handle the error and emit a warning with specified severity and effect if a context has been set. |
handle [Wp.Warning] | Handle the error and emit a warning with specified severity and effect if a context has been set. |
has_ctype [Cvalues] | |
has_dkey [Wp_parameters] | |
has_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_ltype [Cvalues] | |
has_print_generated [Wp_parameters] | Debugging Categories |
has_print_generated [Wp.Wp_parameters] | Debugging Categories |
has_verdict [Wpo] | |
has_verdict [Wp.Wpo] | |
hash [Sigs.Chunk] | |
hash [Lang.F] | Constant time |
hash [Ctypes.AinfoComparable] | |
hash [Ctypes] | |
hash [Wp.Sigs.Chunk] | |
hash [Wp.Lang.F] | Constant time |
hash [Wp.Ctypes.AinfoComparable] | |
hash [Wp.Ctypes] | |
have [Conditions] | Predicate for Have and such, True for any other |
have [Wp.Conditions] | Predicate for Have and such, True for any other |
havoc [Auto] | |
havoc [CfgCompiler.Cfg] | Inserts an assigns effect between nodes |
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. |
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 [Lang] | |
hypotheses [Wp.Lang] | |
I | |
i_bits [Ctypes] | size in bits |
i_bits [Wp.Ctypes] | size in bits |
i_bytes [Ctypes] | size in bytes |
i_bytes [Wp.Ctypes] | size in bytes |
i_convert [Ctypes] | |
i_convert [Wp.Ctypes] | |
i_iter [Ctypes] | |
i_iter [Wp.Ctypes] | |
i_memo [Ctypes] | memoized, not-projectified |
i_memo [Wp.Ctypes] | memoized, not-projectified |
iadd [Cint] | |
iadd [Wp.Cint] | |
id [LogicBuiltins] | |
id [Matrix] | unique w.r.t |
id [Wp.LogicBuiltins] | |
ident [Factory] | |
ident [Tactical] | |
ident [Script] | |
ident [Wp.Tactical] | |
ident [Wp.Factory] | |
idents [Script] | |
idiv [Cint] | |
idiv [Wp.Cint] | |
if_else [Splitter] | |
if_else [Wp.Splitter] | |
if_then [Splitter] | |
if_then [Wp.Splitter] | |
imod [Cint] | |
imod [Wp.Cint] | |
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] | |
included [Sigs.Model] | Return the formula that tests if two segment are included |
included [Cvalues.Logic] | |
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 [Wp.Conditions] | Compute steps' id of sequent left hand-side. |
index [Wp.Mstate] | |
infoprover [Lang] | same information for all the provers |
infoprover [Wp.Lang] | same information for all the provers |
init [StmtSemantics.Make] | connect init to here. |
init [CfgCompiler.Cfg.T] | |
init [Sigs.CodeSemantics] | Express that some variable has some initial value at the given memory state. |
init [LogicBuiltins] | Reset the context to a newly created driver |
init [Mcfg.S] | |
init [Clabels] | |
init [Wp.StmtSemantics.Make] | |
init [Wp.CfgCompiler.Cfg.T] | |
init [Wp.Sigs.CodeSemantics] | Express that some variable has some initial value at the given memory state. |
init [Wp.LogicBuiltins] | Reset the context to a newly created driver |
init [Wp.Mcfg.S] | |
init [Wp.Clabels] | |
init' [CfgCompiler.Cfg.T] | |
init' [Wp.CfgCompiler.Cfg.T] | |
insert [Tactical] | |
insert [Conditions] | Insert a step in the sequent immediately |
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_loc [Sigs.Model] | Cast a memory location into its absolute memory address, given as an integer with the given C-type. |
int_of_loc [Wp.Sigs.Model] | Cast a memory location into its absolute memory address, given as an integer with the given C-type. |
int_of_real [Cmath] | |
inter [Cvalues.Logic] | |
inter [Vset] | |
inter [Set.S] | Set intersection. |
inter [Wp.Vset] | |
intersect [Conditions] | |
intersect [Lang.F] | |
intersect [Wp.Conditions] | |
intersect [Wp.Lang.F] | |
intersectp [Lang.F] | |
intersectp [Wp.Lang.F] | |
introduction [Conditions] | Performs existential, universal and hypotheses introductions |
introduction [Wp.Conditions] | Performs existential, universal and hypotheses introductions |
intros [Conditions] | |
intros [Wp.Conditions] | |
intuition [Auto] | |
intuition [Wp.Auto] | |
invalid [VCS] | |
invalid [Sigs.Model] | Returns the formula that tests if the entire memory is invalid for write access. |
invalid [Cvalues.Logic] | |
invalid [Wp.VCS] | |
invalid [Wp.Sigs.Model] | Returns the formula that tests if the entire memory is invalid for write access. |
iopp [Cint] | |
iopp [Wp.Cint] | |
ip_lemma [LogicUsage] | |
ip_lemma [Wp.LogicUsage] | |
isGlobalInitConst [WpStrategy] | True if the variable is global, not extern, with a |
isInitConst [WpStrategy] | True if both options |
is_absorbant [Lang.F] | |
is_absorbant [Wp.Lang.F] | |
is_arith [Lang.F] | Integer or Real sort |
is_arith [Wp.Lang.F] | Integer or Real sort |
is_array [Ctypes] | |
is_array [Wp.Ctypes] | |
is_assigns [WpPropId] | |
is_assigns [Wp.WpPropId] | |
is_atomic [Lang.F] | Constants and variables |
is_atomic [Wp.Lang.F] | Constants and variables |
is_auto [VCS] | |
is_auto [Wp.VCS] | |
is_back_edge [Cil2cfg] | |
is_builtin [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 [Wpo] | |
is_check [WpPropId] | |
is_check [Wp.Wpo] | |
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_composed [WpAnnot] | whether a proof needs several lemma to be complete |
is_default [LogicBuiltins] | |
is_default [Wp.LogicBuiltins] | |
is_default_behavior [WpStrategy] | |
is_dnf [WpTac] | |
is_empty [Tactical] | |
is_empty [Proof] | |
is_empty [Conditions] | No step at all |
is_empty [Vset] | |
is_empty [Passive] | |
is_empty [Wp.Tactical] | |
is_empty [Map.S] | Test whether a map is empty or not. |
is_empty [Set.S] | Test whether a set is empty or not. |
is_empty [Wp.Conditions] | No step at all |
is_empty [Wp.Vset] | |
is_empty [Wp.Passive] | |
is_empty [FCMap.S] | Test whether a map is empty or not. |
is_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_here [Clabels] | |
is_here [Wp.Clabels] | |
is_int [Lang.F] | Integer sort |
is_int [Wp.Lang.F] | Integer sort |
is_loop_preservation [WpPropId] | |
is_loop_preservation [Wp.WpPropId] | |
is_main_init [WpStrategy] | The function is the main entry point AND it is not a lib entry |
is_model_defined [Model] | |
is_model_defined [Wp.Model] | |
is_neutral [Lang.F] | |
is_neutral [Wp.Lang.F] | |
is_null [Sigs.Model] | Return the formula that check if a given location is null |
is_null [Cvalues] | |
is_null [Wp.Sigs.Model] | Return the formula that check if a given location is null |
is_object [Cvalues] | |
is_out [Wp_parameters] | |
is_out [Wp.Wp_parameters] | |
is_pfalse [Lang.F] | |
is_pfalse [Wp.Lang.F] | |
is_pointer [Ctypes] | |
is_pointer [Wp.Ctypes] | |
is_positive_or_null [Cint] | |
is_positive_or_null [Wp.Cint] | |
is_precond_generated [WpRTE] | |
is_primitive [Lang.F] | Constants only |
is_primitive [Wp.Lang.F] | Constants only |
is_prop [Lang.F] | Boolean or Property |
is_prop [Wp.Lang.F] | Boolean or Property |
is_proved [VC] | |
is_proved [Wpo] | do not tries simplification, check prover results |
is_proved [WpAnnot] | whether all partial proofs have been accumulated or not |
is_proved [Wp.Wpo] | do not tries simplification, check prover results |
is_proved [Wp.VC] | |
is_prover [ProofScript] | |
is_ptrue [Lang.F] | |
is_ptrue [Wp.Lang.F] | |
is_real [Lang.F] | Real sort |
is_real [Wp.Lang.F] | Real sort |
is_recursive [LogicUsage] | |
is_recursive [Wp.LogicUsage] | |
is_requires [WpPropId] | |
is_requires [Wp.WpPropId] | |
is_set [Lang.F.Check] | |
is_set [Wp.Lang.F.Check] | |
is_simple [Lang.F] | Constants, variables, functions of arity 0 |
is_simple [Wp.Lang.F] | Constants, variables, functions of arity 0 |
is_subterm [Lang.F] | |
is_subterm [Wp.Lang.F] | |
is_tactic [ProofScript] | |
is_tactic [Wpo] | |
is_tactic [WpPropId] | |
is_tactic [Wp.Wpo] | |
is_tactic [Wp.WpPropId] | |
is_trivial [VC] | |
is_trivial [Wpo.VC_Annot] | |
is_trivial [Wpo.VC_Lemma] | |
is_trivial [Wpo.GOAL] | |
is_trivial [Wpo] | do not tries simplification, do not check prover results |
is_trivial [Conditions] | |
is_trivial [Wp.Wpo.VC_Annot] | |
is_trivial [Wp.Wpo.VC_Lemma] | |
is_trivial [Wp.Wpo.GOAL] | |
is_trivial [Wp.Wpo] | do not tries simplification, do not check prover results |
is_trivial [Wp.VC] | |
is_trivial [Wp.Conditions] | |
is_true [Conditions] | Only true or empty steps |
is_true [Cvalues] |
|
is_true [Lang.F] | Constant time. |
is_true [Separation] | |
is_true [Wp.Conditions] | Only true or empty steps |
is_true [Wp.Lang.F] | Constant time. |
is_true [Wp.Separation] | |
is_unknown [Wpo] | |
is_unknown [Wp.Wpo] | |
is_valid [Wpo] |
|
is_valid [VCS] | |
is_valid [Wp.Wpo] |
|
is_valid [Wp.VCS] | |
is_verdict [VCS] | |
is_verdict [Wp.VCS] | |
is_void [Ctypes] | |
is_void [Wp.Ctypes] | |
is_zero [Sigs.CodeSemantics] | Express that the object (of specified type) at the given location is filled with zeroes. |
is_zero [Lang.F] | |
is_zero [Wp.Sigs.CodeSemantics] | Express that the object (of specified type) at the given location is filled with zeroes. |
is_zero [Wp.Lang.F] | |
isub [Cint] | |
isub [Wp.Cint] | |
iter [ProofEngine] | |
iter [Strategy] | |
iter [Tactical] | |
iter [Footprint] | Width-first full iterator. |
iter [Wpo] | |
iter [Pcfg] | |
iter [Conditions] | Iterate only over the head steps of the sequence |
iter [Mstate] | |
iter [Sigs.Model] | Debug |
iter [Sigs.Sigma] | Iterates over the chunks and associated variables already accessed so far in the environment. |
iter [Letify.Sigma] | |
iter [Definitions] | |
iter [Splitter] | |
iter [Passive] | |
iter [Lang.Alpha] | |
iter [Lang.F.Check] | |
iter [Model.Registry] | |
iter [Model] | |
iter [RefUsage] | |
iter [Wp.Wpo] | |
iter [Wp.Strategy] | |
iter [Wp.Tactical] | |
iter [Map.S] |
|
iter [Set.S] |
|
iter [Hashtbl.S] | |
iter [Wp.Pcfg] | |
iter [Wp.Conditions] | Iterate only over the head steps of the sequence |
iter [Wp.Mstate] | |
iter [Wp.Sigs.Model] | Debug |
iter [Wp.Sigs.Sigma] | Iterates over the chunks and associated variables already accessed so far in the environment. |
iter [Wp.Definitions] | |
iter [Wp.Splitter] | |
iter [Wp.Passive] | |
iter [Wp.Lang.Alpha] | |
iter [Wp.Lang.F.Check] | |
iter [Wp.Model.Registry] | |
iter [Wp.Model] | |
iter [Wp.RefUsage] | |
iter [FCMap.S] |
|
iter2 [Sigs.Sigma] | Same as |
iter2 [Wp.Sigs.Sigma] | Same as |
iter_composer [Tactical] | |
iter_composer [Wp.Tactical] | |
iter_edges [Cil2cfg] | |
iter_ip [VC] | |
iter_ip [Wp.VC] | |
iter_kf [VC] | |
iter_kf [Wp.VC] | |
iter_lemmas [LogicUsage] | |
iter_lemmas [Wp.LogicUsage] | |
iter_nodes [Cil2cfg] | |
iter_on_goals [Wpo] | Dynamically exported. |
iter_on_goals [Wp.Wpo] | Dynamically exported. |
iter_session [Register] | |
iter_sorted [Model.Registry] | |
iter_sorted [Wp.Model.Registry] | |
J | |
job [Wp_parameters] | |
job [Wp.Wp_parameters] | |
job_key [Register] | |
join [Sigs.Sigma] | Make two environment pairwise equal via the passive form. |
join [Passive] | |
join [Wp.Sigs.Sigma] | Make two environment pairwise equal via the passive form. |
join [Wp.Passive] | |
json_of_param [ProofScript] | |
json_of_parameters [ProofScript] | |
json_of_result [ProofScript] | |
json_of_selection [ProofScript] | |
json_of_tactic [ProofScript] | |
jtactic [ProofScript] | |
K | |
key [Script] | |
kf_context [Wpo] | |
kf_context [Wp.Wpo] | |
kfailed [VCS] | |
kfailed [Wp.VCS] | |
kind_of_id [WpPropId] | get the 'kind' information. |
kind_of_id [Wp.WpPropId] | get the 'kind' information. |
kind_of_tau [LogicBuiltins] | |
kind_of_tau [Wp.LogicBuiltins] | |
ko_status [GuiProver] | |
L | |
l_and [Cint] | |
l_and [Wp.Cint] | |
l_lsl [Cint] | |
l_lsl [Wp.Cint] | |
l_lsr [Cint] | |
l_lsr [Wp.Cint] | |
l_not [Cint] | |
l_not [Wp.Cint] | |
l_or [Cint] | |
l_or [Wp.Cint] | |
l_xor [Cint] | |
l_xor [Wp.Cint] | |
label [Mcfg.S] | |
label [Wp.Mcfg.S] | |
label_of_prop_id [WpPropId] | Short description of the kind of PO |
label_of_prop_id [Wp.WpPropId] | Short description of the kind of PO |
labels_assert_after [NormAtLabels] | |
labels_assert_after [Wp.NormAtLabels] | |
labels_assert_before [NormAtLabels] | |
labels_assert_before [Wp.NormAtLabels] | |
labels_axiom [NormAtLabels] | |
labels_axiom [Wp.NormAtLabels] | |
labels_empty [NormAtLabels] | |
labels_empty [Wp.NormAtLabels] | |
labels_fct_assigns [NormAtLabels] | |
labels_fct_assigns [Wp.NormAtLabels] | |
labels_fct_post [NormAtLabels] | |
labels_fct_post [Wp.NormAtLabels] | |
labels_fct_pre [NormAtLabels] | |
labels_fct_pre [Wp.NormAtLabels] | |
labels_loop_assigns [NormAtLabels] | |
labels_loop_assigns [Wp.NormAtLabels] | |
labels_loop_inv [NormAtLabels] | |
labels_loop_inv [Wp.NormAtLabels] | |
labels_predicate [NormAtLabels] | |
labels_predicate [Wp.NormAtLabels] | |
labels_stmt_assigns [NormAtLabels] | |
labels_stmt_assigns [Wp.NormAtLabels] | |
labels_stmt_post [NormAtLabels] | |
labels_stmt_post [Wp.NormAtLabels] | |
labels_stmt_pre [NormAtLabels] | |
labels_stmt_pre [Wp.NormAtLabels] | |
language_of_name [VCS] | |
language_of_name [Wp.VCS] | |
language_of_prover [VCS] | |
language_of_prover [Wp.VCS] | |
language_of_prover_name [VCS] | |
language_of_prover_name [Wp.VCS] | |
launch [Register] | |
lc_closed [Lang.F] | |
lc_closed [Wp.Lang.F] | |
lc_iter [Lang.F] | |
lc_iter [Wp.Lang.F] | |
lc_map [Lang.F] | |
lc_map [Wp.Lang.F] | |
ldomain [Cvalues] | |
lemma [Auto] | |
lemma [LogicCompiler.Make] | |
lemma [Conditions] | Performs existential, universal and hypotheses introductions |
lemma [Sigs.LogicSemantics] | Compile a lemma definition. |
lemma [Wp.Auto] | |
lemma [Wp.LogicCompiler.Make] | |
lemma [Wp.Conditions] | Performs existential, universal and hypotheses introductions |
lemma [Wp.Sigs.LogicSemantics] | Compile a lemma definition. |
lemma_id [Lang] | |
lemma_id [Wp.Lang] | |
length [Splitter] | |
length [Hashtbl.S] | |
length [Wp.Splitter] | |
lfun [Repr] | |
lfun [Wp.Repr] | |
lift [Vset] | |
lift [Lang.F] | |
lift [Wp.Vset] | |
lift [Wp.Lang.F] | |
lift_add [Vset] | |
lift_add [Wp.Vset] | |
lift_sub [Vset] | |
lift_sub [Wp.Vset] | |
list [Conditions] | The internal list of steps |
list [Wp.Conditions] | The internal list of steps |
literal [Sigs.Model] | Return the memory location of a constant string, the id is a unique identifier. |
literal [Wp.Sigs.Model] | Return the memory location of a constant string, the id is a unique identifier. |
load [ProofSession] | |
load [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. |
loadscripts [Proof] | Load scripts from |
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 [Map.S] |
|
map [Set.S] |
|
map [Wp.Vset] | |
map [Wp.Splitter] | |
map [FCMap.S] |
|
map_condition [Conditions] | |
map_condition [Wp.Conditions] | |
map_l2t [Cvalues.Logic] | |
map_loc [Cvalues.Logic] | |
map_logic [Cvalues] | |
map_opp [Cvalues.Logic] | |
map_opp [Vset] | |
map_opp [Wp.Vset] | |
map_sequence [Conditions] | |
map_sequence [Wp.Conditions] | |
map_sequent [Conditions] | |
map_sequent [Wp.Conditions] | |
map_sloc [Cvalues] | |
map_step [Conditions] | |
map_step [Wp.Conditions] | |
map_t2l [Cvalues.Logic] | |
map_value [Cvalues] | |
mapi [Tactical] | |
mapi [Wp.Tactical] | |
mapi [Map.S] | Same as |
mapi [FCMap.S] | Same as |
mark [Splitter] | |
mark [Wp.Splitter] | |
mark_e [Lang.F] | |
mark_e [Wp.Lang.F] | |
mark_p [Lang.F] | Returns a list of terms to be shared among all shared or marked subterms. |
mark_p [Wp.Lang.F] | Returns a list of terms to be shared among all shared or marked subterms. |
marker [Lang.F] | |
marker [Wp.Lang.F] | |
mask_simplifier [Cint] | |
mask_simplifier [Wp.Cint] | |
matches [Footprint] | Head match |
matrix [Definitions] | |
matrix [Wp.Definitions] | |
max_binding [Map.S] | Same as |
max_binding [FCMap.S] | Same as |
max_binding_opt [Map.S] | Same as |
max_elt [Set.S] | Same as |
max_elt [FCSet.S] | Same as , but returns the largest element of the given set. |
max_elt_opt [Set.S] | Same as |
mem [Sigs.Sigma] | Whether a chunk has been assigned. |
mem [Model.Generator] | |
mem [Model.Registry] | |
mem [Clabels] | |
mem [Wprop.Indexed2] | |
mem [Wprop.Indexed] | |
mem [Map.S] |
|
mem [Set.S] |
|
mem [Hashtbl.S] | |
mem [Wp.Sigs.Sigma] | Whether a chunk has been assigned. |
mem [Wp.Model.Generator] | |
mem [Wp.Model.Registry] | |
mem [FCMap.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 [Model.Registry] | with circularity protection |
memoize [Wp.Model.Registry] | with circularity protection |
merge [Conditions] | |
merge [Sigs.Sigma] | Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins. |
merge [Letify.Defs] | |
merge [Region] | |
merge [Splitter] | |
merge [Matrix] | |
merge [Mcfg.S] | |
merge [Map.S] |
|
merge [Wp.Conditions] | |
merge [Wp.Sigs.Sigma] | Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins. |
merge [Wp.Splitter] | |
merge [Wp.Mcfg.S] | |
merge [FCMap.S] |
|
merge_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 smallest binding of the given map
(with respect to the |
min_binding [FCMap.S] | Return the smallest binding of the given map
(with respect to the |
min_binding_opt [Map.S] | Return the smallest binding of 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 [FCSet.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 |
mk_fct_assigns_id [Wp.WpPropId] | function assigns |
mk_fct_from_id [WpPropId] | \from property of function behavior assigns. |
mk_fct_from_id [Wp.WpPropId] | \from property of function behavior assigns. |
mk_fct_post_id [WpPropId] | |
mk_fct_post_id [Wp.WpPropId] | |
mk_frame [LogicCompiler.Make] | |
mk_frame [Sigs.LogicSemantics] | Full featured constructor for frames, with fresh pool and gamma. |
mk_frame [Wp.LogicCompiler.Make] | |
mk_frame [Wp.Sigs.LogicSemantics] | Full featured constructor for frames, with fresh pool and gamma. |
mk_init_assigns [WpPropId] | |
mk_init_assigns [Wp.WpPropId] | |
mk_inv_hyp_id [WpPropId] | Invariant used as hypothesis |
mk_inv_hyp_id [Wp.WpPropId] | Invariant used as hypothesis |
mk_kf_any_assigns_info [WpPropId] | |
mk_kf_any_assigns_info [Wp.WpPropId] | |
mk_kf_assigns_desc [WpPropId] | |
mk_kf_assigns_desc [Wp.WpPropId] | |
mk_lemma_id [WpPropId] | axiom identification |
mk_lemma_id [Wp.WpPropId] | axiom identification |
mk_loop_any_assigns_info [WpPropId] | |
mk_loop_any_assigns_info [Wp.WpPropId] | |
mk_loop_assigns_desc [WpPropId] | |
mk_loop_assigns_desc [Wp.WpPropId] | |
mk_loop_assigns_id [WpPropId] | |
mk_loop_assigns_id [Wp.WpPropId] | |
mk_loop_from_id [WpPropId] | \from property of loop assigns. |
mk_loop_from_id [Wp.WpPropId] | \from property of loop assigns. |
mk_loop_inv_id [WpPropId] | Invariant establishment and preservation |
mk_loop_inv_id [Wp.WpPropId] | Invariant establishment and preservation |
mk_part [WpPropId] |
|
mk_part [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_stmt_any_assigns_info [WpPropId] | |
mk_stmt_any_assigns_info [Wp.WpPropId] | |
mk_stmt_assigns_desc [WpPropId] | |
mk_stmt_assigns_desc [Wp.WpPropId] | |
mk_stmt_assigns_id [WpPropId] | |
mk_stmt_assigns_id [Wp.WpPropId] | |
mk_stmt_post_id [WpPropId] | |
mk_stmt_post_id [Wp.WpPropId] | |
mk_strategy [WpStrategy] | |
mk_var_decr_id [WpPropId] | Variant decrease |
mk_var_decr_id [Wp.WpPropId] | Variant decrease |
mk_var_pos_id [WpPropId] | Variant positive |
mk_var_pos_id [Wp.WpPropId] | Variant positive |
mk_variant_properties [WpStrategy] | |
mode_of_prover_name [VCS] | |
mode_of_prover_name [Wp.VCS] | |
move_at [LogicCompiler.Make] | |
move_at [Sigs.LogicSemantics] | Move the compilation environment to the specified |
move_at [Wp.LogicCompiler.Make] | |
move_at [Wp.Sigs.LogicSemantics] | Move the compilation environment to the specified |
N | |
name [Model.Data] | |
name [Model.Entries] | |
name [Context] | |
name [Clabels] | |
name [Wp_error] | |
name [Wp.Model.Data] | |
name [Wp.Model.Entries] | |
name [Wp.Context] | |
name [Wp.Clabels] | |
name_of_field [Lang] | |
name_of_field [Wp.Lang] | |
name_of_lfun [Lang] | |
name_of_lfun [Wp.Lang] | |
name_of_prover [VCS] | |
name_of_prover [Wp.VCS] | |
named [TacLemma] | |
natural_id [Matrix] | name for elements in NATURAL |
nearest_elt_ge [FCSet.S] |
|
nearest_elt_le [FCSet.S] |
|
negate [Cvalues] | |
new_env [Mcfg.S] | optionally init env with user logic variables |
new_env [Wp.Mcfg.S] | optionally init env with user logic variables |
new_gamma [Lang] | |
new_gamma [Wp.Lang] | |
new_pool [Lang] | |
new_pool [Wp.Lang] | |
next [Pcfg] | |
next [Clabels] | |
next [Wp.Pcfg] | |
next [Wp.Clabels] | |
nil [Conditions] | |
nil [Wp.Conditions] | |
no_infinite_array [Ctypes] | |
no_infinite_array [Wp.Ctypes] | |
no_result [VCS] | |
no_result [Wp.VCS] | |
no_status [GuiProver] | |
node [CfgCompiler.Cfg] | fresh node |
node [Wp.CfgCompiler.Cfg] | fresh node |
node_model [ProofEngine] | |
node_stmt_opt [Cil2cfg] | |
node_type [Cil2cfg] | |
nodes [CfgCompiler.Cfg.P] | |
nodes [Wp.CfgCompiler.Cfg.P] | |
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 [Region] | |
occurs [Vset] | |
occurs [Lang.F] | |
occurs [Wp.Conditions] | |
occurs [Wp.Sigs.LogicSemantics] | Member of vars. |
occurs [Wp.Sigs.Model] | Test if a location depend on a given logic variable |
occurs [Wp.Vset] | |
occurs [Wp.Lang.F] | |
occurs_e [Strategy] | |
occurs_e [Wp.Strategy] | |
occurs_p [Strategy] | |
occurs_p [Wp.Strategy] | |
occurs_q [Strategy] | |
occurs_q [Wp.Strategy] | |
occurs_x [Strategy] | |
occurs_x [Wp.Strategy] | |
occurs_y [Strategy] | |
occurs_y [Wp.Strategy] | |
occursp [Lang.F] | |
occursp [Wp.Lang.F] | |
of_array [Matrix] | |
of_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_pred [Definitions.Trigger] | |
of_pred [Wp.Definitions.Trigger] | |
of_real [Cint] | |
of_real [Wp.Cint] | |
of_term [Definitions.Trigger] | |
of_term [Wp.Definitions.Trigger] | |
off [Parameter_sig.Bool] | Set the boolean to |
ok_status [GuiProver] | |
old [Clabels] | |
old [Wp.Clabels] | |
on [Parameter_sig.Bool] | Set the boolean to |
on_global [Model] | on_scope None |
on_global [Wp.Model] | on_scope None |
on_kf [Model] | on_scope (Some kf) |
on_kf [Wp.Model] | on_scope (Some kf) |
on_model [Model] | |
on_model [Wp.Model] | |
on_reload [GuiPanel] | |
on_remove [Wpo] | |
on_remove [Wp.Wpo] | |
on_scope [Model] | |
on_scope [Wp.Model] | |
on_update [GuiPanel] | |
once [Footprint] | Width-first once iterator. |
open_file [Script] | |
opened [ProofEngine] | not proved |
ordered [Vset] | - |
ordered [Wp.Vset] | - |
output_dot [CfgCompiler.Cfg] | |
output_dot [Wp.CfgCompiler.Cfg] | |
overflow [TacOverflow] | |
P | |
p_all [Lang.F] | |
p_all [Wp.Lang.F] | |
p_and [Lang.F] | |
p_and [Wp.Lang.F] | |
p_any [Lang.F] | |
p_any [Wp.Lang.F] | |
p_apply [Letify.Sigma] | |
p_apply [Letify.Ground] | |
p_apply [Lang.Subst] | |
p_apply [Lang.F] | |
p_apply [Wp.Lang.Subst] | |
p_apply [Wp.Lang.F] | |
p_bind [Lang.F] | |
p_bind [Wp.Lang.F] | |
p_bool [Lang.F] | |
p_bool [Wp.Lang.F] | |
p_bools [Lang.F] | |
p_bools [Wp.Lang.F] | |
p_call [Lang.F] | |
p_call [Wp.Lang.F] | |
p_close [Lang.F] | Quantify over (sorted) free variables |
p_close [Wp.Lang.F] | Quantify over (sorted) free variables |
p_conj [Lang.F] | |
p_conj [Wp.Lang.F] | |
p_disj [Lang.F] | |
p_disj [Wp.Lang.F] | |
p_equal [Lang.F] | |
p_equal [Wp.Lang.F] | |
p_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_group [ProverTask] | Put pattern in group |
p_group [Wp.ProverTask] | Put pattern in group |
p_havoc [MemTyped] | |
p_havoc [Wp.MemTyped] | |
p_hyps [Lang.F] | |
p_hyps [Wp.Lang.F] | |
p_if [Lang.F] | |
p_if [Wp.Lang.F] | |
p_imply [Lang.F] | |
p_imply [Wp.Lang.F] | |
p_included [MemTyped] | |
p_included [Wp.MemTyped] | |
p_int [ProverTask] | Int group pattern |
p_int [Wp.ProverTask] | Int group pattern |
p_invalid [MemTyped] | |
p_invalid [Wp.MemTyped] | |
p_iter [Lang.F] | |
p_iter [Wp.Lang.F] | |
p_leq [Lang.F] | |
p_leq [Wp.Lang.F] | |
p_lt [Lang.F] | |
p_lt [Wp.Lang.F] | |
p_neq [Lang.F] | |
p_neq [Wp.Lang.F] | |
p_not [Lang.F] | |
p_not [Wp.Lang.F] | |
p_or [Lang.F] | |
p_or [Wp.Lang.F] | |
p_positive [Lang.F] | |
p_positive [Wp.Lang.F] | |
p_separated [MemTyped] | |
p_separated [Wp.MemTyped] | |
p_string [ProverTask] | String group pattern |
p_string [Wp.ProverTask] | String group pattern |
p_subst [Lang.F] | |
p_subst [Wp.Lang.F] | |
p_true [Lang.F] | |
p_true [Wp.Lang.F] | |
p_until_space [ProverTask] | No space group pattern "\\( |
p_until_space [Wp.ProverTask] | No space group pattern "\\( |
p_valid_rd [MemTyped] | |
p_valid_rd [Wp.MemTyped] | |
p_valid_rw [MemTyped] | |
p_valid_rw [Wp.MemTyped] | |
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 [ProverWhy3] | |
parse [Wp.Factory] | Apply specifications to default setup. |
parse_coqproof [Proof] |
|
parse_scripts [Proof] |
|
partition [Map.S] |
|
partition [Set.S] |
|
partition [FCMap.S] |
|
parts_of_id [WpPropId] | get the 'part' information. |
parts_of_id [Wp.WpPropId] | get the 'part' information. |
path [Region] | Empty, but Full for the path |
pattern [Footprint] | Generate head footprint up to size |
pending [ProofEngine] | |
pending [ProofScript] | pending goals |
plain [Cvalues] | |
pointer [MemTyped] | |
pointer [Lang] | type of pointers |
pointer [Wp.MemTyped] | |
pointer [Wp.Lang] | type of pointers |
pointer_loc [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 [Plang] | |
pool [Lang.F] | |
pool [Wp.Plang] | |
pool [Wp.Lang.F] | |
pop [Context] | |
pop [Wp.Context] | |
post [Clabels] | |
post [Wp.Clabels] | |
pp [CfgCompiler.Cfg.Node] | |
pp [Wp.CfgCompiler.Cfg.Node] | |
pp_annots [WpStrategy] | |
pp_assign_info [WpPropId] | |
pp_assign_info [Wp.WpPropId] | |
pp_assigns [Wp_error] | |
pp_assigns_desc [WpPropId] | |
pp_assigns_desc [Wp.WpPropId] | |
pp_axiom_info [WpPropId] | |
pp_axiom_info [Wp.WpPropId] | |
pp_axiomatics [Wpo] | |
pp_axiomatics [Wp.Wpo] | |
pp_bound [Vset] | |
pp_bound [Wp.Vset] | |
pp_call_type [Cil2cfg] | |
pp_calls [Dyncall] | |
pp_clause [Tactical] | Debug only |
pp_clause [Separation] | Prints the separation in ACSL format. |
pp_clause [Wp.Tactical] | Debug only |
pp_clause [Wp.Separation] | Prints the separation in ACSL format. |
pp_cluster [Definitions] | |
pp_cluster [Wp.Definitions] | |
pp_depend [Wpo] | |
pp_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_language [VCS] | |
pp_language [Wp.VCS] | |
pp_logfile [Wpo] | |
pp_logfile [Wp.Wpo] | |
pp_logic [Sigs.LogicSemantics] | |
pp_logic [Wp.Sigs.LogicSemantics] | |
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 [Separation] | |
pp_param [Wp.Separation] | |
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 [Sigs.LogicSemantics] | |
pp_region [Wp.Sigs.LogicSemantics] | |
pp_result [VCS] | |
pp_result [Wp.VCS] | |
pp_result_perf [VCS] | |
pp_result_perf [Wp.VCS] | |
pp_selection [Tactical] | Debug only |
pp_selection [Wp.Tactical] | Debug only |
pp_sloc [Sigs.LogicSemantics] | |
pp_sloc [Wp.Sigs.LogicSemantics] | |
pp_string_list [Wp_error] | |
pp_tau [Lang.F] | |
pp_tau [Wp.Lang.F] | |
pp_term [Lang.F] | |
pp_term [Wp.Lang.F] | |
pp_time [Rformat] | Pretty print time in hour, minutes, seconds, or milliseconds, as appropriate |
pp_time_range [Rformat] | |
pp_title [Wpo] | |
pp_title [Wp.Wpo] | |
pp_value [Sigs.CodeSemantics] | |
pp_value [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 [ProverWhy3.Goal] | |
pretty [Why3_xml] | |
pretty [ProofEngine] | |
pretty [ProofSession] | |
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 [Region] | |
pretty [Vlist] | |
pretty [Vset] | |
pretty [Splitter] | |
pretty [Passive] | |
pretty [Model.Key] | |
pretty [Model.Entries] | |
pretty [Warning] | |
pretty [Mcfg.S] | |
pretty [WpPropId] | |
pretty [Clabels] | |
pretty [Ctypes] | |
pretty [Rformat] | |
pretty [Wp.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.Model.Key] | |
pretty [Wp.Model.Entries] | |
pretty [Wp.Warning] | |
pretty [Wp.Mcfg.S] | |
pretty [Wp.WpPropId] | |
pretty [Wp.Clabels] | |
pretty [Wp.Ctypes] | |
pretty_context [WpPropId] | |
pretty_context [Wp.WpPropId] | |
pretty_local [WpPropId] | |
pretty_local [Wp.WpPropId] | |
prev [Pcfg] | |
prev [Wp.Pcfg] | |
print_generated [Wp_parameters] | print the given file if the debugging category "print-generated" is set |
print_generated [Wp.Wp_parameters] | print the given file if the debugging category "print-generated" is set |
promote [Ctypes] | |
promote [Wp.Ctypes] | |
proof [VC] | List of proof obligations computed for a given property. |
proof [ProofEngine] | |
proof [Wp.VC] | List of proof obligations computed for a given property. |
proof_context [LogicUsage] | Lemmas that are not in an axiomatic. |
proof_context [Wp.LogicUsage] | Lemmas that are not in an axiomatic. |
prop_id_keys [WpPropId] | |
prop_id_keys [Wp.WpPropId] | |
property [Dyncall] | Returns an property identifier for the precondition. |
property [Wprop.Info] | |
property [Wprop.Indexed2] | |
property [Wprop.Indexed] | |
property_of_id [WpPropId] | returns the annotation which lead to the given PO. |
property_of_id [Wp.WpPropId] | returns the annotation which lead to the given PO. |
prove [VC] | Returns a ready-to-schedule task. |
prove [ProverScript] | |
prove [Prover] | |
prove [ProverWhy3ide] | |
prove [ProverWhy3] | The string must be a valid why3 prover identifier Return NoResult if it is already proved by Qed |
prove [ProverCoq] | |
prove [ProverErgo] | |
prove [Wp.Prover] | |
prove [Wp.VC] | Returns a ready-to-schedule task. |
proved [Register] | |
proved [ProofEngine] | not opened |
prover [ProverWhy3] | |
prover_of_json [ProofScript] | |
prover_of_name [Wpo] | Dynamically exported. |
prover_of_name [VCS] | |
prover_of_name [Wp.Wpo] | Dynamically exported. |
prover_of_name [Wp.VCS] | |
provers [Register] | |
pruning [Conditions] | |
pruning [Wp.Conditions] | |
push [Context] | |
push [Wp.Context] | |
Q | |
qed_time [Wpo.GOAL] | |
qed_time [Wpo] | |
qed_time [Wp.Wpo.GOAL] | |
qed_time [Wp.Wpo] | |
R | |
range [Auto] | |
range [Tactical] | |
range [Vset] | |
range [Cfloat] | |
range [Cint] | Dependent on model |
range [Wp.Auto] | |
range [Wp.Tactical] | |
range [Wp.Vset] | |
range [Wp.Cfloat] | |
range [Wp.Cint] | Dependent on model |
ranges [Auto.Range] | |
ranges [Wp.Auto.Range] | |
rdescr [Cvalues.Logic] | |
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_int [Cmath] | |
record [Lang] | |
record [Wp.Lang] | |
record_with [Lang.F] | |
record_with [Wp.Lang.F] | |
region [LogicCompiler.Make] | When |
region [Sigs.LogicSemantics] | Compile a term representing a set of memory locations into an abstract region. |
region [Cvalues.Logic] | |
region [Wp.LogicCompiler.Make] | When |
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 [Pcfg] | |
register [Model] | |
register [Context] | Register a global configure, to be executed once per project/ast. |
register [Wp.Strategy] | |
register [Wp.Tactical] | |
register [Wp.Pcfg] | |
register [Wp.Model] | |
register [Wp.Context] | Register a global configure, to be executed once per project/ast. |
release [Lang.F] | Empty local caches |
release [Wp.Lang.F] | Empty local caches |
reload [GuiPanel] | |
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 [Model.Generator] | |
remove [Model.Registry] | |
remove [Cil2cfg.HEsig] | |
remove [Wp.Wpo] | |
remove [Wp.VC] | |
remove [Map.S] |
|
remove [Set.S] |
|
remove [Hashtbl.S] | |
remove [Wp.Model.Generator] | |
remove [Wp.Model.Registry] | |
remove [FCMap.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. |
replace [Tactical] | |
replace [Conditions] | replace a step in the sequent, the one |
replace [Cil2cfg.HEsig] | |
replace [Wp.Tactical] | |
replace [Hashtbl.S] | |
replace [Wp.Conditions] | replace a step in the sequent, the one |
repr [Lang.F] | Constant time |
repr [Model] | |
repr [Wp.Lang.F] | Constant time |
repr [Wp.Model] | |
requires [Separation] | Build the separation clause from a partition |
requires [Wp.Separation] | Build the separation clause from a partition |
reset [ProofEngine] | |
reset [Lang.F.Check] | |
reset [Wp_parameters] | |
reset [Hashtbl.S] | |
reset [Wp.Lang.F.Check] | |
reset [Wp.Wp_parameters] | |
resolve [Wpo.VC_Annot] | |
resolve [Wpo] | tries simplification |
resolve [Wp.Wpo.VC_Annot] | |
resolve [Wp.Wpo] | tries simplification |
result [VCS] | |
result [StmtSemantics.Make] | |
result [LogicCompiler.Make] | |
result [Sigs.LogicSemantics] | Result location of the current function in the current frame. |
result [Sigs.CodeSemantics] | Value of an abstract result container. |
result [Wp.VCS] | |
result [Wp.StmtSemantics.Make] | |
result [Wp.LogicCompiler.Make] | |
result [Wp.Sigs.LogicSemantics] | Result location of the current function in the current frame. |
result [Wp.Sigs.CodeSemantics] | Value of an abstract result container. |
result_of_json [ProofScript] | |
return [StmtSemantics.Make] | |
return [LogicCompiler.Make] | |
return [Sigs.LogicSemantics] | Result type of the current function in the current frame. |
return [Sigs.CodeSemantics] | Return an expression with a given type. |
return [Mcfg.S] | |
return [Wp.StmtSemantics.Make] | |
return [Wp.LogicCompiler.Make] | |
return [Wp.Sigs.LogicSemantics] | Result type of the current function in the current frame. |
return [Wp.Sigs.CodeSemantics] | Return an expression with a given type. |
return [Wp.Mcfg.S] | |
rewrite [Tactical] | For each pattern |
rewrite [Wp.Tactical] | For each pattern |
rpath [Region] | Empty, but Full for the r-paths |
run [Register] | |
run [ProverWhy3ide] | |
run_and_prove [GuiPanel] | |
S | |
s_bool [WpTac] | |
s_cnf_iff [WpTac] | |
s_cnf_ite [WpTac] | |
s_cnf_xor [WpTac] | |
s_dnf_iff [WpTac] | |
s_dnf_ite [WpTac] | |
s_dnf_xor [WpTac] | |
same_edge [Cil2cfg] | |
same_node [Cil2cfg] | |
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 name. |
select_by_name [Wp.WpPropId] | test if the prop_id has to be selected for the asked name. |
select_call_pre [WpPropId] | test if the prop_id has to be selected when we want to select the call
precondition the the |
select_call_pre [Wp.WpPropId] | test if the prop_id has to be selected when we want to select the call
precondition the the |
select_e [Strategy] | Lookup the first occurrence of term in the sequent and returns the associated selection. |
select_e [Wp.Strategy] | Lookup the first occurrence of term in the sequent and returns the associated selection. |
select_p [Strategy] | Same as |
select_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 [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 |
separation [MemVar.VarUsage] | |
separation [Sigs.Model] | Computes the separation clauses to be verified for this model. |
separation [Wp.MemVar.VarUsage] | |
separation [Wp.Sigs.Model] | Computes the separation clauses to be verified for this model. |
seq_branch [Conditions] | |
seq_branch [Wp.Conditions] | |
sequence [Register] | |
sequence [StmtSemantics.Make] | Chain compiler by introducing fresh nodes between each element of the list. |
sequence [Pcond] | |
sequence [Conditions] | |
sequence [Wp.StmtSemantics.Make] | Chain compiler by introducing fresh nodes between each element of the list. |
sequence [Wp.Pcond] | |
sequence [Wp.Conditions] | |
server [VC] | Default number of parallel tasks is given by |
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 [Lang.F.Check] | |
set [Context] | Define the current value. |
set [Separation] | |
set [Wp.Tactical.Fmap] | |
set [Wp.StmtSemantics.Make] | |
set [Wp.Lang.F.Check] | |
set [Wp.Context] | Define the current value. |
set [Wp.Separation] | |
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.F] | |
set_builtin [Wp.Lang.F] | |
set_builtin_1 [Lang.F] | |
set_builtin_1 [Wp.Lang.F] | |
set_builtin_2 [Lang.F] | |
set_builtin_2 [Wp.Lang.F] | |
set_builtin_eq [Lang.F] | |
set_builtin_eq [Wp.Lang.F] | |
set_builtin_eqp [Lang.F] | |
set_builtin_eqp [Wp.Lang.F] | |
set_builtin_leq [Lang.F] | |
set_builtin_leq [Wp.Lang.F] | |
set_builtin_type [Lang] | |
set_builtin_type [Wp.Lang] | |
set_model [Register] | |
set_model [Wp_error] | |
set_option [LogicBuiltins] | reset and add a value to an option (group, name) |
set_option [Wp.LogicBuiltins] | reset and add a value to an option (group, name) |
set_possible_values [Parameter_sig.String] | Set what are the acceptable values for this parameter. |
set_range [Parameter_sig.Int] | Set what is the possible range of values for this parameter. |
set_result [Wpo] | |
set_result [Wp.Wpo] | |
set_saved [ProofEngine] | |
set_strategies [ProofEngine] | |
severe [Warning] | |
severe [Wp.Warning] | |
shareable [Vlist] | |
shift [Sigs.Model] | Return the memory location obtained by array access at an index
represented by the given |
shift [Cvalues.Logic] | |
shift [Wp.Sigs.Model] | Return the memory location obtained by array access at an index
represented by the given |
sigma [Lang.Subst] | |
sigma [Lang.F] | |
sigma [Wp.Lang.Subst] | |
sigma [Wp.Lang.F] | |
signature [Tactical] | |
signature [Wp.Tactical] | |
signed [Ctypes] |
|
signed [Wp.Ctypes] |
|
simplify [Conditions] | |
simplify [Mcfg.Splitter] | |
simplify [Wp.Conditions] | |
simplify [Wp.Mcfg.Splitter] | |
singleton [Letify.Ground] | |
singleton [Vset] | |
singleton [Splitter] | |
singleton [Map.S] |
|
singleton [Set.S] |
|
singleton [Wp.Vset] | |
singleton [Wp.Splitter] | |
singleton [FCMap.S] |
|
size [Conditions] | |
size [Matrix] | |
size [Wp.Conditions] | |
sizeof_defined [Ctypes] | |
sizeof_defined [Wp.Ctypes] | |
sizeof_object [Ctypes] | |
sizeof_object [Wp.Ctypes] | |
skip [Script] | |
sort [Lang.F] | Constant time |
sort [Wp.Lang.F] | Constant time |
source_of_id [WpPropId] | |
source_of_id [Wp.WpPropId] | |
spawn [VC] | Same as |
spawn [ProverScript] | |
spawn [Prover] | |
spawn [ProverTask] | Spawn all the tasks over the server and retain the first 'validated' one. |
spawn [Wp.Prover] | |
spawn [Wp.ProverTask] | Spawn all the tasks over the server and retain the first 'validated' one. |
spawn [Wp.VC] | Same as |
spawn_wp_proofs_iter [Register] | |
spec [StmtSemantics.Make] | |
spec [Wp.StmtSemantics.Make] | |
spinner [Tactical] | Unless specified, default is |
spinner [Wp.Tactical] | Unless specified, default is |
split [Auto] | |
split [Tactical] | |
split [WpAnnot] | splits a prop_id goals into prop_id parts for each sub-goals |
split [Mcfg.Splitter] | |
split [Wp.Auto] | |
split [Wp.Tactical] | |
split [Map.S] |
|
split [Set.S] |
|
split [Wp.Mcfg.Splitter] | |
split [FCSet.S] |
|
split [FCMap.S] |
|
spy [Register] | |
start_edge [Cil2cfg] | get the starting edges |
start_stmt_of_node [Cil2cfg] | |
state [ProofEngine] | |
state [Conditions] | |
state [Mstate] | |
state [Sigs.Model] | Returns a memory state description from a memory environement. |
state [Wp.Conditions] | |
state [Wp.Mstate] | |
state [Wp.Sigs.Model] | Returns a memory state description from a memory environement. |
stats [Hashtbl.S] | |
status [ProofEngine] | |
status [ProofScript] | minimum of pending goals |
status [LogicCompiler.Make] | |
status [Sigs.LogicSemantics] | Exit status for the current frame. |
status [Wp.LogicCompiler.Make] | |
status [Wp.Sigs.LogicSemantics] | Exit status for the current frame. |
step [Conditions] | |
step [Wp.Conditions] | |
step_at [Conditions] | Retrieve a step by |
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] | |
stored [Sigs.Model] | Return a set of formula that express a modification between two memory state. |
stored [Wp.Sigs.Model] | Return a set of formula that express a modification between two memory state. |
str_id [Cstring] | Non-zero integer, unique for each different string literal |
str_id [Wp.Cstring] | Non-zero integer, unique for each different string literal |
str_len [Cstring] | Property defining the size of the string in bytes,
with |
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 [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 [Region] | |
subset [Vset] | |
subset [Set.S] |
|
subset [Wp.Vset] | |
subst [Conditions] | Apply the atomic substitution recursively using |
subst [Wp.Conditions] | Apply the atomic substitution recursively using |
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 | |
t_absurd [Auto] | Find a contradiction. |
t_absurd [Wp.Auto] | Find a contradiction. |
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_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_id [Auto] | Keep goal unchanged. |
t_id [Wp.Auto] | Keep goal unchanged. |
t_int [Lang] | |
t_int [Wp.Lang] | |
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 [TacShift] | |
tactical [TacBitrange] | |
tactical [TacBitwised] | |
tactical [TacRewrite] | |
tactical [TacNormalForm] | |
tactical [TacCut] | |
tactical [TacFilter] | |
tactical [TacLemma] | |
tactical [TacInstance] | |
tactical [TacHavoc.Validity] | |
tactical [TacHavoc.Separated] | |
tactical [TacHavoc.Havoc] | |
tactical [TacUnfold] | |
tactical [TacCompound] | |
tactical [TacArray] | |
tactical [TacRange] | |
tactical [TacChoice.Contrapose] | |
tactical [TacChoice.Absurd] | |
tactical [TacChoice.Choice] | |
tactical [TacSplit] | |
tactical [WpPropId] | |
tactical [Wp.WpPropId] | |
target [WpAnnot] | |
tau [Matrix] | |
tau_of_chunk [Sigs.Chunk] | The type of data hold in a chunk. |
tau_of_chunk [Wp.Sigs.Chunk] | The type of data hold in a chunk. |
tau_of_comp [Lang] | |
tau_of_comp [Wp.Lang] | |
tau_of_ctype [Lang] | |
tau_of_ctype [Wp.Lang] | |
tau_of_field [Lang] | |
tau_of_field [Wp.Lang] | |
tau_of_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_of_mode [VCS] | |
title_of_mode [Wp.VCS] | |
title_of_prover [VCS] | |
title_of_prover [Wp.VCS] | |
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] | |
token [Script] | |
top [Letify.Ground] | |
tracelog [Register] | |
tree_model [ProofEngine] | |
trigger [LogicCompiler.Make] | |
trigger [Wp.LogicCompiler.Make] | |
trivial [Wpo.GOAL] | |
trivial [Conditions] | |
trivial [Wp.Wpo.GOAL] | |
trivial [Wp.Conditions] | |
try_sequence [Register] | |
type_id [Lang] | |
type_id [Wp.Lang] | |
typeof [Lang.F] | Try to extract a type of term. |
typeof [Wp.Lang.F] | Try to extract a type of term. |
U | |
unchanged [Sigs.CodeSemantics] | Express that a given variable has the same value in two memory states. |
unchanged [Wp.Sigs.CodeSemantics] | Express that a given variable has the same value in two memory states. |
union [Sigs.Sigma] | Same as |
union [Cvalues.Logic] | |
union [Vset] | |
union [Splitter] | |
union [Passive] | |
union [Map.S] |
|
union [Set.S] | Set union. |
union [Wp.Sigs.Sigma] | Same as |
union [Wp.Vset] | |
union [Wp.Splitter] | |
union [Wp.Passive] | |
unknown [VCS] | |
unknown [Wp.VCS] | |
unreachable_nodes [Cil2cfg] | |
unsupported [Wp_error] | |
update [GuiPanel] | |
update [Region] | |
update [Model.Registry] | set current value, with no protection |
update [Context] | Modification of the current value |
update [Map.S] |
|
update [Wp.Model.Registry] | set current value, with no protection |
update [Wp.Context] | Modification of the current value |
update_cond [Conditions] | Updates the condition of a step and merges |
update_cond [Wp.Conditions] | Updates the condition of a step and merges |
update_hints_for_goal [Proof] | Update the hints for one specific goal. |
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_assigns [Mcfg.S] |
|
use_assigns [Wp.Mcfg.S] |
|
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 |
vanti [TacFilter] | |
variables [Lang] | |
variables [Wp.Lang] | |
vars [Sigs.LogicSemantics] | Qed variables appearing in a region expression. |
vars [Sigs.Model] | Return the logic variables from which the given location depend on. |
vars [Region] | |
vars [Vset] | |
vars [Definitions.Trigger] | |
vars [Lang.F] | Constant time |
vars [Wp.Sigs.LogicSemantics] | Qed variables appearing in a region expression. |
vars [Wp.Sigs.Model] | Return the logic variables from which the given location depend on. |
vars [Wp.Vset] | |
vars [Wp.Definitions.Trigger] | |
vars [Wp.Lang.F] | Constant time |
vars_hyp [Conditions] | |
vars_hyp [Wp.Conditions] | |
vars_seq [Conditions] | |
vars_seq [Wp.Conditions] | |
varsp [Lang.F] | Constant time |
varsp [Wp.Lang.F] | Constant time |
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 | |
warnings [Wpo] | |
warnings [Wp.Wpo] | |
wg_status [GuiProver] | |
with_current_loc [Context] | |
with_current_loc [Wp.Context] | |
with_model [Model] | |
with_model [Wp.Model] | |
without_assume [Lang] | |
without_assume [Wp.Lang] | |
wp_iter_model [Register] | |
wp_print_separation [Register] | |
wp_warn_separation [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] |
|