A |
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 [Map.S] |
add x y m returns a map containing the same bindings as
m , plus a binding of x to y .
|
add [Wp.Warning] |
|
add [FCMap.S] |
add x y m returns a map containing the same bindings as
m , plus a binding of x to y .
|
add_alias [LogicBuiltins] |
|
add_alias [Wp.LogicBuiltins] |
|
add_all_axioms [WpStrategy] |
|
add_assigns [Mcfg.S] |
|
add_assigns [WpStrategy] |
generic function to add an assigns property.
|
add_assigns [Wp.Mcfg.S] |
|
add_assigns_any [WpStrategy] |
generic function to add a WriteAny assigns property.
|
add_axiom [Mcfg.S] |
|
add_axiom [WpStrategy] |
|
add_axiom [Wp.Mcfg.S] |
|
add_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_ctor [LogicBuiltins] |
|
add_ctor [Wp.LogicBuiltins] |
|
add_definitions [Letify] |
add_definitions sigma defs xs ps keep all
definitions of variables xs from sigma that comes from defs .
|
add_fct_bhv_assigns_hyp [WpStrategy] |
|
add_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_node_annots cfg annots v (before, (after, exits))
add the annotations for the node :
|
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 impl_assumes , add b_assumes => b_requires
else add both the b_requires and the b_assumes
|
add_prop_fct_post [WpStrategy] |
|
add_prop_fct_pre [WpStrategy] |
Add the predicate as a function precondition.
|
add_prop_loop_inv [WpStrategy] |
|
add_prop_stmt_bhv_requires [WpStrategy] |
Add all the b_requires .
|
add_prop_stmt_post [WpStrategy] |
Add the predicate as a stmt precondition.
|
add_prop_stmt_pre [WpStrategy] |
Add the predicate as a stmt precondition.
|
add_prop_stmt_spec_pre [WpStrategy] |
Process the stmt spec precondition as an hypothesis for external properties.
|
add_script [Proof] |
new_script goal keys proof qed registers the script proof terminated by qed
for goal goal and keywords keys
|
add_step [Register] |
|
add_stmt_spec_assigns_hyp [WpStrategy] |
shortcut to add a stmt spec assigns property as an hypothesis.
|
add_time [Register] |
|
add_type [LogicBuiltins] |
|
add_type [Wp.LogicBuiltins] |
|
age [Wpo] |
|
alloc_for_type [VarUsage] |
Size of dimensions in the type (0 for unknown size)
|
alloc_for_type [VarUsageRef] |
Size of dimensions in the type (0 for unknown size)
|
already_valid [Register] |
|
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 [Cvalues.Logic] |
|
apply [Passive] |
|
apply [Wp.Passive] |
|
apply_add [Cvalues.Logic] |
|
apply_sub [Cvalues.Logic] |
|
array [Lang] |
|
array [Wp.Lang] |
|
array_dim [Ctypes] |
|
array_dim [Wp.Ctypes] |
|
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_wpo [ProverWhy3] |
None if the po is trivial
|
assign [Mcfg.S] |
|
assign [Wp.Mcfg.S] |
|
assigned [LogicAssigns.Make] |
|
assigned [Memory.Model] |
Return a set of formula that express that two memory state are the same
except at the given set of memory location.
|
assigned [Memory.Sigma] |
equal chunks outside domain
|
assigned [Wp.Memory.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.Memory.Sigma] |
equal chunks outside domain
|
assigns [LogicSemantics.Make] |
|
assigns [Wp.LogicSemantics.Make] |
|
assigns_from [LogicSemantics.Make] |
|
assigns_from [Wp.LogicSemantics.Make] |
|
assigns_info_id [WpPropId] |
|
assigns_info_id [Wp.WpPropId] |
|
assigns_upper_bound [WpStrategy] |
|
assume [Conditions] |
|
assume [Letify.Sigma] |
|
assume [Lang] |
|
assume [Wp.Conditions] |
|
assume [Wp.Lang] |
|
atype [Lang] |
|
atype [Wp.Lang] |
|
auto_check_valid [Register] |
|
axiomatic [Definitions] |
|
axiomatic [LogicUsage] |
|
axiomatic [Wp.Definitions] |
|
axiomatic [Wp.LogicUsage] |
|
B |
band [Cint] |
|
band [Wp.Cint] |
|
bar [Wpo] |
|
base_addr [Memory.Model] |
Return the memory location of the base address of a given memory
location
|
base_addr [Wp.Memory.Model] |
Return the memory location of the base address of a given memory
location
|
basename [LogicUsage] |
Trims the original name
|
basename [Ctypes] |
|
basename [Wp.LogicUsage] |
Trims the original name
|
basename [Wp.Ctypes] |
|
basename_of_chunk [Memory.Chunk] |
|
basename_of_chunk [Wp.Memory.Chunk] |
|
begin_session [Register] |
|
behavior_name_of_strategy [WpStrategy] |
|
bind [Letify] |
bind sigma defs xs select definitions in defs
targeting variables xs .
|
bind [Passive] |
|
bind [Context] |
Performs the job with local context bound to local value.
|
bind [Wp.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 [Memory.Model] |
Returns the length (in bytes) of the allocated block containing
the given location
|
block_length [Wp.Memory.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_add [Vset] |
|
bound_add [Wp.Vset] |
|
bound_shift [Vset] |
|
bound_shift [Wp.Vset] |
|
bound_sub [Vset] |
|
bound_sub [Wp.Vset] |
|
brackets_typ [Variables_analysis] |
brackets_typ typ returns the numbre of brackets of the type typ .
|
branch [Conditions] |
|
branch [Wp.Conditions] |
|
build_prop_of_from [Mcfg.S] |
build p => alpha(p) for functional dependencies verification.
|
build_prop_of_from [Wp.Mcfg.S] |
build p => alpha(p) for functional dependencies verification.
|
builtin_type [Lang] |
|
builtin_type [Wp.Lang] |
|
bundle [Pcond] |
|
bxor [Cint] |
|
bxor [Wp.Cint] |
|
C |
c_bool [Ctypes] |
Returns the type of int
|
c_bool [Wp.Ctypes] |
Returns the type of int
|
c_char [Ctypes] |
Returns the type of char
|
c_char [Wp.Ctypes] |
Returns the type of char
|
c_float [Ctypes] |
Conforms to
|
c_float [Wp.Ctypes] |
Conforms to
|
c_int [Ctypes] |
Conforms to
|
c_int [Wp.Ctypes] |
Conforms to
|
c_int_all [Ctypes] |
|
c_int_all [Wp.Ctypes] |
|
c_int_bounds [Ctypes] |
|
c_int_bounds [Wp.Ctypes] |
|
c_label [Clabels] |
Assumes the logic label only comes from normalized labels.
|
c_label [Wp.Clabels] |
Assumes the logic label only comes from normalized labels.
|
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_log [Wpo.DISK] |
|
call [LogicSemantics.Make] |
|
call [LogicCompiler.Make] |
|
call [CodeSemantics.Make] |
|
call [Splitter] |
|
call [Mcfg.S] |
|
call [Wp.LogicSemantics.Make] |
|
call [Wp.LogicCompiler.Make] |
|
call [Wp.CodeSemantics.Make] |
|
call [Wp.Splitter] |
|
call [Wp.Mcfg.S] |
|
call_dynamic [Mcfg.S] |
|
call_dynamic [Wp.Mcfg.S] |
|
call_env [LogicSemantics.Make] |
|
call_env [Wp.LogicSemantics.Make] |
|
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_post [LogicSemantics.Make] |
|
call_post [LogicCompiler.Make] |
|
call_post [Wp.LogicSemantics.Make] |
|
call_post [Wp.LogicCompiler.Make] |
|
call_pre [LogicSemantics.Make] |
|
call_pre [LogicCompiler.Make] |
|
call_pre [Wp.LogicSemantics.Make] |
|
call_pre [Wp.LogicCompiler.Make] |
|
call_pred [LogicCompiler.Make] |
|
call_pred [Definitions] |
|
call_pred [Wp.LogicCompiler.Make] |
|
call_pred [Wp.Definitions] |
|
callback [Model.Registry] |
|
callback [Wp.Model.Registry] |
|
cardinal [Map.S] |
Return the number of bindings of a map.
|
cardinal [FCMap.S] |
Return the number of bindings of a map.
|
cases [Splitter] |
|
cases [Wp.Splitter] |
|
cast [CodeSemantics.Make] |
|
cast [Memory.Model] |
Cast a memory location into another memory location.
|
cast [Wp.CodeSemantics.Make] |
|
cast [Wp.Memory.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] |
|
cells_in_type [VarUsage] |
Number of cells in the type (raise NoSize for unknown size)
|
cells_in_type [VarUsageRef] |
Number of cells in the type (raise NoSize for unknown size)
|
cfg_kf [Cil2cfg] |
|
cfg_of_strategy [WpStrategy] |
|
cfg_spec_only [Cil2cfg] |
returns true is this CFG is degenerated (no code available)
|
char [Ctypes] |
|
char [Wp.Ctypes] |
|
char_at [Cstring] |
|
char_at [Wp.Cstring] |
|
check_tau [Vlist] |
|
check_term [Vlist] |
|
checked [VCS] |
|
checked [Wp.VCS] |
|
choose [Map.S] |
Return one binding of the given map, or raise Not_found if
the map is empty.
|
choose [FCMap.S] |
Return one binding of the given map, or raise Not_found if
the map is empty.
|
clean [Conditions] |
|
clean [Wp.Conditions] |
|
clear [VC] |
|
clear [Wpo] |
|
clear [Proof] |
|
clear [Context] |
Clear the current value.
|
clear [Cil2cfg.HEsig] |
|
clear [Wp.VC] |
|
clear [Wp.Context] |
Clear the current value.
|
clear_scheduled [Register] |
|
clear_session [Register] |
|
cloc [CodeSemantics.Make] |
|
cloc [Wp.CodeSemantics.Make] |
|
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
|
comp [Lang] |
|
comp [Wp.Lang] |
|
comp_id [Lang] |
|
comp_id [Wp.Lang] |
|
compare [ProverWhy3.Goal] |
|
compare [Map.OrderedType] |
A total ordering function over the keys.
|
compare [VCS] |
|
compare [Memory.Chunk] |
|
compare [LogicBuiltins] |
|
compare [Model.Key] |
|
compare [Model.Entries] |
|
compare [Warning] |
|
compare [Clabels.T] |
|
compare [Ctypes.AinfoComparable] |
|
compare [Ctypes] |
|
compare [Map.S] |
Total ordering between maps.
|
compare [Wp.VCS] |
|
compare [Wp.Memory.Chunk] |
|
compare [Wp.LogicBuiltins] |
|
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] |
|
compare_ptr_conflated [Wp.Ctypes] |
|
comparep [Lang.F] |
|
comparep [Wp.Lang.F] |
|
compile [Model.Data] |
|
compile [Model.Registry] |
with circularity protection
|
compile [Wp.Model.Data] |
|
compile [Wp.Model.Registry] |
with circularity protection
|
compile_lemma [Definitions] |
|
compile_lemma [Wp.Definitions] |
|
compinfo [Definitions] |
|
compinfo [Wp.Definitions] |
|
compute [Calculus.Cfg] |
|
compute [Wpo.GOAL] |
|
compute [RefUsage] |
|
compute [VarUsage] |
|
compute [VarUsageRef] |
|
compute [LogicUsage] |
To force computation
|
compute [Dyncall] |
Forces computation of dynamic calls.
|
compute [Wp.RefUsage] |
|
compute [Wp.LogicUsage] |
To force computation
|
compute_call [Generator] |
|
compute_descr [Wpo.GOAL] |
|
compute_ip [Generator] |
|
compute_kf [Generator] |
|
compute_proof [Wpo.GOAL] |
|
compute_provers [Register] |
|
compute_selection [Generator] |
|
computer [Register] |
|
computer [CfgWP] |
|
computing [VCS] |
|
computing [Wp.VCS] |
|
concat [Conditions] |
|
concat [Wp.Conditions] |
|
concretize [Vset] |
|
concretize [Wp.Vset] |
|
cond [CodeSemantics.Make] |
|
cond [Wp.CodeSemantics.Make] |
|
condition [Conditions] |
With free variables kept.
|
condition [Wp.Conditions] |
With free variables kept.
|
conditions [Passive] |
|
conditions [Wp.Passive] |
|
configure [Factory] |
|
configure [Memory.Model] |
|
configure [Cfloat] |
|
configure [Cint] |
|
configure [Wp.Factory] |
|
configure [Wp.Cfloat] |
|
configure [Wp.Cint] |
|
configure [Wp.Memory.Model] |
|
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] |
|
convert [Lang.Alpha] |
|
convert [Wp.Lang.Alpha] |
|
convertp [Lang.Alpha] |
|
convertp [Wp.Lang.Alpha] |
|
copied [Memory.Model] |
Return a set of formula that express a copy between two memory state.
|
copied [Wp.Memory.Model] |
Return a set of formula that express a copy between two memory state.
|
copy [Memory.Sigma] |
|
copy [Wp.Memory.Sigma] |
|
copy [Datatype.S] |
Deep copy: no possible sharing between x and copy x .
|
create [CfgDump] |
|
create [Memory.Sigma] |
|
create [LogicBuiltins] |
Create a new driver.
|
create [Cleaning] |
|
create [Letify.Split] |
|
create [Lang.Alpha] |
|
create [Context] |
Creates a new context with name
|
create [Cil2cfg.HEsig] |
|
create [Wp.Memory.Sigma] |
|
create [Wp.LogicBuiltins] |
Create a new driver.
|
create [Wp.Lang.Alpha] |
|
create [Wp.Context] |
Creates a new context with name
|
create_option [LogicBuiltins] |
add_option_sanitizer ~driver_dir group name
add a sanitizer for group group and option name
|
create_option [Wp.LogicBuiltins] |
add_option_sanitizer ~driver_dir group name
add a sanitizer for group group and option name
|
create_proof [WpAnnot] |
to be used only once for one of the related prop_id
|
create_tbl [WpStrategy] |
|
ctor [LogicBuiltins] |
|
ctor [Wp.LogicBuiltins] |
|
cval [CodeSemantics.Make] |
|
cval [Wp.CodeSemantics.Make] |
|
cvar [Memory.Model] |
Return the location of a C variable
|
cvar [Wp.Memory.Model] |
Return the location of a C variable
|
D |
datatype [MemVar.VarUsage] |
|
datatype [Memory.Model] |
for projectification
|
datatype [Lang] |
|
datatype [Wp.MemVar.VarUsage] |
|
datatype [Wp.Memory.Model] |
for projectification
|
datatype [Wp.Lang] |
|
debugp [Lang.F] |
|
debugp [Wp.Lang.F] |
|
default [Factory] |
"Var,Typed,Nat,Real" memory model.
|
default [Wp.Factory] |
"Var,Typed,Nat,Real" memory model.
|
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.
|
degree_of_type [VarUsage] |
Dimensions in the type (0 for non-array)
|
degree_of_type [VarUsageRef] |
Dimensions in the type (0 for non-array)
|
delete_script [Proof] |
|
denv [Matrix] |
|
dependencies [LogicBuiltins] |
Of external theories.
|
dependencies [WpAnnot] |
|
dependencies [Wp.LogicBuiltins] |
Of external theories.
|
descr [Factory] |
|
descr [Vset] |
|
descr [LogicBuiltins] |
|
descr [Wp.Factory] |
|
descr [Wp.Vset] |
|
descr [Wp.LogicBuiltins] |
|
detect_provers [ProverWhy3] |
|
detect_why3 [ProverWhy3] |
|
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 "-wp-out" directory
|
directory [Wp.Model] |
Current model in "-wp-out" directory
|
disjoint [Region] |
|
disjoint [Vset] |
|
disjoint [Wp.Vset] |
|
dispatch_cvar [Variables_analysis] |
dispatch_cvar v returns the var_kind associated to the C variable v
according the current optimisations activated.
|
dispatch_lvar [Variables_analysis] |
dispatch_lvar v returns the var_kind associated to the logic variable v
according the current optimisations activated.
|
do_checks [Lang.F] |
|
do_checks [Wp.Lang.F] |
|
do_list_scheduled [Register] |
|
do_list_scheduled_result [Register] |
|
do_prover_detect [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_prover [Register] |
|
do_wpo_result [Register] |
|
do_wpo_start [Register] |
|
do_wpo_stat [Register] |
|
do_wpo_success [Register] |
|
do_wpo_wait [Register] |
|
domain [LogicAssigns.Make] |
|
domain [Memory.Model] |
Give the set of chunk where an object of the given type at the
given location is stored.
|
domain [Memory.Sigma] |
|
domain [Conditions] |
|
domain [Letify.Defs] |
|
domain [Letify.Sigma] |
|
domain [Wp.Memory.Model] |
Give the set of chunk where an object of the given type at the
given location is stored.
|
domain [Wp.Memory.Sigma] |
|
domain [Wp.Conditions] |
|
driver [LogicBuiltins] |
|
driver [Wp.LogicBuiltins] |
|
dummy [Wpo.GOAL] |
|
dump [LogicBuiltins] |
|
dump [Pcond] |
|
dump [RefUsage] |
|
dump [VarUsage] |
|
dump [VarUsageRef] |
|
dump [LogicUsage] |
Print on output
|
dump [Wp.LogicBuiltins] |
|
dump [Wp.RefUsage] |
|
dump [Wp.LogicUsage] |
Print on output
|
dump_scripts [Proof] |
dump_scripts f saves all scripts from the database into file f .
|
E |
e_apply [Letify.Sigma] |
|
e_bigint [Lang.F] |
|
e_bigint [Wp.Lang.F] |
|
e_fact [Lang.F] |
|
e_fact [Wp.Lang.F] |
|
e_hexfloat [Lang.F] |
|
e_hexfloat [Wp.Lang.F] |
|
e_int64 [Lang.F] |
|
e_int64 [Wp.Lang.F] |
|
e_minus_one [Lang.F] |
|
e_minus_one [Wp.Lang.F] |
|
e_mthfloat [Lang.F] |
|
e_mthfloat [Wp.Lang.F] |
|
e_one [Lang.F] |
|
e_one [Wp.Lang.F] |
|
e_one_real [Lang.F] |
|
e_one_real [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_setfield [Lang.F] |
|
e_setfield [Wp.Lang.F] |
|
e_subst [Lang.F] |
|
e_subst [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] |
|
eat [Script] |
|
edge_dst [Cil2cfg] |
|
edge_src [Cil2cfg] |
node and edges relations
|
either [Conditions] |
|
either [Wp.Conditions] |
|
emit [Warning] |
Emit a warning in current context.
|
emit [Wp.Warning] |
Emit a warning in current context.
|
empty [Region] |
|
empty [Vset] |
|
empty [Conditions] |
|
empty [Letify.Defs] |
|
empty [Letify.Sigma] |
|
empty [Splitter] |
|
empty [Passive] |
|
empty [Mcfg.S] |
|
empty [Map.S] |
The empty map.
|
empty [Wp.Passive] |
|
empty [Wp.Vset] |
|
empty [Wp.Conditions] |
|
empty [Wp.Splitter] |
|
empty [Wp.Mcfg.S] |
|
empty [FCMap.S] |
The empty map.
|
empty_acc [WpStrategy] |
|
empty_assigns_info [WpPropId] |
|
empty_assigns_info [Wp.WpPropId] |
|
end_session [Register] |
|
env [Lang.F] |
|
env [Wp.Lang.F] |
|
env_at [LogicCompiler.Make] |
|
env_at [Wp.LogicCompiler.Make] |
|
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] |
|
epred [Lang.F] |
|
epred [Wp.Lang.F] |
|
epsilon [Lang] |
|
epsilon [Rformat] |
|
epsilon [Wp.Lang] |
|
eqp [Lang.F] |
|
eqp [Wp.Lang.F] |
|
equal [Vset] |
|
equal [Letify.Sigma] |
|
equal [Clabels] |
|
equal [Ctypes.AinfoComparable] |
|
equal [Ctypes] |
|
equal [Map.S] |
equal cmp m1 m2 tests whether the maps m1 and m2 are
equal, that is, contain equal keys and associate them with
equal data.
|
equal [Wp.Vset] |
|
equal [FCMap.S] |
equal cmp m1 m2 tests whether the maps m1 and m2 are
equal, that is, contain equal keys and associate them with
equal data.
|
equal [Wp.Clabels] |
|
equal [Wp.Ctypes.AinfoComparable] |
|
equal [Wp.Ctypes] |
|
equal_array [Cvalues] |
|
equal_but [Region] |
|
equal_comp [Cvalues] |
|
equal_obj [LogicAssigns.Code] |
|
equal_obj [CodeSemantics.Make] |
|
equal_obj [Wp.CodeSemantics.Make] |
|
equal_object [Cvalues] |
|
equal_typ [CodeSemantics.Make] |
|
equal_typ [Wp.CodeSemantics.Make] |
|
error [Script] |
|
error [Warning] |
|
error [Wp.Warning] |
|
exercised [Register] |
|
exists [Splitter] |
|
exists [Parameter_sig.Set] |
Is there some element satisfying the given predicate?
|
exists [Map.S] |
exists p m checks if at least one binding of the map
satisfy the predicate p .
|
exists [Wp.Splitter] |
|
exists [FCMap.S] |
exists p m checks if at least one binding of the map
satisfy the predicate p .
|
exp [CodeSemantics.Make] |
|
exp [Wp.CodeSemantics.Make] |
|
export [WpReport] |
|
export_decl [Mcfg.Export] |
|
export_decl [Wp.Mcfg.Export] |
|
export_goal [Mcfg.Export] |
|
export_goal [Wp.Mcfg.Export] |
|
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_concat [Vlist] |
|
f_convert [Ctypes] |
|
f_convert [Wp.Ctypes] |
|
f_delta [Cfloat] |
|
f_delta [Wp.Cfloat] |
|
f_epsilon [Cfloat] |
|
f_epsilon [Wp.Cfloat] |
|
f_iabs [Cfloat] |
|
f_iabs [Wp.Cfloat] |
|
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_model [Cfloat] |
|
f_model [Wp.Cfloat] |
|
f_rabs [Cfloat] |
|
f_rabs [Wp.Cfloat] |
|
f_sqrt [Cfloat] |
|
f_sqrt [Wp.Cfloat] |
|
fadd [Cfloat] |
|
fadd [Wp.Cfloat] |
|
failed [VCS] |
|
failed [Wp.VCS] |
|
farray [Lang] |
|
farray [Wp.Lang] |
|
fconvert [Cfloat] |
|
fconvert [Wp.Cfloat] |
|
fcstat [WpReport] |
|
fdiv [Cfloat] |
|
fdiv [Wp.Cfloat] |
|
field [Memory.Model] |
Return the memory location obtained by field access from a given
memory location
|
field [Cvalues.Logic] |
|
field [Lang] |
|
field [Wp.Memory.Model] |
Return the memory location obtained by field access from a given
memory location
|
field [Wp.Lang] |
|
field_id [Lang] |
|
field_id [Wp.Lang] |
|
field_offset [Ctypes] |
|
field_offset [Wp.Ctypes] |
|
fields_of_field [Lang] |
|
fields_of_field [Wp.Lang] |
|
fields_of_tau [Lang] |
|
fields_of_tau [Wp.Lang] |
|
file_goal [Wpo.DISK] |
|
file_kf [Wpo.DISK] |
|
file_logerr [Wpo.DISK] |
|
file_logout [Wpo.DISK] |
|
filename_for_prover [VCS] |
|
filename_for_prover [Wp.VCS] |
|
filter [Script] |
|
filter [Conditions] |
|
filter [Splitter] |
|
filter [Map.S] |
filter p m returns the map with all the bindings in m
that satisfy predicate p .
|
filter [Wp.Conditions] |
|
filter [Wp.Splitter] |
|
filter [FCMap.S] |
filter p m returns the map with all the bindings in m
that satisfy predicate p .
|
filter_pred [Cleaning] |
|
filter_status [WpAnnot] |
|
filter_type [Cleaning] |
|
find [ProverWhy3] |
|
find [Letify.Sigma] |
|
find [Model.Registry] |
|
find [Model] |
|
find [Cil2cfg.HEsig] |
|
find [Map.S] |
find x m returns the current binding of x in m ,
or raises Not_found if no such binding exists.
|
find [Wp.Model.Registry] |
|
find [Wp.Model] |
|
find [FCMap.S] |
find x m returns the current binding of x in m ,
or raises Not_found if no such binding exists.
|
find_all [Cil2cfg.HEsig] |
|
find_lemma [Definitions] |
raises Not_found
|
find_lemma [Wp.Definitions] |
raises Not_found
|
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_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.
|
float_of_int [Cfloat] |
|
float_of_int [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] |
|
flt_sqrt [Cfloat] |
|
flt_sqrt [Wp.Cfloat] |
|
flush [Warning] |
|
flush [Wp.Warning] |
|
fmemo [Ctypes] |
|
fmemo [Wp.Ctypes] |
|
fmul [Cfloat] |
|
fmul [Wp.Cfloat] |
|
fold [Splitter] |
|
fold [Map.S] |
fold f m a computes (f kN dN ... (f k1 d1 a)...) ,
where k1 ... kN are the keys of all bindings in m
(in increasing order), and d1 ... dN are the associated data.
|
fold [Wp.Splitter] |
|
fold [FCMap.S] |
fold f m a computes (f kN dN ... (f k1 d1 a)...) ,
where k1 ... kN are the keys of all bindings in m
(in increasing order), and d1 ... dN are the associated data.
|
fold_bhv_post_cond [WpStrategy] |
apply f_normal on the Normal postconditions,
f_exits on the Exits postconditions, and warn on the others.
|
fold_nodes [Cil2cfg] |
iterators
|
fopp [Cfloat] |
|
fopp [Wp.Cfloat] |
|
for_all [Splitter] |
|
for_all [Map.S] |
for_all p m checks if all the bindings of the map
satisfy the predicate p .
|
for_all [Wp.Splitter] |
|
for_all [FCMap.S] |
for_all p m checks if all the bindings of the map
satisfy the predicate p .
|
formal [LogicCompiler.Make] |
|
formal [Wp.LogicCompiler.Make] |
|
frame [LogicSemantics.Make] |
|
frame [LogicCompiler.Make] |
|
frame [Wp.LogicSemantics.Make] |
|
frame [Wp.LogicCompiler.Make] |
|
frange [Cfloat] |
|
frange [Wp.Cfloat] |
|
free [Context] |
Performs the job with local context cleared.
|
free [Wp.Context] |
Performs the job with local context cleared.
|
freshen [Lang] |
|
freshen [Wp.Lang] |
|
freshvar [Lang] |
|
freshvar [Wp.Lang] |
|
from_file [Why3_xml] |
returns the list of XML elements from the given file.
|
fsub [Cfloat] |
|
fsub [Wp.Cfloat] |
|
full [Region] |
|
G |
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 [Memory.Sigma] |
|
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.Memory.Sigma] |
|
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_asgn_goal [WpStrategy] |
|
get_asgn_hyp [WpStrategy] |
|
get_bhv [WpStrategy] |
|
get_both_hyp_goals [WpStrategy] |
|
get_call_asgn [WpStrategy] |
|
get_call_hyp [WpStrategy] |
To be used as hypotheses arround a call, (the pre are in
get_call_pre_goal )
|
get_call_out_edges [Cil2cfg] |
similar to succ_e g v
but gives the edge to VcallOut first and the edge to Vexit second.
|
get_call_pre [WpStrategy] |
Preconditions of a called function to be considered as hyp and goal
(similar to get_both_hyp_goals ).
|
get_call_pre_strategies [WpAnnot] |
|
get_call_type [Cil2cfg] |
|
get_called_assigns [WpAnnot] |
Properties for assigns of kf
|
get_called_exit_conditions [WpAnnot] |
|
get_called_post_conditions [WpAnnot] |
|
get_called_preconditions_at [WpAnnot] |
|
get_cut [WpStrategy] |
the bool in get_cut results says if the property has to be
considered as a both goal and hyp (goal=true , or hyp only (goal=false )
|
get_descr [Wpo.GOAL] |
|
get_descr [Model] |
|
get_descr [Wp.Model] |
|
get_description [VC] |
|
get_description [Wp.VC] |
|
get_edge_labels [Cil2cfg] |
|
get_edge_next_stmt [Cil2cfg] |
|
get_emitter [Model] |
|
get_emitter [Wp.Model] |
|
get_env [Wp_parameters] |
|
get_exit_edges [Cil2cfg] |
Find the edges e that goes to the Vexit node inside the statement
begining at node n
|
get_file_logerr [Wpo] |
only filename, might not exists
|
get_file_logout [Wpo] |
only filename, might not exists
|
get_files [Wpo] |
|
get_formula [VC] |
|
get_formula [Wp.VC] |
|
get_frame [LogicSemantics.Make] |
|
get_frame [LogicCompiler.Make] |
|
get_frame [Wp.LogicSemantics.Make] |
|
get_frame [Wp.LogicCompiler.Make] |
|
get_function_name [Parameter_sig.String] |
|
get_function_strategies [WpAnnot] |
|
get_gamma [Lang] |
|
get_gamma [Wp.Lang] |
|
get_gid [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_index [Wpo] |
|
get_induction [WpPropId] |
Quite don't understand what is going on here...
|
get_induction [Wp.WpPropId] |
|
get_induction_labels [LogicUsage] |
Given an inductive phi{...A...} .
|
get_induction_labels [Wp.LogicUsage] |
Given an inductive phi{...A...} .
|
get_int [Ctypes] |
|
get_int [Wp.Ctypes] |
|
get_internal_edges [Cil2cfg] |
Find the edges e of the statement node n postcondition
and the set of edges that are inside the statement (e excluded).
|
get_kf [WpStrategy] |
|
get_label [Wpo] |
|
get_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.VC] |
|
get_model [Wp.Model] |
Current model
|
get_model_id [Wpo] |
|
get_model_name [Wpo] |
|
get_name [LogicUsage] |
|
get_name [Wp.LogicUsage] |
|
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_dir [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_logic_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_property [VC] |
|
get_property [Wpo] |
Dynamically exported
|
get_property [Wp.VC] |
|
get_propid [WpPropId] |
Unique identifier of prop_id
|
get_propid [Wp.WpPropId] |
Unique identifier of prop_id
|
get_prover_names [Register] |
|
get_pstat [Register] |
|
get_range [Parameter_sig.Int] |
What is the possible range of values for this parameter.
|
get_result [VC] |
|
get_result [Wpo] |
Dynamically exported.
|
get_result [Wp.VC] |
|
get_results [VC] |
|
get_results [Wpo] |
|
get_results [Wp.VC] |
|
get_scope [Model] |
|
get_scope [Wp.Model] |
|
get_separation [Model] |
|
get_separation [Wp.Model] |
|
get_steps [Wpo] |
|
get_switch_edges [Cil2cfg] |
similar to succ_e g v
but give the switch cases and the default edge
|
get_test_edges [Cil2cfg] |
similar to succ_e g v
but tests the branch to return (then-edge, else-edge)
|
get_time [Wpo] |
|
get_time [Rformat] |
get_time T t returns k such that T[k-1] <= t <= T[k] ,
T is extended with T[-1]=0 and T[N]=+oo .
|
get_variables [Lang] |
|
get_variables [Wp.Lang] |
|
global [Memory.Model] |
Given a pointer value p , assumes this pointer p (when valid)
is allocated outside the function frame under analysis.
|
global [Wp.Memory.Model] |
Given a pointer value p , assumes this pointer p (when valid)
is allocated outside the function frame under analysis.
|
global_axioms [WpStrategy] |
|
goals_of_property [Wpo] |
All POs related to a given property.
|
group [Splitter] |
|
group [Wp.Splitter] |
|
guards [LogicSemantics.Make] |
|
guards [LogicCompiler.Make] |
|
guards [Wp.LogicSemantics.Make] |
|
guards [Wp.LogicCompiler.Make] |
|
H |
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_exit [Cil2cfg] |
wether an exit edge exists or not
|
has_init [Mcfg.S] |
|
has_init [Wp.Mcfg.S] |
|
has_ltype [Cvalues] |
|
hash [Memory.Chunk] |
|
hash [Ctypes.AinfoComparable] |
|
hash [Ctypes] |
|
hash [Wp.Memory.Chunk] |
|
hash [Wp.Ctypes.AinfoComparable] |
|
hash [Wp.Ctypes] |
|
havoc [Memory.Sigma] |
|
havoc [Wp.Memory.Sigma] |
|
havoc_any [Memory.Sigma] |
|
havoc_any [Wp.Memory.Sigma] |
|
havoc_chunk [Memory.Sigma] |
|
havoc_chunk [Wp.Memory.Sigma] |
|
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] |
|
iadd [Cint] |
|
iadd [Wp.Cint] |
|
iconvert [Cint] |
|
iconvert [Wp.Cint] |
|
id [LogicBuiltins] |
|
id [Matrix] |
unique w.r.t equal
|
id [Wp.LogicBuiltins] |
|
ident [Factory] |
|
ident [Script] |
|
ident [Wp.Factory] |
|
idents [Script] |
|
idiv [Cint] |
|
idiv [Wp.Cint] |
|
idp [Lang.F] |
|
idp [Wp.Lang.F] |
|
if_else [Splitter] |
|
if_else [Wp.Splitter] |
|
if_then [Splitter] |
|
if_then [Wp.Splitter] |
|
imemo [Ctypes] |
|
imemo [Wp.Ctypes] |
|
imod [Cint] |
|
imod [Wp.Cint] |
|
imul [Cint] |
|
imul [Wp.Cint] |
|
in_frame [LogicSemantics.Make] |
|
in_frame [LogicCompiler.Make] |
|
in_frame [Wp.LogicSemantics.Make] |
|
in_frame [Wp.LogicCompiler.Make] |
|
in_range [Vset] |
|
in_range [Wp.Vset] |
|
in_size [Vset] |
|
in_size [Wp.Vset] |
|
included [LogicSemantics.Make] |
|
included [Memory.Model] |
Return the formula that tests if two segment are included
|
included [Cvalues.Logic] |
|
included [Wp.LogicSemantics.Make] |
|
included [Wp.Memory.Model] |
Return the formula that tests if two segment are included
|
incr [Parameter_sig.Int] |
Increment the integer.
|
infoprover [Lang] |
same information for all the provers
|
infoprover [Wp.Lang] |
same information for all the provers
|
init [LogicBuiltins] |
Reset the context to a newly created driver
|
init [Wp.LogicBuiltins] |
Reset the context to a newly created driver
|
init_const [Mcfg.S] |
the (entire) variable has its initial value
|
init_const [Wp.Mcfg.S] |
the (entire) variable has its initial value
|
init_range [Mcfg.S] |
init_range env lv t_elt a b wp :
put default values of type t_elt in lvk with a <= k < b
|
init_range [Wp.Mcfg.S] |
init_range env lv t_elt a b wp :
put default values of type t_elt in lvk with a <= k < b
|
init_value [Mcfg.S] |
init_value env lv t v_opt wp:
put value of type t (or default if None) in lv
|
init_value [Wp.Mcfg.S] |
init_value env lv t v_opt wp:
put value of type t (or default if None) in lv
|
instance [Factory] |
|
instance [Wp.Factory] |
|
instance_of [CodeSemantics.Make] |
|
instance_of [Wp.CodeSemantics.Make] |
|
int_of_loc [Memory.Model] |
Cast a memory location into an integer of the given type
|
int_of_loc [Wp.Memory.Model] |
Cast a memory location into an integer of the given type
|
inter [Cvalues.Logic] |
|
inter [Vset] |
|
inter [Wp.Vset] |
|
intersect [Conditions] |
|
intersect [Lang.F] |
|
intersect [Wp.Conditions] |
|
intersect [Wp.Lang.F] |
|
intersectp [Lang.F] |
|
intersectp [Wp.Lang.F] |
|
intros [Conditions] |
|
intros [Wp.Conditions] |
|
invalid [VCS] |
|
invalid [Wp.VCS] |
|
iopp [Cint] |
|
iopp [Wp.Cint] |
|
ip_lemma [LogicUsage] |
|
ip_lemma [Wp.LogicUsage] |
|
irange [Cint] |
|
irange [Wp.Cint] |
|
isGlobalInitConst [WpStrategy] |
True if the variable is global, not extern, with a "const" qualifier type.
|
isInitConst [WpStrategy] |
True if both options -const-readonly and -wp-init are positionned,
and the variable is global, not extern, with a "const" type
(see hasConstAttribute ).
|
is_assigns [WpPropId] |
|
is_assigns [Wp.WpPropId] |
|
is_back_edge [Cil2cfg] |
|
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.WpPropId] |
|
is_cint [Cint] |
Raises Not_found if not.
|
is_cint [Wp.Cint] |
Raises Not_found if not.
|
is_cint_simplifier [Cint] |
Remove the is_cint in formulas that are
redondant with other conditions.
|
is_cint_simplifier [Wp.Cint] |
Remove the is_cint in formulas that are
redondant with other conditions.
|
is_composed [WpAnnot] |
whether a proof needs several lemma to be complete
|
is_default [LogicBuiltins] |
|
is_default [Wp.LogicBuiltins] |
|
is_default_behavior [WpStrategy] |
|
is_empty [Proof] |
|
is_empty [Conditions] |
|
is_empty [Map.S] |
Test whether a map is empty or not.
|
is_empty [Wp.Conditions] |
|
is_empty [FCMap.S] |
Test whether a map is empty or not.
|
is_equal [Lang.F] |
|
is_equal [Wp.Lang.F] |
|
is_exp_range [CodeSemantics.Make] |
|
is_exp_range [Wp.CodeSemantics.Make] |
|
is_false [Cvalues] |
p ? 0 : 1
|
is_framed [Memory.Chunk] |
Whether the Chunk is local to a function.
|
is_framed [Wp.Memory.Chunk] |
Whether the Chunk is local to a function.
|
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_null [Memory.Model] |
Return the formula that check if a given location is null
|
is_null [Cvalues] |
|
is_null [Wp.Memory.Model] |
Return the formula that check if a given location is null
|
is_object [Cvalues] |
|
is_out [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_proved [WpAnnot] |
wether all partial proofs have been accumulated or not
|
is_ptrue [Lang.F] |
|
is_ptrue [Wp.Lang.F] |
|
is_recursive [LogicUsage] |
|
is_recursive [Wp.LogicUsage] |
|
is_requires [WpPropId] |
|
is_requires [Wp.WpPropId] |
|
is_to_scope [Variables_analysis] |
is_to_scope v returns true if v has to been scoped into the inner
memory model : cvar of ref
|
is_trivial [VC] |
|
is_trivial [Wpo.VC_Annot] |
|
is_trivial [Wpo.VC_Lemma] |
|
is_trivial [Wpo.GOAL] |
|
is_trivial [Wpo] |
|
is_trivial [Wp.VC] |
|
is_true [Cvalues] |
p ? 1 : 0
|
is_true [Separation] |
Returns true if the clause is degenerated.
|
is_true [Wp.Separation] |
Returns true if the clause is degenerated.
|
is_user_formal_in_builtin [Variables_analysis] |
is_user_formal_in_builtins lv tests if the address
of the by-reference formal lv of user definition is an argument
of (one or more) ACSL builtin predicate(s) or function :
valid and family, separated, block_length, initialized
|
is_valid [Wpo] |
true if the result is valid.
|
is_verdict [VCS] |
|
is_verdict [Wp.VCS] |
|
is_void [Ctypes] |
|
is_void [Wp.Ctypes] |
|
is_zero [CodeSemantics.Make] |
|
is_zero [Lang.F] |
|
is_zero [Wp.CodeSemantics.Make] |
|
is_zero [Wp.Lang.F] |
|
isub [Cint] |
|
isub [Wp.Cint] |
|
iter [Wpo] |
|
iter [Memory.Sigma] |
|
iter [Definitions] |
|
iter [Conditions] |
|
iter [Letify.Sigma] |
|
iter [Splitter] |
|
iter [Lang.Alpha] |
|
iter [Model.Registry] |
|
iter [Model] |
|
iter [RefUsage] |
|
iter [Map.S] |
iter f m applies f to all bindings in map m .
|
iter [Wp.Memory.Sigma] |
|
iter [Wp.Conditions] |
|
iter [Wp.Definitions] |
|
iter [Wp.Splitter] |
|
iter [Wp.Lang.Alpha] |
|
iter [Wp.Model.Registry] |
|
iter [Wp.Model] |
|
iter [Wp.RefUsage] |
|
iter [FCMap.S] |
iter f m applies f to all bindings in map m .
|
iter2 [Memory.Sigma] |
|
iter2 [Wp.Memory.Sigma] |
|
iter_checks [Lang.F] |
|
iter_checks [Wp.Lang.F] |
|
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_session [Register] |
|
iter_sorted [Model.Registry] |
|
iter_sorted [Wp.Model.Registry] |
|
iteri [Conditions] |
|
iteri [Wp.Conditions] |
|
J |
job [Wp_parameters] |
|
job_key [Register] |
|
join [Memory.Sigma] |
pairwise equal
|
join [Passive] |
|
join [Wp.Memory.Sigma] |
pairwise equal
|
join [Wp.Passive] |
|
K |
key [Script] |
|
kf_context [Wpo] |
|
kfailed [VCS] |
|
kfailed [Wp.VCS] |
|
kind_of_id [WpPropId] |
get the 'kind' information.
|
kind_of_id [Wp.WpPropId] |
get the 'kind' information.
|
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] |
|
ldomain [Cvalues] |
|
lemma [LogicSemantics.Make] |
|
lemma [LogicCompiler.Make] |
|
lemma [Wp.LogicSemantics.Make] |
|
lemma [Wp.LogicCompiler.Make] |
|
lemma_id [Lang] |
|
lemma_id [Wp.Lang] |
|
length [Splitter] |
|
length [Wp.Splitter] |
|
letify [Conditions] |
|
letify [Wp.Conditions] |
|
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] |
|
literal [Memory.Model] |
Return the memory location of a constant string,
the id is a unique identifier.
|
literal [Wp.Memory.Model] |
Return the memory location of a constant string,
the id is a unique identifier.
|
load [Memory.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.Memory.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.
|
loadscripts [Proof] |
Load scripts from -wp-script f .
|
loc [Cvalues.Logic] |
|
loc [Splitter] |
|
loc [Wp.Splitter] |
|
loc_diff [Memory.Model] |
Compute the length in bytes between two memory locations
|
loc_diff [Wp.Memory.Model] |
Compute the length in bytes between two memory locations
|
loc_eq [Memory.Model] |
|
loc_eq [Wp.Memory.Model] |
|
loc_leq [Memory.Model] |
Memory location comparisons
|
loc_leq [Wp.Memory.Model] |
Memory location comparisons
|
loc_lt [Memory.Model] |
|
loc_lt [Wp.Memory.Model] |
|
loc_neq [Memory.Model] |
|
loc_neq [Wp.Memory.Model] |
|
loc_of_exp [CodeSemantics.Make] |
|
loc_of_exp [Wp.CodeSemantics.Make] |
|
loc_of_int [Memory.Model] |
Cast a term representing a pointer to a c_object into a memory
location
|
loc_of_int [Wp.Memory.Model] |
Cast a term representing a pointer to a c_object into a memory
location
|
loc_of_term [LogicSemantics.Make] |
|
loc_of_term [Wp.LogicSemantics.Make] |
|
local [Lang] |
|
local [Wp.Lang] |
|
location [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 [Clabels] |
lookup bindings lparam retrieves the actual label
for the label in bindings for label parameter lparam .
|
lookup [Wp.Clabels] |
lookup bindings lparam retrieves the actual label
for the label in bindings for label parameter lparam .
|
lookup_name [Clabels] |
|
lookup_name [Wp.Clabels] |
|
loop_entry [Mcfg.S] |
|
loop_entry [Wp.Mcfg.S] |
|
loop_head_label [Clabels] |
|
loop_head_label [Wp.Clabels] |
|
loop_step [Mcfg.S] |
|
loop_step [Wp.Mcfg.S] |
|
lval [CodeSemantics.Make] |
|
lval [Wp.CodeSemantics.Make] |
|
M |
main [Register] |
|
make [GuiNavigator] |
|
make [Wpo.GOAL] |
|
make_output_dir [Wp_parameters] |
|
make_type [Datatype.Hashtbl] |
|
map [Cvalues.Logic] |
|
map [Vset] |
|
map [Splitter] |
|
map [Map.S] |
map f m returns a map with same domain as m , where the
associated value a of all bindings of m has been
replaced by the result of the application of f to a .
|
map [Wp.Vset] |
|
map [Wp.Splitter] |
|
map [FCMap.S] |
map f m returns a map with same domain as m , where the
associated value a of all bindings of m has been
replaced by the result of the application of f to a .
|
map_l2t [Cvalues.Logic] |
|
map_loc [Cvalues.Logic] |
|
map_logic [Cvalues] |
|
map_opp [Cvalues.Logic] |
|
map_opp [Vset] |
|
map_opp [Wp.Vset] |
|
map_sloc [Cvalues] |
|
map_t2l [Cvalues.Logic] |
|
map_value [Cvalues] |
|
mapi [Map.S] |
Same as Map.S.map , but the function receives as arguments both the
key and the associated value for each binding of the map.
|
mapi [FCMap.S] |
Same as FCMap.S.map , but the function receives as arguments both the
key and the associated value for each binding of the map.
|
mark [Splitter] |
|
mark [Wp.Splitter] |
|
mark_e [Lang.F] |
|
mark_e [Wp.Lang.F] |
|
mark_p [Lang.F] |
|
mark_p [Wp.Lang.F] |
|
marker [Lang.F] |
|
marker [Wp.Lang.F] |
|
matrix [Definitions] |
|
matrix [Wp.Definitions] |
|
max_binding [Map.S] |
|
max_binding [FCMap.S] |
|
max_elt [FCSet.S] |
Same as , but returns the largest element of the
given set.
|
mem [Memory.Sigma] |
|
mem [Model.Registry] |
|
mem [Parameter_sig.Set] |
Does the given element belong to the set?
|
mem [Wprop.Indexed2] |
|
mem [Wprop.Indexed] |
|
mem [Map.S] |
mem x m returns true if m contains a binding for x ,
and false otherwise.
|
mem [Wp.Memory.Sigma] |
|
mem [Wp.Model.Registry] |
|
mem [FCMap.S] |
mem x m returns true if m contains a binding for x ,
and false otherwise.
|
mem_at [LogicSemantics.Make] |
|
mem_at [LogicCompiler.Make] |
|
mem_at [Wp.LogicSemantics.Make] |
|
mem_at [Wp.LogicCompiler.Make] |
|
mem_at_frame [LogicSemantics.Make] |
|
mem_at_frame [LogicCompiler.Make] |
|
mem_at_frame [Wp.LogicSemantics.Make] |
|
mem_at_frame [Wp.LogicCompiler.Make] |
|
mem_frame [LogicSemantics.Make] |
|
mem_frame [LogicCompiler.Make] |
|
mem_frame [Wp.LogicSemantics.Make] |
|
mem_frame [Wp.LogicCompiler.Make] |
|
member [Vset] |
|
member [Wp.Vset] |
|
memo [Datatype.Hashtbl] |
memo tbl k f returns the binding of k in tbl .
|
memoize [Model.Registry] |
with circularity protection
|
memoize [Wp.Model.Registry] |
with circularity protection
|
memory [Factory] |
|
memory [Wp.Factory] |
|
merge [Memory.Sigma] |
|
merge [Region] |
|
merge [Conditions] |
|
merge [Letify.Defs] |
|
merge [Splitter] |
|
merge [Matrix] |
|
merge [Mcfg.S] |
|
merge [Ctypes] |
|
merge [Map.S] |
merge f m1 m2 computes a map whose keys is a subset of keys of m1
and of m2 .
|
merge [Wp.Memory.Sigma] |
|
merge [Wp.Conditions] |
|
merge [Wp.Splitter] |
|
merge [Wp.Mcfg.S] |
|
merge [FCMap.S] |
merge f m1 m2 computes a map whose keys is a subset of keys of m1
and of m2 .
|
merge [Wp.Ctypes] |
|
merge_all [Splitter] |
|
merge_all [Wp.Splitter] |
|
merge_assign_info [WpPropId] |
|
merge_assign_info [Wp.WpPropId] |
|
min_binding [Map.S] |
Return the smallest binding of the given map
(with respect to the Ord.compare ordering), or raise
Not_found if the map is empty.
|
min_binding [FCMap.S] |
Return the smallest binding of the given map
(with respect to the Ord.compare ordering), or raise
Not_found if the map is empty.
|
min_elt [FCSet.S] |
Return the smallest element of the given set
(with respect to the Ord.compare ordering), or raise
Not_found if the set is empty.
|
missing_rte [WpAnnot] |
|
mk_asm_assigns_desc [WpPropId] |
|
mk_asm_assigns_desc [Wp.WpPropId] |
|
mk_assert_id [WpPropId] |
|
mk_assert_id [Wp.WpPropId] |
|
mk_assigns_info [WpPropId] |
|
mk_assigns_info [Wp.WpPropId] |
|
mk_axiom_info [WpPropId] |
|
mk_axiom_info [Wp.WpPropId] |
|
mk_bhv_from_id [WpPropId] |
\from property of function or statement behavior assigns.
|
mk_bhv_from_id [Wp.WpPropId] |
\from property of function or statement behavior assigns.
|
mk_call_pre_id [WpPropId] |
mk_call_pre_id called_kf s_call called_pre
|
mk_call_pre_id [Wp.WpPropId] |
mk_call_pre_id called_kf s_call called_pre
|
mk_check [WpPropId] |
|
mk_check [Wp.WpPropId] |
|
mk_code_annot_ids [WpPropId] |
|
mk_code_annot_ids [Wp.WpPropId] |
|
mk_compl_bhv_id [WpPropId] |
complete behaviors property.
|
mk_compl_bhv_id [Wp.WpPropId] |
complete behaviors property.
|
mk_decrease_id [WpPropId] |
|
mk_decrease_id [Wp.WpPropId] |
|
mk_disj_bhv_id [WpPropId] |
disjoint behaviors property.
|
mk_disj_bhv_id [Wp.WpPropId] |
disjoint behaviors property.
|
mk_establish_id [WpPropId] |
Invariant establishment
|
mk_establish_id [Wp.WpPropId] |
Invariant establishment
|
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_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_logic_label [Clabels] |
create a virtual label to a statement (it can have no label)
|
mk_logic_label [Wp.Clabels] |
create a virtual label to a statement (it can have no label)
|
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_label [Clabels] |
|
mk_loop_label [Wp.Clabels] |
|
mk_part [WpPropId] |
mk_part pid (k, n) build the identification for the k/n part of pid .
|
mk_part [Wp.WpPropId] |
mk_part pid (k, n) build the identification for the k/n part of pid .
|
mk_pre_id [WpPropId] |
|
mk_pre_id [Wp.WpPropId] |
|
mk_pred_info [WpPropId] |
|
mk_pred_info [Wp.WpPropId] |
|
mk_preserve_id [WpPropId] |
Invariant preservation
|
mk_preserve_id [Wp.WpPropId] |
Invariant preservation
|
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_label [Clabels] |
|
mk_stmt_label [Wp.Clabels] |
|
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 [LogicSemantics.Make] |
|
move [LogicCompiler.Make] |
|
move [Wp.LogicSemantics.Make] |
|
move [Wp.LogicCompiler.Make] |
|
N |
name [Model.Data] |
|
name [Model.Entries] |
|
name [Context] |
|
name [Wp_error] |
|
name [Wp.Model.Data] |
|
name [Wp.Model.Entries] |
|
name [Wp.Context] |
|
name_of_mode [VCS] |
|
name_of_mode [Wp.VCS] |
|
name_of_prover [VCS] |
|
name_of_prover [Wp.VCS] |
|
natural_id [Matrix] |
name for elements in NATURAL
|
nearest_elt_ge [FCSet.S] |
nearest_elt_ge v s returns the smallest element of s that is
bigger or equal to v .
|
nearest_elt_le [FCSet.S] |
nearest_elt_le v s returns the largest element of s that is
smaller or equal to v .
|
negate [Cvalues] |
|
new_env [LogicSemantics.Make] |
|
new_env [LogicCompiler.Make] |
|
new_env [Mcfg.S] |
optionally init env with user logic variables
|
new_env [Wp.LogicSemantics.Make] |
|
new_env [Wp.LogicCompiler.Make] |
|
new_env [Wp.Mcfg.S] |
optionally init env with user logic variables
|
new_gamma [Lang] |
|
new_gamma [Wp.Lang] |
|
new_loop_computation [WpStrategy] |
|
new_pool [Lang] |
|
new_pool [Wp.Lang] |
|
nil [Conditions] |
|
nil [Wp.Conditions] |
|
no_infinite_array [Ctypes] |
|
no_infinite_array [Wp.Ctypes] |
|
no_result [VCS] |
|
no_result [Wp.VCS] |
|
node_stmt_opt [Cil2cfg] |
|
node_type [Cil2cfg] |
|
normalize [WpStrategy] |
|
not_yet_implemented [Wp_error] |
|
null [Memory.Model] |
Return the location of the null pointer
|
null [Cvalues] |
test for null pointer value
|
null [Wp.Memory.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 [LogicSemantics.Make] |
|
occurs [Memory.Model] |
Test if a location depend on a given logic variable
|
occurs [Region] |
|
occurs [Vset] |
|
occurs [Conditions] |
|
occurs [Lang.F] |
|
occurs [Wp.LogicSemantics.Make] |
|
occurs [Wp.Memory.Model] |
Test if a location depend on a given logic variable
|
occurs [Wp.Vset] |
|
occurs [Wp.Conditions] |
|
occurs [Wp.Lang.F] |
|
occursp [Lang.F] |
|
occursp [Wp.Lang.F] |
|
of_array [Matrix] |
|
of_cvar [VarUsage] |
|
of_cvar [VarUsageRef] |
|
of_formal [VarUsage] |
|
of_formal [VarUsageRef] |
|
of_lvar [VarUsage] |
|
of_lvar [VarUsageRef] |
|
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 false .
|
on [Parameter_sig.Bool] |
Set the boolean to true .
|
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_scope [Model] |
|
on_scope [Wp.Model] |
|
on_update [GuiPanel] |
|
once [Context] |
A global configure, executed once.
|
once [Wp.Context] |
A global configure, executed once.
|
open_file [Script] |
|
ordered [Vset] |
- limit : result when either parameter is None strict : if true , comparison is < instead of <=
|
ordered [Wp.Vset] |
- limit : result when either parameter is None strict : if true , comparison is < instead of <=
|
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_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_equiv [Lang.F] |
|
p_equiv [Wp.Lang.F] |
|
p_exists [Lang.F] |
|
p_exists [Wp.Lang.F] |
|
p_false [Lang.F] |
|
p_false [Wp.Lang.F] |
|
p_float [ProverTask] |
Float group pattern \([0-9.]+\)
|
p_forall [Lang.F] |
|
p_forall [Wp.Lang.F] |
|
p_group [ProverTask] |
Put pattern in group \(p\)
|
p_hyps [Lang.F] |
|
p_hyps [Wp.Lang.F] |
|
p_if [Lang.F] |
|
p_if [Wp.Lang.F] |
|
p_imply [Lang.F] |
|
p_imply [Wp.Lang.F] |
|
p_int [ProverTask] |
Int group pattern \([0-9]+\)
|
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_string [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 "\\(^ \t\n *\\)"
|
p_vars [Lang.F] |
Sorted
|
p_vars [Wp.Lang.F] |
Sorted
|
param [MemVar.VarUsage] |
|
param [Wp.MemVar.VarUsage] |
|
parameters [Lang] |
definitions
|
parameters [Wp.Lang] |
definitions
|
parse [Factory] |
Apply specifications to default setup.
|
parse [ProverWhy3] |
|
parse [Wp.Factory] |
Apply specifications to default setup.
|
parse_coqproof [Proof] |
parse_coqproof f parses a coq-file f and fetch the first proof.
|
parse_scripts [Proof] |
parse_scripts f parses all scripts from file f and put them in the database.
|
partition [Map.S] |
partition p m returns a pair of maps (m1, m2) , where
m1 contains all the bindings of s that satisfy the
predicate p , and m2 is the map with all the bindings of
s that do not satisfy p .
|
partition [FCMap.S] |
partition p m returns a pair of maps (m1, m2) , where
m1 contains all the bindings of s that satisfy the
predicate p , and m2 is the map with all the bindings of
s that do not satisfy p .
|
parts_of_id [WpPropId] |
get the 'part' infomation.
|
parts_of_id [Wp.WpPropId] |
get the 'part' infomation.
|
path [Region] |
Empty, but Full for the path
|
pointer [MemTyped] |
|
pointer [Lang] |
type of pointers
|
pointer [Wp.MemTyped] |
|
pointer [Wp.Lang] |
type of pointers
|
pointer_loc [Memory.Model] |
???
|
pointer_loc [Wp.Memory.Model] |
???
|
pointer_val [Memory.Model] |
???
|
pointer_val [Wp.Memory.Model] |
???
|
poly [Lang] |
polymorphism
|
poly [Wp.Lang] |
polymorphism
|
pool [Plang] |
|
pop [Context] |
|
pop [Wp.Context] |
|
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_bound [Vset] |
|
pp_bound [Wp.Vset] |
|
pp_call_type [Cil2cfg] |
|
pp_calls [Dyncall] |
|
pp_clause [Separation] |
Prints the separation in ACSL format.
|
pp_clause [Wp.Separation] |
Prints the separation in ACSL format.
|
pp_cluster [Definitions] |
|
pp_cluster [Wp.Definitions] |
|
pp_concat [Vlist] |
|
pp_depend [Wpo] |
|
pp_dependencies [Wpo] |
|
pp_dependency [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_float [Ctypes] |
|
pp_float [Wp.Ctypes] |
|
pp_frame [LogicSemantics.Make] |
|
pp_frame [LogicCompiler.Make] |
|
pp_frame [Wp.LogicSemantics.Make] |
|
pp_frame [Wp.LogicCompiler.Make] |
|
pp_function [Wpo] |
|
pp_goal [Wpo] |
|
pp_goal_flow [Wpo] |
|
pp_index [Wpo] |
|
pp_info_of_strategy [WpStrategy] |
|
pp_int [Ctypes] |
|
pp_int [Wp.Ctypes] |
|
pp_language [VCS] |
|
pp_language [Wp.VCS] |
|
pp_logfile [Wpo] |
|
pp_logic [LogicAssigns.Logic] |
|
pp_logic [LogicSemantics.Make] |
|
pp_logic [Wp.LogicSemantics.Make] |
|
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_pred [Lang.F] |
|
pp_pred [Wp.Lang.F] |
|
pp_pred_info [WpPropId] |
|
pp_pred_info [Wp.WpPropId] |
|
pp_pred_of_pred_info [WpPropId] |
|
pp_pred_of_pred_info [Wp.WpPropId] |
|
pp_profile [LogicUsage] |
|
pp_profile [Wp.LogicUsage] |
|
pp_propid [WpPropId] |
Print unique id of prop_id
|
pp_propid [Wp.WpPropId] |
Print unique id of prop_id
|
pp_prover [VCS] |
|
pp_prover [Wp.VCS] |
|
pp_region [LogicAssigns.Logic] |
|
pp_region [LogicSemantics.Make] |
|
pp_region [Separation] |
Prints region in ACSL format
|
pp_region [Wp.LogicSemantics.Make] |
|
pp_region [Wp.Separation] |
Prints region in ACSL format
|
pp_result [VCS] |
|
pp_result [Wp.VCS] |
|
pp_sloc [LogicAssigns.Logic] |
|
pp_sloc [LogicSemantics.Make] |
|
pp_sloc [Wp.LogicSemantics.Make] |
|
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_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_wp_parameters [Register] |
|
precondition_compute [Variables_analysis] |
precondition_compute () adds warnings and precondition suitable
to the current optimisations which are activated
|
pred [LogicSemantics.Make] |
|
pred [LogicCompiler.Make] |
|
pred [Lang.F] |
|
pred [Wp.LogicSemantics.Make] |
|
pred [Wp.LogicCompiler.Make] |
|
pred [Wp.Lang.F] |
|
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] |
|
preproc_label [NormAtLabels] |
|
preproc_label [Wp.NormAtLabels] |
|
pretty [ProverWhy3.Goal] |
|
pretty [Why3_xml] |
|
pretty [Wpo.DISK] |
|
pretty [Memory.Model] |
pretty printing of memory location
|
pretty [Memory.Sigma] |
|
pretty [Memory.Chunk] |
|
pretty [Cstring] |
|
pretty [Region] |
|
pretty [Pcond] |
|
pretty [Letify.Sigma] |
|
pretty [Splitter] |
|
pretty [Passive] |
|
pretty [Model.Key] |
|
pretty [Model.Entries] |
|
pretty [Warning] |
|
pretty [Mcfg.S] |
|
pretty [WpPropId] |
|
pretty [VarUsage] |
|
pretty [VarUsageRef] |
|
pretty [Clabels] |
|
pretty [Ctypes] |
|
pretty [Rformat] |
|
pretty [Wp.Memory.Model] |
pretty printing of memory location
|
pretty [Wp.Memory.Sigma] |
|
pretty [Wp.Memory.Chunk] |
|
pretty [Wp.Passive] |
|
pretty [Wp.Cstring] |
|
pretty [Wp.Splitter] |
|
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] |
|
print_generated [Wp_parameters] |
Debugging Categories
|
promote [Ctypes] |
|
promote [Wp.Ctypes] |
|
proof [VC] |
List of proof obligations computed for a given property.
|
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.
|
protect [Wp_error] |
|
protect_function [Wp_error] |
|
protect_map [Wp_error] |
|
protect_translation [Wp_error] |
|
protect_translation3 [Wp_error] |
|
protect_translation4 [Wp_error] |
|
protect_translation5 [Wp_error] |
|
prove [VC] |
Returns a ready-to-schedule task.
|
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.VC] |
Returns a ready-to-schedule task.
|
proved [Register] |
|
prover_of_name [Wpo] |
Dynamically exported.
|
prover_of_name [VCS] |
|
prover_of_name [Wp.VCS] |
|
provers [Register] |
|
pruning [Conditions] |
|
pruning [Wp.Conditions] |
|
push [Context] |
|
push [Wp.Context] |
|
Q |
qed_time [Wpo.GOAL] |
|
R |
range [Vset] |
|
range [Wp.Vset] |
|
rdescr [Cvalues.Logic] |
|
real_of_int [Cfloat] |
|
real_of_int [Wp.Cfloat] |
|
record [Lang] |
|
record [Wp.Lang] |
|
region [LogicSemantics.Make] |
|
region [LogicCompiler.Make] |
|
region [Wp.LogicSemantics.Make] |
|
region [Wp.LogicCompiler.Make] |
|
register [GuiPanel] |
|
register [Model] |
|
register [Wp.Model] |
|
release [Lang.F] |
|
release [Wp.Lang.F] |
|
reload [GuiPanel] |
|
remove [VC] |
|
remove [Wpo] |
|
remove [Cil2cfg.HEsig] |
|
remove [Wp.VC] |
|
remove [Map.S] |
remove x m returns a map containing the same bindings as
m , except for x which is unbound in the returned map.
|
remove [FCMap.S] |
remove x m returns a map containing the same bindings as
m , except for x which is unbound in the returned map.
|
replace [Cil2cfg.HEsig] |
|
repr [Model] |
|
repr [Wp.Model] |
|
requires [Separation] |
Filter out is_true clauses
|
requires [Wp.Separation] |
Filter out is_true clauses
|
reset [Wp_parameters] |
|
resolve [Wpo.VC_Annot] |
|
resolve [Wpo] |
|
result [VCS] |
|
result [LogicSemantics.Make] |
|
result [LogicCompiler.Make] |
|
result [Wp.VCS] |
|
result [Wp.LogicSemantics.Make] |
|
result [Wp.LogicCompiler.Make] |
|
return [LogicSemantics.Make] |
|
return [LogicCompiler.Make] |
|
return [CodeSemantics.Make] |
|
return [Mcfg.S] |
|
return [Wp.LogicSemantics.Make] |
|
return [Wp.LogicCompiler.Make] |
|
return [Wp.CodeSemantics.Make] |
|
return [Wp.Mcfg.S] |
|
rpath [Region] |
Empty, but Full for the r-paths
|
run [Register] |
|
run [ProverWhy3ide] |
|
run_and_prove [GuiPanel] |
|
S |
same_edge [Cil2cfg] |
|
same_node [Cil2cfg] |
|
savescripts [Proof] |
If necessary, dump the scripts database into the file
specified by -wp-script f .
|
scheduled [Register] |
|
scope [Memory.Model] |
Manage the scope of variables.
|
scope [Mcfg.S] |
|
scope [Wp.Memory.Model] |
Manage the scope of variables.
|
scope [Wp.Mcfg.S] |
|
script_for [Proof] |
|
script_for_ide [Proof] |
|
section [Definitions] |
|
section [Wp.Definitions] |
|
section_of_lemma [LogicUsage] |
|
section_of_lemma [Wp.LogicUsage] |
|
section_of_logic [LogicUsage] |
|
section_of_logic [Wp.LogicUsage] |
|
section_of_type [LogicUsage] |
|
section_of_type [Wp.LogicUsage] |
|
select [Letify.Split] |
|
select_by_name [WpPropId] |
test if the prop_id has to be selected for the asked name.
|
select_by_name [Wp.WpPropId] |
test if the prop_id has to be selected for the asked name.
|
select_call_pre [WpPropId] |
test if the prop_id has to be selected when we want to select the call
precondition the the stmt call (None means all the call preconditions).
|
select_call_pre [Wp.WpPropId] |
test if the prop_id has to be selected when we want to select the call
precondition the the stmt call (None means all the call preconditions).
|
self [Memory.Chunk] |
Chunk names, for pretty-printing
|
self [Wp.Memory.Chunk] |
Chunk names, for pretty-printing
|
separated [LogicSemantics.Make] |
|
separated [Memory.Model] |
Return the formula that tests if two segment are separated
|
separated [Cvalues.Logic] |
|
separated [Wp.LogicSemantics.Make] |
|
separated [Wp.Memory.Model] |
Return the formula that tests if two segment are separated
|
separation [MemVar.VarUsage] |
|
separation [Memory.Model] |
|
separation [Wp.MemVar.VarUsage] |
|
separation [Wp.Memory.Model] |
|
seq_branch [Conditions] |
|
seq_branch [Wp.Conditions] |
|
seq_list [Conditions] |
|
seq_list [Wp.Conditions] |
|
sequence [Register] |
|
sequence [Pcond] |
|
sequence [Conditions] |
|
sequence [Wp.Conditions] |
|
server [VC] |
Default number of parallel tasks is given by -wp-par command-line option.
|
server [ProverTask] |
|
server [Wp.VC] |
Default number of parallel tasks is given by -wp-par command-line option.
|
session [Register] |
|
set [Context] |
Define the current value.
|
set [Wp.Context] |
Define the current value.
|
set_builtin_1 [Lang.F] |
|
set_builtin_1 [Wp.Lang.F] |
|
set_builtin_2 [Lang.F] |
|
set_builtin_2 [Wp.Lang.F] |
|
set_builtin_eqp [Lang.F] |
|
set_builtin_eqp [Wp.Lang.F] |
|
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] |
|
severe [Warning] |
|
severe [Wp.Warning] |
|
shift [Memory.Model] |
Return the memory location obtained by array access at an index
represented by the given term .
|
shift [Cvalues.Logic] |
|
shift [Wp.Memory.Model] |
Return the memory location obtained by array access at an index
represented by the given term .
|
sigma [LogicSemantics.Make] |
|
sigma [LogicCompiler.Make] |
|
sigma [Wp.LogicSemantics.Make] |
|
sigma [Wp.LogicCompiler.Make] |
|
signed [Ctypes] |
true if signed
|
signed [Wp.Ctypes] |
true if signed
|
simplify [Mcfg.Splitter] |
|
simplify [Wp.Mcfg.Splitter] |
|
singleton [Vset] |
|
singleton [Splitter] |
|
singleton [Map.S] |
singleton x y returns the one-element map that contains a binding y
for x .
|
singleton [Wp.Vset] |
|
singleton [Wp.Splitter] |
|
singleton [FCMap.S] |
singleton x y returns the one-element map that contains a binding y
for x .
|
size [Matrix] |
|
sizeof_defined [Ctypes] |
|
sizeof_defined [Wp.Ctypes] |
|
sizeof_object [Ctypes] |
|
sizeof_object [Wp.Ctypes] |
|
skip [Script] |
|
sloc [Cvalues.Logic] |
|
source_of_id [WpPropId] |
|
source_of_id [Wp.WpPropId] |
|
spawn [VC] |
Same as prove but schedule the tasks into the global server returned
by server function below.
|
spawn [Prover] |
|
spawn [ProverTask] |
Spawn all the tasks over the server and retain the first 'validated' one.
|
spawn [Wp.VC] |
Same as prove but schedule the tasks into the global server returned
by server function below.
|
spawn_wp_proofs_iter [Register] |
|
split [Mcfg.Splitter] |
|
split [WpAnnot] |
splits a prop_id goals into prop_id parts for each sub-goals
|
split [Map.S] |
split x m returns a triple (l, data, r) , where
l is the map with all the bindings of m whose key
is strictly less than x ;
r is the map with all the bindings of m whose key
is strictly greater than x ;
data is None if m contains no binding for x ,
or Some v if m binds v to x .
|
split [Wp.Mcfg.Splitter] |
|
split [FCMap.S] |
split x m returns a triple (l, data, r) , where
l is the map with all the bindings of m whose key
is strictly less than x ;
r is the map with all the bindings of m whose key
is strictly greater than x ;
data is None if m contains no binding for x ,
or Some v if m binds v to x .
|
spy [Register] |
|
start_edge [Cil2cfg] |
get the starting edges
|
start_stmt_of_node [Cil2cfg] |
|
status [LogicSemantics.Make] |
|
status [LogicCompiler.Make] |
|
status [Wp.LogicSemantics.Make] |
|
status [Wp.LogicCompiler.Make] |
|
step [Conditions] |
|
step [Wp.Conditions] |
|
stepout [VCS] |
|
stepout [Wp.VCS] |
|
stored [Memory.Model] |
Return a set of formula that express a modification between two
memory state.
|
stored [Wp.Memory.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] |
|
str_len [Wp.Cstring] |
|
str_val [Cstring] |
The array containing all char of the constant
|
str_val [Wp.Cstring] |
The array containing all char of the constant
|
strange_loops [Cil2cfg] |
detect is there are non natural loops or natural loops where we didn't
manage to compute back edges (see mark_loops ).
|
strategy_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_float [Ctypes] |
|
sub_c_float [Wp.Ctypes] |
|
sub_c_int [Ctypes] |
|
sub_c_int [Wp.Ctypes] |
|
sub_range [Vset] |
|
sub_range [Wp.Vset] |
|
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 [Wp.Vset] |
|
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 |
target [WpAnnot] |
|
tau [Matrix] |
|
tau_of_chunk [Memory.Chunk] |
|
tau_of_chunk [Wp.Memory.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] |
|
term [LogicSemantics.Make] |
|
term [LogicCompiler.Make] |
|
term [Wp.LogicSemantics.Make] |
|
term [Wp.LogicCompiler.Make] |
|
test [Mcfg.S] |
|
test [Wp.Mcfg.S] |
|
timeout [VCS] |
|
timeout [Wp.VCS] |
|
to_cint [Cint] |
Raises Not_found if not.
|
to_cint [Wp.Cint] |
Raises Not_found if not.
|
token [Script] |
|
tracelog [Register] |
|
trigger [LogicCompiler.Make] |
|
trigger [Wp.LogicCompiler.Make] |
|
trivial [Wpo.GOAL] |
|
try_sequence [Register] |
|
type_id [Lang] |
|
type_id [Wp.Lang] |
|
type_of_cells [VarUsage] |
Type of multi-dimensional array cells
|
type_of_cells [VarUsageRef] |
Type of multi-dimensional array cells
|
U |
union [Cvalues.Logic] |
|
union [Vset] |
|
union [Splitter] |
|
union [Passive] |
|
union [Wp.Passive] |
|
union [Wp.Vset] |
|
union [Wp.Splitter] |
|
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 [Wp.Model.Registry] |
set current value, with no protection
|
update [Wp.Context] |
Modification of the current value
|
update_hints_for_goal [Proof] |
Update the hints for one specific goal.
|
update_symbol [Definitions] |
|
update_symbol [Wp.Definitions] |
|
use_assigns [Mcfg.S] |
use_assigns env hid kind assgn goal performs the havoc on the goal.
|
use_assigns [Wp.Mcfg.S] |
use_assigns env hid kind assgn goal performs the havoc on the goal.
|
V |
val_of_exp [CodeSemantics.Make] |
|
val_of_exp [Wp.CodeSemantics.Make] |
|
val_of_term [LogicSemantics.Make] |
|
val_of_term [Wp.LogicSemantics.Make] |
|
valid [VCS] |
|
valid [LogicSemantics.Make] |
|
valid [Memory.Model] |
Return the formula that tests if a memory state is valid
(according to Memory.acs ) in the given memory state at the given
segment.
|
valid [Cvalues.Logic] |
|
valid [Wp.VCS] |
|
valid [Wp.LogicSemantics.Make] |
|
valid [Wp.Memory.Model] |
Return the formula that tests if a memory state is valid
(according to Wp.Memory.acs ) in the given memory state at the given
segment.
|
validated_cvar [VarUsage] |
|
validated_cvar [VarUsageRef] |
|
validated_lvar [VarUsage] |
|
validated_lvar [VarUsageRef] |
|
value [Memory.Sigma] |
|
value [Cvalues.Logic] |
|
value [Wp.Memory.Sigma] |
|
variables [Lang] |
|
variables [Wp.Lang] |
|
vars [LogicAssigns.Logic] |
|
vars [LogicAssigns.Make] |
|
vars [LogicSemantics.Make] |
|
vars [Memory.Model] |
Return the logic variables from which the given location depend on.
|
vars [Region] |
|
vars [Vset] |
|
vars [Definitions.Trigger] |
|
vars [Wp.LogicSemantics.Make] |
|
vars [Wp.Memory.Model] |
Return the logic variables from which the given location depend on.
|
vars [Wp.Vset] |
|
vars [Wp.Definitions.Trigger] |
|
vars_hyp [Conditions] |
|
vars_hyp [Wp.Conditions] |
|
vars_seq [Conditions] |
|
vars_seq [Wp.Conditions] |
|
varsp [Lang.F] |
|
varsp [Wp.Lang.F] |
|
very_strange_loops [Cil2cfg] |
detect is there are natural loops where we didn't manage to compute
back edges (see mark_loops ).
|
vset [Cvalues.Logic] |
|
W |
warnings [Wpo] |
|
with_current_loc [Context] |
|
with_current_loc [Wp.Context] |
|
with_model [Model] |
|
with_model [Wp.Model] |
|
without_assume [Lang] |
|
without_assume [Wp.Lang] |
|
wp_clear [Register] |
|
wp_compute [Register] |
|
wp_compute_call [Register] |
|
wp_compute_deprecated [Register] |
|
wp_compute_ip [Register] |
|
wp_compute_kf [Register] |
|
wp_iter_model [Register] |
|
wp_print_separation [Register] |
|
X |
xmark [Plang] |
|
xmark_e [Plang] |
|
xmark_hyp [Pcond] |
|
xmark_p [Plang] |
|
xmark_seq [Pcond] |
|