Index of values


(&&&) [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_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 [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_depend [Partitioning]
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]
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]
base_addr [MemTyped]
base_addr [MemVar.Make]
base_addr [MemEmpty]
base_id_prop_txt [WpPropId.Names]
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]
basename_of_prop_id [WpPropId.Names]
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]
binders [Definitions.Trigger]
bindings [FCMap.S]
Return the list of all bindings of the given map.
bitk_positive [Cint]
bkind_stmt [Cil2cfg]
blit [String]
String.blit src srcoff dst dstoff len copies len characters from string src, starting at character number srcoff, to string dst, starting at character number dstoff.
block_length [Memory.Model]
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]
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.Index]
callenv [Calculus.Cfg]
calls [GuiNavigator]
calls_collection_computed [Variables_analysis]
cancel [Wpo.Results]
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 [FCMap.S]
Return the number of bindings of a map.
cartesian [Vset]
case_of_optimization [Variables_analysis]
cases [Splitter]
cast [Memory.Model]
cast [MemTyped]
cast [MemVar.Make]
cast [MemEmpty]
cast [CodeSemantics.Make]
cast [RefUsage]
cast [VarUsage.Context]
cast_ctyp [RefUsage]
cast_ltyp [RefUsage]
cast_obj [RefUsage]
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 [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]
classes [Partitioning]
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]
closed [Lang.F]
closure [Partitioning]
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 [Partitioning]
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]
color [Partitioning]
color_of [Partitioning]
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 [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.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]
The comparison function for strings, with the same specification as Pervasives.compare.
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_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.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_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]
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 [Partitioning]
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 string 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]
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.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.Index]
denv [Matrix]
depend [Driver]
depend [Partitioning]
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]
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 [Wpo.GOAL]
empty [Region]
empty [Vset]
empty [Conditions.Bundle]
empty [Conditions]
empty [Letify.Defs]
empty [Letify.Sigma]
empty [Splitter]
empty [Passive]
empty [Lang.F]
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.Index]
enumerate [Splitter]
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 [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 [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_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]
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 string s in place, replacing len characters by 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 [Wpo.Results]
filter [Proof]
filter [Script]
filter [Partitioning]
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_goal [Partitioning]
filter_hyp [Partitioning]
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 [Letify.Sigma]
find [Model.Registry]
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]
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.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 [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 [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]
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.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 character number 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_basename [WpPropId.Names]
returns the basename of the property.
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_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_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]
head [Lang.F]
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]
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 character number of the first occurrence of character c in string s.
index_from [String]
String.index_from s i c returns the character number 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_cfg [Cil2cfg]
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]
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]
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 [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_negative [Cint]
is_next_edge [Cil2cfg]
is_nil [CfgTypes.Cfg]
is_nil [CfgLib.Make]
is_null [Memory.Model]
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 [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_varray [Partitioning]
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 [Wpo]
iter [MemVar.Make.Sigma]
iter [Sigma.Make]
iter [Letify.Sigma]
iter [Letify]
iter [Splitter]
iter [Lang.Alpha]
iter [Model.Registry]
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.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]
literal [MemTyped]
literal [MemVar.Make]
literal [MemEmpty]
literal [Letify.Split]
lkind [LogicBuiltins]
load [Memory.Model]
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]
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]
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]
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 [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 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 [FCMap.S]
Same as FCMap.S.map, but the function receives as arguments both the key and the associated value for each binding of the map.
mark [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]
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 [FCMap.S]
Same as FCMap.S.min_binding, but returns the largest binding of the given map.
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 [MemVar.Make.Sigma]
mem [Sigma.Make]
mem [Letify.Sigma]
mem [Model.Registry]
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.Index]
memories [MemTyped]
merge [Memory.Sigma]
merge [Mcfg.S]
merge [CfgWP.VC]
merge [CfgDump.VC]
merge [MemVar.Make.Sigma]
merge [Sigma.Make]
merge [Region]
merge [Conditions]
merge [Partitioning]
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 [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_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
normalize_basename [WpPropId.Names]
function used to normanize basename
noskipkey [Driver]
not_arg_computed [Variables_analysis]
not_computed [Variables_analysis]
not_half_computed [Variables_analysis]
not_param_computed [Variables_analysis]
not_posteffect [CfgWP.VC]
not_yet_implemented [Wp_error]
null [Memory.Model]
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]
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_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]
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 [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]
plug [Definitions.Trigger]
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_info_id [WpPropId]
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_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 [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.F.ZInteger]
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_property [WpReport]
print_section [WpReport]
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 [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]
reserve_name_id [WpPropId.Names]
returns the name that should be returned by the function get_prop_name_id if the given property has name as basename.
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 character number of the last occurrence of character c in string s.
rindex_from [String]
String.rindex_from s i c returns the character number 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]
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]
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 string s in place, replacing the character number n by 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]
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_any [CfgWP.VC]
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 [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_char [VarUsage]
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 [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]
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]
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_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_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.
unify [Partitioning]
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.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]
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]
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_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
walk [Partitioning]
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]

Z
zero [Partitioning]