|
(&&&) [Register] |
|
__ocaml_lex_attributes_rec [Why3_xml] |
|
__ocaml_lex_bal_rec [Driver] |
|
__ocaml_lex_command_rec [Rformat] |
|
__ocaml_lex_comment_rec [Driver] |
|
__ocaml_lex_comment_rec [Script] |
|
__ocaml_lex_elements_rec [Why3_xml] |
|
__ocaml_lex_proof_rec [Script] |
|
__ocaml_lex_reclink_bis_rec [Driver] |
|
__ocaml_lex_reclink_rec [Driver] |
|
__ocaml_lex_reclink_ter_rec [Driver] |
|
__ocaml_lex_recorstring_rec [Driver] |
|
__ocaml_lex_recstring_bis_rec [Driver] |
|
__ocaml_lex_recstring_rec [Driver] |
|
__ocaml_lex_recstring_ter_rec [Driver] |
|
__ocaml_lex_skip_rec [Script] |
|
__ocaml_lex_string_val_rec [Driver] |
|
__ocaml_lex_string_val_rec [Why3_xml] |
|
__ocaml_lex_tables [Driver] |
|
__ocaml_lex_tables [Why3_xml] |
|
__ocaml_lex_tables [Script] |
|
__ocaml_lex_tables [Rformat] |
|
__ocaml_lex_tok_rec [Driver] |
|
__ocaml_lex_token_rec [Script] |
|
__ocaml_lex_value_rec [Driver] |
|
__ocaml_lex_value_rec [Why3_xml] |
|
__ocaml_lex_word_rec [Rformat] |
|
__ocaml_lex_xml_doctype_rec [Why3_xml] |
|
__ocaml_lex_xml_prolog_rec [Why3_xml] |
|
_bkind_sid [Cil2cfg] |
|
_brackets_var_type_typ [Variables_analysis] |
|
_dkey [CfgDump] |
|
_find_stmt_node [Cil2cfg] |
|
_iter_succ_e [Cil2cfg] |
|
_merge_dim [VarUsage] |
|
_print [VarUsage.Usage] |
|
_rte_downCast_status [WpAnnot] |
|
_split [WpPropId] |
|
A |
a_addr [MemTyped] |
|
a_base [MemTyped] |
|
a_cast [MemTyped] |
|
a_global [MemTyped] |
|
a_hardware [MemTyped] |
|
a_leq [MemTyped] |
|
a_lt [MemTyped] |
|
a_mk_addr [MemTyped] |
|
a_null [MemTyped] |
|
a_offset [MemTyped] |
|
a_shift [MemTyped] |
|
ac [Cint] |
|
access [MemTyped] |
|
access [MemVar.Make] |
|
access [Region] |
|
access [RefUsage.E] |
|
access_offset [LogicSemantics.Make] |
|
acsl_lit [Cfloat] |
|
add [Indexer.Make] |
Log complexity.
|
add [CfgTypes.Cfg] |
|
add [Factory] |
|
add [Set.S] |
add x s returns a set containing all elements of s ,
plus x .
|
add [Map.S] |
add x y m returns a map containing the same bindings as
m , plus a binding of x to y .
|
add [Wpo] |
|
add [Conditions.Bundle] |
|
add [Cleaning] |
|
add [Letify.Split] |
|
add [Letify.Sigma] |
|
add [Model.MODELS] |
|
add [Warning] |
|
add [Cil2cfg.HEsig] |
|
add [Cil2cfg.HE] |
|
add [Hashtbl.S] |
|
add [Cil2cfg.PMAP] |
|
add [FCMap.S] |
add x y m returns a map containing the same bindings as
m , plus a binding of x to y .
|
add [State_builder.Hashtbl] |
Add a new binding.
|
add [Fixpoint.Make] |
add x y requires x >= y
|
add [CfgLib.Make] |
|
add0 [Fixpoint.Make] |
add0 x d requires x >= d
|
add1 [Fixpoint.Make] |
add x f y requires x >= f(y)
|
add2 [Fixpoint.Make] |
add x f y z requires x >= f(y,z)
|
add_alias [LogicBuiltins] |
|
add_all_axioms [WpStrategy] |
|
add_array [MemTyped.Layout] |
|
add_array_reference_arg [Variables_analysis] |
|
add_array_reference_param [Variables_analysis] |
|
add_assigns [Mcfg.S] |
|
add_assigns [CfgWP.VC] |
|
add_assigns [CfgDump.VC] |
|
add_assigns [WpStrategy] |
generic function to add an assigns property.
|
add_assigns_any [WpStrategy] |
generic function to add a WriteAny assigns property.
|
add_assigns_goal [Calculus.Cfg] |
|
add_assigns_hyp [Calculus.Cfg] |
|
add_atom [MemTyped.Layout] |
|
add_axiom [Mcfg.S] |
|
add_axiom [CfgWP.VC] |
|
add_axiom [CfgDump.VC] |
|
add_axiom [WpStrategy] |
|
add_behaviors_props [WpAnnot] |
|
add_block [MemTyped.Layout] |
|
add_builtin [LogicBuiltins] |
|
add_call [LogicUsage] |
|
add_call_annots [WpAnnot] |
|
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_called_post [WpAnnot] |
|
add_called_pre [WpAnnot] |
|
add_case [Conditions] |
|
add_complete_behaviors_props [WpAnnot] |
|
add_const [LogicBuiltins] |
|
add_cover [WpReport] |
|
add_ctor [LogicBuiltins] |
|
add_def [Letify.Defs] |
|
add_definitions [Letify] |
add_definitions sigma defs xs ps keep all
definitions of variables xs from sigma that comes from defs .
|
add_dim [Matrix] |
|
add_disjoint_behaviors_props [WpAnnot] |
|
add_edge [Cil2cfg.CFG] |
|
add_edge [Cil2cfg] |
|
add_edge_e [Cil2cfg.CFG] |
|
add_edges_before [Cil2cfg] |
|
add_eq [Letify] |
|
add_equals [Letify] |
|
add_false [Cleaning] |
|
add_fct_assigns_goal [WpAnnot] |
|
add_fct_bhv_assigns_hyp [WpStrategy] |
|
add_fct_pre [WpAnnot] |
|
add_fmodel [Cfloat] |
|
add_fun [Cleaning] |
|
add_global_annotations [WpAnnot] |
|
add_goal [Mcfg.S] |
|
add_goal [CfgWP.VC] |
|
add_goal [CfgDump.VC] |
|
add_goal [Calculus.Cfg] |
|
add_goal [WpReport] |
|
add_hint [WpPropId] |
|
add_hook [Wprop.Indexed2] |
|
add_hook [Wprop.Indexed] |
|
add_hook_on_update [State_builder.S] |
Add an hook which is applied each time (just before) the project library
changes the local value of the state.
|
add_hyp [Mcfg.S] |
|
add_hyp [CfgWP.VC] |
|
add_hyp [CfgDump.VC] |
|
add_hyp [Calculus.Cfg] |
|
add_include [ProverCoq] |
|
add_infer [Conditions] |
|
add_irreducible [Cil2cfg.WeiMaoZouChenInput] |
store the node as an irreducible loop header.
|
add_irreducible [Cil2cfg.LoopInfo] |
|
add_kf [Generator] |
|
add_library [LogicBuiltins] |
External theories
|
add_linear [Letify.Defs] |
|
add_logic [LogicBuiltins] |
|
add_logics_value [Variables_analysis] |
|
add_loop_annots [WpStrategy] |
|
add_loop_assigns_goal [WpAnnot] |
|
add_loop_assigns_hyp [WpStrategy] |
shortcut to add a loop assigns property as an hypothesis.
|
add_loop_header [Cil2cfg.WeiMaoZouChenInput] |
store the node as a loop header.
|
add_loop_header [Cil2cfg.LoopInfo] |
|
add_loop_invariant_annot [WpAnnot] |
|
add_many [MemTyped.Layout] |
|
add_memo [Calculus.Cfg.R] |
|
add_model [Cfloat] |
|
add_node [Cil2cfg] |
|
add_node_annots [WpStrategy] |
add_node_annots cfg annots v (before, (after, exits))
add the annotations for the node :
|
add_oblig [Calculus.Cfg.R] |
|
add_on_edges [WpStrategy] |
|
add_option [LogicBuiltins] |
add a value to an option (group, name)
|
add_pred [Cleaning] |
|
add_predicate [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_inv_establish [WpAnnot] |
|
add_prop_inv_fixpoint [WpAnnot] |
|
add_prop_inv_preserve [WpAnnot] |
|
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_ptr_reference_arg [Variables_analysis] |
|
add_ptr_reference_param [Variables_analysis] |
|
add_qed_check [CfgWP] |
|
add_qedstat [WpReport] |
|
add_rank [Matrix] |
|
add_reentry_edge [Cil2cfg.WeiMaoZouChenInput] |
store the edge between the two nodes (n1, n2) as a reentry edge.
|
add_reentry_edge [Cil2cfg.LoopInfo] |
|
add_required [WpPropId] |
|
add_requires [Variables_analysis] |
|
add_results [WpReport] |
|
add_script [Proof] |
new_script goal keys proof registers the script proof for goal goal
and keywords keys
|
add_source [ProverCoq] |
|
add_spaces [Rformat] |
|
add_stat [WpReport] |
|
add_step [Register] |
|
add_stmt_assigns_goal [WpAnnot] |
|
add_stmt_bhv_as_goal [WpAnnot] |
we want to prove this behavior: add the requires as preconditions to both prove and use as hyp,, add the assumes as hypotheses,, add the postconditions as goals.
|
add_stmt_invariant_annot [WpAnnot] |
|
add_stmt_spec_annots [WpAnnot] |
|
add_stmt_spec_assigns_hyp [WpStrategy] |
shortcut to add a stmt spec assigns property as an hypothesis.
|
add_stmt_spec_post_as_hyp [WpAnnot] |
Add the post condition of the whole spec as hypothesis.
|
add_terminates [WpAnnot] |
|
add_time [Register] |
|
add_true [Cleaning] |
|
add_type [LogicBuiltins] |
|
add_type [Cleaning] |
|
add_var [Cleaning] |
|
add_variant [WpAnnot] |
|
add_variant_annot [WpAnnot] |
|
add_vc [CfgWP.VC] |
|
add_vertex [Cil2cfg.CFG] |
|
add_warnings [CfgWP.VC] |
|
addbox_of_type [VarUsage] |
|
added [Wpo] |
|
addn [Fixpoint.Make] |
add x f ys requires x >= f(ys)
|
addr_lval [LogicSemantics.Make] |
|
addr_lval [RefUsage] |
|
adds [Fixpoint.Make] |
|
adt_set [Vset] |
|
agamma [Lang] |
|
age [Wpo] |
|
alloc_for_type [VarUsage] |
Size of dimensions in the type (0 for unknown size)
|
alloc_var [MemVar.Make] |
|
allocates [MemTyped] |
|
allocates [MemVar.Make] |
|
already_valid [Register] |
|
altergo_gui [ProverErgo] |
|
annot_hints [WpPropId] |
|
apool [Lang] |
|
append_file [ProverErgo] |
|
apply [Wpo.GOAL] |
|
apply [Cvalues.Logic] |
|
apply [Passive] |
|
apply [VarUsage.Context] |
|
apply_add [Cvalues.Logic] |
|
apply_config [Factory] |
|
apply_depend [GuiSource] |
|
apply_effect [GuiSource] |
|
apply_goal [GuiSource] |
|
apply_hyp [Conditions] |
|
apply_lift [Cvalues.Logic] |
|
apply_path [GuiSource] |
|
apply_sub [Cvalues.Logic] |
|
apply_tag [GuiSource] |
|
arith [LogicSemantics.Make] |
|
arith [CodeSemantics.Make] |
|
arith_int [CodeSemantics.Make] |
|
array [Lang] |
|
array_dim [Ctypes] |
|
array_dimensions [Ctypes] |
Returns the list of dimensions the array consists of.
|
array_name [Cvalues.STRUCTURAL] |
|
array_reference [Variables_analysis] |
|
array_size [Ctypes] |
|
as_atom [Cleaning] |
|
as_have [Cleaning] |
|
as_type [Cleaning] |
|
assemble [ProverCoq] |
|
assemble [ProverErgo] |
|
assemble_check [ProverWhy3] |
|
assemble_cluster [ProverWhy3] |
|
assemble_cluster [ProverCoq] |
|
assemble_cluster [ProverErgo] |
|
assemble_coqlib [ProverCoq] |
|
assemble_file [ProverErgo] |
|
assemble_goal [ProverWhy3] |
|
assemble_goal [ProverCoq] |
|
assemble_goal [ProverErgo] |
|
assemble_lib [ProverErgo] |
|
assemble_wpo [ProverWhy3] |
None if the po is trivial
|
assign [Mcfg.S] |
|
assign [CfgWP.VC] |
|
assign [CfgDump.VC] |
|
assignable [LogicSemantics.Make] |
|
assignable_lval [LogicSemantics.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 [MemTyped] |
|
assigned [MemVar.Make.Sigma] |
|
assigned [MemVar.Make] |
|
assigned [MemEmpty] |
|
assigned [Sigma.Make] |
|
assigned [LogicAssigns.Make] |
|
assigned [VarUsage.Context] |
|
assigned_loc [MemTyped] |
|
assigned_path [MemVar.Make] |
|
assigned_range [MemTyped] |
|
assigned_seq [LogicAssigns.Make] |
|
assigns [LogicSemantics.Make] |
|
assigns_condition [CfgWP.VC] |
|
assigns_from [LogicSemantics.Make] |
|
assigns_hints [WpPropId] |
|
assigns_info_id [WpPropId] |
|
assigns_upper_bound [WpStrategy] |
|
assume [Conditions] |
|
assume [Letify.Sigma] |
|
assume [Lang] |
|
assume_vc [CfgWP.VC] |
|
atoms [Letify.Defs] |
|
attributes [Why3_xml] |
|
atype [Lang] |
|
auto_check_valid [Register] |
|
avoid_leading_backlash [Lang] |
|
axiomatic [Definitions] |
|
axiomatic [LogicUsage] |
|
axiomatic_of_global [LogicUsage] |
|
B |
back [Model] |
|
bal [Driver] |
|
balance [Cint] |
|
band [Cint] |
|
bar [Wpo] |
|
base_addr [Memory.Model] |
Return the memory location of the base address of a given memory
location
|
base_addr [MemTyped] |
|
base_addr [MemVar.Make] |
|
base_addr [MemEmpty] |
|
base_output [Wp_parameters] |
call the construction of the directory only once
|
basename [Lang.ADT] |
|
basename [Lang] |
|
basename [LogicUsage] |
Trims the original name
|
basename [Ctypes] |
|
basename_of_chunk [Memory.Chunk] |
|
basename_of_chunk [MemTyped.Chunk] |
|
basename_of_chunk [MemVar.Make.Chunk] |
|
basename_of_chunk [MemVar.Make.VALLOC] |
|
basename_of_chunk [MemVar.Make.VAR] |
|
basename_of_chunk [MemEmpty.Chunk] |
|
begin_session [Register] |
|
behavior_name_of_config [WpAnnot] |
|
behavior_name_of_strategy [WpStrategy] |
|
best_result [WpReport] |
|
big_inter [Conditions.Bundle] |
|
bind [Letify] |
bind sigma defs xs select definitions in defs
targeting variables xs .
|
bind [Passive] |
|
bind [Model] |
|
bind [Context] |
Performs the job with local context bound to local value.
|
bind [RefUsage.E] |
|
bind_dseq [Conditions] |
|
bind_labels [LogicCompiler.Make] |
|
bind_quantifiers [LogicSemantics.Make] |
|
bind_with [Context] |
|
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.
|
bitk_positive [Cint] |
|
bkind_stmt [Cil2cfg] |
|
blit [String] |
Same as Bytes.blit_string .
|
block_length [Memory.Model] |
Returns the length (in bytes) of the allocated block containing
the given location
|
block_length [MemTyped] |
|
block_length [MemVar.Make] |
|
block_length [MemEmpty] |
|
blocks_closed_by_edge [Cil2cfg] |
|
blsl [Cint] |
|
blsr [Cint] |
|
bnot [Cint] |
|
bool_and [Cvalues] |
|
bool_attribute [Why3_session] |
|
bool_eq [Cvalues] |
|
bool_leq [Cvalues] |
|
bool_lt [Cvalues] |
|
bool_neq [Cvalues] |
|
bool_of_comp [CodeSemantics.Make] |
|
bool_of_exp [CodeSemantics.Make] |
|
bool_or [Cvalues] |
|
bool_val [Cvalues] |
|
bootstrap_logic [LogicCompiler.Make] |
|
bootstrap_pred [LogicCompiler.Make] |
|
bootstrap_region [LogicCompiler.Make] |
|
bootstrap_term [LogicCompiler.Make] |
|
bor [Cint] |
|
bot [RefUsage.E] |
|
bot [Fixpoint.Domain] |
|
bound_add [Vset] |
|
bound_shift [Vset] |
|
bound_sub [Vset] |
|
box_of_type [VarUsage] |
|
bracket_exp [Variables_analysis] |
|
bracket_term [Variables_analysis] |
|
brackets_and_stars_lv_typ [Variables_analysis] |
|
brackets_and_stars_typ [Variables_analysis] |
|
brackets_and_stars_var_type_typ [Variables_analysis] |
|
brackets_lv_typ [Variables_analysis] |
|
brackets_off [Variables_analysis] |
|
brackets_toff [Variables_analysis] |
|
brackets_typ [Variables_analysis] |
brackets_typ typ returns the numbre of brackets of the type typ .
|
branch [Conditions] |
|
branch_vc [CfgWP.VC] |
|
buf [Why3_xml] |
|
build_bhv_strategy [WpAnnot] |
|
build_configs [WpAnnot] |
|
build_prop_of_from [Mcfg.S] |
build p => alpha(p) for functional dependencies verification.
|
build_prop_of_from [CfgWP.VC] |
|
build_prop_of_from [CfgDump.VC] |
|
builtin_abs [Cfloat] |
|
builtin_driver [LogicBuiltins] |
|
builtin_error [Cfloat] |
|
builtin_model [Cfloat] |
|
builtin_positive_eq [Cfloat] |
|
builtin_positive_leq [Cfloat] |
|
builtin_round [Cfloat] |
|
builtin_sqrt [Cfloat] |
|
builtin_type [Lang] |
|
builtins [Lang] |
|
bxor [Cint] |
|
by_array_reference [Variables_analysis] |
|
by_array_reference_pattern [Variables_analysis] |
|
by_array_reference_pattern_term [Variables_analysis] |
|
by_array_reference_usage [Variables_analysis] |
|
by_array_reference_usage_term [Variables_analysis] |
|
by_pointer_reference_pattern [Variables_analysis] |
|
by_pointer_reference_pattern_term [Variables_analysis] |
|
by_pointer_reference_usage [Variables_analysis] |
|
by_pointer_reference_usage_term [Variables_analysis] |
|
by_ptr_reference [Variables_analysis] |
|
bytags [Splitter] |
|
C |
c_bool [Ctypes] |
Returns the type of int
|
c_char [Ctypes] |
Returns the type of char
|
c_float [Ctypes] |
Conforms to
|
c_int [Ctypes] |
Conforms to
|
c_int_all [Ctypes] |
|
c_int_bounds [Ctypes] |
|
c_label [Clabels] |
Assumes the logic label only comes from normalized labels.
|
c_option [ProverCoq] |
|
c_ptr [Ctypes] |
Returns the type of pointers
|
cache_descr [Wpo.VC_Annot] |
|
cache_descr [Wpo.VC_Lemma] |
|
cache_descr [Wpo.DISK] |
|
cache_log [Wpo.DISK] |
|
call [Mcfg.S] |
|
call [CfgWP.VC] |
|
call [CfgDump.VC] |
|
call [LogicSemantics.Make] |
|
call [CodeSemantics.Make] |
|
call [Splitter] |
|
call [RefUsage] |
|
call [VarUsage.Usage] |
|
call_contract [CfgWP.VC] |
|
call_dynamic [Mcfg.S] |
|
call_dynamic [CfgWP.VC] |
|
call_dynamic [CfgDump.VC] |
|
call_fun [LogicCompiler.Make] |
|
call_fun [Definitions] |
|
call_goal_precond [Mcfg.S] |
|
call_goal_precond [CfgWP.VC] |
|
call_goal_precond [CfgDump.VC] |
|
call_ide [ProverWhy3] |
|
call_instances [CfgWP.VC] |
|
call_kf [RefUsage] |
|
call_lg [RefUsage] |
|
call_node [CodeSemantics.Make] |
|
call_params [LogicCompiler.Make] |
|
call_post [LogicSemantics.Make] |
|
call_post [LogicCompiler.Make] |
|
call_pre [LogicSemantics.Make] |
|
call_pre [LogicCompiler.Make] |
|
call_preconditions [WpAnnot] |
|
call_pred [LogicCompiler.Make] |
|
call_pred [Definitions] |
|
call_proper [CfgWP.VC] |
|
callback [Model.Registry] |
|
callback [Model.Static] |
|
callback [Model.Index] |
|
callenv [Calculus.Cfg] |
|
calls [GuiNavigator] |
|
calls_collection_computed [Variables_analysis] |
|
cap [Fixpoint.Domain] |
|
capitalize [String] |
Return a copy of the argument, with the first character set to uppercase.
|
cardinal [Set.S] |
Return the number of elements of a set.
|
cardinal [Map.S] |
Return the number of bindings of a map.
|
cardinal [FCMap.S] |
Return the number of bindings of a map.
|
cartesian [Vset] |
|
case_of_optimization [Variables_analysis] |
|
cases [Splitter] |
|
cast [Memory.Model] |
Cast a memory location into another memory location.
|
cast [MemTyped] |
|
cast [MemVar.Make] |
|
cast [MemEmpty] |
|
cast [CodeSemantics.Make] |
|
cast [RefUsage] |
|
cast [VarUsage.Context] |
|
cast_ctyp [RefUsage] |
|
cast_ltyp [RefUsage] |
|
cast_obj [RefUsage] |
|
cat_print_generated [Wp_parameters] |
|
catch [Warning] |
Set up a context for the job.
|
catch_label_error [NormAtLabels] |
|
category [Lang.Fun] |
|
cc_assigned [CfgWP.VC] |
|
cc_call_domain [CfgWP.VC] |
|
cc_call_effects [CfgWP.VC] |
|
cc_callenv [CfgWP.VC] |
|
cc_case [CfgWP.VC] |
|
cc_case_values [CfgWP.VC] |
|
cc_contract_hyp [CfgWP.VC] |
|
cc_default [CfgWP.VC] |
|
cc_effect [CfgWP.VC] |
|
cc_from [CfgWP.VC] |
|
cc_group_case [CfgWP.VC] |
|
cc_havoc [CfgWP.VC] |
|
cc_logic [LogicCompiler.Make] |
|
cc_lval [CfgWP.VC] |
|
cc_posteffect [CfgWP.VC] |
|
cc_pred [LogicCompiler.Make] |
|
cc_region [LogicCompiler.Make] |
|
cc_result [CfgWP.VC] |
|
cc_result_domain [CfgWP.VC] |
|
cc_status [CfgWP.VC] |
|
cc_stored [CfgWP.VC] |
|
cc_term [LogicCompiler.Make] |
|
cdomain [Cvalues] |
|
cdriver [LogicBuiltins] |
|
cells_in_type [VarUsage] |
Number of cells in the type (raise NoSize for unknown size)
|
cfg_block [Cil2cfg] |
|
cfg_from_definition [Cil2cfg] |
|
cfg_from_proto [Cil2cfg] |
|
cfg_graph [Cil2cfg] |
|
cfg_kf [Cil2cfg] |
|
cfg_of_strategy [WpStrategy] |
|
cfg_spec_only [Cil2cfg] |
returns true is this CFG is degenerated (no code available)
|
cfg_start [Cil2cfg] |
|
cfg_stmt [Cil2cfg] |
|
cfg_stmts [Cil2cfg] |
build the nodes for the stmts , connect the last one with next ,
and return the node of the first stmt.
|
cfg_switch [Cil2cfg] |
|
cframe [LogicCompiler.Make] |
|
cgamma [Lang] |
|
change_mode_if_needed [Calculus.Cfg.R] |
If needed, clear wp table to compute Pass2.
|
change_node_kind [Cil2cfg] |
|
char [Ctypes] |
|
char_at [Cstring] |
|
check_assigns [CfgWP.VC] |
|
check_nothing [CfgWP.VC] |
|
check_session [ProverCoq] |
|
choose [Set.S] |
Return one element of the given set, or raise Not_found if
the set is empty.
|
choose [Map.S] |
Return one binding of the given map, or raise Not_found if
the map is empty.
|
choose [Proof] |
|
choose [FCMap.S] |
Return one binding of the given map, or raise Not_found if
the map is empty.
|
chop_backslash [LogicBuiltins] |
|
chop_version [ProverWhy3] |
|
ckind [LogicBuiltins] |
|
class_of [Letify.Sigma] |
|
class_of_prover [Wpo.Results] |
|
clean [Conditions] |
|
clean_cond [Conditions] |
|
clean_graph [Cil2cfg] |
|
clean_seq [Conditions] |
|
clean_steps [Conditions] |
|
clear [Wpo] |
|
clear [Proof] |
|
clear [Context] |
Clear the current value.
|
clear [Cil2cfg.HEsig] |
|
clear [Cil2cfg.HE] |
|
clear [Hashtbl.S] |
|
clear [Cil2cfg.PMAP] |
|
clear [State_builder.Hashtbl] |
Clear the table.
|
clear [State_builder.Ref] |
Reset the reference to its default value.
|
clear_scheduled [Register] |
|
clear_session [Register] |
|
clear_system [Wpo] |
|
cloc [CodeSemantics.Make] |
|
close [Mcfg.S] |
|
close [CfgWP.VC] |
|
close [CfgDump.VC] |
|
close [Script] |
|
close [Conditions] |
|
cluster [Cstring] |
The cluster where all strings are defined.
|
cluster [Definitions] |
|
cluster_age [Definitions] |
|
cluster_compare [Definitions] |
|
cluster_file [ProverWhy3] |
|
cluster_file [ProverCoq] |
|
cluster_file [ProverErgo] |
|
cluster_globals [MemTyped] |
|
cluster_id [Definitions] |
Unique
|
cluster_memory [MemTyped] |
|
cluster_position [Definitions] |
|
cluster_title [Definitions] |
|
cmdline [Register] |
|
cmdline_run [Register] |
|
cmp [Ctypes] |
|
cmp_prover [VCS] |
|
cmpopt [Wpo.Index] |
|
code_annot_names [WpPropId] |
|
code_lit [Cfloat] |
|
codomain [Letify.Sigma] |
|
collect [Definitions.Trigger] |
|
collect [Splitter] |
|
collect [Passive] |
|
collect [Matrix] |
|
collect_apps [Variables_analysis] |
|
collect_apps_builtin [Variables_analysis] |
|
collect_apps_rec [Variables_analysis] |
|
collect_arg_array_call [Variables_analysis] |
|
collect_arg_ptr_call [Variables_analysis] |
|
collect_calls [Variables_analysis] |
|
collect_calls_rec [Variables_analysis] |
|
collect_cond [Conditions] |
|
collect_formal_array_call [Variables_analysis] |
|
collect_formal_ptr_call [Variables_analysis] |
|
collect_refparams [Variables_analysis] |
|
collect_scripts [Proof] |
|
collect_sepstars [Variables_analysis] |
|
collect_seq [Conditions] |
|
collect_steps [Conditions] |
|
collection_of_term [LogicSemantics.Make] |
|
collector [Warning] |
|
command [Rformat] |
|
comment [Driver] |
|
comment [Script] |
|
comp [Lang] |
|
comp_id [Lang] |
|
compact [Splitter] |
|
compare [Memory.Chunk] |
|
compare [CfgWP.VC.EFFECT] |
|
compare [CfgWP.VC.TARGET] |
|
compare [Set.S] |
Total ordering between sets.
|
compare [Map.S] |
Total ordering between maps.
|
compare [Wpo.Index] |
|
compare [MemTyped.Layout] |
|
compare [MemTyped.LITERAL] |
|
compare [MemTyped.Chunk] |
|
compare [MemVar.Make.Chunk] |
|
compare [MemVar.Make.VALLOC] |
|
compare [MemVar.Make.VAR] |
|
compare [MemEmpty.Chunk] |
|
compare [CodeSemantics.Make] |
|
compare [Cstring.STR] |
|
compare [LogicBuiltins] |
|
compare [Splitter] |
|
compare [Matrix.COBJ] |
|
compare [Matrix.KEY] |
|
compare [Lang.Fun] |
|
compare [Lang.Field] |
|
compare [Lang.ADT] |
|
compare [Model.Key] |
|
compare [Model.Entries] |
|
compare [Model.Static.KEY] |
|
compare [Model.Index.KEY] |
|
compare [Warning.SELF] |
|
compare [Cil2cfg.EL] |
|
compare [Cil2cfg.VL] |
|
compare [RefUsage.Var] |
|
compare [VarUsage.Root] |
|
compare [FCMap.S] |
Total ordering between maps.
|
compare [Clabels.T] |
|
compare [Ctypes.AinfoComparable] |
|
compare [Ctypes] |
|
compare [String] |
|
compare_array_ptr_conflated [Ctypes] |
|
compare_c_float [Ctypes] |
|
compare_c_int [Ctypes] |
|
compare_dim [Matrix.KEY] |
|
compare_edge_type [Cil2cfg.EL] |
|
compare_kind [WpPropId] |
|
compare_lemma [Definitions] |
|
compare_prop_id [WpPropId] |
|
compare_ptr_conflated [Ctypes] |
|
compare_symbol [Definitions] |
|
compare_term [LogicSemantics.Make] |
|
comparep [Lang.F] |
|
compatible [VarUsage] |
|
compilation_unit_names [Config] |
List of names of all kernel compilation units.
|
compile [CfgWP.VC] |
|
compile [Model.Data] |
|
compile [Model.Registry] |
with circularity protection
|
compile [Model.Static] |
|
compile [Model.Index] |
|
compile_headers [ProverCoq] |
|
compile_lbinduction [LogicCompiler.Make] |
|
compile_lbnone [LogicCompiler.Make] |
|
compile_lbpred [LogicCompiler.Make] |
|
compile_lbpure [LogicCompiler.Make] |
|
compile_lbreads [LogicCompiler.Make] |
|
compile_lbterm [LogicCompiler.Make] |
|
compile_lemma [CfgWP.VC] |
|
compile_lemma [LogicCompiler.Make] |
|
compile_lemma [Definitions] |
|
compile_logic [LogicCompiler.Make] |
|
compile_rec [LogicCompiler.Make] |
|
compile_step [LogicCompiler.Make] |
|
compinfo [Definitions] |
|
component [WTO] |
|
compute [Calculus.Cfg] |
|
compute [Wpo.GOAL] |
|
compute [Variables_analysis] |
|
compute [VarUsage] |
|
compute [LogicUsage] |
To force computation
|
compute [Dyncall] |
Forces computation of dynamic calls.
|
compute_call [Generator] |
|
compute_calls_collection [Variables_analysis] |
|
compute_descr [Wpo.GOAL] |
|
compute_f_of_int [Cfloat] |
|
compute_global_init [Calculus.Cfg] |
|
compute_ip [Generator] |
|
compute_kf [Generator] |
|
compute_logic_params [Variables_analysis] |
|
compute_logicname [LogicUsage] |
|
compute_parameters_usage [Variables_analysis] |
|
compute_proof [Wpo.GOAL] |
|
compute_provers [Register] |
|
compute_rte_for [WpAnnot] |
|
compute_selection [Generator] |
|
compute_wp_edge [Calculus.Cfg] |
|
computer [Register] |
|
computer [Factory] |
|
computing [VCS] |
|
concat [String] |
String.concat sep sl concatenates the list of strings sl ,
inserting the separator string sep between each.
|
concretize [Vset] |
|
concretize_vset [Vset] |
|
cond [CodeSemantics.Make] |
|
cond_node [CodeSemantics.Make] |
|
condition [CfgWP.VC] |
|
conditions [Passive] |
|
configure [Memory.Model] |
|
configure [Factory] |
|
configure [MemTyped] |
|
configure [MemVar.Make] |
|
configure [MemEmpty] |
|
configure [Cfloat] |
|
configure [Cint] |
|
configure_mheap [Factory] |
|
constant [Cvalues] |
|
constant [LogicBuiltins] |
|
constant [Ctypes] |
|
constant_exp [Cvalues] |
|
constant_term [Cvalues] |
|
constrained_comp [Cvalues.STRUCTURAL] |
|
constrained_elt [Cvalues.STRUCTURAL] |
|
constructor [Lang] |
|
contains [String] |
String.contains s c tests if character c
appears in the string s .
|
contains_from [String] |
String.contains_from s start c tests if character c
appears in s after position start .
|
context [Warning] |
|
conv_bal [Driver] |
|
convert [Lang.Alpha] |
|
convertp [Lang.Alpha] |
|
copied [Memory.Model] |
Return a set of formula that express a copy between two memory state.
|
copied [MemTyped] |
|
copied [MemVar.Make] |
|
copied [MemEmpty] |
|
copy [Memory.Sigma] |
|
copy [MemVar.Make.Sigma] |
|
copy [Sigma.Make] |
|
copy [Hashtbl.S] |
|
copy [Cil2cfg.PMAP] |
|
copy [String] |
Return a copy of the given string.
|
copy [Datatype.S] |
Deep copy: no possible sharing between x and copy x .
|
copy [CfgLib.Transform] |
Duplicates A into B with the provided morphism.
|
coq_timeout [ProverCoq] |
|
coqidelock [ProverCoq] |
|
coqlibs [ProverCoq] |
|
coverage [WpReport] |
|
cpool [Lang] |
|
create [Memory.Sigma] |
|
create [CfgTypes.Cfg] |
|
create [CfgWP.Computer] |
|
create [CfgDump] |
|
create [Wpo.Results] |
|
create [MemVar.Make.Sigma] |
|
create [Sigma.Make] |
|
create [Cleaning] |
|
create [Letify.Split] |
|
create [Lang.Alpha] |
|
create [Context] |
Creates a new context with name
|
create [Cil2cfg.HEsig] |
|
create [Cil2cfg.HE] |
|
create [Hashtbl.S] |
|
create [Cil2cfg.PMAP] |
|
create [Cil2cfg] |
|
create [String] |
String.create n returns a fresh byte sequence of length n .
|
create [Fixpoint.Make] |
|
create [CfgLib.Transform] |
Graph A should be static : further nodes in A can not be indexed.
|
create [CfgLib.Labels] |
|
create [CfgLib.Attr] |
|
create [CfgLib.Make] |
|
create_from [Cil2cfg.PMAP] |
|
create_option [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_system [Wpo] |
|
create_tbl [WpStrategy] |
|
ctor [LogicBuiltins] |
|
ctor_id [Lang] |
|
cup [Cleaning] |
|
cup [RefUsage.E] |
|
cup [RefUsage.Access] |
|
cup [Fixpoint.Domain] |
|
cup_false [Cleaning] |
|
cup_true [Cleaning] |
|
cur_fct_default_bhv [WpAnnot] |
|
current [Wp_error] |
|
current_age [Wpo] |
|
cval [CodeSemantics.Make] |
|
cvar [Memory.Model] |
Return the location of a C variable
|
cvar [MemTyped] |
|
cvar [MemVar.Make] |
|
cvar [MemEmpty] |
|
cvar [RefUsage] |
|
cvsort_of_type [LogicSemantics.Make] |
|
D |
datadir [Config] |
Directory where architecture independent files are.
|
datatype [Memory.Model] |
for projectification
|
datatype [Factory.VarRef2] |
|
datatype [Factory.VarRef0] |
|
datatype [Factory.VarHoare] |
|
datatype [MemTyped] |
|
datatype [MemVar.VarUsage] |
|
datatype [MemVar.Make] |
|
datatype [MemEmpty] |
|
datatype [Lang] |
|
date [Config] |
Compilation date.
|
db_filename [Why3_session] |
2 Create a session
|
debug [Calculus.Cfg] |
|
debug [Lang.Fun] |
|
debug [Lang.Field] |
|
debug [Lang.ADT] |
|
debug [WpAnnot] |
|
debug [WpStrategy] |
|
debug [Cil2cfg] |
|
debug [Variables_analysis] |
|
debug2 [Cil2cfg] |
|
debugp [Lang.F] |
|
decide_branch [Conditions] |
|
decode_chapter [WpReport] |
|
decr_addr_taken [Variables_analysis] |
|
decr_addr_taken_bool [Variables_analysis] |
|
default [Warning] |
|
default [Cil2cfg.EL] |
|
default_edge_attributes [Cil2cfg.Printer] |
|
default_label [LogicCompiler.Make] |
|
default_vertex_attributes [Cil2cfg.Printer] |
|
define [Lang.F] |
|
define [Model.Registry] |
no redefinition ; circularity protected
|
define [Model.Static] |
|
define [Model.Index] |
|
define_axiomatic [LogicCompiler.Make] |
|
define_lemma [LogicCompiler.Make] |
|
define_lemma [Definitions] |
|
define_logic [LogicCompiler.Make] |
|
define_symbol [Definitions] |
|
define_type [LogicCompiler.Make] |
|
define_type [Definitions] |
|
defined [Context] |
The current value is defined.
|
defs [Letify.Defs] |
|
defs_affine [Letify.Defs] |
|
defs_eq [Letify.Defs] |
|
degree_of_type [VarUsage] |
Dimensions in the type (0 for non-array)
|
del_pred [CfgLib.Make] |
|
delete_script [Proof] |
|
delta [MemVar.Make] |
|
delta_array [Variables_analysis] |
|
delta_array_term [Variables_analysis] |
|
delta_ptr [Variables_analysis] |
|
delta_ptr_term [Variables_analysis] |
|
demon [Model.Static] |
|
demon [Model.Index] |
|
denv [Matrix] |
|
depend [Driver] |
|
depend [Fixpoint.Make] |
|
dependencies [LogicBuiltins] |
Of external theories.
|
dependencies [WpAnnot] |
|
dependencies [Dyncall.CInfo] |
|
deref [Variables_analysis] |
|
descr [Factory] |
|
descr [Vset] |
|
descr [LogicBuiltins] |
|
descr_cfloat [Factory] |
|
descr_cint [Factory] |
|
descr_mheap [Factory] |
|
descr_mtyped [Factory] |
|
descr_mvar [Factory] |
|
descr_setup [Factory] |
|
descriptions [Factory] |
|
detect_provers [ProverWhy3] |
|
detect_why3 [ProverWhy3] |
|
diff [Set.S] |
Set difference.
|
diff [Conditions.Bundle] |
|
diff [Letify.Defs] |
|
dim_of_type [VarUsage] |
|
dimension [Ctypes] |
|
dimension_of_object [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
|
disjoint [Region] |
|
disjoint [Vset] |
|
disjoint_bounds [Vset] |
|
disjoint_fields [Region] |
|
disjoint_indices [Region] |
|
disjoint_vset [Vset] |
|
disjunction [Conditions] |
|
disjunction [Splitter] |
|
dispatch [Prover] |
|
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.
|
dispatch_var [Variables_analysis] |
|
dkey [Calculus.Cfg] |
|
dkey [Driver] |
|
dkey [ProverWhy3] |
|
dkey [ProverCoq] |
|
dkey [ProverErgo] |
|
dkey [Wpo.GOAL] |
|
dkey [WpAnnot] |
|
dkey [WpStrategy] |
|
dkey [Cil2cfg] |
|
dkey [Variables_analysis] |
|
dkey [VarUsage] |
|
dkey [Dyncall] |
|
dkey [Wp_parameters] |
|
do_assigns [CfgWP.VC] |
|
do_assigns_everything [CfgWP.VC] |
|
do_checks [Lang.F] |
|
do_finally [Register] |
|
do_labels [Calculus.Cfg] |
Before storing something at a program point, we have to process the label
at that point.
|
do_lemmas [Generator] |
|
do_list_scheduled [Register] |
|
do_list_scheduled_result [Register] |
|
do_merge [Matrix] |
|
do_prover_detect [Register] |
|
do_wp_check [Register] |
|
do_wp_check_for [Register] |
|
do_wp_check_iter [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_feedback [Register] |
|
do_wpo_start [Register] |
|
dofs [MemVar.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 [MemTyped] |
|
domain [MemVar.Make.Sigma] |
|
domain [MemVar.Make] |
|
domain [MemEmpty] |
|
domain [Sigma.Make] |
|
domain [LogicAssigns.Make] |
|
domain [Conditions] |
|
domain [Letify.Defs] |
|
domain [Letify.Sigma] |
|
domain_alloc [MemVar.Make.Sigma] |
|
domain_mem [MemVar.Make.Sigma] |
|
domain_partition [MemVar.Make.Sigma] |
|
domain_var [MemVar.Make.Sigma] |
|
dot [CfgTypes.Cfg] |
Dump the graph into provided file.
|
dot [Config] |
Dot command name.
|
dot [CfgLib.Make] |
|
driver [LogicBuiltins] |
|
dseq_of_step [Conditions] |
|
dsize [MemVar.Make] |
|
dsloc [LogicAssigns.Make] |
|
dstats [WpReport] |
|
dummy [Wpo.GOAL] |
|
dump [LogicBuiltins] |
|
dump [Conditions] |
|
dump [VarUsage] |
|
dump [LogicUsage] |
Print on output
|
dump_buffer [ProverTask] |
|
dump_file [Wpo.DISK] |
|
dump_lemma [LogicUsage] |
|
dump_logic [LogicUsage] |
|
dump_lvar [VarUsage] |
|
dump_profile [LogicUsage] |
|
dump_scripts [Proof] |
dump_scripts f saves all scripts from the database into file f .
|
dump_type [LogicUsage] |
|
dval [Matrix] |
|
E |
e_add [Lang.F] |
|
e_apply [Letify.Sigma] |
|
e_bigint [Lang.F] |
|
e_eq [Lang.F] |
|
e_fact [Lang.F] |
|
e_fun [Lang.F] |
|
e_hexfloat [Lang.F] |
|
e_int64 [Lang.F] |
|
e_leq [Lang.F] |
|
e_lt [Lang.F] |
|
e_minus_one [Lang.F] |
|
e_mthfloat [Lang.F] |
|
e_neq [Lang.F] |
|
e_one [Lang.F] |
|
e_one_real [Lang.F] |
|
e_opp [Lang.F] |
|
e_prop [Lang.F] |
|
e_props [Lang.F] |
|
e_range [Lang.F] |
e_range a b = b+1-a
|
e_setfield [Lang.F] |
|
e_sum [Lang.F] |
|
e_times [Lang.F] |
|
e_zero [Lang.F] |
|
e_zero_real [Lang.F] |
|
eat [Script] |
|
echo_buffer [ProverTask] |
|
edge_attributes [Cil2cfg.Printer] |
|
edge_dst [Cil2cfg] |
|
edge_key [Cil2cfg] |
|
edge_src [Cil2cfg] |
node and edges relations
|
edge_type [Cil2cfg] |
|
either [Conditions] |
|
either [Dyncall] |
|
elements [Why3_xml] |
|
elements [Set.S] |
Return the list of all elements of the given set.
|
elements [Letify] |
|
emit [Warning] |
Emit a warning in current context.
|
emitter [Variables_analysis] |
|
empty [Indexer.Make] |
|
empty [Mcfg.S] |
|
empty [CfgTypes.Transition] |
|
empty [CfgWP.VC] |
|
empty [CfgDump.VC] |
|
empty [Calculus.Cfg.R] |
|
empty [Set.S] |
The empty set.
|
empty [Map.S] |
The empty map.
|
empty [Wpo.GOAL] |
|
empty [Region] |
|
empty [Vset] |
|
empty [Conditions.Bundle] |
|
empty [Conditions] |
|
empty [Letify.Defs] |
|
empty [Letify.Sigma] |
|
empty [Splitter] |
|
empty [Passive] |
|
empty [Cil2cfg.PMAP] |
|
empty [VarUsage.Occur] |
|
empty [FCMap.S] |
The empty map.
|
empty_acc [WpStrategy] |
|
empty_assigns_info [WpPropId] |
|
empty_database [LogicUsage] |
|
empty_range [Vset] |
|
empty_session [Why3_session] |
|
empty_vc [CfgWP.VC] |
|
end_session [Register] |
|
engine [ProverWhy3] |
|
engine [ProverCoq] |
|
engine [ProverErgo] |
|
entries [Model.Static] |
|
entries [Model.Index] |
|
enumerate [Splitter] |
|
env [Lang.F] |
|
env [Rformat] |
|
env_at [LogicCompiler.Make] |
|
env_chapter [WpReport] |
|
env_let [LogicCompiler.Make] |
|
env_letval [LogicCompiler.Make] |
|
env_property [WpReport] |
|
env_section [WpReport] |
|
env_toplevel [WpReport] |
|
epsilon [Lang] |
|
epsilon [VarUsage.Context] |
|
epsilon [Rformat] |
|
eq_nodes [Cil2cfg.WeiMaoZouChenInput] |
|
eq_nodes [Cil2cfg.LoopInfo] |
|
eq_shift [MemTyped] |
|
eqatom [MemTyped.Layout] |
|
eqmem [MemTyped] |
|
eqp [Lang.F] |
|
eqsort_of_comparison [LogicSemantics.Make] |
|
eqsort_of_type [LogicSemantics.Make] |
|
equal [CfgWP.VC.TARGET] |
|
equal [Set.S] |
equal s1 s2 tests whether the sets s1 and s2 are
equal, that is, contain equal elements.
|
equal [Map.S] |
equal cmp m1 m2 tests whether the maps m1 and m2 are
equal, that is, contain equal keys and associate them with
equal data.
|
equal [MemTyped.Chunk] |
|
equal [MemVar.Make.Chunk] |
|
equal [MemVar.Make.VALLOC] |
|
equal [MemVar.Make.VAR] |
|
equal [MemEmpty.Chunk] |
|
equal [Vset] |
|
equal [Letify.Sigma] |
|
equal [Lang.Fun] |
|
equal [Lang.Field] |
|
equal [Lang.ADT] |
|
equal [Cil2cfg.VL] |
|
equal [RefUsage.Var] |
|
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 [Clabels] |
|
equal [Ctypes.AinfoComparable] |
|
equal [Ctypes] |
|
equal_array [Cvalues] |
|
equal_but [Region] |
|
equal_but_fields [Region] |
|
equal_but_index [Region] |
|
equal_comp [Cvalues] |
|
equal_loc [MemTyped] |
|
equal_obj [LogicAssigns.Code] |
|
equal_obj [CodeSemantics.Make] |
|
equal_object [Cvalues] |
|
equal_typ [CodeSemantics.Make] |
|
equal_typ [Cvalues] |
|
error [Script] |
|
error [Warning] |
|
escaped [String] |
Return a copy of the argument, with special characters
represented by escape sequences, following the lexical
conventions of OCaml.
|
eval [VarUsage.Context] |
|
exists [Set.S] |
exists p s checks if at least one element of
the set satisfies the predicate p .
|
exists [Map.S] |
exists p m checks if at least one binding of the map
satisfy the predicate p .
|
exists [Splitter] |
|
exists [FCMap.S] |
exists p m checks if at least one binding of the map
satisfy the predicate p .
|
exp [CodeSemantics.Make] |
|
exp_binop [CodeSemantics.Make] |
|
exp_compare [LogicSemantics.Make] |
|
exp_diff [LogicSemantics.Make] |
|
exp_equal [LogicSemantics.Make] |
|
exp_handler [CodeSemantics.Make] |
|
exp_node [CodeSemantics.Make] |
|
exp_protected [CodeSemantics.Make] |
|
exp_unop [CodeSemantics.Make] |
|
export [WpReport] |
|
export [Cil2cfg] |
|
export_decl [Mcfg.Export] |
|
export_goal [Mcfg.Export] |
|
export_section [Mcfg.Export] |
|
expr [RefUsage] |
|
expr [VarUsage] |
|
ext_compare [Lang] |
|
extern_f [Lang] |
balance just give a default when link is not specified
|
extern_fp [Lang] |
|
extern_p [Lang] |
|
extern_s [Lang] |
|
extract [Conditions] |
|
extract [Letify.Defs] |
|
extract [Letify] |
|
F |
f_base [MemTyped] |
|
f_bit [Cint] |
|
f_bits [Ctypes] |
|
f_bytes [Ctypes] |
|
f_convert [Ctypes] |
|
f_delta [Cfloat] |
|
f_empty [Vset] |
|
f_epsilon [Cfloat] |
|
f_global [MemTyped] |
|
f_iabs [Cfloat] |
|
f_inter [Vset] |
|
f_land [Cint] |
|
f_lnot [Cint] |
|
f_lor [Cint] |
|
f_lsl [Cint] |
|
f_lsr [Cint] |
|
f_lxor [Cint] |
|
f_mk_addr [MemTyped] |
|
f_model [Cfloat] |
|
f_null [MemTyped] |
|
f_of_int [Cfloat] |
|
f_offset [MemTyped] |
|
f_rabs [Cfloat] |
|
f_range [Vset] |
|
f_range_all [Vset] |
|
f_range_inf [Vset] |
|
f_range_sup [Vset] |
|
f_region [MemTyped] |
|
f_shift [MemTyped] |
|
f_singleton [Vset] |
|
f_sqrt [Cfloat] |
|
f_to_int [Cint] |
|
f_truncate [Cint] |
|
f_union [Vset] |
|
factorize [Conditions.Bundle] |
|
fadd [Cfloat] |
|
failed [VCS] |
|
farray [Lang] |
|
fbinop [Cfloat] |
|
fc [CfgDump.VC] |
|
fconvert [Cfloat] |
|
fcstat [WpReport] |
|
fcup [RefUsage.E] |
|
fcup [RefUsage] |
|
fdiv [Cfloat] |
|
fdx [Ctypes] |
|
field [Memory.Model] |
Return the memory location obtained by field access from a given
memory location
|
field [MemTyped] |
|
field [MemVar.Make] |
|
field [MemEmpty] |
|
field [Cvalues.Logic] |
|
field [Lang] |
|
field [RefUsage] |
|
field [VarUsage.Model] |
|
field_id [Lang] |
|
field_offset [Ctypes] |
|
fields_of_field [Lang] |
|
fields_of_tau [Lang] |
|
file [Wpo.DISK] |
|
file_goal [Wpo.DISK] |
|
file_kf [Wpo.DISK] |
|
file_logerr [Wpo.DISK] |
|
file_logout [Wpo.DISK] |
|
filename_for_prover [VCS] |
|
filenoext [ProverWhy3] |
|
fill [Script] |
|
fill [String] |
String.fill s start len c modifies byte sequence s in place,
replacing len bytes with c , starting at start .
|
filter [Indexer.Make] |
Linear.
|
filter [Set.S] |
filter p s returns the set of all elements in s
that satisfy predicate p .
|
filter [Map.S] |
filter p m returns the map with all the bindings in m
that satisfy predicate p .
|
filter [Proof] |
|
filter [Script] |
|
filter [Splitter] |
|
filter [WpAnnot] |
|
filter [FCMap.S] |
filter p m returns the map with all the bindings in m
that satisfy predicate p .
|
filter_asked [WpAnnot] |
|
filter_assign [WpAnnot] |
|
filter_both [WpStrategy] |
|
filter_configstatus [WpAnnot] |
|
filter_pred [Cleaning] |
|
filter_speconly [WpAnnot] |
|
filter_status [WpAnnot] |
|
filter_type [Cleaning] |
|
find [Calculus.Cfg.R] |
|
find [ProverWhy3] |
|
find [Set.S] |
find x s returns the element of s equal to x (according
to Ord.compare ), or raise Not_found if no such element
exists.
|
find [Map.S] |
find x m returns the current binding of x in m ,
or raises Not_found if no such binding exists.
|
find [Letify.Sigma] |
|
find [Model.Registry] |
|
find [Model.Static] |
|
find [Model.Index] |
|
find [Model.MODELS] |
|
find [Model] |
|
find [Cil2cfg.HEsig] |
|
find [Cil2cfg.HE] |
|
find [Hashtbl.S] |
|
find [Cil2cfg.PMAP] |
|
find [FCMap.S] |
find x m returns the current binding of x in m ,
or raises Not_found if no such binding exists.
|
find [State_builder.Hashtbl] |
Return the current binding of the given key.
|
find_all [Cil2cfg.HEsig] |
|
find_all [Cil2cfg.HE] |
|
find_all [Hashtbl.S] |
|
find_all [State_builder.Hashtbl] |
Return the list of all data associated with the given key.
|
find_and_raise [Cil2cfg.PMAP] |
|
find_behaviors [WpAnnot] |
empty bhv_names means all (whatever ki is)
|
find_call [Dyncall] |
|
find_lemma [Definitions] |
raises Not_found
|
find_lib [LogicBuiltins] |
find a file in the includes of the current drivers
|
find_nonwin_column [ProverCoq] |
|
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.
|
fire [Model.Static] |
|
fire [Model.Index] |
|
first [GuiNavigator] |
|
first_index [MemVar.Make] |
|
fits [MemTyped.Layout] |
|
fix [WTO] |
|
fixpoint [Conditions] |
|
fixpoint [VarUsage] |
|
fixpoint [Fixpoint.Make] |
Computes the least fixpoint solution satifying all added
requirements.
|
fixpoint [WTO] |
Iterate over a weak partial order.
|
flat_concat [Conditions] |
|
flat_cons [Conditions] |
|
flatten_sequence [Conditions] |
|
flayout [MemTyped.Layout] |
|
float_of_int [Cfloat] |
|
floc_path [MemVar.Make] |
|
flow [Wpo] |
|
flt_add [Cfloat] |
|
flt_div [Cfloat] |
|
flt_mul [Cfloat] |
|
flt_rnd [Cfloat] |
|
flt_sqrt [Cfloat] |
|
flush [CfgDump.VC] |
|
flush [Cvalues.Logic] |
|
flush [Warning] |
|
flush [Rformat] |
|
fmap [Fixpoint.Make] |
|
fmemo [Ctypes] |
|
fmul [Cfloat] |
|
focus_of_selection [GuiNavigator] |
|
fold [Set.S] |
fold f s a computes (f xN ... (f x2 (f x1 a))...) ,
where x1 ... xN are the elements of s , in increasing order.
|
fold [Map.S] |
fold f m a computes (f kN dN ... (f k1 d1 a)...) ,
where k1 ... kN are the keys of all bindings in m
(in increasing order), and d1 ... dN are the associated data.
|
fold [Splitter] |
|
fold [Hashtbl.S] |
|
fold [Cil2cfg.PMAP] |
|
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 [State_builder.Hashtbl] |
|
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
|
fold_pred [Cil2cfg] |
|
fold_pred_e [Cil2cfg] |
|
fold_sorted [State_builder.Hashtbl] |
|
fold_succ [Cil2cfg.WeiMaoZouChenInput] |
apply the function on the node successors
|
fold_succ [Cil2cfg.LoopInfo] |
|
fold_succ [Cil2cfg] |
|
fold_succ_e [Cil2cfg] |
|
footprint [MemTyped] |
|
footprint_comp [MemTyped] |
|
fopp [Cfloat] |
|
for_all [Set.S] |
for_all p s checks if all elements of the set
satisfy the predicate p .
|
for_all [Map.S] |
for_all p m checks if all the bindings of the map
satisfy the predicate p .
|
for_all [Splitter] |
|
for_all [FCMap.S] |
for_all p m checks if all the bindings of the map
satisfy the predicate p .
|
formal [LogicCompiler.Make] |
|
frame [LogicSemantics.Make] |
|
frame [LogicCompiler.Make] |
|
frame_copy [LogicSemantics.Make] |
|
frame_copy [LogicCompiler.Make] |
|
framed [MemTyped] |
|
framed [MemVar.Make] |
|
frange [Cfloat] |
|
free [Context] |
Performs the job with local context cleared.
|
freeze [Conditions.Bundle] |
|
fresh_cvar [LogicCompiler.Make] |
|
fresh_lvar [LogicCompiler.Make] |
|
freshen [Lang] |
|
freshvar [Lang] |
|
from_file [Why3_xml] |
returns the list of XML elements from the given file.
|
fsub [Cfloat] |
|
full [Region] |
|
funcall [VarUsage] |
|
funcall_params [VarUsage] |
|
function_param [VarUsage.Context] |
|
funop [Cfloat] |
|
G |
gbranch [CfgWP.VC] |
|
generate [MemTyped.MONOTONIC] |
|
generated_f [Lang] |
|
generated_p [Lang] |
|
get [Indexer.Make] |
raises Not_found.
|
get [Memory.Sigma] |
|
get [Wpo.Results] |
|
get [MemVar.Make.Sigma] |
|
get [Sigma.Make] |
|
get [Cleaning] |
|
get [Lang.Alpha] |
|
get [Model.Registry] |
|
get [Model.Generator] |
|
get [Model.Static] |
|
get [Model.Index] |
|
get [Context] |
Retrieves the current value of the context.
|
get [Cil2cfg] |
|
get [RefUsage.E] |
|
get [Dyncall] |
Returns empty list if there is no specified dynamic call.
|
get [String] |
String.get s n returns the character at index n in string s .
|
get [State_builder.Ref] |
Get the referenced value.
|
get [Fixpoint.Make] |
|
get [CfgLib.Attr] |
Returns default if not found.
|
get_alloc [MemTyped] |
|
get_annots [WpStrategy] |
|
get_asgn_goal [WpStrategy] |
|
get_asgn_hyp [WpStrategy] |
|
get_behav [WpAnnot] |
Select in bhv_list the behavior that has to be processed
according to config and ki current statement.
|
get_behavior_annots [WpAnnot] |
Builds tables that give hypotheses and goals relative to b behavior
for edges of the cfg to consider during wp computation.
|
get_bhv [WpStrategy] |
|
get_both_hyp_goals [WpStrategy] |
|
get_call [Dyncall] |
|
get_call_annots [WpAnnot] |
|
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_kf [Dyncall] |
|
get_called_post_conditions [WpAnnot] |
|
get_called_postconds [WpAnnot] |
|
get_called_preconditions_at [WpAnnot] |
|
get_calls [Dyncall] |
|
get_cfg [WpAnnot] |
|
get_class [Letify] |
|
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_depend [Wpo] |
|
get_descr [Wpo.GOAL] |
|
get_descr [Model] |
|
get_edge_labels [Cil2cfg] |
|
get_edge_next_stmt [Cil2cfg] |
|
get_emitter [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_fct_post_annots [WpAnnot] |
|
get_fct_pre_annots [WpAnnot] |
|
get_file_logerr [Wpo] |
only filename, might not exists
|
get_file_logout [Wpo] |
only filename, might not exists
|
get_files [Wpo] |
|
get_formal [VarUsage] |
|
get_frame [LogicSemantics.Make] |
|
get_frame [LogicCompiler.Make] |
|
get_function_strategies [WpAnnot] |
|
get_gamma [Lang] |
|
get_gid [Wpo] |
Dynamically exported
|
get_goal_only [WpStrategy] |
|
get_hyp_only [WpStrategy] |
|
get_hypotheses [Lang] |
|
get_id [Model] |
|
get_id_prop_strategies [WpAnnot] |
|
get_iloop_header [Cil2cfg.WeiMaoZouChenInput] |
get the node innermost loop header if any
|
get_iloop_header [Cil2cfg.LoopInfo] |
|
get_includes [Wp_parameters] |
|
get_index [Wpo] |
|
get_induction [WpPropId] |
Quite don't understand what is going on here...
|
get_induction_labels [LogicUsage] |
Given an inductive phi{...A...} .
|
get_int [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_kind_for_tk [WpPropId] |
|
get_label [Wpo] |
|
get_last [MemTyped] |
|
get_lemma [LogicUsage] |
|
get_link [Conditions] |
|
get_logfile [Wpo] |
|
get_loop_annots [WpAnnot] |
Returns the annotations for the three edges of the loop node: loop_entry : goals for the edge entering in the loop, loop_back : goals for the edge looping to the entry point, loop_core : fix-point hypothesis for the edge starting the loop core
|
get_loop_stmt [WpPropId] |
find the outer loop in which the stmt is.
|
get_model [Wpo] |
|
get_model [Model] |
Current model
|
get_model_id [Wpo] |
|
get_model_name [Wpo] |
|
get_name [LogicUsage] |
|
get_named_bhv [WpAnnot] |
find the behavior named name in the list
|
get_node [Cil2cfg] |
|
get_only_succ [Calculus.Cfg] |
|
get_option [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_pool [Lang] |
|
get_pos [Cil2cfg.WeiMaoZouChenInput] |
get the previously stored position of the node or 0 if nothing has been
stored
|
get_pos [Cil2cfg.LoopInfo] |
|
get_pos_if_traversed [Cil2cfg.WeiMaoZouChenInput] |
get the previously stored position of the node if any, or None
if set_pos hasn't been called already for this node.
|
get_pos_if_traversed [Cil2cfg.LoopInfo] |
|
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_precond_strategies [WpAnnot] |
|
get_proof [Wpo] |
|
get_prop_id_name [WpPropId.Names] |
returns a unique name identifying the property.
|
get_property [WpReport] |
|
get_property [Wpo] |
Dynamically exported
|
get_propid [WpPropId] |
Unique identifier of prop_id
|
get_prover [WpReport] |
|
get_prover_names [Register] |
|
get_pstat [Register] |
|
get_result [Wpo] |
Dynamically exported.
|
get_results [Wpo] |
|
get_section [WpReport] |
|
get_steps [Wpo] |
|
get_stmt_annots [WpAnnot] |
|
get_stmt_node [Cil2cfg] |
In some cases (goto for instance) we have to create a node before having
processed if through cfg_stmt .
|
get_strategies [WpAnnot] |
|
get_subgraph [Cil2cfg.Printer] |
|
get_switch_edges [Cil2cfg] |
similar to succ_e g v
but give the switch cases and the default edge
|
get_term [MemVar.Make] |
|
get_test_edges [Cil2cfg] |
Get the edges going out a test node with the then branch first
|
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_var [MemVar.Make] |
|
get_variables [Lang] |
|
get_weakest_precondition [Calculus.Cfg] |
|
get_wp_edge [Calculus.Cfg] |
|
gid [Wpo] |
|
glinker [Conditions] |
|
global [Memory.Model] |
Given a pointer value p , assumes this pointer p (when valid)
is allocated outside the function frame under analysis.
|
global [MemTyped] |
|
global [MemVar.Make] |
|
global [MemEmpty] |
|
global_axioms [WpStrategy] |
|
gmap [CfgWP.VC] |
|
gmerge [CfgWP.VC] |
|
goal_of_selection [GuiNavigator] |
|
goal_to_select [WpAnnot] |
|
goals_of_property [Wpo] |
All POs related to a given property.
|
graph_attributes [Cil2cfg.Printer] |
|
group [Splitter] |
|
group_vc [CfgWP.VC] |
|
guards [LogicSemantics.Make] |
|
guards [LogicCompiler.Make] |
|
H |
h [Model.MODELS] |
|
handle [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 [CfgWP.VC] |
|
has_init [CfgDump.VC] |
|
has_ltype [Cvalues] |
|
has_prefix [Clabels] |
|
hash [Memory.Chunk] |
|
hash [CfgWP.VC.TARGET] |
|
hash [MemTyped.Chunk] |
|
hash [MemVar.Make.Chunk] |
|
hash [MemVar.Make.VALLOC] |
|
hash [MemVar.Make.VAR] |
|
hash [MemEmpty.Chunk] |
|
hash [Cstring.STR] |
|
hash [Lang.Fun] |
|
hash [Lang.Field] |
|
hash [Lang.ADT] |
|
hash [Cil2cfg.VL] |
|
hash [RefUsage.Var] |
|
hash [Ctypes.AinfoComparable] |
|
hash [Ctypes] |
|
havoc [Memory.Sigma] |
|
havoc [MemTyped] |
|
havoc [MemVar.Make.Sigma] |
|
havoc [Sigma.Make] |
|
havoc_any [Memory.Sigma] |
|
havoc_any [MemVar.Make.Sigma] |
|
havoc_any [Sigma.Make] |
|
havoc_chunk [Memory.Sigma] |
|
havoc_chunk [MemVar.Make.Sigma] |
|
havoc_chunk [Sigma.Make] |
|
havoc_range [MemTyped] |
|
head [Proof] |
|
heap_case [LogicCompiler.Make] |
|
help_array_reference_pattern_term [Variables_analysis] |
|
help_by_array_reference_pattern [Variables_analysis] |
|
hex_of_float [Lang.F] |
|
hints_for [Proof] |
|
hooks [Wprop.Indexed] |
|
host [RefUsage] |
|
howto_marshal [State_builder.S] |
howto_marshal marshal unmarshal registers a custom couple of
functions (marshal, unmarshal) to be used for serialization.
|
hsh [Ctypes] |
|
hsrc [CfgWP.VC.TARGET] |
|
hypotheses [Conditions] |
|
hypotheses [Lang] |
|
I |
i_bits [Ctypes] |
size in bits
|
i_bytes [Ctypes] |
size in bytes
|
i_convert [Ctypes] |
|
iadd [Cint] |
|
ibinop [Cint] |
|
icon [GuiGoal] |
|
iconvert [Cint] |
|
iconvert_unsigned [Cint] |
|
id [CfgTypes.Cfg] |
|
id [LogicBuiltins] |
|
id [Matrix] |
unique w.r.t equal
|
id [Fixpoint.Make] |
|
id [CfgLib.Make] |
|
ident [Factory] |
|
ident [Driver] |
|
ident [Script] |
|
ident_names [WpPropId] |
|
identified_term [VarUsage] |
|
identify_loops [Cil2cfg.WeiMaoZouChen] |
|
idents [Script] |
|
idiv [Cint] |
|
idp [Lang.F] |
|
idx [Ctypes] |
|
if_else [Splitter] |
|
if_then [Splitter] |
|
image [CfgLib.Transform] |
|
imemo [Ctypes] |
|
imod [Cint] |
|
imul [Cint] |
|
in_frame [LogicSemantics.Make] |
|
in_frame [LogicCompiler.Make] |
|
in_pred [LogicCompiler.Make] |
|
in_range [Vset] |
|
in_reads [LogicCompiler.Make] |
|
in_size [Vset] |
|
in_spec [VarUsage.Context] |
|
in_term [LogicCompiler.Make] |
|
in_wenv [CfgWP.VC] |
|
included [Memory.Model] |
Return the formula that tests if two segment are included
|
included [MemTyped] |
|
included [MemVar.Make] |
|
included [MemEmpty] |
|
included [LogicSemantics.Make] |
|
included [Cvalues.Logic] |
|
included_delta [MemVar.Make] |
|
included_sloc [Cvalues.Logic] |
|
incr_addr_taken [Variables_analysis] |
|
index [Indexer.Make] |
raise Not_found.
|
index [MemVar.Make] |
|
index [String] |
String.index s c returns the index of the first
occurrence of character c in string s .
|
index_from [String] |
String.index_from s i c returns the index of the
first occurrence of character c in string s after position i .
|
index_of_lemma [GuiNavigator] |
|
index_wpo [Wpo] |
|
infoprover [Lang] |
same information for all the provers
|
init [CfgDump.VC] |
|
init [Cil2cfg.WeiMaoZouChenInput] |
build a new env from a graph,
and also return the entry point of the graph which has to be unique.
|
init [Cil2cfg.LoopInfo] |
|
init [String] |
String.init n f returns a string of length n , with character
i initialized to the result of f i (called in increasing
index order).
|
init_cfg [Cil2cfg] |
|
init_const [Mcfg.S] |
the (entire) variable has its initial value
|
init_const [CfgWP.VC] |
|
init_const [CfgDump.VC] |
|
init_global_variable [Calculus.Cfg] |
|
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 [CfgWP.VC] |
|
init_range [CfgDump.VC] |
|
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 [CfgWP.VC] |
|
init_value [CfgDump.VC] |
|
input_string [Driver] |
|
insert_loop_node [Cil2cfg] |
|
install_builtins [Cint] |
|
instance [Factory] |
|
instance_of [CodeSemantics.Make] |
|
instances [Factory] |
|
instructions [GuiSource] |
|
int64_max [Ctypes] |
|
int_attribute [Why3_session] |
|
int_attribute_def [Why3_session] |
|
int_of_loc [Memory.Model] |
Cast a memory location into an integer of the given type
|
int_of_loc [MemTyped] |
|
int_of_loc [MemVar.Make] |
|
int_of_loc [MemEmpty] |
|
inter [Set.S] |
Set intersection.
|
inter [Cvalues.Logic] |
|
inter [Vset] |
|
internal_function_behaviors [WpAnnot] |
|
intersect [Conditions] |
|
intersect [Lang.F] |
|
intersect_vc [CfgWP.VC] |
|
intersectp [Lang.F] |
|
introduction [CfgWP.VC] |
|
introduction_bit_test_positive [Cint] |
|
intros [CfgWP.VC] |
|
intros [Conditions] |
|
invalid [VCS] |
|
iopp [Cint] |
|
ip_lemma [LogicUsage] |
|
ip_of_axiomatic [LogicUsage] |
|
irange [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 ).
|
isVarTypePointerType [Variables_analysis] |
|
is_absurd [Conditions] |
|
is_annot_for_config [WpAnnot] |
(see test_behav_res above).
|
is_array [Cvalues.STRUCTURAL] |
|
is_assigns [WpPropId] |
|
is_back_edge [Cil2cfg] |
|
is_call_assigns [WpPropId] |
|
is_char [Ctypes] |
|
is_check [Wpo] |
|
is_check [WpPropId] |
|
is_cint [Cint] |
Raises Not_found if not.
|
is_cint_map [Cint] |
|
is_collected [CfgWP.VC] |
|
is_composed [WpAnnot] |
whether a proof needs several lemma to be complete
|
is_computed [State_builder.S] |
Returns true iff the registered state will not change again for the
given project (default is current () ).
|
is_computing [Wpo] |
|
is_cond_true [Conditions] |
|
is_constrained [Cvalues] |
|
is_constrained_comp [Cvalues] |
|
is_default [LogicBuiltins] |
|
is_default_behavior [WpStrategy] |
|
is_delta [Cfloat] |
|
is_empty [CfgWP.VC] |
|
is_empty [Set.S] |
Test whether a set is empty or not.
|
is_empty [Map.S] |
Test whether a map is empty or not.
|
is_empty [Proof] |
|
is_empty [Conditions.Bundle] |
|
is_empty [Cil2cfg.PMAP] |
|
is_empty [FCMap.S] |
Test whether a map is empty or not.
|
is_empty_behavior [WpAnnot] |
|
is_empty_spec [WpAnnot] |
|
is_eq0 [Cfloat] |
|
is_equal [Lang.F] |
|
is_err [ProverTask] |
|
is_false [Cvalues] |
p ? 0 : 1
|
is_false [Cleaning] |
|
is_float [Cvalues.CASES] |
|
is_formal_var_type [Variables_analysis] |
|
is_framed [Memory.Chunk] |
Whether the Chunk is local to a function.
|
is_framed [MemTyped.Chunk] |
|
is_framed [MemVar.Make.Chunk] |
|
is_framed [MemVar.Make.VALLOC] |
|
is_framed [MemVar.Make.VAR] |
|
is_framed [MemEmpty.Chunk] |
|
is_framed_var [MemVar.Make] |
|
is_global_axiomatic [LogicUsage] |
|
is_gui [Config] |
Is the Frama-C GUI running?
|
is_int [Cvalues.CASES] |
|
is_irreducible [Cil2cfg.LoopInfo] |
|
is_le0 [Cfloat] |
|
is_leq [Cint] |
|
is_lformal [Variables_analysis] |
|
is_loop_preservation [WpPropId] |
|
is_lt0 [Cfloat] |
|
is_main_init [WpStrategy] |
The function is the main entry point AND it is not a lib entry
|
is_mem [MemVar.Make] |
|
is_memvar [Variables_analysis] |
|
is_model [Cfloat] |
|
is_model_defined [Model] |
|
is_negative [Cint] |
|
is_next_edge [Cil2cfg] |
|
is_nil [CfgTypes.Cfg] |
|
is_nil [CfgLib.Make] |
|
is_null [Memory.Model] |
Return the formula that check if a given location is null
|
is_null [MemTyped] |
|
is_null [MemVar.Make] |
|
is_null [MemEmpty] |
|
is_null [Cvalues] |
|
is_obj [Cvalues.STRUCTURAL] |
|
is_object [Cvalues] |
|
is_opt [ProverTask] |
|
is_out [ProverTask] |
|
is_out [Wp_parameters] |
|
is_overloaded [LogicUsage] |
|
is_pass1 [Calculus.Cfg.R] |
|
is_pfalse [Lang.F] |
|
is_pointer [MemVar.Make.VAR] |
|
is_pointer [Cvalues.CASES] |
|
is_pointer [Ctypes] |
|
is_positive_or_null [Cint] |
|
is_proved [WpAnnot] |
wether all partial proofs have been accumulated or not
|
is_ptrue [Lang.F] |
|
is_pure_logic [Variables_analysis] |
|
is_record [Cvalues.STRUCTURAL] |
|
is_recursive [LogicCompiler.Make] |
|
is_recursive [LogicUsage] |
|
is_ref [MemVar.Make] |
|
is_ref [Variables_analysis] |
|
is_requires [WpPropId] |
|
is_rte_generated [GuiSource] |
|
is_rte_precond [GuiSource] |
|
is_seq_true [Conditions] |
|
is_single [Cvalues.Logic] |
|
is_stopeffect [CfgWP.VC] |
|
is_to_cint [Cint] |
|
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 [CfgWP.VC] |
|
is_trivial [Wpo.VC_Annot] |
|
is_trivial [Wpo.VC_Lemma] |
|
is_trivial [Wpo.GOAL] |
|
is_trivial [Wpo] |
|
is_trivial [Conditions] |
|
is_true [Cvalues] |
p ? 1 : 0
|
is_true [Conditions.Bundle] |
|
is_true [Cleaning] |
|
is_typ [Cvalues.STRUCTURAL] |
|
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_var [Cleaning] |
|
is_verdict [Register] |
|
is_verdict [Wpo] |
true if the result is meaningfull (Valid, Unknown or Timeout)
|
is_void [Ctypes] |
|
is_zero [CodeSemantics.Make] |
|
is_zero [Lang.F] |
|
is_zero_float [CodeSemantics.Make] |
|
is_zero_int [CodeSemantics.Make] |
|
is_zero_ptr [CodeSemantics.Make] |
|
is_zero_range [CodeSemantics.Make] |
|
isub [Cint] |
|
iter [Indexer.Make] |
Linear.
|
iter [Memory.Sigma] |
|
iter [CfgTypes.Cfg] |
|
iter [CfgTypes.Transition] |
|
iter [Set.S] |
iter f s applies f in turn to all elements of s .
|
iter [Map.S] |
iter f m applies f to all bindings in map m .
|
iter [Wpo] |
|
iter [MemVar.Make.Sigma] |
|
iter [Sigma.Make] |
|
iter [Letify.Sigma] |
|
iter [Letify] |
|
iter [Splitter] |
|
iter [Lang.Alpha] |
|
iter [Model.Registry] |
|
iter [Model.Static] |
|
iter [Model.Index] |
|
iter [Model.MODELS] |
|
iter [Model] |
|
iter [Hashtbl.S] |
|
iter [Cil2cfg.PMAP] |
|
iter [FCMap.S] |
iter f m applies f to all bindings in map m .
|
iter [String] |
String.iter f s applies function f in turn to all
the characters of s .
|
iter [State_builder.Hashtbl] |
|
iter [CfgLib.Labels] |
|
iter [CfgLib.Attr] |
|
iter [CfgLib.Make] |
|
iter2 [Memory.Sigma] |
|
iter2 [MemVar.Make.Sigma] |
|
iter2 [Sigma.Make] |
|
iter_checks [Lang.F] |
|
iter_edges [Cil2cfg] |
|
iter_edges_e [Cil2cfg.Printer] |
|
iter_fct [Generator] |
|
iter_ip [GuiNavigator] |
|
iter_ips [GuiNavigator] |
|
iter_kf [GuiNavigator] |
|
iter_kf [Generator] |
|
iter_lemmas [LogicUsage] |
|
iter_libs [LogicBuiltins] |
|
iter_nodes [Cil2cfg] |
|
iter_on_goals [Wpo] |
Dynamically exported.
|
iter_pred [CfgTypes.Cfg] |
Iterate over pred
|
iter_pred [CfgLib.Make] |
|
iter_pred_e [Cil2cfg] |
|
iter_session [Register] |
|
iter_sorted [Model.Registry] |
|
iter_sorted [Model.Static] |
|
iter_sorted [Model.Index] |
|
iter_sorted [State_builder.Hashtbl] |
|
iter_stat [WpReport] |
generic iterator
|
iter_succ [CfgTypes.Cfg] |
Iterate over succ
|
iter_succ [Cil2cfg] |
|
iter_succ [CfgLib.Make] |
|
iter_table [LogicBuiltins] |
|
iter_vertex [Cil2cfg.Printer] |
|
iteri [Indexer.Make] |
Linear.
|
iteri [String] |
Same as String.iter , but the
function is applied to the index of the element as first argument
(counting from 0), and the character itself as second argument.
|
iunop [Cint] |
|
J |
job [Wp_parameters] |
|
job_key [Register] |
|
join [Memory.Sigma] |
pairwise equal
|
join [MemVar.Make.Sigma] |
|
join [Sigma.Make] |
|
join [Passive] |
|
join_with [CfgWP.VC] |
|
K |
kernel_functions_separation_hyps [Variables_analysis] |
|
key [Driver] |
|
key [Script] |
|
key_of_chunk [MemTyped.Chunk] |
|
keywords [Driver] |
|
kf_context [Wpo] |
|
kf_of_selection [GuiPanel] |
|
kind [Driver] |
|
kind_of_formal [Variables_analysis] |
|
kind_of_property [GuiSource] |
|
kind_order [WpPropId] |
|
kind_to_select [WpAnnot] |
|
kinstr_hints [WpPropId] |
|
knode [CfgDump.VC] |
|
L |
l_and [Cint] |
|
l_lsl [Cint] |
|
l_lsr [Cint] |
|
l_not [Cint] |
|
l_or [Cint] |
|
l_xor [Cint] |
|
label [Mcfg.S] |
|
label [CfgWP.VC] |
|
label [CfgDump.VC] |
|
label [CfgLib.Labels] |
Retrieve (or create) the node associated to the label.
|
label_of_kind [WpPropId] |
|
label_of_prop_id [WpPropId] |
Short description of the kind of PO
|
labels_assert_after [NormAtLabels] |
|
labels_assert_before [NormAtLabels] |
|
labels_axiom [NormAtLabels] |
|
labels_empty [NormAtLabels] |
|
labels_fct_assigns [NormAtLabels] |
|
labels_fct_post [NormAtLabels] |
|
labels_fct_pre [NormAtLabels] |
|
labels_loop_assigns [NormAtLabels] |
|
labels_loop_inv [NormAtLabels] |
|
labels_predicate [NormAtLabels] |
|
labels_stmt_assigns [NormAtLabels] |
|
labels_stmt_post [NormAtLabels] |
|
labels_stmt_pre [NormAtLabels] |
|
ladder [WpReport] |
|
language_of_name [VCS] |
|
language_of_prover [VCS] |
|
language_of_prover_name [VCS] |
|
layout [MemTyped.Layout] |
|
ldomain [Cvalues] |
|
lemma [LogicSemantics.Make] |
|
lemma [LogicCompiler.Make] |
|
lemma_id [Lang] |
|
lemma_of_global [LogicUsage] |
|
lemmas [GuiSource] |
|
length [Splitter] |
|
length [Hashtbl.S] |
|
length [String] |
Return the length (number of characters) of the given string.
|
length [State_builder.Hashtbl] |
Length of the table.
|
leq [Lang.F.ZInteger] |
|
leq [VarUsage.Usage] |
|
leq [Fixpoint.Domain] |
|
leq_box [VarUsage] |
|
letify [Conditions] |
|
letify_assume [Conditions] |
|
letify_case [Conditions] |
|
letify_seq [Conditions] |
|
letify_step [Conditions] |
|
letify_type [Conditions] |
|
libdir [Config] |
Directory where the Frama-C kernel library is.
|
library [MemTyped] |
|
library [Vset] |
|
library [Cfloat] |
|
library [Cint] |
|
lift [Vset] |
|
lift [Lang.F] |
|
lift_add [Vset] |
|
lift_sub [Vset] |
|
lift_vset [Vset] |
|
link [CfgDump.VC] |
|
link [Driver] |
|
link [Cfloat] |
|
linker [Conditions] |
|
linkstring [Driver] |
|
list [Wpo.Results] |
|
literal [Memory.Model] |
Return the memory location of a constant string,
the id is a unique identifier.
|
literal [MemTyped] |
|
literal [MemVar.Make] |
|
literal [MemEmpty] |
|
literal [Letify.Split] |
|
lkind [LogicBuiltins] |
|
load [Memory.Model] |
Return the value of the object of the given type at the given
location in the given memory state
|
load [Driver] |
|
load [MemTyped] |
|
load [MemVar.Make] |
|
load [MemEmpty] |
|
load [Cvalues.Logic] |
|
load [RefUsage] |
|
load [VarUsage.Context] |
|
load [VarUsage.Model] |
|
load_driver [Driver] |
Memoized loading of drivers according to current
WP options.
|
load_file [Why3_session] |
|
load_goal [Why3_session] |
|
load_ident [Why3_session] |
|
load_loc [LogicSemantics.Make] |
|
load_option [Why3_session] |
|
load_session [Why3_session] |
|
load_theory [Why3_session] |
|
loaded [Driver] |
|
loadrec [MemTyped] |
|
loadscripts [Proof] |
Load scripts from -wp-script f .
|
loadsloc [Cvalues.Logic] |
|
loadvalue [MemTyped] |
|
loc [Cvalues.Logic] |
|
loc [Splitter] |
|
loc_compare [MemTyped] |
|
loc_compare [MemVar.Make] |
|
loc_diff [Memory.Model] |
Compute the length in bytes between two memory locations
|
loc_diff [MemTyped] |
|
loc_diff [MemVar.Make] |
|
loc_diff [MemEmpty] |
|
loc_eq [Memory.Model] |
|
loc_eq [MemTyped] |
|
loc_eq [MemVar.Make] |
|
loc_eq [MemEmpty] |
|
loc_leq [Memory.Model] |
Memory location comparisons
|
loc_leq [MemTyped] |
|
loc_leq [MemVar.Make] |
|
loc_leq [MemEmpty] |
|
loc_lt [Memory.Model] |
|
loc_lt [MemTyped] |
|
loc_lt [MemVar.Make] |
|
loc_lt [MemEmpty] |
|
loc_neq [Memory.Model] |
|
loc_neq [MemTyped] |
|
loc_neq [MemVar.Make] |
|
loc_neq [MemEmpty] |
|
loc_of_exp [CodeSemantics.Make] |
|
loc_of_int [Memory.Model] |
Cast a term representing a pointer to a c_object into a memory
location
|
loc_of_int [MemTyped] |
|
loc_of_int [MemVar.Make] |
|
loc_of_int [MemEmpty] |
|
loc_of_lhost [CodeSemantics.Make] |
|
loc_of_offset [CodeSemantics.Make] |
|
loc_of_term [LogicSemantics.Make] |
|
local [Lang] |
|
locals [Conditions] |
|
locate_error [ProverErgo] |
|
location [ProverTask] |
|
locseg [MemVar.Make] |
|
logic [LogicSemantics.Make] |
|
logic [LogicCompiler.Make] |
|
logic [LogicBuiltins] |
|
logic_body [VarUsage] |
|
logic_call [VarUsage] |
|
logic_constant [Cvalues] |
|
logic_frame [LogicCompiler.Make] |
|
logic_id [Lang] |
|
logic_info [Lang] |
|
logic_lemma [LogicUsage] |
|
logic_link [Driver] |
|
logic_of_value [LogicSemantics.Make] |
|
logic_param [VarUsage.Context] |
|
logic_param_memory_info [Variables_analysis] |
|
logic_var [LogicSemantics.Make] |
|
logic_var [LogicCompiler.Make] |
|
lookup [LogicBuiltins] |
|
lookup [Clabels] |
lookup bindings lparam retrieves the actual label
for the label in bindings for label parameter lparam .
|
lookup_name [Clabels] |
|
loop [WTO] |
|
loop_entry [Mcfg.S] |
|
loop_entry [CfgWP.VC] |
|
loop_entry [CfgDump.VC] |
|
loop_head_label [Clabels] |
|
loop_nodes [Cil2cfg] |
|
loop_step [Mcfg.S] |
|
loop_step [CfgWP.VC] |
|
loop_step [CfgDump.VC] |
|
loop_with_cut [Calculus.Cfg] |
|
lowercase [String] |
Return a copy of the argument, with all uppercase letters
translated to lowercase, including accented letters of the ISO
Latin-1 (8859-1) character set.
|
lval [CodeSemantics.Make] |
|
lval_hints [WpPropId] |
|
lval_host [VarUsage] |
|
lval_offset [VarUsage] |
|
lval_option [VarUsage] |
|
lvalue [RefUsage] |
|
lvalue [VarUsage] |
|
M |
m_int [MemTyped] |
|
main [Register] |
|
main [Factory] |
|
make [GuiNavigator] |
|
make [Wpo.GOAL] |
|
make [String] |
String.make n c returns a fresh string of length n ,
filled with the character c .
|
make_c_float [Ctypes] |
|
make_c_int [Ctypes] |
|
make_fun_float [Cfloat] |
|
make_fun_int [Cint] |
|
make_gui_dir [Wp_parameters] |
|
make_oblig [CfgWP.VC] |
|
make_output_dir [Wp_parameters] |
|
make_pred_float [Cfloat] |
|
make_pred_int [Cint] |
|
make_script [ProverCoq] |
|
make_tmp_dir [Wp_parameters] |
|
make_trivial [CfgWP.VC] |
|
make_type [Datatype.Hashtbl] |
|
make_vcqs [CfgWP.VC] |
|
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 [Cvalues.Logic] |
|
map [Vset] |
|
map [Conditions.Bundle] |
|
map [Splitter] |
|
map [Cil2cfg.PMAP] |
|
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 [String] |
String.map f s applies function f in turn to all the
characters of s (in increasing index order) and stores the
results in a new string that is returned.
|
map [Fixpoint.Make] |
|
map_infoprover [Lang] |
|
map_l2t [Cvalues.Logic] |
|
map_lift [Cvalues.Logic] |
|
map_loc [Cvalues.Logic] |
|
map_logic [Cvalues] |
|
map_opp [Cvalues.Logic] |
|
map_opp [Vset] |
|
map_opt [Vset] |
|
map_sloc [Cvalues] |
|
map_t2l [Cvalues.Logic] |
|
map_value [Cvalues] |
|
map_vset [Vset] |
|
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.
|
mapi [String] |
String.mapi f s calls f with each character of s and its
index (in increasing index order) and stores the results in a new
string that is returned.
|
mark [CfgWP.VC] |
|
mark [Splitter] |
|
mark_as_computed [State_builder.S] |
Indicate that the registered state will not change again for the
given project (default is current () ).
|
mark_e [Lang.F] |
|
mark_loops [Cil2cfg] |
|
mark_p [Lang.F] |
|
mark_seq [Conditions] |
|
mark_vars [Lang.F] |
|
marker [Lang.F] |
|
marks [CfgTypes.Cfg] |
Create new markers
|
marks [CfgLib.Make] |
|
masked [Lang] |
|
match_fun [Cint] |
|
match_integer [Cint] |
|
match_integer_arg1 [Cint] |
|
match_integer_extraction [Cint] |
|
match_positive_integer [Cint] |
|
match_positive_integer_arg2 [Cint] |
|
match_power2 [Cint] |
|
match_power2_extraction [Cint] |
|
match_ufun [Cint] |
|
matches [Proof] |
|
matrix [Definitions] |
|
max_binding [Map.S] |
|
max_binding [FCMap.S] |
|
max_elt [Set.S] |
Same as Set.S.min_elt , but returns the largest element of the
given set.
|
max_elt [FCSet.S] |
Same as , but returns the largest element of the
given set.
|
mem [Indexer.Make] |
Log complexity.
|
mem [Memory.Sigma] |
|
mem [Set.S] |
mem x s tests whether x belongs to the set s .
|
mem [Map.S] |
mem x m returns true if m contains a binding for x ,
and false otherwise.
|
mem [MemVar.Make.Sigma] |
|
mem [Sigma.Make] |
|
mem [Letify.Sigma] |
|
mem [Model.Registry] |
|
mem [Model.Static] |
|
mem [Model.Index] |
|
mem [Model.MODELS] |
|
mem [Hashtbl.S] |
|
mem [Cil2cfg.PMAP] |
|
mem [FCMap.S] |
mem x m returns true if m contains a binding for x ,
and false otherwise.
|
mem [Wprop.Indexed2] |
|
mem [State_builder.Hashtbl] |
|
mem [Wprop.Indexed] |
|
mem_at [LogicSemantics.Make] |
|
mem_at [LogicCompiler.Make] |
|
mem_at_frame [LogicSemantics.Make] |
|
mem_at_frame [LogicCompiler.Make] |
|
mem_frame [LogicSemantics.Make] |
|
mem_frame [LogicCompiler.Make] |
|
member [Vset] |
|
memo [Datatype.Hashtbl] |
memo tbl k f returns the binding of k in tbl .
|
memo [State_builder.Hashtbl] |
Memoization.
|
memoize [Model.Registry] |
with circularity protection
|
memoize [Model.Static] |
|
memoize [Model.Index] |
|
memories [MemTyped] |
|
merge [Memory.Sigma] |
|
merge [Mcfg.S] |
|
merge [CfgWP.VC] |
|
merge [CfgDump.VC] |
|
merge [Map.S] |
merge f m1 m2 computes a map whose keys is a subset of keys of m1
and of m2 .
|
merge [MemVar.Make.Sigma] |
|
merge [Sigma.Make] |
|
merge [Region] |
|
merge [Conditions] |
|
merge [Letify.Defs] |
|
merge [Splitter] |
|
merge [Matrix] |
|
merge [VarUsage.Usage] |
|
merge [FCMap.S] |
merge f m1 m2 computes a map whose keys is a subset of keys of m1
and of m2 .
|
merge [Ctypes] |
|
merge [CfgLib.Attr] |
Update with old value.
|
merge_acc [WpStrategy] |
|
merge_all [Splitter] |
|
merge_all_vcs [CfgWP.VC] |
|
merge_assign_info [WpPropId] |
|
merge_box [VarUsage] |
|
merge_calls [WpStrategy] |
|
merge_fields [Region] |
|
merge_op [CfgLib.Attr] |
Helper for merge with a binary operator.
|
merge_sigma [CfgWP.VC] |
|
merge_vc [CfgWP.VC] |
|
merge_vcs [CfgWP.VC] |
|
merge_with [VarUsage.Occur] |
|
merged [CfgLib.Attr] |
Helper for merge and finally get .
|
merged_op [CfgLib.Attr] |
Helper for merged with a binary operator.
|
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 [Set.S] |
Return the smallest element of the given set
(with respect to the Ord.compare ordering), or raise
Not_found if the set is empty.
|
min_elt [FCSet.S] |
Return the smallest element of the given set
(with respect to the Ord.compare ordering), or raise
Not_found if the set is empty.
|
missing_rte [WpAnnot] |
|
mk_annot_id [WpPropId] |
|
mk_annot_ids [WpPropId] |
|
mk_assert_id [WpPropId] |
|
mk_assigns_info [WpPropId] |
|
mk_axiom_info [WpPropId] |
|
mk_bhv_from_id [WpPropId] |
\from property of function or statement behavior assigns
|
mk_call_pre_id [WpAnnot] |
|
mk_call_pre_id [WpPropId] |
mk_call_pre_id called_kf s_call called_pre
|
mk_check [WpPropId] |
|
mk_code_annot_ids [WpPropId] |
|
mk_compl_bhv_id [WpPropId] |
complete behaviors property.
|
mk_decrease_id [WpPropId] |
|
mk_disj_bhv_id [WpPropId] |
disjoint behaviors property.
|
mk_establish_id [WpPropId] |
Invariant establishment
|
mk_fct_assigns_id [WpPropId] |
function assigns
|
mk_fct_from_id [WpPropId] |
|
mk_fct_post_id [WpPropId] |
|
mk_init_assigns [WpPropId] |
|
mk_inv_hyp_id [WpPropId] |
Invariant used as hypothesis
|
mk_kf_any_assigns_info [WpPropId] |
|
mk_kf_assigns_desc [WpPropId] |
|
mk_lemma_id [WpPropId] |
axiom identification
|
mk_logic_label [Clabels] |
create a virtual label to a statement (it can have no label)
|
mk_loop_any_assigns_info [WpPropId] |
|
mk_loop_assigns_desc [WpPropId] |
|
mk_loop_assigns_id [WpPropId] |
|
mk_loop_from_id [WpPropId] |
\from property of loop assigns
|
mk_loop_label [Clabels] |
|
mk_part [WpPropId] |
mk_part pid (k, n) build the identification for the k/n part of pid .
|
mk_pre_id [WpPropId] |
|
mk_pred_info [WpPropId] |
|
mk_preserve_id [WpPropId] |
Invariant preservation
|
mk_prop [WpPropId] |
|
mk_property [WpPropId] |
|
mk_stmt_any_assigns_info [WpPropId] |
|
mk_stmt_assigns_desc [WpPropId] |
|
mk_stmt_assigns_id [WpPropId] |
|
mk_stmt_label [Clabels] |
|
mk_stmt_post_id [WpPropId] |
|
mk_strategy [WpStrategy] |
|
mk_var_decr_id [WpPropId] |
Variant decrease
|
mk_var_pos_id [WpPropId] |
Variant positive
|
mk_variant_properties [WpStrategy] |
|
mload [MemVar.Make] |
|
mloc [MemVar.Make] |
|
mloc_of_loc [MemVar.Make] |
|
mode_of_prover_name [VCS] |
|
model [Cvalues.CASES] |
|
model [Cfloat] |
|
model [Cint] |
|
model [Model] |
|
model_int [Cvalues.STRUCTURAL] |
|
models [Cfloat] |
|
module_name [Dyncall.PInfo] |
|
most_suitable [Proof] |
|
move [LogicSemantics.Make] |
|
move [LogicCompiler.Make] |
|
mstored [MemVar.Make] |
|
N |
name [MemTyped.Chunk] |
|
name [State_builder.S] |
|
name [Model.Data] |
|
name [Model.Entries] |
|
name [Context] |
|
name [Dyncall.CInfo] |
|
name [Wp_error] |
|
name_of_asked_bhv [WpAnnot] |
|
name_of_mode [VCS] |
|
name_of_path [ProverCoq] |
|
name_of_prover [VCS] |
|
named_predicate [VarUsage] |
|
names_at [Clabels] |
|
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 .
|
need_recompile [ProverCoq] |
|
needback [Proof] |
|
needsave [Proof] |
|
needwarn [Proof] |
|
new_cfg_env [Cil2cfg] |
|
new_driver [LogicBuiltins] |
reset the context to an empty driver
|
new_env [Mcfg.S] |
optionally init env with user logic variables
|
new_env [CfgWP.VC] |
|
new_env [CfgDump.VC] |
|
new_env [LogicSemantics.Make] |
|
new_env [LogicCompiler.Make] |
|
new_extern [Lang] |
|
new_extern_id [Lang] |
|
new_gamma [Lang] |
|
new_loop_computation [WpStrategy] |
|
new_pool [Lang] |
|
newcluster [Definitions] |
|
newline [Driver] |
|
newline [Script] |
|
next [CfgTypes.Cfg] |
|
next [CfgLib.Make] |
|
next_edge [Cil2cfg] |
|
next_stat4chap [WpReport] |
next chapters stats
|
next_stat4prop [WpReport] |
next property stats
|
next_stat4sect [WpReport] |
next section stats
|
nid [CfgTypes.Cfg] |
|
nid [CfgLib.Make] |
|
nil [CfgTypes.Cfg] |
|
nil [CfgLib.Make] |
|
no_infinite_array [Ctypes] |
|
no_pointer [MemEmpty] |
|
no_result [VCS] |
|
node [CfgTypes.Cfg] |
|
node [CfgDump.VC] |
|
node [CfgLib.Make] |
|
node_after [Cil2cfg] |
Find the node that follows the input node statement.
|
node_id [Cil2cfg] |
|
node_stmt_exn [Cil2cfg] |
|
node_stmt_opt [Cil2cfg] |
|
node_type [Cil2cfg] |
|
node_type_id [Cil2cfg] |
gives a identifier to each CFG node in order to hash them
|
noskipkey [Driver] |
|
not_arg_computed [Variables_analysis] |
|
not_computed [Variables_analysis] |
|
not_computing [Wpo.Results] |
|
not_half_computed [Variables_analysis] |
|
not_param_computed [Variables_analysis] |
|
not_posteffect [CfgWP.VC] |
|
not_yet_implemented [Wp_error] |
|
null [Memory.Model] |
Return the location of the null pointer
|
null [MemTyped] |
|
null [MemVar.Make] |
|
null [MemEmpty] |
|
null [Cvalues] |
test for null pointer value
|
num_of_bhv_from [WpPropId] |
|
number [WpReport] |
|
O |
object_of [Ctypes] |
|
object_of_array_elem [Ctypes] |
|
object_of_logic_pointed [Ctypes] |
|
object_of_logic_type [Ctypes] |
|
object_of_pointed [Ctypes] |
|
ocamlc [Config] |
Name of the bytecode compiler.
|
ocamlopt [Config] |
Name of the native compiler.
|
occur [Letify.Split] |
|
occur [VarUsage] |
|
occurrence [VarUsage] |
|
occurs [Memory.Model] |
Test if a location depend on a given logic variable
|
occurs [MemTyped] |
|
occurs [MemVar.Make] |
|
occurs [MemEmpty] |
|
occurs [LogicSemantics.Make] |
|
occurs [Region] |
|
occurs [Vset] |
|
occurs [Conditions] |
|
occurs [Letify] |
|
occurs [Lang.F] |
|
occurs_idx [Region] |
|
occurs_opt [LogicSemantics.Make] |
|
occurs_opt [Vset] |
|
occurs_sloc [LogicSemantics.Make] |
|
occurs_vc [CfgWP.VC] |
|
occurs_vset [Vset] |
|
occursp [Lang.F] |
|
of_array [Matrix] |
|
of_context [VarUsage.Usage] |
|
of_cvar [VarUsage] |
|
of_exp [Definitions.Trigger] |
|
of_formal [VarUsage] |
|
of_list [Set.S] |
of_list l creates a set from a list of elements.
|
of_lvar [VarUsage] |
|
of_pred [Definitions.Trigger] |
|
of_real [Cint] |
|
of_term [Definitions.Trigger] |
|
of_value [VarUsage.Usage] |
|
offset [MemVar.Make] |
|
offset [RefUsage] |
|
offset_of_field [MemTyped] |
|
ofs_occurs [MemVar.Make] |
|
ofs_vars [MemVar.Make] |
|
ok_array_term [Variables_analysis] |
|
ok_array_term_arg [Variables_analysis] |
|
ok_array_term_formal [Variables_analysis] |
|
ok_pointer_term [Variables_analysis] |
|
ok_ptr_term_arg [Variables_analysis] |
|
ok_ptr_term_formal [Variables_analysis] |
|
okind [LogicBuiltins] |
|
on_model [Model] |
|
on_reload [GuiPanel] |
|
on_reset [Wp_parameters] |
|
on_spec [VarUsage.Context] |
|
on_update [GuiPanel] |
|
once [CfgTypes.Cfg] |
Return true only if the node is not yet marked, then mark it.
|
once [Context] |
A global configure, executed once.
|
once [Dyncall] |
|
once [CfgLib.Make] |
|
op [Driver] |
|
op_elt [Driver] |
|
op_land [Cint] |
|
op_link [Driver] |
|
op_lor [Cint] |
|
op_lxor [Cint] |
|
open_file [Script] |
|
open_scope [Calculus.Cfg] |
|
option_file [ProverWhy3] |
|
option_file [ProverCoq] |
|
option_file [ProverErgo] |
|
option_import [ProverWhy3] |
|
oracle [Variables_analysis] |
|
ordered [Vset] |
- limit : result when either parameter is None strict : if true , comparison is < instead of <=
|
out [CfgDump.VC] |
|
P |
p_all [Lang.F] |
|
p_and [Lang.F] |
|
p_any [Lang.F] |
|
p_apply [Letify.Sigma] |
|
p_bind [Lang.F] |
|
p_bool [Lang.F] |
|
p_bools [Lang.F] |
|
p_call [Lang.F] |
|
p_close [Lang.F] |
|
p_conj [Lang.F] |
|
p_disj [Lang.F] |
|
p_eqmem [MemTyped] |
|
p_equal [Lang.F] |
|
p_equiv [Lang.F] |
|
p_error [ProverWhy3] |
|
p_exists [Lang.F] |
|
p_false [Lang.F] |
|
p_float [ProverTask] |
Float group pattern \([0-9.]+\)
|
p_forall [Lang.F] |
|
p_framed [MemTyped] |
|
p_goal [ProverWhy3] |
|
p_group [ProverTask] |
Put pattern in group \(p\)
|
p_havoc [MemTyped] |
|
p_hyps [Lang.F] |
|
p_if [Lang.F] |
|
p_imply [Lang.F] |
|
p_included [MemTyped] |
|
p_int [ProverTask] |
Int group pattern \([0-9]+\)
|
p_is_int [Cint] |
|
p_leq [Lang.F] |
|
p_limit [ProverWhy3] |
|
p_limit [ProverErgo] |
|
p_linked [MemTyped] |
|
p_loc [ProverErgo] |
|
p_lt [Lang.F] |
|
p_member [Vset] |
|
p_neq [Lang.F] |
|
p_not [Lang.F] |
|
p_or [Lang.F] |
|
p_positive [Lang.F] |
|
p_sconst [MemTyped] |
|
p_separated [MemTyped] |
|
p_string [ProverTask] |
String group pattern "\(...\)"
|
p_subst [Lang.F] |
|
p_true [Lang.F] |
|
p_unknown [ProverWhy3] |
|
p_unsat [ProverErgo] |
|
p_until_space [ProverTask] |
No space group pattern "\\(^ \t\n *\\)"
|
p_valid [ProverWhy3] |
|
p_valid [ProverErgo] |
|
p_valid_rd [MemTyped] |
|
p_valid_rw [MemTyped] |
|
param [Factory.VarRef2] |
|
param [Factory.VarRef0] |
|
param [Factory.VarHoare] |
|
param [MemVar.VarUsage] |
|
param [RefUsage] |
|
param_of_lv [LogicCompiler.Make] |
|
parameter [Driver] |
|
parameters [Driver] |
|
parameters [Definitions] |
|
parameters [Lang.Fun] |
|
parameters [Lang] |
definitions
|
params [Cfloat] |
|
params [Lang.Fun] |
|
parse [Factory] |
|
parse [Driver] |
|
parse [ProverWhy3] |
|
parse_c_option [ProverCoq] |
|
parse_coqproof [Proof] |
parse_coqproof f parses a coq-file f and fetch the first proof.
|
parse_error [Why3_xml] |
|
parse_scripts [Proof] |
parse_scripts f parses all scripts from file f and put them in the database.
|
partition [Set.S] |
partition p s returns a pair of sets (s1, s2) , where
s1 is the set of all the elements of s that satisfy the
predicate p , and s2 is the set of all the elements of
s that do not satisfy p .
|
partition [Map.S] |
partition p m returns a pair of maps (m1, m2) , where
m1 contains all the bindings of s that satisfy the
predicate p , and m2 is the map with all the bindings of
s that do not satisfy p .
|
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 .
|
partition [WTO] |
Returns a weak partial order with Bourdoncle's algorithm.
|
parts_of_id [WpPropId] |
get the 'part' infomation.
|
passify_vc [CfgWP.VC] |
|
path [Region] |
Empty, but Full for the path
|
pcstats [WpReport] |
|
pe_prover [ProverWhy3] |
|
percent [WpReport] |
|
phi_base [MemTyped] |
|
phi_offset [MemTyped] |
|
phi_shift [MemTyped] |
|
pid [Conditions] |
|
plain_of_exp [LogicCompiler.Make] |
|
plugin_dir [Config] |
Directory where the Frama-C dynamic plug-ins are.
|
pointer [MemTyped] |
|
pointer [Lang] |
type of pointers
|
pointer_loc [Memory.Model] |
???
|
pointer_loc [MemTyped] |
|
pointer_loc [MemVar.Make] |
|
pointer_loc [MemEmpty] |
|
pointer_val [Memory.Model] |
???
|
pointer_val [MemTyped] |
|
pointer_val [MemVar.Make] |
|
pointer_val [MemEmpty] |
|
poly [Lang] |
polymorphism
|
pop [Context] |
|
pop_all [Why3_xml] |
|
populate [LogicUsage] |
|
pp_access [VarUsage.Context] |
|
pp_annots [WpStrategy] |
|
pp_args [ProverTask] |
|
pp_asked_prop [WpAnnot] |
|
pp_assign_info [WpPropId] |
|
pp_assigns [Wp_error] |
|
pp_assigns_desc [WpPropId] |
|
pp_assigns_mode [WpAnnot] |
|
pp_atom [MemTyped.Layout] |
|
pp_axiom_info [WpPropId] |
|
pp_axiomatics [Wpo] |
|
pp_bkind [Cil2cfg] |
|
pp_block [MemTyped.Layout] |
|
pp_block [Conditions] |
|
pp_bound [LogicSemantics.Make] |
|
pp_bound [Vset] |
|
pp_box [VarUsage] |
|
pp_call [Variables_analysis] |
|
pp_call_type [Cil2cfg] |
|
pp_calls [Dyncall] |
|
pp_chaincall [Variables_analysis] |
|
pp_clause [Conditions] |
|
pp_cluster [Definitions] |
|
pp_condition [Conditions] |
|
pp_depend [ProverErgo] |
|
pp_depend [Wpo] |
|
pp_depend [Conditions] |
|
pp_dependencies [Wpo] |
|
pp_dependency [Wpo] |
|
pp_descr [Conditions] |
|
pp_dim [VarUsage] |
|
pp_edge [CfgTypes.Cfg] |
Print the attributes of the edge in the .dot file.
|
pp_edge [Cil2cfg] |
|
pp_edge [CfgLib.Make] |
|
pp_effect [Wpo.VC_Annot] |
|
pp_epred [Lang.F] |
|
pp_eterm [Lang.F] |
|
pp_file [ProverTask] |
|
pp_float [Ctypes] |
|
pp_formals [Variables_analysis] |
|
pp_frame [LogicSemantics.Make] |
|
pp_frame [LogicCompiler.Make] |
|
pp_function [Wpo] |
|
pp_goal [Wpo] |
|
pp_goal_flow [Wpo] |
|
pp_goal_kind [WpPropId] |
|
pp_goal_part [WpPropId] |
|
pp_gvcs [CfgWP.VC] |
|
pp_index [Wpo] |
|
pp_info_of_strategy [WpStrategy] |
|
pp_int [Ctypes] |
|
pp_kind [LogicBuiltins] |
|
pp_kinds [LogicBuiltins] |
|
pp_language [VCS] |
|
pp_layout [MemTyped.Layout] |
|
pp_libs [LogicBuiltins] |
|
pp_link [LogicBuiltins] |
|
pp_link [Conditions] |
|
pp_loc [Conditions] |
|
pp_local [WpPropId.Pretty] |
|
pp_logfile [Wpo] |
|
pp_logic [LogicAssigns.Logic] |
|
pp_logic [LogicSemantics.Make] |
|
pp_logic [LogicUsage] |
|
pp_logic_label [Wp_error] |
|
pp_mismatch [MemTyped] |
|
pp_mode [VCS] |
|
pp_names [WpPropId] |
|
pp_node [CfgTypes.Cfg] |
Print the attributes of the node in the .dot file.
|
pp_node [Cil2cfg] |
|
pp_node [CfgLib.Make] |
|
pp_node_type [Cil2cfg] |
|
pp_object [Ctypes] |
|
pp_ofs [MemVar.Make] |
|
pp_opt [CfgWP.VC] |
|
pp_part [WpPropId.Pretty] |
|
pp_perf [VCS] |
|
pp_pred [Lang.F] |
|
pp_pred_info [WpPropId] |
|
pp_pred_of_pred_info [WpPropId] |
|
pp_profile [LogicUsage] |
|
pp_prop [WpPropId.Pretty] |
|
pp_propid [WpPropId] |
Print unique id of prop_id
|
pp_prover [VCS] |
|
pp_region [LogicAssigns.Logic] |
|
pp_region [LogicSemantics.Make] |
|
pp_result [Register] |
|
pp_result [VCS] |
|
pp_scope [CfgDump.VC] |
|
pp_section [LogicUsage] |
|
pp_seq [Conditions] |
|
pp_sequence [Conditions] |
|
pp_sloc [LogicAssigns.Logic] |
|
pp_sloc [LogicSemantics.Make] |
|
pp_step [Conditions] |
|
pp_stmt [Conditions] |
|
pp_strategy_info [WpAnnot] |
|
pp_string_list [Wp_error] |
|
pp_subprop [WpPropId.Pretty] |
|
pp_target [VarUsage.Context] |
|
pp_term [Lang.F] |
|
pp_time [Rformat] |
Pretty print time in hour, minutes, seconds, or milliseconds, as appropriate
|
pp_time_range [Rformat] |
|
pp_title [Wpo] |
|
pp_token [Script] |
|
pp_var [Lang.F] |
|
pp_var_type [Variables_analysis] |
|
pp_vars [Lang.F] |
|
pp_vc [CfgWP.VC] |
|
pp_vcs [CfgWP.VC] |
|
pp_warning [Conditions] |
|
pp_warnings [Wpo] |
|
pp_wp_parameters [Register] |
|
pp_zero [WpReport] |
|
precondition_compute [Variables_analysis] |
precondition_compute () adds warnings and precondition suitable
to the current optimisations which are activated
|
preconditions_at_call [WpAnnot] |
|
pred [CfgTypes.Cfg] |
Reversed With repetitions
|
pred [LogicSemantics.Make] |
|
pred [LogicCompiler.Make] |
|
pred [Lang.F] |
|
pred [RefUsage] |
|
pred [CfgLib.Make] |
|
pred_cond [Conditions] |
|
pred_e [Cil2cfg] |
|
pred_handler [LogicSemantics.Make] |
|
pred_info_id [WpPropId] |
|
pred_protected [LogicSemantics.Make] |
|
pred_seq [Conditions] |
|
pred_trigger [LogicSemantics.Make] |
|
predicate [LogicSemantics.Make] |
|
predicate [Splitter] |
|
predicate [VarUsage] |
|
prefix [Cvalues.CASES] |
|
preproc_annot [NormAtLabels] |
|
preproc_assigns [NormAtLabels] |
|
preproc_label [NormAtLabels] |
|
preprocess [Wpo.GOAL] |
|
preprocessor [Config] |
Name of the default command to call the preprocessor.
|
preprocessor_is_gnu_like [Config] |
whether the default preprocessor accepts the same options as gcc
(i.e.
|
preprocessor_keep_comments [Config] |
true if the default preprocessor selected during compilation is
able to keep comments (hence ACSL annotations) in its output.
|
pretty [Memory.Model] |
pretty printing of memory location
|
pretty [Memory.Sigma] |
|
pretty [Memory.Chunk] |
|
pretty [Mcfg.S] |
|
pretty [CfgWP.VC.TARGET] |
|
pretty [CfgWP.VC] |
|
pretty [CfgDump.VC] |
|
pretty [Driver] |
|
pretty [Wpo.VC_Check] |
|
pretty [Wpo.VC_Annot] |
|
pretty [Wpo.VC_Lemma] |
|
pretty [Wpo.DISK] |
|
pretty [MemTyped.Layout] |
|
pretty [MemTyped.LITERAL] |
|
pretty [MemTyped.Chunk] |
|
pretty [MemTyped] |
|
pretty [MemVar.Make.Sigma] |
|
pretty [MemVar.Make.Chunk] |
|
pretty [MemVar.Make.VALLOC] |
|
pretty [MemVar.Make.VAR] |
|
pretty [MemVar.Make] |
|
pretty [MemEmpty.Chunk] |
|
pretty [MemEmpty] |
|
pretty [Sigma.Make] |
|
pretty [Cstring.STR] |
|
pretty [Cstring] |
|
pretty [Region] |
|
pretty [Conditions] |
|
pretty [Letify.Sigma] |
|
pretty [Splitter] |
|
pretty [Passive] |
|
pretty [Matrix.KEY] |
|
pretty [Lang.Fun] |
|
pretty [Lang.Field] |
|
pretty [Lang.ADT] |
|
pretty [Model.Key] |
|
pretty [Model.Entries] |
|
pretty [Warning] |
|
pretty [WpPropId] |
|
pretty [Cil2cfg.EL] |
|
pretty [Cil2cfg.VL] |
|
pretty [RefUsage.Var] |
|
pretty [VarUsage.Usage] |
|
pretty [VarUsage.Root] |
|
pretty [VarUsage] |
|
pretty [Clabels] |
|
pretty [Ctypes] |
|
pretty [Rformat] |
|
pretty [Fixpoint.Domain] |
|
pretty [WTO] |
|
pretty_context [WpPropId] |
|
pretty_local [WpPropId] |
|
pretty_raw_stmt [Cil2cfg.Printer] |
|
print [WpReport] |
|
print_chapter [WpReport] |
|
print_generated [Wp_parameters] |
Debugging Categories
|
print_property [WpReport] |
|
print_section [WpReport] |
|
print_value [CodeSemantics.Make] |
|
process_global_const [Calculus.Cfg] |
|
process_global_init [Calculus.Cfg] |
|
process_unreached_annots [WpAnnot] |
|
profile_env [LogicCompiler.Make] |
|
promote [Ctypes] |
|
proof [Script] |
|
proof_context [LogicUsage] |
Lemmas that are not in an axiomatic.
|
prop_id [CfgWP.VC.TARGET] |
|
prop_id_keys [WpPropId] |
|
propagate [VarUsage.Occur] |
|
properties [WpReport] |
|
property [Dyncall] |
Returns an property identifier for the precondition.
|
property [Wprop.Info] |
|
property [Wprop.Indexed2] |
|
property [Wprop.Indexed] |
|
property_hints [WpPropId] |
|
property_of_id [WpPropId] |
returns the annotation which lead to the given PO.
|
propid_hints [WpPropId] |
|
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] |
|
protect_warning [Wp_error] |
|
protected [Wp_error] |
|
prove [Prover] |
|
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_annot [ProverCoq] |
|
prove_annot [ProverErgo] |
|
prove_check [ProverCoq] |
|
prove_check [ProverErgo] |
|
prove_file [ProverWhy3] |
|
prove_file [ProverErgo] |
|
prove_lemma [CfgWP.VC] |
|
prove_lemma [ProverCoq] |
|
prove_lemma [ProverErgo] |
|
prove_prop [ProverWhy3] |
|
prove_prop [ProverCoq] |
|
prove_prop [ProverErgo] |
|
prove_session [ProverCoq] |
|
proved [Register] |
|
prover_of_name [Wpo] |
Dynamically exported.
|
prover_of_name [VCS] |
|
provers [Register] |
|
pruning [Conditions] |
|
pstats [WpReport] |
|
ptr_reference [Variables_analysis] |
|
push [Context] |
|
Q |
qed_time [Prover] |
|
qed_time [Wpo.GOAL] |
|
R |
r_disjoint [MemTyped] |
|
r_included [MemTyped] |
|
r_separated [MemTyped] |
|
random [CfgWP.VC] |
|
range [MemTyped] |
|
range [MemVar.Make] |
|
range [Vset] |
|
range_offset [MemVar.Make] |
|
range_set [MemTyped] |
|
rank [MemTyped.Chunk] |
|
raw_add_file [Why3_session] |
|
raw_add_no_task [Why3_session] |
|
raw_add_theory [Why3_session] |
|
rbinop [Cfloat] |
|
rcontains_from [String] |
String.rcontains_from s stop c tests if character c
appears in s before position stop+1 .
|
rdescr [Cvalues.Logic] |
|
rdiv [Rformat] |
|
re_error [ProverWhy3] |
|
re_error [ProverErgo] |
|
re_limit [ProverWhy3] |
|
re_limit [ProverErgo] |
|
re_unknown [ProverWhy3] |
|
re_unsat [ProverErgo] |
|
re_valid [ProverWhy3] |
|
re_valid [ProverErgo] |
|
read_session [Why3_session] |
Read a session stored on the disk.
|
reads [LogicCompiler.Make] |
|
real_of_int [Cfloat] |
|
reclink [Driver] |
|
reclink_bis [Driver] |
|
reclink_ter [Driver] |
|
record [Lang] |
|
recorstring [Driver] |
|
recstring [Driver] |
|
recstring_bis [Driver] |
|
recstring_ter [Driver] |
|
reference [RefUsage] |
|
reference_parameter_usage [Variables_analysis] |
|
reference_parameter_usage_lval [Variables_analysis] |
|
reference_parameter_usage_term [Variables_analysis] |
|
regexp_col [ProverWhy3] |
|
regexp_com [ProverWhy3] |
|
region [LogicSemantics.Make] |
|
region [LogicCompiler.Make] |
|
register [GuiPanel] |
|
register [LogicBuiltins] |
|
register [Model] |
|
register [Dyncall] |
|
register_axiomatic [LogicUsage] |
|
register_cases [LogicUsage] |
|
register_lemma [LogicUsage] |
|
register_logic [LogicUsage] |
|
register_script [Proof] |
|
register_type [LogicUsage] |
|
relation [LogicSemantics.Make] |
|
reload [GuiPanel] |
|
reload_callback [GuiPanel] |
|
remove [Indexer.Make] |
Log complexity.
|
remove [Set.S] |
remove x s returns a set containing all elements of s ,
except x .
|
remove [Map.S] |
remove x m returns a map containing the same bindings as
m , except for x which is unbound in the returned map.
|
remove [Wpo] |
|
remove [Cil2cfg.HEsig] |
|
remove [Cil2cfg.HE] |
|
remove [Hashtbl.S] |
|
remove [Cil2cfg.PMAP] |
|
remove [FCMap.S] |
remove x m returns a map containing the same bindings as
m , except for x which is unbound in the returned map.
|
remove [State_builder.Hashtbl] |
|
remove [CfgLib.Make] |
|
remove_array_reference_arg [Variables_analysis] |
|
remove_array_reference_param [Variables_analysis] |
|
remove_edge [Cil2cfg.CFG] |
|
remove_edge [Cil2cfg] |
|
remove_edge_e [Cil2cfg.CFG] |
|
remove_ptr_reference_arg [Variables_analysis] |
|
remove_ptr_reference_param [Variables_analysis] |
|
remove_vertex [Cil2cfg.CFG] |
|
render_prover_result [GuiList] |
|
replace [Wpo.Results] |
|
replace [Cil2cfg.HEsig] |
|
replace [Cil2cfg.HE] |
|
replace [Hashtbl.S] |
|
replace [State_builder.Hashtbl] |
Add a new binding.
|
repr [Wpo.VC_Annot] |
|
repr [Model] |
|
reset [Hashtbl.S] |
|
reset [Wp_parameters] |
|
reset_pos [Cil2cfg.WeiMaoZouChenInput] |
reset the position (set the position to 0), but should keep the
information that the node has been seen already.
|
reset_pos [Cil2cfg.LoopInfo] |
|
resetdemon [Wp_parameters] |
|
reshape [VarUsage] |
|
residual [Conditions] |
|
resolve [Prover] |
|
resolve [Wpo.VC_Annot] |
|
resolve [Wpo] |
|
resolve_addr_taken [Variables_analysis] |
|
resolved_call_chain_arg [Variables_analysis] |
|
resolved_call_chain_param [Variables_analysis] |
|
restrict [Cvalues.Logic] |
|
result [WpReport] |
|
result [VCS] |
|
result [LogicSemantics.Make] |
|
result [LogicCompiler.Make] |
|
result [Cfloat] |
|
result [Cint] |
|
return [Mcfg.S] |
|
return [CfgWP.VC] |
|
return [CfgDump.VC] |
|
return [LogicSemantics.Make] |
|
return [LogicCompiler.Make] |
|
return [CodeSemantics.Make] |
|
rindex [String] |
String.rindex s c returns the index of the last
occurrence of character c in string s .
|
rindex_from [String] |
String.rindex_from s i c returns the index of the
last occurrence of character c in string s before position i+1 .
|
rlayout [MemTyped.Layout] |
|
rloc [Cvalues.Logic] |
|
round_lit [Cfloat] |
|
rpath [Region] |
Empty, but Full for the r-paths
|
rsize [MemVar.Make] |
|
rte_divMod_status [WpAnnot] |
|
rte_find [WpAnnot] |
|
rte_generated [GuiPanel] |
|
rte_memAccess_status [WpAnnot] |
|
rte_precond_status [WpAnnot] |
|
rte_signedOv_status [WpAnnot] |
|
rte_unsignedOv_status [WpAnnot] |
|
rte_wp [WpAnnot] |
|
run [Register] |
|
run_and_prove [GuiPanel] |
|
run_prover [Prover] |
|
runop [Cfloat] |
|
S |
s_cond [CodeSemantics.Make] |
|
s_eq [Cvalues] |
|
s_exp [CodeSemantics.Make] |
|
s_valid [MemTyped] |
|
same_edge [Cil2cfg] |
|
same_node [Cil2cfg] |
|
sanitize [Proof] |
|
sanitize [LogicBuiltins] |
|
sanitize_why3 [VCS] |
|
sanitizers [LogicBuiltins] |
|
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 [CfgWP.VC] |
|
scope [CfgDump.VC] |
|
scope [MemTyped] |
|
scope [MemVar.Make] |
|
scope [MemEmpty] |
|
scope_vars [MemVar.Make] |
|
script_for [Proof] |
|
script_for_ide [Proof] |
|
scriptbase [Proof] |
|
scriptfile [Proof] |
|
section [Definitions] |
|
section_of_lemma [LogicUsage] |
|
section_of_logic [LogicUsage] |
|
section_of_type [LogicUsage] |
|
select [Letify.Split] |
|
select_by_name [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).
|
selection_of_localizable [GuiSource] |
|
self [Memory.Chunk] |
|
self [MemTyped.Chunk] |
|
self [MemVar.Make.Chunk] |
|
self [MemVar.Make.VALLOC] |
|
self [MemVar.Make.VAR] |
|
self [MemEmpty.Chunk] |
|
self [State_builder.S] |
The kind of the registered state.
|
sem [Fixpoint.Make] |
|
separated [Memory.Model] |
Return the formula that tests if two segment are separated
|
separated [MemTyped] |
|
separated [MemVar.Make] |
|
separated [MemEmpty] |
|
separated [LogicSemantics.Make] |
|
separated [Cvalues.Logic] |
|
separated_delta [MemVar.Make] |
|
separated_from [Cvalues.Logic] |
|
separated_regions [Cvalues.Logic] |
|
separated_sloc [Cvalues.Logic] |
|
separated_terms [LogicSemantics.Make] |
|
sequence [Register] |
|
server [ProverTask] |
|
session [Register] |
|
session_dir_for_save [Why3_session] |
|
set [CfgTypes.Cfg] |
|
set [Calculus.Cfg.R] |
store the result p for the computation of the edge e.
|
set [Context] |
Define the current value.
|
set [String] |
String.set s n c modifies byte sequence s in place,
replacing the byte at index n with c .
|
set [State_builder.Ref] |
Change the referenced value.
|
set [CfgLib.Attr] |
Replace old value.
|
set [CfgLib.Make] |
|
set_back_edge [Cil2cfg] |
|
set_builtin_1 [Lang.F] |
|
set_builtin_2 [Lang.F] |
|
set_builtin_eqp [Lang.F] |
|
set_iloop_header [Cil2cfg.WeiMaoZouChenInput] |
set_iloop_header env b h store h as the innermost loop header for b.
|
set_iloop_header [Cil2cfg.LoopInfo] |
|
set_image [CfgLib.Transform] |
|
set_label [CfgLib.Labels] |
Register the label to points to the given node.
|
set_model [Register] |
|
set_model [Wp_error] |
|
set_of_term [LogicSemantics.Make] |
|
set_option [LogicBuiltins] |
reset and add a value to an option (group, name)
|
set_pos [Cil2cfg.WeiMaoZouChenInput] |
store the position for the node and also the fact that the node has
been seen
|
set_pos [Cil2cfg.LoopInfo] |
|
set_pred [CfgLib.Make] |
|
set_result [Wpo] |
|
set_top [Cleaning] |
|
set_unreachable [WpAnnot] |
|
setup_preconditions_proxies [Cil2cfg] |
Setup the preconditions at all the call points of e_kf , when possible
|
severe [Warning] |
|
shape [VarUsage] |
|
shared [ProverCoq] |
|
shared_demon [ProverCoq] |
|
shared_headers [ProverCoq] |
|
shift [Memory.Model] |
Return the memory location obtained by array access at an index
represented by the given term .
|
shift [MemTyped] |
|
shift [MemVar.Make] |
|
shift [MemEmpty] |
|
shift [Cvalues.Logic] |
|
shift [RefUsage] |
|
shift [VarUsage.Context] |
|
shift [VarUsage.Model] |
|
shift_offset [LogicSemantics.Make] |
|
shift_set [Cvalues.Logic] |
|
sigma [LogicSemantics.Make] |
|
sigma [LogicCompiler.Make] |
|
sigma_at [CfgWP.VC] |
|
sigma_opt [CfgWP.VC] |
|
sigma_union [CfgWP.VC] |
|
signal [Prover] |
|
signature [Driver] |
|
signature [MemTyped] |
|
signature [LogicCompiler.Make] |
|
signed [Ctypes] |
true if signed
|
simplify [Mcfg.Splitter] |
|
simplify [Prover] |
|
simplify [Conditions] |
|
single [Vset] |
|
singleton [Set.S] |
singleton x returns the one-element set containing only x .
|
singleton [Map.S] |
singleton x y returns the one-element map that contains a binding y
for x .
|
singleton [Vset] |
|
singleton [Splitter] |
|
singleton [FCMap.S] |
singleton x y returns the one-element map that contains a binding y
for x .
|
size [Indexer.Make] |
Number of elements in the collection.
|
size [CfgTypes.Cfg] |
|
size [Matrix] |
|
size [VarUsage] |
|
size [Dyncall.CInfo] |
|
size [CfgLib.Make] |
|
size_int [VarUsage] |
|
size_of_array_type [MemVar.Make] |
|
size_of_comp [MemTyped] |
|
size_of_field [MemTyped] |
|
size_of_object [MemTyped] |
|
size_of_typ [MemTyped] |
|
sizeof_object [Ctypes] |
|
sizeof_typ [Ctypes] |
|
skind [LogicBuiltins] |
|
skip [Driver] |
|
skip [Script] |
|
skipkey [Driver] |
|
sloc [Cvalues.Logic] |
|
sloc_descr [MemVar.Make] |
|
sloc_of_vset [Cvalues.Logic] |
|
smp1 [Cint] |
|
smp2 [Cint] |
|
smp_bitk_positive [Cint] |
|
smp_eq_with_land [Cint] |
|
smp_eq_with_lnot [Cint] |
|
smp_eq_with_lor [Cint] |
|
smp_eq_with_lsl [Cint] |
|
smp_eq_with_lsr [Cint] |
|
smp_eq_with_lxor [Cint] |
|
smp_land [Cint] |
|
smp_shift [Cint] |
|
sort [Lang.Fun] |
|
sort [Lang.Field] |
|
sort_of_ctype [Lang] |
|
sort_of_ltype [Lang] |
|
sort_of_object [Lang] |
|
source [CfgWP.VC.TARGET] |
|
source [MemEmpty] |
|
source_of_id [WpPropId] |
|
spaces [Rformat] |
|
spawn [Prover] |
|
spawn [ProverTask] |
Spawn all the tasks over the server and retain the first 'validated' one
|
split [Mcfg.Splitter] |
|
split [Factory] |
|
split [ProverWhy3] |
|
split [Set.S] |
split x s returns a triple (l, present, r) , where
l is the set of elements of s that are
strictly less than x ;
r is the set of elements of s that are
strictly greater than x ;
present is false if s contains no element equal to x ,
or true if s contains an element equal to x .
|
split [Map.S] |
split x m returns a triple (l, data, r) , where
l is the map with all the bindings of m whose key
is strictly less than x ;
r is the map with all the bindings of m whose key
is strictly greater than x ;
data is None if m contains no binding for x ,
or Some v if m binds v to x .
|
split [WpAnnot] |
splits a prop_id goals into prop_id parts for each sub-goals
|
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 .
|
spwan_wp_proofs_iter [Register] |
|
spy [Register] |
|
stars_exp [Variables_analysis] |
|
stars_lv_typ [Variables_analysis] |
|
stars_term [Variables_analysis] |
|
stars_typ [Variables_analysis] |
|
stars_var_type_typ [Variables_analysis] |
|
start_edge [Cil2cfg] |
get the starting edges
|
start_stat4chap [WpReport] |
start chapter stats
|
start_stat4prop [WpReport] |
start property stats of a section
|
start_stat4sect [WpReport] |
start section stats of a chapter
|
start_stmt_of_node [Cil2cfg] |
|
stat [WpReport] |
|
static_gui_plugins [Config] |
GUI of plug-ins statically linked within Frama-C.
|
static_plugins [Config] |
Plug-ins statically linked within Frama-C.
|
stats [WpReport] |
|
stats [Hashtbl.S] |
|
status [LogicSemantics.Make] |
|
status [LogicCompiler.Make] |
|
step [Conditions] |
|
stepout [VCS] |
|
stmt_hints [WpPropId] |
|
stored [Memory.Model] |
Return a set of formula that express a modification between two
memory state.
|
stored [MemTyped] |
|
stored [MemVar.Make] |
|
stored [MemEmpty] |
|
str_id [Cstring] |
Non-zero integer, unique for each different string literal
|
str_len [Cstring] |
|
str_val [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_addr [Variables_analysis] |
|
string_attribute [Why3_session] |
|
string_attribute_def [Why3_session] |
|
string_of_termination_kind [WpPropId] |
TODO: should probably be somewhere else
|
string_val [Driver] |
|
string_val [Why3_xml] |
|
strip_forall [LogicCompiler.Make] |
|
sub [String] |
String.sub s start len returns a fresh string of length len ,
containing the substring of s that starts at position start and
has length len .
|
sub_c_float [Ctypes] |
|
sub_c_int [Ctypes] |
|
sub_range [Vset] |
|
subproof_idx [WpPropId] |
subproof index of this propr_id
|
subproofs [WpPropId] |
How many subproofs
|
subrange [Vset] |
|
subset [Set.S] |
subset s1 s2 tests whether the set s1 is a subset of
the set s2 .
|
subset [Region] |
|
subset [Vset] |
|
subset_fields [Region] |
|
subset_index [Region] |
|
subset_indices [Region] |
|
succ [CfgTypes.Cfg] |
Reversed with repetitions
|
succ [CfgLib.Make] |
|
succ_e [Cil2cfg] |
|
suffixed [Cfloat] |
|
switch [Mcfg.S] |
|
switch [CfgWP.VC] |
|
switch [CfgDump.VC] |
|
switch_cases [Splitter] |
|
switch_default [Splitter] |
|
symbolf [Lang] |
|
T |
t_addr [MemTyped] |
|
tag [CfgDump.VC] |
|
target [WpAnnot] |
|
tau [Matrix] |
|
tau_of_chunk [Memory.Chunk] |
|
tau_of_chunk [MemTyped.Chunk] |
|
tau_of_chunk [MemVar.Make.Chunk] |
|
tau_of_chunk [MemVar.Make.VALLOC] |
|
tau_of_chunk [MemVar.Make.VAR] |
|
tau_of_chunk [MemEmpty.Chunk] |
|
tau_of_comp [Lang] |
|
tau_of_ctype [Lang] |
|
tau_of_field [Lang] |
|
tau_of_lfun [Lang] |
|
tau_of_ltype [Lang] |
|
tau_of_object [Lang] |
|
tau_of_record [Lang] |
|
tau_of_return [Lang] |
|
tau_of_set [Vset] |
|
tc [Conditions] |
|
term [LogicSemantics.Make] |
|
term [LogicCompiler.Make] |
|
term [RefUsage] |
|
term [VarUsage] |
|
term_binop [LogicSemantics.Make] |
|
term_cast [LogicSemantics.Make] |
|
term_coffset [VarUsage] |
|
term_diff [LogicSemantics.Make] |
|
term_equal [LogicSemantics.Make] |
|
term_handler [LogicSemantics.Make] |
|
term_hints [WpPropId] |
|
term_host [VarUsage] |
|
term_indices [RefUsage] |
|
term_indices [VarUsage] |
|
term_lval [LogicSemantics.Make] |
|
term_lval [RefUsage] |
|
term_lval [VarUsage] |
|
term_node [LogicSemantics.Make] |
|
term_offset [RefUsage] |
|
term_option [VarUsage] |
|
term_protected [LogicSemantics.Make] |
|
term_trigger [LogicSemantics.Make] |
|
term_unop [LogicSemantics.Make] |
|
terms [Letify.Defs] |
|
test [Mcfg.S] |
|
test [CfgWP.VC] |
|
test [CfgDump.VC] |
|
test_case [Conditions] |
|
test_cases [Conditions] |
|
test_edge_loop_ok [Calculus.Cfg] |
|
test_range [Vset] |
|
theories [MemEmpty] |
|
theory_name_of_cluster [ProverWhy3] |
|
theory_name_of_pid [ProverWhy3] |
|
timeout [VCS] |
|
to_cint [Cint] |
Raises Not_found if not.
|
to_cint_map [Cint] |
|
tok [Driver] |
|
token [Driver] |
|
token [Script] |
|
toreal [LogicSemantics.Make] |
|
touch [Definitions] |
|
tracelog [Register] |
|
trigger [LogicCompiler.Make] |
|
trim [LogicUsage] |
|
trim [String] |
Return a copy of the argument, without leading and trailing
whitespace.
|
trivial [Wpo.GOAL] |
|
try_coqide [ProverCoq] |
|
try_hints [ProverCoq] |
|
try_prove [ProverCoq] |
|
try_prove [ProverErgo] |
|
try_script [ProverCoq] |
|
two_power_k_minus1 [Cint] |
|
typ_of_param [MemVar.Make.VAR] |
|
type_for_signature [LogicCompiler.Make] |
|
type_id [Lang] |
|
type_of_cells [VarUsage] |
Type of multi-dimensional array cells
|
typecheck [Dyncall] |
|
U |
uncapitalize [String] |
Return a copy of the argument, with the first character set to lowercase.
|
unindex_wpo [Wpo] |
|
union [Set.S] |
Set union.
|
union [Cvalues.Logic] |
|
union [Vset] |
|
union [Splitter] |
|
union [Passive] |
|
unique_tmp [Wp_parameters] |
|
unknown [VCS] |
|
unreachable_nodes [Cil2cfg] |
|
unstructuredness [Cil2cfg.LoopInfo] |
|
unsupported [Wp_error] |
|
unwrap [Splitter] |
|
update [GuiPanel] |
|
update [Indexer.Make] |
update x y t replaces x by y
and returns the range a..b of modified indices.
|
update [Prover] |
|
update [MemVar.Make] |
|
update [Region] |
|
update [Model.Registry] |
set current value, with no protection
|
update [Model.Static] |
|
update [Model.Index] |
|
update [Context] |
Modification of the current value
|
update [VarUsage.Occur] |
|
update [Fixpoint.Make] |
|
update_callback [GuiPanel] |
|
update_config [Factory] |
|
update_hints_for_goal [Proof] |
Update the hints for one specific goal.
|
update_offset [LogicSemantics.Make] |
|
update_property_status [Wpo] |
|
update_symbol [Definitions] |
|
update_wpo_from_session [Prover] |
Update Wpo from Sessions
|
updated [MemTyped] |
|
uppercase [String] |
Return a copy of the argument, with all lowercase letters
translated to uppercase, including accented letters of the ISO
Latin-1 (8859-1) character set.
|
usage [VarUsage] |
|
use_assigns [Mcfg.S] |
use_assigns env hid kind assgn goal performs the havoc on the goal.
|
use_assigns [CfgWP.VC] |
|
use_assigns [CfgDump.VC] |
|
use_equal [LogicSemantics.Make] |
|
use_loop_assigns [Calculus.Cfg] |
|
used_of_dseq [Conditions] |
|
user_prop_names [WpPropId] |
This is used to give the name of the property that the user can give
to select it from the command line (-wp-prop option)
|
V |
val_of_chunk [MemTyped.Chunk] |
|
val_of_exp [CodeSemantics.Make] |
|
val_of_term [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 [VCS] |
|
valid [MemTyped] |
|
valid [MemVar.Make] |
|
valid [MemEmpty] |
|
valid [LogicSemantics.Make] |
|
valid [Cvalues.Logic] |
|
valid_array [MemVar.Make] |
|
valid_base [MemVar.Make] |
|
valid_loc [MemVar.Make] |
|
valid_offset [MemVar.Make] |
|
valid_offsetrange [MemVar.Make] |
|
valid_path [MemVar.Make] |
|
valid_pathrange [MemVar.Make] |
|
valid_range [MemVar.Make] |
|
valid_sloc [Cvalues.Logic] |
|
validate_buffer [ProverTask] |
|
validate_pattern [ProverTask] |
|
validated_cvar [VarUsage] |
|
validated_lvar [VarUsage] |
|
validity [VarUsage.Context] |
|
value [Memory.Sigma] |
|
value [Driver] |
|
value [Why3_xml] |
|
value [MemVar.Make.Sigma] |
|
value [Sigma.Make] |
|
value [Cvalues.Logic] |
|
value [RefUsage] |
|
var [Fixpoint.Make] |
|
var_type_of_lvar [Variables_analysis] |
|
variables [Lang] |
|
varpoly [Lang] |
|
vars [Memory.Model] |
Return the logic variables from which the given location depend on.
|
vars [MemTyped] |
|
vars [MemVar.Make] |
|
vars [MemEmpty] |
|
vars [LogicAssigns.Logic] |
|
vars [LogicAssigns.Make] |
|
vars [LogicSemantics.Make] |
|
vars [Region] |
|
vars [Vset] |
|
vars [Definitions.Trigger] |
|
vars [Conditions.Bundle] |
|
vars_cond [Conditions] |
|
vars_list [Conditions] |
|
vars_opt [LogicSemantics.Make] |
|
vars_opt [Vset] |
|
vars_seq [Conditions] |
|
vars_sequent [Conditions] |
|
vars_sloc [LogicSemantics.Make] |
|
vars_vset [Vset] |
|
varsp [Lang.F] |
|
vcup [RefUsage] |
|
version [Config] |
Frama-C Version identifier.
|
vertex_attributes [Cil2cfg.Printer] |
|
vertex_name [Cil2cfg.Printer] |
|
very_strange_loops [Cil2cfg] |
detect is there are natural loops where we didn't manage to compute
back edges (see mark_loops ).
|
vexpr [RefUsage] |
|
visit [Fixpoint.Make] |
|
visit [WTO] |
|
visit_k [Fixpoint.Make] |
|
visit_r [Fixpoint.Make] |
|
vmem [Letify] |
|
vset [Cvalues.Logic] |
|
vset_of_sloc [Cvalues.Logic] |
|
vterm [RefUsage] |
|
vtermopt [RefUsage] |
|
W |
warning [Wp_parameters] |
|
warnings [Wpo] |
|
why3_goal_name [ProverWhy3] |
|
why3ide_running [Prover] |
Different instance of why3ide can't be run simultanely
|
wide [Fixpoint.Domain] |
|
widen [Fixpoint.Make] |
|
with_current_loc [Context] |
|
with_model [Model] |
|
without_assume [Lang] |
|
word [Rformat] |
|
wp [Factory] |
|
wp_call_any [Calculus.Cfg] |
|
wp_call_kf [Calculus.Cfg] |
|
wp_calls [Calculus.Cfg] |
|
wp_clear [Register] |
|
wp_compute [Register] |
|
wp_compute_call [Register] |
|
wp_compute_deprecated [Register] |
|
wp_compute_ip [Register] |
|
wp_compute_kf [Register] |
|
wp_configure_model [GuiPanel] |
|
wp_dir [GuiPanel] |
|
wp_generation [Wp_parameters] |
|
wp_loop [Calculus.Cfg] |
Compute the result for edge e which goes to the loop node nloop .
|
wp_model [Wp_parameters] |
|
wp_panel [GuiPanel] |
|
wp_po [Wp_parameters] |
|
wp_prover [Wp_parameters] |
|
wp_proverlibs [Wp_parameters] |
|
wp_scope [Calculus.Cfg] |
|
wp_script [GuiPanel] |
|
wp_stmt [Calculus.Cfg] |
|
wp_strategy [Wp_parameters] |
|
wp_unreachable [WpAnnot] |
|
wp_update_model [GuiPanel] |
|
wp_update_script [GuiPanel] |
|
wp_why3ide [Prover] |
|
wp_why3ide_launch [Register] |
|
wpcheck_provers [Wp_parameters] |
|
wrap_lvar [LogicCompiler.Make] |
|
wrap_mem [LogicCompiler.Make] |
|
wrap_var [LogicCompiler.Make] |
|
write [Rformat] |
|
write_cluster [ProverWhy3] |
|
write_cluster [ProverCoq] |
|
write_cluster [ProverErgo] |
|
X |
xml_doctype [Why3_xml] |
|
xml_prolog [Why3_xml] |
|