Index of values


($) [Extlib]
Composition.
(<->) [Dotgraph.Record]
(<|>) [Dotgraph.Record]
(>>!) [Task]
callback infix.
(>>-) [Bottom.Type]
This monad propagates the `Bottom value if needed.
(>>-:) [Bottom.Type]
Use this monad if the following function returns a simple value.
(>>=) [Task]
sequence infix.
(>>>) [Task]
bind infix.
(>>?) [Task]
finally infix.
__ocaml_lex_chr_rec [Logic_lexer]
__ocaml_lex_comment_rec [Logic_lexer]
__ocaml_lex_endline_rec [Logic_lexer]
__ocaml_lex_file_rec [Logic_lexer]
__ocaml_lex_hash_rec [Logic_lexer]
__ocaml_lex_tables [Logic_lexer]
__ocaml_lex_token_rec [Logic_lexer]

A
abort [Log.Messages]
user error stopping the plugin.
abs [Integer]
abs [Float_sig.S]
abs [Float_interval_sig.S]
accept_c_comments_into_acsl_spec [Logic_lexer]
access [Db.From]
access [Db.Value]
access_expr [Db.Value]
access_location [Db.Value]
adapt_filename [Extlib]
Ensure that the given filename has the extension "cmo" in bytecode and "cmxs" in native
add [Vector]
Element will be added at index size.
add [Type.Obj_tbl]
add [Type.Ty_tbl]
add [Type.Heterogeneous_table]
add tbl s ty v binds s to the value v in the table tbl.
add [Task]
Auto-flush
add [State_builder.Queue]
add [State_builder.Weak_hashtbl]
add x adds x to the table.
add [State_builder.List_ref]
add [Rgmap]
Returns a new map with the added entry.
add [Rangemap.S]
add x y m returns a map containing the same bindings as m, plus a binding of x to y.
add [Qstack.Make]
Add at the beginning of the stack.
add [Parameter_sig.Collection]
Add an element to the collection
add [Parameter_sig.Collection_category]
Adds a new category for this collection with the given name, accessor and dependencies.
add [Offsetmap_sig]
add (min, max) (v, size, offset) m maps the interval min..max (inclusive) to the value v in m.
add [Map_lattice.MapSet_Lattice]
add key v t binds the value v to key in t.
add [Logic_env.Logic_builtin_used]
add [Logic_builtin]
add [Locations.Location_Bytes]
add b i loc binds b to i in loc when i is not Ival.bottom, and returns bottom otherwise.
add [Journal.Binding]
add ty v var binds the value v to the variable name var.
add [Integer]
add [Int_val]
Addition of two integer abstractions.
add [Int_set]
add [Int_interval]
add [Indexer.Make]
Log complexity.
add [Hptset.S_Basic_Compare]
add [Hptmap_sig.S]
add k d m returns a map whose bindings are all bindings in m, plus a binding of the key k to the datum d.
add [Globals.Functions]
TODO: remove this function and replace all calls by:
add [Globals.Vars]
add [Float_sig.S]
add [Float_interval_sig.S]
add [Emitter.Make_table]
add [Dynamic.Parameter.StringList]
add [Dynamic.Parameter.StringSet]
add [Dotgraph.Map]
add [Dotgraph.Node]
add [Datatype.Sub_caml_weak_hashtbl]
add [Dataflow2.StmtStartData]
add [State_builder.Set_ref]
add [State_builder.Hashtbl]
Add a new binding.
add [Cabshelper.Comments]
add [Bag]
add [Abstract_interp.Rel]
addAttribute [Cil]
Add an attribute.
addAttributes [Cil]
Add a list of attributes.
addOffset [Cil]
addOffset o1 o2 adds o1 to the end of o2.
addOffsetLval [Cil]
Add an offset at the end of an lvalue.
addTermOffset [Logic_const]
Equivalent to addOffset for terms.
addTermOffsetLval [Logic_const]
Equivalent to addOffsetLval for terms.
add_abs [Abstract_interp.Rel]
add_aliases [Parameter_sig.S_no_parameter]
Add some aliases for this option.
add_allocates [Annotations]
Add new allocates into the given behavior.
add_allocates_nothing [Allocates]
Add default allocates \nothing clauses to all functions and loops.
add_allocates_nothing_funspec [Allocates]
Adds allocates \nothing to the default behavior of the function if it does not have and allocation clause yet.
add_assert [Db.Properties]
add_assert [Annotations]
Add an assertion attached to the given statement.
add_assigns [Annotations]
Add new assigns into the given behavior.
add_assumes [Annotations]
Add new assumes clauses into the given behavior.
add_at_end [Qstack.Make]
Add at the end of the stack.
add_attr [Dotgraph]
Add attributes to the buffer.
add_attribute_glob_annot [Logic_utils]
add an attribute to a global annotation
add_base [Lmap_sig]
add_base b o m adds base b bound to o, replacing any previous bindings of b.
add_base [Lmap_bitwise.Location_map_bitwise]
add_base_value [Lmap_sig]
Creates the offsetmap described by size, v and size_v, and binds it to the base.
add_behaviors [Annotations]
Add new behaviors into the given contract.
add_binding [Lmap_sig]
add_binding ~exact initial_mem loc v simulates the effect of writing v at location loc, in the initial memory state given by initial_mem.
add_binding [Lmap_bitwise.Location_map_bitwise]
add_binding_intervals [Offsetmap_bitwise_sig]
add_binding_ival [Offsetmap_bitwise_sig]
add_binding_loc [Lmap_bitwise.Location_map_bitwise]
add_builtin_logic_ctor [Logic_env]
add_builtin_logic_function_gen [Logic_env]
see add_logic_function_gen above
add_builtin_logic_type [Logic_env]
add_char [Sanitizer]
add_char [Rich_text]
Buffer-like
add_char [Dotgraph]
add_check [Annotations]
Add a checking assertion attached to the given statement.
add_code_annot [Annotations]
Add a new code annotation attached to the given statement.
add_code_transformation_after_cleanup [File]
Same as above, but the hook is applied after clean up.
add_code_transformation_before_cleanup [File]
add_code_transformation_before_cleanup name hook adds an hook in the corresponding category that will be called during the normalization of a linked file, before clean up and removal of temps and unused declarations.
add_codependencies [State_dependency_graph.S]
Add an edge in graph from each state of the list to the state onto.
add_complete [Annotations]
Add a new complete behaviors clause into the contract of the given function.
add_debug_keys [Log.Messages]
adds categories corresponding to string (including potential subcategories) to the set of categories for which messages are to be displayed.
add_decl [Globals.Vars]
add_decreases [Annotations]
Add a decrease clause into the contract of the given function.
add_dependencies [State_dependency_graph.S]
Add an edge in graph from the state from to each state of the list.
add_dependency [Hook.S_ordered]
add_dependency hook1 hook2 indicates that hook1 must be executed before hook2.
add_disjoint [Annotations]
Add a new disjoint behaviors clause into the contract of the given function.
add_ensures [Annotations]
Add new ensures clauses into the given behavior.
add_extended [Annotations]
add_formals_to_state [Db.Value]
add_formals_to_state state kf exps evaluates exps in state and binds them to the formal arguments of kf in the resulting state
add_function_name_transformation [Parameter_customize]
Adds a mangling operation to allow writing user-friendly function names on command-line.
add_global [Annotations]
Add a new global annotation into the program.
add_group [Plugin.S_no_log]
Create a new group inside the plug-in.
add_hook_on_remove [Emitter.Make_table]
Register a hook to be applied whenever a binding is removed from the table.
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_hook_on_update [State]
Add an hook which is applied each time the project library changes the local value of the state.
add_hook_on_update [Ast]
Apply the given hook each time the reference to the AST is updated, including on a project switch.
add_identifier [Lexerhack]
add_identifier [Clexer]
Add a new string as a variable name
add_int [Ival]
Addition of two integer (ie.
add_int_under [Ival]
Underapproximation of the same operation
add_label [Dotgraph]
add_list [Sanitizer]
Separated with '_'
add_listener [Log]
Register a hook that is called each time an event is emitted.
add_logic_ctor [Logic_env]
add_logic_function [Logic_utils]
add a logic function in the environment.
add_logic_function_gen [Logic_env]
add_logic_function_gen takes as argument a function eq_logic_info which decides whether two logic_info are identical.
add_logic_info [Logic_typing.Lenv]
add_logic_label [Logic_typing.Lenv]
add_logic_type [Logic_env]
add_margin [Pretty_utils]
Updates the marger with new text dimension.
add_model_field [Logic_env]
add_monotonic_state [Ast]
indicates that the given state (which must depend on Ast.self) is robust against additions to the AST, that is, it will be able to compute information on the new nodes whenever needed.
add_offset_lval [Logic_typing]
add_once [Journal.Binding]
Same as function add above but raise the exception Already_exists if the binding previously exists
add_options [Dotgraph]
Only add attributes with a true boolean flag
add_plugin_output_aliases [Plugin.S_no_log]
Adds aliases to the options -plugin-help, -plugin-verbose, -plugin-log, -plugin-msg-key, and -plugin-warn-key.
add_requires [Annotations]
Add new requires clauses into the given behavior.
add_result [Logic_typing]
add \result in the environment.
add_sep [Sanitizer]
Adds '_' character
add_set_hook [Parameter_sig.S_no_parameter]
Add a hook to be called after the function Parameter_sig.S_no_parameter.set is called.
add_singleton [Int_val]
Addition of an integer abstraction with a singleton integer.
add_singleton [Int_set]
add_singleton_int [Ival]
Addition of an integer ival with an integer.
add_singleton_int [Int_interval]
add_special_builtin [Cil]
register a new special built-in function
add_special_builtin_family [Cil]
register a new family of special built-in functions.
add_state [State_dependency_graph]
add_string [Sanitizer]
add_string [Rich_text]
Buffer-like
add_substring [Rich_text]
Buffer-like
add_symbolic_dir [Filepath]
add_symbolic_dir name dir indicates that the (absolute) path dir must be replaced by name when pretty-printing paths.
add_syntactic_transformation [Frontc]
add a syntactic transformation that will be applied to all freshly parsed C files.
add_terminates [Annotations]
Add a terminates clause into a contract.
add_to_list [Bottom]
elt >:: list adds elt to the list if it is not bottom.
add_type [Lexerhack]
add_type [Clexer]
Add a new string as a type name
add_type_var [Logic_typing.Lenv]
add_typename [Logic_env]
marks an identifier as being a typename in the logic
add_under [Int_val]
Under-approximation of the addition of two integer abstractions
add_under [Int_set]
add_under [Int_interval]
add_update_hook [Parameter_sig.S_no_parameter]
Add a hook to be called when the value of the parameter changes (by calling Parameter_sig.S_no_parameter.set or indirectly by the project library.
add_var [Logic_typing.Lenv]
add_var [Logic_typing]
adds a given variable in local environment.
add_whole [Rangemap.Make]
addi [Vector]
Return index of added (last) element.
address_of_value [Extlib]
all [Parameter_sig.Collection_category]
The '@all' category.
all [Bottom]
all_addr_dpds [Db.Pdg]
Similar to Db.Pdg.all_data_dpds for address dependencies.
all_call_preconditions_at [Statuses_by_call]
all_call_preconditions_at create kf stmt returns the copies of all the requires of kf for the call statement at stmt.
all_ctrl_dpds [Db.Pdg]
Similar to Db.Pdg.all_data_dpds for control dependencies.
all_data_dpds [Db.Pdg]
Gives the data dependencies of the given nodes, and recursively, all the dependencies of those nodes (regardless to their kind).
all_digits [Logic_lexer]
all_dpds [Db.Pdg]
Transitive closure of Db.Pdg.direct_dpds for all the given nodes.
all_functions_with_preconditions [Statuses_by_call]
Returns the set of functions that can be called at the given statement and for which a precondition has been specialized at this call.
all_uses [Db.Pdg]
build a list of all the nodes that have dependencies (even indirect) on the given nodes.
all_values [Ival]
all_values ~size v returns true iff v contains all integer values representable in size bits.
all_values [Int_val]
all_values ~size v returns true iff v contains all integer values representable in size bits.
allow_return_collapse [Cabs2cil]
Given a call lv = f(), if tf is the return type of f and tlv the type of lv, allow_return_collapse ~tlv ~tf returns false if a temporary must be introduced to hold the result of f, and true otherwise.
analysis_options [Kernel]
anisotropic_cast [Offsetmap_lattice_with_isotropy]
Optionnally change the representation of the given value, under the assumption that it fits in size bits.
annot [Logic_typing.Make]
annot [Logic_parser]
annot [Logic_lexer]
annot_char [Clexer]
The character to recognize logic formulae in comments
annotate_kf [Db.RteGen]
Generates RTE for a single function.
annotation_visible [Filter.RemoveInfo]
tells if the annotation, attached to the given statement is visible.
anonCompFieldName [Cabs2cil]
app_under_info [Cil]
Apply some function on underlying expression if Info or else on expression
appears_in_expr [Cil]
append [Warning_manager]
Append a new message warning.
append [Bag]
append_after [Parameter_sig.List]
append a list at the end of the current state
append_after [Dynamic.Parameter.StringList]
append_before [Parameter_sig.List]
append a list in front of the current state
append_before [Dynamic.Parameter.StringList]
append_here_label [Logic_typing]
appends the Here label in the environment
append_init_label [Logic_typing]
appends the "Init" label in the environment
append_old_and_post_labels [Logic_typing]
append the Old and Post labels in the environment
append_pre_label [Logic_typing]
appends the "Pre" label in the environment
apply [Logic_env.Builtins]
adds all requested objects in the environment.
apply [Hook.S]
Apply all the functions of the hook on the given parameter.
apply1 [Lattice_type.Lattice_Set]
apply2 [Lattice_type.Lattice_Set]
apply_after_computed [Ast]
Apply the given hook just after building the AST.
apply_hooks_on_remove [Emitter.Make_table]
This function must be called on each binding which is removed from the table without directly calling the function remove.
apply_once [State_builder]
apply_once name dep f returns a closure applying f only once and the state internally used.
apply_tag [Gtk_helper]
arch_bigendian [Unmarshal]
arch_sixtyfour [Unmarshal]
areCompatibleTypes [Cabs2cil]
areCompatibleTypes ot nt checks that the two given types are compatible (C99, 6.2.7).
are_consistent [Structural_descr]
Not symmetrical: check that the second argument is a correct refinement of the first one.
are_preconds_unfolded [Pretty_source]
arg_name [Parameter_sig.Input_with_arg]
A standard name for the argument which may be used in the description.
argsToList [Cil]
Obtain the argument list ([] if None).
argsToPairOfLists [Cil]
argument_is_function_name [Parameter_customize]
Indicate that the string argument of the parameter must be a valid function name.
argument_may_be_fundecl [Parameter_customize]
Indicate that the argument of the parameter can match a valid function declaration (otherwise it has to match a defined functions).
argument_must_be_existing_fun [Parameter_customize]
Indicate that if the argument of the parameter does not match a valid function name, it raises an error whatever the value of the option -permissive is.
argument_must_be_fundecl [Parameter_customize]
Indicate that the argument of the parameter must match a valid function declaration.
arithmeticConversion [Cil]
returns the type of the result of an arithmetic operator applied to values of the corresponding input types.
arithmeticConversion [Cabs2cil]
returns the type of the result of an arithmetic operator applied to values of the corresponding input types.
arithmetic_conversion [Logic_typing]
array [Json]
Extract the array of an Array object.
array [Datatype]
array_exists [Extlib]
array_existsi [Extlib]
array_size [Ast_info]
array_to_ptr [Logic_utils]
transforms an array into pointer.
array_type [Ast_info]
array_with_range [Logic_utils]
array_with_range arr size returns the logic term array'+{0..(size-1)}, array' being array cast to a pointer to char
as_singleton [Extlib]
returns the unique element of a singleton list.
assigns_from_prototype [Infer_annotations]
assigns_inputs_to_zone [Db.Value]
Evaluation of the \from clause of an assigns clause.
assigns_outputs_to_locations [Db.Value]
Evaluation of the left part of assigns clause (without \from).
assigns_outputs_to_zone [Db.Value]
Evaluation of the left part of assigns clause (without \from).
assoc [Json]
Extract the list of an Assoc object.
ast_dependencies [Parameter_builder]
async [Task]
low level command for managing ressource with active wait
at_error_exit [Cmdline]
Register a hook executed whenever Frama-C exits with error (the exit code is greater than 0).
at_normal_exit [Cmdline]
Register a hook executed whenever Frama-C exits without error (the exit code is 0).
atan2 [Float_sig.S]
atan2 [Float_interval_sig.S]
atan2f [Floating_point]
attr [Cil_datatype.Global_annotation]
attributes tied to the global annotation.
attr [Cil_datatype.Global]
attributeClass [Cil]
Return the class of an attributes.
attributeName [Cil]
Returns the name of an attribute.
attributes [Dotgraph]
Flushes the buffer into a list of attributes
automatically_proven [Property_status]
Is the status of the given property only automatically handled by the kernel?
auxiliary_kf_stmt_state [Kernel_function]

B
back [History]
If possible, go back one step in the history.
back_edges [Loop]
Statements that are the origin of a back-edge to a natural loop.
backward_add [Float_interval_sig.S]
backward_cast [Float_interval_sig.S]
backward_cast_double_to_real [Fval]
backward_cast_float_to_double [Fval]
backward_cast_float_to_double d return all possible float32 f such that (double)f = d.
backward_comp_float_left_false [Ival]
Same as Ival.backward_comp_int_left, except that the arguments should now be floating-point values.
backward_comp_float_left_true [Ival]
backward_comp_int_left [Ival]
backward_comp_int op l r reduces l into l' so that l' op r holds.
backward_comp_left_false [Float_interval_sig.S]
backward_comp_left_false op prec f1 f2 attempts to reduce f1 into f1' so that the relation f1' op f2 doesn't holds.
backward_comp_left_true [Float_interval_sig.S]
backward_comp_left_true op prec f1 f2 attempts to reduce f1 into f1' so that the relation f1' op f2 holds.
backward_is_finite [Float_interval_sig.S]
backward_is_nan [Float_interval_sig.S]
backward_mult_int_left [Ival]
backward_sub [Float_interval_sig.S]
band [Bitvector]
base_access [Locations]
Conversion into a base access, with the size information.
behavior_assumes [Ast_info]
Builds the conjunction of the b_assumes.
behavior_names_of_stmt_in_kf [Annotations]
behavior_postcondition [Ast_info]
Builds the postcondition from b_assumes and b_post_cond clauses.
behavior_precondition [Ast_info]
Builds the precondition from b_assumes and b_requires clauses.
behaviors [Annotations]
Get the behaviors clause of the contract associated to the given function.
beq [Bitvector]
billion_one [Integer]
binary_predicate [Hptmap_sig.S]
Same functionality as generic_predicate but with a different signature.
bincopy [Command]
copy buffer cin cout reads cin until end-of-file and copy it in cout.
bind [Task]
bind t k first runs t.
bindings [Rangemap.S]
Return the list of all bindings of the given map.
bitfield_attribute_name [Cil]
Name of the attribute that is automatically inserted (with an AINT size argument when querying the type of a field that is a bitfield
bitsOffset [Cil]
Give a type of a base and an offset, returns the number of bits from the base address and the width (also expressed in bits) for the subobject denoted by the offset.
bitsSizeOf [Cil]
The size of a type, in bits.
bitsSizeOfBitfield [Cil]
Returns the size of the given type, in bits.
bitsSizeOfInt [Cil]
bits_of_float32_list [Float_interval_sig.S]
Bitwise reinterpretation of a floating-point interval of single precision into consecutive ranges of integers.
bits_of_float64_list [Float_interval_sig.S]
Bitwise reinterpretation of a floating-point interval of double precision into consecutive ranges of integers.
bits_of_max_double [Floating_point]
binary representation of -DBL_MAX and DBL_MAX as 64 bits signed integers
bits_of_max_float [Floating_point]
binary representation of -FLT_MAX and FLT_MAX as 32 bits signed integers
bits_of_most_negative_double [Floating_point]
bits_of_most_negative_float [Floating_point]
bits_sizeof [Base]
bitwise_and [Ival]
bitwise_and [Int_val]
bitwise_not [Ival]
bitwise_op2 [Bitvector]
bitwise_op3 [Bitvector]
bitwise_op4 [Bitvector]
bitwise_or [Ival]
bitwise_or [Int_val]
bitwise_signed_not [Ival]
bitwise_signed_not [Int_val]
bitwise_signed_not [Int_set]
bitwise_unsigned_not [Ival]
bitwise_unsigned_not [Int_val]
bitwise_xor [Ival]
bitwise_xor [Int_val]
block [Markdown]
Block element
block_from_unspecified_sequence [Cil]
creates a block with empty attributes from an unspecified sequence.
block_of_local [Ast_info]
local_block f vi returns the block of f in which vi is declared.
blocks_closed_by_edge [Kernel_function]
blocks_closed_by_edge s1 s2 returns the (possibly empty) list of blocks that are closed when going from s1 to s2.
blocks_opened_by_edge [Kernel_function]
blocks_opened_by_edge s1 s2 returns the (possibly empty) list of blocks that are opened when going from s1 to s2.
bnot [Bitvector]
body_visible [Filter.RemoveInfo]
tells if the body of a function definition is visible.
bold [Markdown]
Bold text
bool [Json]
Extract True and False only.
bool [Datatype]
boolean [Utf8_logic]
boolean_type [Logic_const]
bor [Bitvector]
bot_of_list [Bottom]
bottom [Utf8_logic]
bottom [Origin]
bottom [Map_lattice.MapSet_Lattice]
bottom [Map_lattice.Value]
bottom [Lmap_sig]
Every location is associated to the value bottom of type v in this state.
bottom [Dataflows.JOIN_SEMILATTICE]
Must verify that forall a, join a bottom = a.
bottom [Lattice_type.Bounded_Join_Semi_Lattice]
smallest element
bottom_string [Unicode]
box [Wbox]
Generic packing.
bprintf [Rich_text]
bprintf [Dotgraph]
Add text material to buffer label.
breakpoint [Project.Undo]
bs_identifier [Logic_lexer]
buffer [Source_viewer]
buffer [Dotgraph]
Create a buffer initialized with the given attributes.
build_cil_file [Filter.F]
build_wto [Interpreted_automata.Compute]
Extract an exit strategy from a component, i.e.
build_wto_index_table [Interpreted_automata.Compute]
Compute the index table from a wto
builtinLoc [Cil]
This is used as the location of the prototypes of builtin functions.
builtin_states [Logic_env]
builtin_types_as_typenames [Logic_env]
marks builtin logical types as logical typenames for the logic lexer.
button [Gtk_form]
bxor [Bitvector]
bytesAlignOf [Cil]
The minimum alignment (in bytes) for a type.
bytesSizeOf [Cil]
The size of a type, in bytes.
bytesSizeOfInt [Cil]
Returns the number of bytes (resp.

C
c_div [Integer]
Truncated division towards 0 (like in C99).
c_div_rem [Integer]
c_div_rem a b returns (c_div a b, c_rem a b).
c_rem [Ival]
c_rem [Integer]
Remainder of the truncated division towards 0 (like in C99).
c_rem [Int_val]
c_rem [Int_set]
c_rem [Int_interval]
cabslu [Cabshelper]
cache_size [Binary_cache]
Size of the caches.
cached_fold [Map_lattice.MapSet_Lattice]
cached_fold [Locations.Zone]
cached_fold [Locations.Location_Bytes]
Cached version of fold_i, for advanced users
cached_fold [Lmap_sig]
cached_fold [Hptmap_sig.S]
cached_map [Lmap_sig]
cached_map [Hptmap_sig.S]
call [Task]
The task that, when started, invokes a function and immediately returns the result.
call_to_kernel_function [Db.Value]
Return the functions that can be called from this call.
callback [Task]
Same as finally but the status of the task is discarded.
called_info [Filter.RemoveInfo]
called_info will be called only if the call statement is visible.
callers [Db.Value]
can_be_cea_function [Ast_info]
can_go_back [History]
Are there past events in the history.
can_go_forward [History]
Are there events to redo in the history.
cancel [Task]
cancel [Db]
Interrupt the currently running job at the next call to Db.yield as a Cancel exception is raised.
cancel_all [Task]
Cancel all scheduled tasks
canceled [Task]
The task that is immediately canceled
capacity [Vector]
Low-level interface.
capacity [Bitvector]
Maximum number of bits in the bitvector.
cardinal [State_selection.S]
Size of a selection.
cardinal [Rangemap.S]
Return the number of bindings of a map.
cardinal [Locations.Location_Bytes]
None if the cardinal is unbounded
cardinal [Ival]
cardinal v returns n if v has finite cardinal n, or None if the cardinal is not finite.
cardinal [Int_val]
cardinal [Int_set]
Returns the number of integers in a set.
cardinal [Int_interval]
Returns the number of integers represented by the given interval.
cardinal [Hptset.S_Basic_Compare]
cardinal [Hptmap_sig.S]
cardinal m returns m's cardinal, that is, the number of keys it binds, or, in other words, its domain's cardinal.
cardinal_estimate [Ival]
cardinal_estimate v ~size returns an estimation of the cardinal of v, knowing that v fits in size bits.
cardinal_estimate [Int_val]
cardinal_is_less_than [Ival]
Same than cardinal_less_than but just return if it is the case.
cardinal_is_less_than [Int_val]
cardinal_less_than [Locations.Location_Bytes]
cardinal_less_than v card returns the cardinal of v if it is less than card, or raises Not_less_than.
cardinal_less_than [Ival]
cardinal_less_than t n returns the cardinal of t is this cardinal is at most n.
cardinal_less_than [Int_val]
cardinal_less_than [Lattice_type.With_Enumeration]
Raises Abstract_interp.Not_less_than whenever the cardinal of the given lattice is strictly higher than the given integer.
cardinal_zero_or_one [Offsetmap_sig]
Returns true if and only if all the interval bound in the offsetmap are mapped to values with cardinal at most 1.
cardinal_zero_or_one [Locations.Location_Bytes]
cardinal_zero_or_one [Locations]
Is the location bottom or a singleton?
cardinal_zero_or_one [Ival]
cardinal_zero_or_one [Int_val]
cardinal_zero_or_one [Int_Base]
cardinal_zero_or_one [Lattice_type.With_Cardinal_One]
cast [Integer]
cast [Int_interval]
cast_float_to_float [Ival]
Cast the given float to the given size.
cast_float_to_int [Ival]
Casts the given float into an integer.
cast_float_to_int_inverse [Ival]
floating-point
cast_int_to_float [Ival]
cast_int_to_float [Float_interval_sig.S]
cast_int_to_float_inverse [Ival]
integer
cast_int_to_int [Ival]
cast_int_to_int [Int_val]
catch [Command]
category [Asm_contracts]
the corresponding code transformation category.
ceil [Fval]
ceil [Float_sig.S]
ceil [Float_interval_sig.S]
cfgFun [Cfg]
Compute a control flow graph for fd.
change_varinfo_name [Cil_const]
change_varinfo_name vi name changes the name of vi to name.
char [Datatype]
charConstPtrType [Cil]
char const *
charConstToInt [Cil]
Given the character c in a (CChr c), sign-extend it to 32 bits.
charConstToIntConstant [Cil]
charPtrType [Cil]
char *
charType [Cil]
char
char_at [Rich_text]
check [Int_interval]
Checks that the interval defined by min, max, rem, modu is well formed.
check [Gtk_form]
check [Abstract_interp.Rel]
check_ast [Filecheck]
Visits the given AST (defaults to the AST of the current project) to check whether it is consistent.
check_sequences [Undefined_sequence]
checks [Kernel]
childrenBehavior [Cil]
choose [Rangemap.S]
Return one binding of the given map, or raise Not_found if the map is empty.
choose [Hptset.S_Basic_Compare]
chr [Logic_lexer]
clean [Log]
Flushes the last transient message if necessary.
cleanup [Structural_descr]
cleanup_all_tags [Gtk_helper]
cleanup_at_exit [Extlib]
cleanup_at_exit file indicates that file must be removed when the program exits (except if exit is caused by a signal).
cleanup_tag [Gtk_helper]
clear [Warning_manager]
Clear all the stored warnings.
clear [Vector]
Do not modify actual capacity.
clear [State_builder.Weak_hashtbl]
Clear the table.
clear [State.Local]
How to clear a state.
clear [Source_manager]
Remove all pages added by load_file
clear [Sanitizer]
clear [Qstack.Make]
Remove all the elements of a stack.
clear [Project]
Clear the given project.
clear [Pretty_source.Locs]
clear [Parameter_sig.S_no_parameter]
Set the option to its default value, that is the value if set was never called.
clear [Gtk_helper.Icon]
Reloads the builtin icons from the theme specified in the configuration.
clear [Dynamic.Parameter.Common]
clear [Dotgraph.Node]
clear [Hook.S]
Clear the hook.
clear [Dataflow2.StmtStartData]
clear [State_builder.Ref]
Reset the reference to its default value.
clear [State_builder.Hashtbl]
Clear the table.
clear [Bitvector]
clear [Binary_cache.Arity_Three]
clear [Binary_cache.Arity_Two]
clear [Binary_cache.Arity_One]
clear [Binary_cache.Symmetric_Binary_Predicate]
clear [Binary_cache.Binary_Predicate]
clear [Binary_cache.Symmetric_Binary]
clearCFGinfo [Cfg]
clear the sid, succs, and preds fields of each statement in a function
clearConfiguration [Cilconfig]
Clear all configuration data
clearFileCFG [Cfg]
clear the sid (except when clear_id is explicitly set to false), succs, and preds fields of each statement.
clear_all [Project]
Clear all the projects: all the internal states of all the projects are now empty (wrt the action registered with register_todo_after_global_clear and Project.register_todo_after_clear.
clear_breakpoint [Project.Undo]
clear_caches [Offsetmap_sig]
Clear the caches local to this module.
clear_caches [Offsetmap_bitwise_sig]
Clear the caches local to this module.
clear_caches [Lmap_sig]
Clear the caches local to this module.
clear_caches [Lmap_bitwise.Location_map_bitwise]
Clear the caches local to this module.
clear_caches [Hptmap_sig.S]
Clear all the persistent caches used internally by the functions of this module.
clear_caches [Hptset.S]
Clear all the caches used internally by the functions of this module.
clear_errors [Errorloc]
clear_funspec [Logic_utils]
Reset the given funspec to empty.
clear_garbled_mix [Locations.Location_Bytes]
Clear the information on created garbled mix.
clear_last_decl [Ast]
reset the mapping between a varinfo and the last global introducing it.
clear_sid_info [Kernel_function]
removes any information related to statements in kernel functions.
clear_some_projects [State.Local]
clear_if_project f x must clear any value v of type project of x such that f v is true.
clone_defined_kernel_function [Clone]
Returns a clone of a kernel function and adds it into the AST next to the old one
close [Dotgraph]
close_predicate [Cil]
Bind all free variables with an universal quantifier
cmp_ieee [Float_sig.S]
IEEE comparison: do not distinguish between -0.0 and 0.0.
code [Markdown]
Inline code
code_annot [Logic_typing.Make]
code_annot loc behaviors rt annot type-checks an in-code annotation.
code_annot [Db.Properties.Interp]
code_annot [Annotations]
Get all the code annotations attached to the given statement.
code_annot_emitter [Annotations]
Same as Annotations.code_annot, but also returns the emitter who emitted the annotation.
code_annot_filter [Db.Properties.Interp.To_zone]
To quickly build an annotation filter
code_annot_of_kf [Annotations]
code_annot_state [Annotations]
The state which stores all the code annotations of the program.
codeblock [Markdown]
codeblock lang "...." returns a Code_block for code, written in lang with the given formatted content.
codename [Fc_config]
Frama-C version codename.
coerce_type [Logic_utils]
C type to logic type, with implicit conversion for arithmetic types.
collapse [Abstract_interp.Collapse]
collections [Parameter_state]
combinePredecessors [Dataflow2.ForwardsTransfer]
Take some old data for the given statement, and some new data for the same point.
combineStmtStartData [Dataflow2.BackwardsTransfer]
When the analysis reaches the start of a block, combine the old data with the one we have just computed.
combineSuccessors [Dataflow2.BackwardsTransfer]
Take the data from two successors and combine it
command [Task]
Immediately launch a system-process.
command [Command]
Same arguments as .
command_async [Command]
Same arguments as .
comment [Logic_lexer]
common_block [Kernel_function]
common_block s1 s2 returns the innermost block that contains both s1 and s2, provided the statements belong to the same function.
compFullName [Cil]
Get the full name of a comp, including the 'struct' or 'union' prefix
compare [Type]
compare [Transitioning.Stdlib]
compare [Project]
compare [Json]
Pervasives
compare [Integer]
compare [Indexer.Elt]
compare [Hptset.S_Basic_Compare]
compare [Hptmap.Shape]
compare [Hook.Comparable]
compare [Fval.F]
compare [Float_sig.S]
Comparison that distinguishes -0.0 and 0.0.
compare [Float_interval_sig.S]
compare [Datatype.Make_input]
compare [Datatype.S_no_copy]
Comparison: same spec than Pervasives.compare.
compare [Datatype.Undefined]
compare [Datatype]
compare [Filepath.Normalized]
Compares normalized paths
compare [Bottom]
compare [Bitvector]
compare [Abstract_interp.Rel]
compareConstant [Cil]
true if the two constant are equal.
compare_basic [Extlib]
Use this function instead of Pervasives.compare, as this makes it easier to find incorrect uses of the latter
compare_ignore_case [Extlib]
Case-insensitive string comparison.
compare_predicate [Logic_utils]
compare_pretty [Filepath.Normalized]
Compares prettified (i.e.
compare_term [Logic_utils]
comparison compatible with is_same_term
compilation_unit_names [Fc_config]
List of names of all kernel compilation units.
compinfo [Visitor_behavior.Fold]
compinfo [Visitor_behavior.Iter]
compinfo [Visitor_behavior.Unset]
compinfo [Visitor_behavior.Set]
compinfo [Visitor_behavior.Get]
compinfo [Visitor_behavior.Reset]
complement_int_under [Ival]
Returns an under-approximation of the integers of the given size and signedness that are *not* represented by the given ival.
complement_under [Int_val]
Returns an under-approximation of the integers of the given size and signedness that are *not* represented by the given value.
complement_under [Int_set]
complement_under [Int_interval]
Returns an under-approximation of the integers between min and max that are *not* represented by the given interval.
complete [Annotations]
Get the complete behaviors clause of the contract associated to the given function.
complete_behaviors [Ast_info]
Builds the disjoint_behaviors property for the behavior names.
complete_types [Logic_utils]
give complete types to terms that refer to a variable whose type has been completed after its use in an annotation.
compose [Hptmap.Comp_unused]
compositional_bool [Hptmap_sig.S]
Value of the compositional boolean associated to the tree, as computed by the Compositional_bool argument of the functor.
compute [Service_graph.S]
compute [Exn_flow]
computes the information if not already done.
compute [Db.INOUTKF]
compute [Db.RteGen]
Same result as having -rte on the command line
compute [Db.PostdominatorsTypes.Sig]
compute [Db.From]
compute [Db.Value]
Compute the value analysis using the entry point of the current project.
compute [Dataflow2.Backwards]
Fill in the T.stmtStartData, given a number of initial statements to start from (the sinks for the backwards data flow).
compute [Dataflow2.Forwards]
Fill in the T.stmtStartData, given a number of initial statements to start from.
compute [Ast]
Enforce the computation of the AST.
computeFileCFG [Cfg]
Compute the CFG for an entire file, by calling cfgFun on each function.
computeFirstPredecessor [Dataflow2.ForwardsTransfer]
computeFirstPredecessor s d is called when s is reached for the first time (i.e.
compute_all [Db.From]
compute_all_calldeps [Db.From]
compute_strategy [Dataflow2.Forwards]
Same as compute but using a given strategy, instead of the default strategy computed by the Wto module.
compute_worklist [Dataflow2.Forwards]
Same as compute but using only a working list of statements instead of iterating on a weak topological ordering.
concat [Datatype.Filepath]
concat [Filepath.Normalized]
concat [Bitvector]
concat b1 s1 b2 s2 concatenates the s1 first bits of b1 with the s2 first bits of b2.
concat [Bag]
concat_allocation [Logic_utils]
Concatenates two allocation clauses if both are defined, returns FreeAllocAny if one (or both) of them is FreeAllocAny.
concat_assigns [Logic_utils]
Concatenates two assigns if both are defined, returns WritesAny if one (or both) of them is WritesAny.
concerned_intervals [Rangemap.Make]
Intervals that match the given key.
cond_edge_visible [Filter.RemoveInfo]
cond_edge_visible f s implies that s is an 'if' in f.
condition_truth_value [Db.Value]
Provided stmt is an 'if' construct, fst (condition_truth_value stmt) (resp.
config_bool [Gtk_helper.Configuration]
config_float [Gtk_helper.Configuration]
config_int [Gtk_helper.Configuration]
config_string [Gtk_helper.Configuration]
config_values [Gtk_helper.Configuration]
The values field is used as a dictionary of available values.
conj [Utf8_logic]
connected_component [Dataflows.FUNCTION_ENV]
constFold [Cil]
Do constant folding on an expression.
constFoldBinOp [Cil]
Do constant folding on a binary operation.
constFoldOffset [Cil]
Do constant folding on a Cil_types.offset.
constFoldTerm [Cil]
Do constant folding on an term.
constFoldTermNodeAtTop [Cil]
Do constant folding on an term at toplevel only.
constFoldTermToInt [Logic_utils]
constFoldToInt [Cil]
Do constant folding on the given expression, just as constFold would.
constFoldVisitor [Cil]
A visitor that does constant folding.
constGlobSubstVisitor [Substitute_const_globals]
constant_expr [Ast_info]
constant_term [Ast_info]
constant_to_lconstant [Logic_utils]
constfold [File]
category for syntactic constfolding (done after cleanup)
contains_a_zero [Float_interval_sig.S]
contains_addresses_of_any_locals [Locations.Location_Bytes]
contains_addresses_of_any_locals loc returns true iff loc contains the address of a local variable or of a formal variable.
contains_addresses_of_locals [Locations.Location_Bytes]
contains_addresses_of_locals is_local loc returns true if loc contains the address of a variable for which is_local returns true
contains_nan [Float_interval_sig.S]
contains_neg_infinity [Float_interval_sig.S]
contains_neg_zero [Float_interval_sig.S]
contains_non_zero [Ival]
contains_non_zero [Int_val]
contains_non_zero [Float_interval_sig.S]
contains_plus_zero [Fval]
contains_pos_infinity [Float_interval_sig.S]
contains_pos_zero [Float_interval_sig.S]
contains_result [Logic_utils]
true if \result is included in the term
contains_single_elt [Hptset.S]
contains_zero [Ival]
contains the zero value (including -0.
contains_zero [Int_val]
contents [Sanitizer]
contents [Rich_text]
Similar to Buffer.contents
convFile [Cabs2cil]
copy [Visitor_behavior]
Makes fresh copies of the mutable structures.
copy [Project]
Copy a project into another one.
copy [Datatype.Make_input]
copy [Datatype.Undefined]
copy [Datatype]
copy [Dataflow2.ForwardsTransfer]
Make a deep copy of the data.
copy [Command]
copy source target copies source file to target file using bincopy.
copy [Datatype.S]
Deep copy: no possible sharing between x and copy x.
copyCompInfo [Cil_const]
Makes a shallow copy of a Cil_types.compinfo changing the name.
copyVarinfo [Cil]
Make a shallow copy of a varinfo and assign a new identifier.
copy_and_rename [Parameter_category]
copy_and_rename s ~register c renames the category c into s and returns the new built category which is registered according to register.
copy_exp [Cil]
performs a deep copy of an expression (especially, avoid eid sharing).
copy_offsetmap [Lmap_sig]
copy_offsetmap alarms loc size m returns the superposition of the ranges of size bits starting at loc within m.
copy_slice [Offsetmap_sig]
copy_slice ~validity ~offsets ~size m copies and merges the slices of m starting at offsets offsets and of size size.
copy_with_new_vid [Cil_const]
returns a copy of the varinfo with a fresh vid.
correctness_parameters [Emitter.Usable_emitter]
correctness_parameters [Emitter]
cos [Float_sig.S]
cos [Float_interval_sig.S]
cosf [Floating_point]
count [State_builder.Weak_hashtbl]
Length of the table.
create [Vector]
create [Type.Obj_tbl]
create [Type.Ty_tbl]
create [Type.Heterogeneous_table]
create n creates a new table of initial size n.
create [Structural_descr.Recursive]
create [State_builder.Proxy]
create s k sk l creates a new proxy with the given name, kinds and states inside it.
create [State.Local]
How to create a new fresh state which must be equal to the initial state: that is, if you never change the state, create () and get
        ()
must be equal (see invariant 1 below).
create [State]
create [Sanitizer]
create [Rich_text]
Create a buffer.
create [Rangemap.S]
create [Qstack.Make]
Create a new empty stack.
create [Project]
Create a new project with the given name and attach it after the existing projects (so the current project, if existing, is unchanged).
create [Printer_tag.Tag]
create [Pretty_source.Locs]
create [Parameter_category]
create name ty ~register states access creates a category of the given name for the given type.
create [Offsetmap_sig]
create ~size v ~size_v creates an offsetmap of size size in which the intervals k*size_v .. (k+1)*size_v-1 with 0<= k <= size/size_v are all mapped to v.
create [Offsetmap_bitwise_sig]
size must be strictly greater than zero.
create [Emitter]
Emitter.create name kind ~correctness ~tuning creates a new emitter with the given name.
create [Datatype.Sub_caml_weak_hashtbl]
create [Bitvector]
Create a vector of n bits, with all bits unset.
create_all_values [Ival]
create_all_values [Int_val]
Builds an abstraction of all integers in a C integer type.
create_alpha_renaming [Cil]
creates a visitor that will replace in place uses of var in the first list by their counterpart in the second list.
create_by_copy [Project]
Return a new project with the given name by copying some states from the project src.
create_by_copy_hook [Project]
Register a hook to call at the end of Project.create_by_copy.
create_isotropic [Offsetmap_sig]
Same as Offsetmap_sig.create, but for values that are isotropic.
create_predicate [Alarms]
Generate the predicate corresponding to a given alarm.
create_project_from_visitor [File]
Return a new project with a new cil file representation by visiting the file of the current project.
create_rebuilt_project_from_visitor [File]
Like File.create_project_from_visitor, but the new generated cil file is generated into a temp .i or .c file according to preprocess, then re-built by Frama-C in the returned project.
create_set [Bitvector]
Create a vector of n bits, with all bits set.
create_variable_validity [Base]
ctype_of_array_elem [Logic_typing]
ctype_of_pointed [Logic_typing]
current [Project]
The current project.
current [Origin]
This is automatically extracted from Cil.CurrentLoc
currentLoc [Errorloc]
currentLoc [Clexer]
current_loc [Origin.LocationLattice]
current_printer [Printer_api.S]
Returns the current pretty-printer, with all the extensions added using Printer_api.S.update_printer.
custom [Logic_typing.Make]
custom_list [Gtk_helper.MAKE_CUSTOM_LIST]
custom_related_nodes [Db.Pdg]
custom_related_nodes get_dpds node_list build a list, starting from the node in node_list, and recursively add the nodes given by the function get_dpds.
cvar_to_lvar [Cil]
Convert a C variable into the corresponding logic variable.

D
d_cabsloc [Cabshelper]
d_formatarg [Cil]
datadir [Fc_config]
Directory where architecture independent files are.
datadirs [Fc_config]
Directories where architecture independent files are in order of priority.
debug [Log.Messages]
Debugging information dedicated to Plugin developers.
debug [Dataflow2.BackwardsTransfer]
Whether to turn on debugging
debug [Dataflow2.ForwardsTransfer]
Whether to turn on debugging
debug_atleast [Log.Messages]
decide_fast_inclusion [Hptmap_sig.S]
Function suitable for the decide_fast argument of binary_predicate, when testing for inclusion of the first map into the second.
decide_fast_intersection [Hptmap_sig.S]
Function suitable for the decide_fast argument of symmetric_binary_predicate when testing for a non-empty intersection between two maps.
declare_markers [Design.Feedback]
Declares the icons used for the property status bullets, as marks in the left-margin of the source buffer.
decorate [Dotgraph]
Concat the attributes with flagged ones
decreases [Annotations]
If any, get the decrease clause of the contract associated to the given function.
def_or_last_decl [Ast]
def_or_last_decl v returns the global g declaring or defining g such that is_def_or_last_decl g is true.
default [Parameter_sig.Collection_category]
The '@default' category.
default [Lmap_bitwise.With_default]
default [Gtk_helper.Icon]
default [Cmdline.Group]
default_behavior_name [Cil]
default_edge_attributes [State_dependency_graph.Attributes]
default_icon [Widget]
default_msg_keys [Plugin]
Debug message keys set by default for the plugin.
default_vertex_attributes [State_dependency_graph.Attributes]
default_widen_hints [Float_sig.Widen_Hints]
define [Dotgraph.Node]
Pushes the callback which will be executed once for all created nodes.
del_debug_keys [Log.Messages]
removes the given categories from the set for which messages are printed.
delete [State]
demon [Gtk_form]
dependencies [State_builder.Info]
Dependencies of this internal state.
dependencies [Parameter_sig.Input_collection]
dependent_pair [Descr]
Similar to Unmarshal.Dependent_pair, but safe.
deprecated [Log.Messages]
deprecated s ~now f indicates that the use of f of name s is now deprecated.
descr [Datatype.S_no_copy]
Datatype descriptor.
description [Markdown]
Description list
diff [State_selection.S]
Difference between two selections.
diff [Locations.Location_Bytes]
Over-approximation of difference.
diff [Lattice_type.With_Diff]
diff t1 t2 is an over-approximation of t1-t2.
diff [Hptset.S_Basic_Compare]
diff [Eva_lattice_type.With_Diff]
diff t1 t2 is an over-approximation of t1-t2.
diff_if_one [Locations.Location_Bytes]
Over-approximation of difference.
diff_if_one [Lattice_type.With_Diff_One]
diff_if_one t1 t2 is an over-approximation of t1-t2.
diff_if_one [Int_set]
diff_if_one [Eva_lattice_type.With_Diff_One]
diff_if_one t1 t2 is an over-approximation of t1-t2.
diff_with_shape [Hptmap_sig.S]
diff_with_shape s m keeps only the elements of m that are not bound in the map s.
digest [Type]
direct_addr_dpds [Db.Pdg]
Similar to Db.Pdg.direct_dpds, but for address dependencies only.
direct_addr_uses [Db.Pdg]
Similar to Db.Pdg.direct_uses, but for address dependencies only.
direct_array_size [Ast_info]
direct_ctrl_dpds [Db.Pdg]
Similar to Db.Pdg.direct_dpds, but for control dependencies only.
direct_ctrl_uses [Db.Pdg]
Similar to Db.Pdg.direct_uses, but for control dependencies only.
direct_data_dpds [Db.Pdg]
Similar to Db.Pdg.direct_dpds, but for data dependencies only.
direct_data_uses [Db.Pdg]
Similar to Db.Pdg.direct_uses, but for data dependencies only.
direct_dpds [Db.Pdg]
Get the nodes to which the given node directly depend on.
direct_element_type [Ast_info]
direct_pointed_type [Ast_info]
direct_uses [Db.Pdg]
build a list of all the nodes that have direct dependencies on the given node.
disj [Utf8_logic]
disjoint [Annotations]
If any, get the disjoint behavior clause of the contract associated to the given function.
disjoint_behaviors [Ast_info]
Builds the disjoint_behaviors property for the behavior names.
display [Db.INOUTKF]
display [Db.PostdominatorsTypes.Sig]
display [Db.From]
display [Db.Value]
display_external [Db.Outputs]
display_source [Pretty_source]
The selector and the highlighter are always host#protected.
display_with_formals [Db.Inputs]
distinct_correctness_parameters [Emitter]
Return the correctness_parameters which distinguishes this usable emitter from the other ones.
distinct_tuning_parameters [Emitter]
Return the tuning parameter which distinguishes this usable emitter from the other ones.
div [Ival]
Integer division
div [Int_val]
div [Int_interval]
div [Float_sig.S]
div [Float_interval_sig.S]
dkey [Project_skeleton.Output]
dkey_alpha [Kernel]
dkey_alpha_undo [Kernel]
dkey_asm_contracts [Kernel]
dkey_ast [Kernel]
dkey_check [Kernel]
dkey_comments [Kernel]
dkey_compilation_db [Kernel]
dkey_constfold [Kernel]
dkey_dataflow [Kernel]
dkey_dataflow_scc [Kernel]
dkey_dominators [Kernel]
dkey_emitter [Kernel]
dkey_emitter_clear [Kernel]
dkey_exn_flow [Kernel]
dkey_file_annot [Kernel]
dkey_file_print_one [Kernel]
dkey_file_transform [Kernel]
dkey_filter [Kernel]
dkey_globals [Kernel]
dkey_kf_blocks [Kernel]
dkey_linker [Kernel]
dkey_linker_find [Kernel]
dkey_loops [Kernel]
dkey_name [Log.Messages]
returns the category name as a string.
dkey_parser [Kernel]
dkey_pp [Kernel]
dkey_print_attrs [Kernel]
dkey_print_bitfields [Kernel]
dkey_print_builtins [Kernel]
dkey_print_logic_coercions [Kernel]
dkey_print_logic_types [Kernel]
dkey_print_sid [Kernel]
dkey_print_unspecified [Kernel]
dkey_print_vid [Kernel]
dkey_prop_status [Kernel]
dkey_prop_status_emit [Kernel]
dkey_prop_status_graph [Kernel]
dkey_prop_status_merge [Kernel]
dkey_prop_status_reg [Kernel]
dkey_referenced [Kernel]
dkey_rmtmps [Kernel]
dkey_task [Kernel]
dkey_typing_cast [Kernel]
dkey_typing_chunk [Kernel]
dkey_typing_global [Kernel]
dkey_typing_init [Kernel]
dkey_typing_pragma [Kernel]
dkey_ulevel [Kernel]
dkey_visitor [Kernel]
doEdge [Dataflow2.ForwardsTransfer]
what to do when following the edge between the two given statements.
doGuard [Dataflow2.ForwardsTransfer]
Generate the successors act_th, act_el to an If statement.
doInstr [Dataflow2.BackwardsTransfer]
The (backwards) transfer function for an instruction.
doInstr [Dataflow2.ForwardsTransfer]
The (forwards) transfer function for an instruction, internally called by Dataflow2.ForwardsTransfer.doStmt when the returned action is not SDone.
doStmt [Dataflow2.BackwardsTransfer]
The (backwards) transfer function for a branch.
doStmt [Dataflow2.ForwardsTransfer]
The (forwards) transfer function for a statement.
doVisit [Cil]
doVisit vis deepCopyVisitor copy action children node visits a node (or its copy according to the result of copy) and if needed its children.
doVisitList [Cil]
same as above, but can return a list of nodes
do_all_rte [Db.RteGen]
Generates all possible RTE for a given function.
do_iterate [Parameter_customize]
Ensure that iter_on_plugins is applied to this parameter.
do_not_iterate [Parameter_customize]
Prevent iter_on_plugins to be applied on the parameter.
do_not_journalize [Parameter_customize]
Prevent journalization of the parameter.
do_not_projectify [Parameter_customize]
Prevent projectification of the parameter: its state is shared by all the existing projects.
do_not_reset_on_copy [Parameter_customize]
Prevents resetting the parameter to its default value when creating a project from a copy visitor.
do_not_save [Parameter_customize]
Prevent serialization of the parameter.
do_rte [Db.RteGen]
Generates all possible RTE except pre-conditions for a given function.
do_tooltip [Gtk_helper]
Add the given tooltip to the given widget.
do_track_garbled_mix [Locations.Location_Bytes]
dominates [Dominators]
dominates a b tells whether a dominates b.
dot [Fc_config]
Dot command name.
doubleType [Cil]
double
dropAttribute [Cil]
Remove all attributes with the given name.
dropAttributes [Cil]
Remove all attributes with names appearing in the string list.
dummy [State]
A dummy state.
dummy [Project_skeleton]
dummy [Kernel_function]
dummy [Emitter]
dummy [Datatype.Filepath]
dummy [Cil_datatype.Varinfo]
dummy [Cil_datatype.Exp]
dummyFile [Cil]
A dummy file
dummyInstr [Cil]
A instr to serve as a placeholder
dummyStmt [Cil]
A statement consisting of just dummyInstr.
dummy_exp [Cil]
creates an expression with a dummy id.
dummy_state_on_disk [State]
dummy_unique_name [State]
dump [State_dependency_graph.Dot]
dump [State_dependency_graph]
dump [Property_status.Consolidation_graph]
dump_messages [Messages]
Dump stored messages to standard channels
dynamic [Descr]
Similar to Unmarshal.Dynamic.

E
e [Hptmap.Comp_unused]
e [Fval]
Real representation of \e.
e_div [Integer]
Euclidean division (that returns a positive rem).
e_div_rem [Integer]
e_div_rem a b returns (e_div a b, e_rem a b).
e_loc_of_stmt [Property]
create a Loc_contract or Loc_stmt depending on the kinstr.
e_rem [Integer]
Remainder of the Euclidean division (always positive).
e_rem [Abstract_interp.Rel]
echo [Log]
Display an event of the terminal, unless echo has been turned off.
edge [Dotgraph]
Create an edge with attributes
edge_attributes [State_dependency_graph.Attributes]
edge_default [Dotgraph]
Set default edge attributes
eight [Integer]
element_type [Ast_info]
elements [Hptset.S_Basic_Compare]
elements [Bag]
Might have n^2 complexity in worst cases.
elt [Bag]
emit [Property_status]
emit e ~hyps p s indicates that the status of p is s, is emitted by e, and is based on the list of hypothesis hyps.
emit [Lattice_messages]
Emit a message.
emit_and_get [Property_status]
Like Property_status.emit but also returns the computed status.
emit_approximation [Lattice_messages]
emit_costly [Lattice_messages]
emit_imprecision [Lattice_messages]
emitter [Db.Value]
Emitter used by Value to emit statuses
emitter [Asm_contracts]
emitter for the generated annotations.
emitter_of_code_annot [Annotations]
emitter_of_global [Annotations]
emph [Markdown]
Emph text
empty [State_selection]
The empty selection.
empty [Rgmap]
The empty map.
empty [Rangemap.S]
The empty map.
empty [Offsetmap_sig]
offsetmap containing no interval.
empty [Offsetmap_bitwise_sig]
offsetmap containing no interval.
empty [Logic_typing.Lenv]
empty [Lmap_bitwise.Location_map_bitwise]
empty [Indexer.Make]
empty [Hptset.S_Basic_Compare]
empty [Hptmap_sig.S]
the empty map
empty [Dotgraph.Map]
empty [Bag]
empty [Lattice_type.Lattice_Set]
emptyFunction [Cil]
Make an empty function
emptyFunctionFromVI [Cil]
Make an empty function from an existing global varinfo.
empty_funspec [Cil]
empty_local_env [Cabs2cil]
an empty local environment.
empty_map [Lmap_sig]
Empty map.
empty_map [Lmap_bitwise.Location_map_bitwise]
empty_size_cache [Cil]
Create a fresh size cache with Not_Computed
emptyset [Utf8_logic]
emptyset_string [Unicode]
enable_all [Parameter_sig.Collection_category]
The category '@all' is enabled in positive occurrences, with the given interpretation.
enable_all_as [Parameter_sig.Collection_category]
The category '@all' is equivalent to the given category.
encapsulate_local_vars [Oneret]
If there are local variables with destructors belonging to the main block of f, encapsulate_local_vars f will move ret, the return statement of f outside of this main block (changing f.sbody to a two-statement block composed of the old block and ret) to avoid having gotos to ret bypassing the initialization of these variables.
end_user [Emitter]
The special emitter corresponding to the end-user.
endline [Logic_lexer]
enter_kw_c_mode [Logic_utils]
enter_post_state [Logic_typing]
enter a given post-state.
enter_rt_type_mode [Logic_utils]
entry_point [Service_graph.S]
compute must be called before
entry_point [Globals]
enum [Markdown]
Enumerated list
enumerate_bits [Locations]
enumerate_bits_under [Locations]
enumerate_valid_bits [Locations]
enumerate_valid_bits_under [Locations]
enuminfo [Visitor_behavior.Fold]
enuminfo [Visitor_behavior.Iter]
enuminfo [Visitor_behavior.Unset]
enuminfo [Visitor_behavior.Set]
enuminfo [Visitor_behavior.Get]
enuminfo [Visitor_behavior.Reset]
enumitem [Visitor_behavior.Fold]
enumitem [Visitor_behavior.Iter]
enumitem [Visitor_behavior.Unset]
enumitem [Visitor_behavior.Set]
enumitem [Visitor_behavior.Get]
enumitem [Visitor_behavior.Reset]
eq [Utf8_logic]
equal [Type]
equal [Qstack.DATA]
equal [Project]
equal [Parameter_sig.S_no_parameter]
equal [Json]
Pervasives
equal [Integer]
equal [Hptset.S_Basic_Compare]
equal [Hptmap.Shape]
equal [Hook.Comparable]
equal [Fval.F]
Those functions distinguish -0.
equal [Float_interval_sig.S]
equal [Datatype.Make_input]
equal [Datatype.S_no_copy]
Equality: same spec than Pervasives.(=).
equal [Datatype.Undefined]
equal [Datatype]
equal [Filepath.Normalized]
equal [Bottom]
equal [Bitvector]
equal [Binary_cache.Cacheable]
equal [Abstract_interp.Rel]
equal_component [Wto.Make]
equal_partition [Wto.Make]
error [Task]
Extract error message form exception
error [Log.Messages]
user error: syntax/typing error, bad expected input, etc.
escape_char [Escape]
escape various constructs in accordance with C lexical rules
escape_string [Escape]
escape_underscores [Pretty_utils]
escape_wchar [Escape]
escape_wstring [Escape]
eval_expr [Db.Value]
eval_expr_with_state [Db.Value]
eval_lval [Db.Value]
eval_predicate [Db.Value.Logic]
Evaluate the given predicate in the given states for the Pre and Here ACSL labels.
evar [Cil]
Creates an expr representing the variable.
evt_category [Log]
Split an event category into its constituants.
exists [Utf8_logic]
exists [Rangemap.S]
exists p m checks if at least one binding of the map satisfy the predicate p.
exists [Map_lattice.MapSet_Lattice]
exists p t checks if one binding of t satisfies p.
exists [Locations.Location_Bytes]
exists [Parameter_sig.Set]
Is there some element satisfying the given predicate?
exists [Int_set]
exists [Hptset.S_Basic_Compare]
exists [Hptmap_sig.S]
for_all p m returns true if at least one binding of the map m satisfies the predicate p.
exists [Lattice_type.Lattice_Set]
exists2 [Rangemap.S]
exists2 f m1 m2 returns true if and only there exists k present in m1 or m2 such that f k v1 v2 holds, v_i being Some (find k m_i) if k is in m_i, and None otherwise (for i=1 or i=2)
existsType [Cil]
Scans a type by applying the function on all elements.
exit_kw_c_mode [Logic_utils]
exit_rt_type_mode [Logic_utils]
exit_strategy [Interpreted_automata.Compute]
Output the automaton in dot format
exit_strategy [Interpreted_automata]
Output the automaton in dot format
exp [Fval]
exp [Float_sig.S]
exp [Float_interval_sig.S]
expToAttrParam [Cil]
Convert an expression into an attrparam, if possible.
exp_info_of_term [Cil]
Extracts term information in an expression information
expand_to_path [Gtk_helper]
expf [Floating_point]
explodeStringToInts [Cabshelper]
expr [Db.Inputs]
expr_to_boolean [Logic_utils]
Returns a boolean term semantically equivalent to the condition of the original C-expression.
expr_to_ipredicate [Logic_utils]
Returns a predicate semantically equivalent to the condition of the original C-expression.
expr_to_kernel_function [Db.Value]
expr_to_kernel_function_state [Db.Value]
expr_to_predicate [Logic_utils]
Returns a predicate semantically equivalent to the condition of the original C-expression.
expr_to_term [Logic_utils]
Returns a logic term that has exactly the same semantics as the original C-expression.
ext_spec [Logic_parser]
ext_spec [Logic_lexer]
extend [State_builder.Proxy]
Add some states in the given proxy.
extend [Logic_env.Builtins]
request an addition in the environment.
extend [Hook.S_ordered]
extend [Hook.S]
Add a new function to the hook.
extend [Db.Main]
Register a function to be called by the Frama-C main entry point.
extend_checker [Filecheck]
Allows to register an extension to current checks.
extend_once [Hook.S_ordered]
extend_once [Hook.S]
Same as extend, but the hook is added only if it is not already present; the comparison is made using (==)
extension_category [Logic_env]
extract [Db.Pdg]
Pretty print pdg into a dot file.
extract_bits [Offsetmap_lattice_with_isotropy]
Extract the bits between start and stop in the value of type t, assuming this value has size bits.
extract_bits [Ival]
Extract bits from start to stop from the given Ival, start and stop being included.
extract_bits [Integer]
extract_bits [Int_val]
Extracts bits from start to stop from the given integer abstraction, start and stop being included.
extract_contract [Logic_utils]
extract_free_logicvars_from_predicate [Cil]
extract logic_var elements from a predicate
extract_free_logicvars_from_term [Cil]
extract logic_var elements from a term
extract_labels_from_annot [Cil]
extract logic_label elements from a code_annotation
extract_labels_from_pred [Cil]
extract logic_label elements from a pred
extract_labels_from_term [Cil]
extract logic_label elements from a term
extract_loop_pragma [Logic_utils]
extract_stmts_from_labels [Cil]
extract stmt elements from logic_label elements
extract_varinfos_from_exp [Cil]
extract varinfo elements from an exp
extract_varinfos_from_lval [Cil]
extract varinfo elements from an lval

F
f [Hptmap.Comp_unused]
failed [Task]
The task that immediately fails by raising a Failure exception.
failure [Log.Messages]
internal error of the plug-in.
fast_equal [Rangemap.Value]
fast_equal is used to reduce memory allocation in some cases.
fatal [Log.Messages]
internal error of the plug-in.
fc_local_static [Cabs2cil]
Name of the attribute used to indicate that a given static variable has a local syntactic scope (despite a global lifetime).
fct_info [Filter.RemoveInfo]
This function will be called for each function of the source program.
fct_name [Filter.RemoveInfo]
useful when we want to have several functions in the result for one source function.
feedback [Log.Messages]
Progress and feedback.
field [Json]
Lookup a field in an object.
fieldinfo [Visitor_behavior.Fold]
fieldinfo [Visitor_behavior.Iter]
fieldinfo [Visitor_behavior.Unset]
fieldinfo [Visitor_behavior.Set]
fieldinfo [Visitor_behavior.Get]
fieldinfo [Visitor_behavior.Reset]
file [Logic_preprocess]
file [Logic_lexer]
file [Cparser]
filename [Command]
files_pre_register_state [File]
fill [Journal.Reverse_binding]
filter [Rangemap.S]
filter p m returns the map with all the bindings in m that satisfy predicate p.
filter [Qstack.Make]
Return all data of the stack satisfying the specified predicate.
filter [Int_set]
filter [Indexer.Make]
Linear.
filter [Hptset.S_Basic_Compare]
filter [Hptmap_sig.S]
filter f t keep only the bindings of m whose key verify f.
filter [Bag]
filter [Lattice_type.Lattice_Set]
filterAttributes [Cil]
Retains attributes with the given name
filterStmt [Dataflow2.BackwardsTransfer]
Whether to put this predecessor block in the worklist.
filter_base [Locations.Zone]
filter_base can't raise Error_Top since it filters bases of Top
        bases
.
filter_base [Locations.Location_Bytes]
filter_base [Locations]
filter_base [Lmap_sig]
Remove from the map all the bases that do not satisfy the predicate.
filter_base [Lmap_bitwise.Location_map_bitwise]
filter_by_shape [Lmap_sig]
Remove from the map all the bases that are not also present in the given Base.t-indexed tree.
filter_keys [Map_lattice.MapSet_Lattice]
filter_map [Extlib]
filter_map' [Extlib]
filter_map_opt [Extlib]
Combines filter and map.
filter_out [Extlib]
Filter out elements that pass the test
filter_qualifier_attributes [Cil]
retains attributes corresponding to type qualifiers (6.7.3)
finally [Task]
finally t cb runs task t and always calls cb s when t exits with status s.
find [Vector]
Default exception is Not_found.
find [Type.Obj_tbl]
find [Type.Ty_tbl]
find [Type.Heterogeneous_table]
find tbl s ty returns the binding of s in the table tbl.
find [State_builder.States]
find [State_builder.Weak_hashtbl]
find x returns an instance of x found in table.
find [Rgmap]
Find the tightest entry containing the specified range.
find [Rangemap.S]
find x m returns the current binding of x in m, or raises Not_found if no such binding exists.
find [Qstack.Make]
Return the first data of the stack satisfying the specified predicate.
find [Parameter_sig.Multiple_map]
find [Offsetmap_sig]
Find the value bound to a set of intervals, expressed as an ival, in the given rangemap.
find [Offsetmap_bitwise_sig]
find [Map_lattice.MapSet_Lattice]
find key t returns the value bound to key in t.
find [Locations.Zone]
find [Locations.Location_Bytes.M]
find [Locations.Location_Bytes]
Destructuring
find [Lmap_sig]
find [Lmap_bitwise.Location_map_bitwise]
find [Parameter_sig.Map]
Search a given key in the map.
find [Journal.Reverse_binding]
find [Hptset.S_Basic_Compare]
find [Hptmap_sig.S]
find [Gtk_helper.Configuration]
Find a configuration elements, given a key.
find [Globals.FileIndex]
find path returns all global C symbols associated with path, plus path itself.
find [Globals.Vars]
find [Emitter.Make_table]
find [Dotgraph.Map]
find [Db.From.Callwise]
find [Db.Value]
find [Dataflow2.StmtStartData]
find [State_builder.Hashtbl]
Return the current binding of the given key.
find [Alarms]
findAttribute [Cil]
Returns the list of parameters associated to an attribute.
findConfiguration [Cilconfig]
Find a configuration elements, given a key.
findConfigurationBool [Cilconfig]
findConfigurationFloat [Cilconfig]
findConfigurationInt [Cilconfig]
Like findConfiguration but extracts the integer
findConfigurationList [Cilconfig]
findConfigurationString [Cilconfig]
findOrCreateFunc [Cil]
Find a function or function prototype with the given name in the file.
find_all [State_builder.Weak_hashtbl]
find_all x returns a list of all the instances of x found in t.
find_all [Rgmap]
Find all entries containing the specified range.
find_all [Project]
Find all projects with the given name.
find_all [State_builder.Hashtbl]
Return the list of all data associated with the given key.
find_all_enclosing_blocks [Kernel_function]
same as above, but returns all enclosing blocks, starting with the innermost one.
find_all_enclosing_blocks [Globals]
find_all_inputs_nodes [Db.Pdg]
Get the nodes corresponding to all inputs.
find_all_labels [Kernel_function]
returns all labels present in a given function.
find_all_logic_functions [Logic_env]
find_all_model_fields [Logic_env]
returns all model fields of the same name.
find_base [Lmap_sig]
find_base_or_default [Lmap_sig]
Same as find_base, but return the default values for bases that are not currently present in the map.
find_bool [Gtk_helper.Configuration]
Same as .
find_by_name [Globals.Functions]
find_call_ctrl_node [Db.Pdg]
find_call_input_node [Db.Pdg]
find_call_out_nodes_to_select [Db.Pdg]
find_call_out_nodes_to_select pdg_called called_selected_nodes
      pdg_caller call_stmt
find_call_output_node [Db.Pdg]
find_call_stmts [Db.Pdg]
Find the call statements to the function (can maybe be somewhere else).
find_check_missing [Hptmap_sig.S]
Both find key m and find_check_missing key m return the value bound to key in m, or raise Not_found is key is unbound.
find_code_annot_nodes [Db.Pdg]
The result is composed of three parts : the first part of the result are the control dependencies nodes of the annotation,, the second part is the list of declaration nodes of the variables used in the annotation;, the third part is similar to find_location_nodes_at_stmt result but for all the locations needed by the annotation. When the third part is globally None, it means that we were not able to compute this information.
find_decl_by_name [Globals.Functions]
find_decl_var_node [Db.Pdg]
Get the node corresponding the declaration of a local variable or a formal parameter.
find_def [FCHashtbl.S]
find_def_by_name [Globals.Functions]
find_def_stmt [Cil]
find_def_stmt b v returns the Local_init instruction within b that initializes v.
find_default_behavior [Cil]
find_default_requires [Cil]
find_defining_kf [Kernel_function]
Finds the kernel function defining the given varinfo as a local or a formal.
find_deps_no_transitivity [Db.From]
find_deps_no_transitivity_state [Db.From]
find_deps_term_no_transitivity_state [Db.From]
find_enclosing_block [Kernel_function]
find_enclosing_block [Globals]
find_enclosing_loop [Kernel_function]
find_enclosing_loop kf stmt returns the statement corresponding to the innermost loop containing stmt in kf.
find_enclosing_stmt_in_block [Kernel_function]
find_enclosing_stmt_in_block b s returns the statements s' inside b.bstmts that contains s.
find_englobing_kf [Kernel_function]
find_englobing_kf [Globals]
find_entry_point_node [Db.Pdg]
Find the node that represent the entry point of the function, i.e.
find_enum_tag [Globals.Types]
Find an enum constant from its name in the AST.
find_field_offset [Cabs2cil]
returns the offset (can be more than one field in case of unnamed members) corresponding to the first field matching the condition.
find_first_stmt [Kernel_function]
Find the first statement in a kernel function.
find_first_stmt [Globals]
find_float [Gtk_helper.Configuration]
find_from_astinfo [Globals.Vars]
Finds a variable from its vname according to its localisation (which might be a local).
find_from_sid [Kernel_function]
find_fun_postcond_nodes [Db.Pdg]
Similar to find_fun_precond_nodes
find_fun_precond_nodes [Db.Pdg]
Similar to find_code_annot_nodes (no control dependencies nodes)
find_fun_variant_nodes [Db.Pdg]
Similar to find_fun_precond_nodes
find_imprecise [Offsetmap_sig]
find_imprecise ~validity m returns an imprecise join of the values bound in m, in the range described by validity.
find_imprecise_everywhere [Offsetmap_sig]
Returns an imprecise join of all the values bound in the offsetmap.
find_in_nodes_to_select_for_this_call [Db.Pdg]
find_in_nodes_to_select_for_this_call
        pdg_caller caller_selected_nodes call_stmt pdg_called
find_in_scope [Globals.Syntactic_search]
find_in_scope orig_name scope finds a variable from its orig_name, according to the syntactic scope in which it should be searched.
find_index [Extlib]
returns the index (starting at 0) of the first element verifying the condition
find_input_node [Db.Pdg]
Get the node corresponding to a given input (parameter).
find_int [Gtk_helper.Configuration]
Like find but extracts the integer.
find_iset [Offsetmap_bitwise_sig]
find_key [Hptmap_sig.S]
This function is useful where there are multiple distinct keys that are equal for Key.equal.
find_kf_by_name [Parameter_builder]
find_kf_decl_by_name [Parameter_builder]
find_kf_def_by_name [Parameter_builder]
find_label [Kernel_function]
Find a given label in a kernel function.
find_label_node [Db.Pdg]
Get the node corresponding to the label.
find_list [Gtk_helper.Configuration]
find_location_nodes_at_begin [Db.Pdg]
Same than Db.Pdg.find_location_nodes_at_stmt for the program point located at the beginning of the function.
find_location_nodes_at_end [Db.Pdg]
Same than Db.Pdg.find_location_nodes_at_stmt for the program point located at the end of the function.
find_location_nodes_at_stmt [Db.Pdg]
Find the nodes that define the value of the location at the given program point.
find_logic_cons [Logic_env]
cons is a logic function with no argument.
find_logic_ctor [Logic_env]
find_logic_info [Logic_typing.Lenv]
find_logic_label [Logic_typing.Lenv]
find_logic_type [Logic_env]
find_lonely_binding [Map_lattice.MapSet_Lattice_with_cardinality]
If t is a singleton map binding k to v, and if cardinal_zero_or_one v holds, returns the pair (k,v).
find_lonely_binding [Map_lattice.Map_Lattice_with_cardinality]
If t is a singleton map binding k to v, if t is not a summary key, and if cardinal_zero_or_one v holds, returns the pair (k,v).
find_lonely_binding [Locations.Location_Bytes]
if there is only one binding -> o in the location (that is, only one base b with cardinal_zero_or_one o), returns the pair b,o.
find_lonely_key [Map_lattice.MapSet_Lattice]
If t is a singleton map binding k to v, then returns the pair (k,v).
find_lonely_key [Map_lattice.Map_Lattice]
If t is a singleton map binding k to v, then returns the pair (k,v).
find_lonely_key [Map_lattice.Map_Lattice_with_cardinality]
If t is a singleton map binding k to v and t is not a summary key, then returns the pair (k,v).
find_lonely_key [Locations.Zone]
find_lonely_key [Locations.Location_Bytes]
if there is only one base b in the location, then returns the pair b,o where o are the offsets associated to b.
find_lv_plus [Db.Value]
returns the list of all decompositions of expr into the sum an lvalue and an interval.
find_model_field [Logic_env]
find_model_info field typ returns the model field associated to field in type typ.
find_next_true [Bitvector]
find_next_true i a returns the first index greater or equal to i with its bit set.
find_offset [Bit_utils]
find_offset typ ~offset ~size finds a subtype t of typ that describes the type of the bits offset..offset+size-1 in typ.
find_opt [FCHashtbl.S]
find_opt [Extlib]
find_option p l returns the value p e, e being the first element of l such that p e is not None.
find_or_bottom [Map_lattice.Map_Lattice]
find key t returns the value bound to key in t, or Value.bottom if key does not belong to t.
find_or_bottom [Locations.Zone]
find_or_bottom [Locations.Location_Bytes]
find_or_none [Extlib]
find_output_nodes [Db.Pdg]
Get the nodes corresponding to a call output key in the called pdg.
find_ret_output_node [Db.Pdg]
Get the node corresponding return stmt.
find_return [Kernel_function]
Find the return statement of a kernel function.
find_return_loc [Db.Value]
Return the location of the returned lvalue of the given function.
find_simple_stmt_nodes [Db.Pdg]
Get the nodes corresponding to the statement.
find_stmt_and_blocks_nodes [Db.Pdg]
Get the nodes corresponding to the statement like Db.Pdg.find_simple_stmt_nodes but also add the nodes of the enclosed statements if stmt contains blocks.
find_stmt_node [Db.Pdg]
Get the node corresponding to the statement.
find_stmts [Dataflow2]
find_string [Gtk_helper.Configuration]
find_syntactic_callsites [Kernel_function]
callsites f collect the statements where f is called.
find_top_input_node [Db.Pdg]
find_type [Globals.Types]
Find a type from its name in the AST.
find_type_var [Logic_typing.Lenv]
find_utf8 [Logic_lexer]
find_var [Logic_typing.Lenv]
finish [Clexer]
finishParsing [Errorloc]
Call this function to finish parsing and close the input channel
fire [Wutil]
fitsInInt [Cil]
True if the integer fits within the kind's range
fixpoint [Interpreted_automata.Dataflow]
flatten [Wto]
flatten_transient_sub_blocks [Cil]
flatten_transient_sub_blocks b flattens all direct sub-blocks of b that have been marked as cleanable, whenever possible
float [Json]
Convert Null, Int, Float, Number and String to float and Null to 0.0.
float [Datatype]
floatKindForSize [Cil]
The float kind for a given size.
floatType [Cil]
float
float_zeros [Ival]
The lattice element containing exactly -0.
floor [Fval]
floor [Float_sig.S]
floor [Float_interval_sig.S]
flush [Wutil]
flush [Transitioning.Stdlib]
flush [Task]
Clean all terminated tasks
flush [Dotgraph]
Flushes the dot file buffer to disk.
flush [Db]
Trigger all daemons immediately.
fmod [Float_sig.S]
fmod [Float_interval_sig.S]
fmodf [Floating_point]
fold [Type.Heterogeneous_table]
fold [State_topological.Make]
fold action g seed allows iterating over the graph g in topological order.
fold [State_selection.S]
Fold over a selection.
fold [State_builder.States]
As iter, but for folding.
fold [State_builder.Weak_hashtbl]
fold [Rangemap.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 [Qstack.Make]
Fold on all the elements from the top to the end of the stack.
fold [Property_status]
fold [Parameter_sig.Collection]
Fold over all the elements of the collection.
fold [Offsetmap_sig]
Same as iter, but with an accumulator.
fold [Offsetmap_bitwise_sig]
fold [Map_lattice.MapSet_Lattice]
fold [Locations.Location_Bytes.M]
fold [Lmap_sig]
fold [Lmap_bitwise.Location_map_bitwise]
The following fold_* functions, as well as Lmap_bitwise.Location_map_bitwise.map2 take arguments of type map to force their user to handle the cases Top and Bottom explicitly.
fold [Json]
Fold over all fields of the object.
fold [Int_set]
fold [Int_Intervals_sig]
Iterators
fold [Hptset.S_Basic_Compare]
fold [Hptmap_sig.S]
fold f m seed invokes f k d accu, in turn, for each binding from key k to datum d in the map m.
fold [Globals.Functions]
fold [Globals.Vars]
fold [Emitter.Make_table]
fold [State_builder.Set_ref]
fold [State_builder.Hashtbl]
fold [Cabshelper.Comments]
fold [Alarms]
Folder over all alarms and the associated annotations at some program point.
fold [Lattice_type.Lattice_Set]
fold [Abstract_interp.Int]
Fold the function on the value between inf and sup at every step.
fold2 [Rangemap.S]
fold2 f m1 m2 v computes (f k_N v1_N v2_N... (f k_1 v1_1 v2_1 a)...) where k_1 ... k_N are all the keys of all the bindings in either m1 or m2 (in increasing order), vi_j being Some (find k_j m_i) if k_j is in m_i, and None otherwise (for i=1 or i=2)
fold2_join_heterogeneous [Locations.Zone]
fold2_join_heterogeneous [Hptmap_sig.S]
fold2_join_heterogeneous ~cache ~empty_left ~empty_right ~both
        ~join ~empty m1 m2
iterates simultaneously on m1 and m2.
fold2_join_heterogeneous [Hptset.S]
foldGlobals [Cil]
Fold over all globals, including the global initializer
foldLeftCompound [Cil]
Fold over the list of initializers in a Compound (not also the nested ones).
fold_all_code_annot [Annotations]
Fold on each code annotation of the program.
fold_allocates [Annotations]
Fold on the allocates of the corresponding behavior.
fold_assigns [Annotations]
Fold on the assigns of the corresponding behavior.
fold_assumes [Annotations]
Fold on the assumes of the corresponding behavior.
fold_base [Lmap_bitwise.Location_map_bitwise]
fold_bases [Locations.Zone]
fold_bases folds also bases of Top bases.
fold_bases [Locations.Location_Bytes]
Fold on all the bases of the location, including Top bases.
fold_behaviors [Annotations]
Fold on the behaviors of the given kernel function.
fold_between [Offsetmap_sig]
fold_between ~direction:`LTR ~entire (start, stop) m acc is similar to fold f m acc, except that only the intervals that intersect start..stop (inclusive) are presented.
fold_code_annot [Annotations]
Fold on each code annotation attached to the given statement.
fold_complete [Annotations]
Fold on the complete clauses of the given kernel function.
fold_decreases [Annotations]
apply f to the decreases term if any.
fold_disjoint [Annotations]
Fold on the disjoint clauses of the given kernel function.
fold_ensures [Annotations]
Fold on the ensures of the corresponding behavior.
fold_enum [Locations.Location_Bytes]
fold_enum f loc acc enumerates the locations in acc, and passes them to f.
fold_enum [Ival]
Iterate on every value of the ival.
fold_enum [Lattice_type.With_Enumeration]
Fold on the elements of the value one by one if possible.
fold_extended [Annotations]
fold_fuse_same [Offsetmap_bitwise_sig]
Same behavior as fold, except if two disjoint intervals r1 and r2 are mapped to the same value and boolean.
fold_fuse_same [Lmap_bitwise.Location_map_bitwise]
Same behavior as fold, except if two non-contiguous ranges r1 and r2 of a given base are mapped to the same value.
fold_global [Annotations]
Fold on each global annotation of the program.
fold_heads [Wto]
fold_i [Locations.Zone]
fold_i f l acc folds l by base.
fold_i [Locations.Location_Bytes]
Fold with offsets.
fold_in_file_order [Globals.Vars]
fold_in_file_rev_order [Globals.Vars]
fold_in_order [State_selection.S]
Fold over a selection in a topological ordering compliant with the State Dependency Graph.
fold_int [Ival]
Iterate on the integer values of the ival in increasing order.
fold_int [Int_val]
Iterates on all integers represented by an abstraction, in increasing order by default.
fold_int [Int_interval]
fold_int_bounds [Ival]
Given i an integer abstraction min..max, fold_int_bounds f i acc tries to apply f to min, max, and i' successively, where i' is i from which min and max have been removed.
fold_int_decrease [Ival]
Iterate on the integer values of the ival in decreasing order.
fold_itv [Offsetmap_bitwise_sig]
See documentation of Offsetmap_sig.fold_between.
fold_join_itvs [Offsetmap_bitwise_sig]
fold_join f join vempty itvs m is an implementation of fold that restricts itself to the intervals in itvs.
fold_join_zone [Lmap_bitwise.Location_map_bitwise]
fold_join_zone ~both ~conv ~empty_map ~join ~empty z m folds over the intervals present in z.
fold_keys [Map_lattice.MapSet_Lattice]
fold_left [State_builder.Array]
fold_left [State_builder.List_ref]
fold_left [Bag]
fold_map [Extlib]
Combines fold_left and map
fold_map_opt [Extlib]
Combines filter fold_left and map
fold_on_projects [Project]
folding on project starting with the current one.
fold_on_result [Dataflows.Simple_forward]
fold_on_result [Dataflows.Simple_backward]
fold_on_statuses [Property_status]
Iteration on all the individual statuses emitted for the given property.
fold_on_values [Offsetmap_sig]
Same as iter_on_values but with an accumulator
fold_preconds_at_callsite [Pretty_source]
fold_range [Rangemap.Make]
fold_requires [Annotations]
Fold on the requires of the corresponding behavior.
fold_rev [Hptmap_sig.S]
fold_rev performs exactly the same job as fold, but presents keys to f in the opposite order.
fold_right [State_builder.Array]
fold_right [Bag]
fold_sorted [FCHashtbl.S]
Fold on the hashtbl, but respecting the order on keys induced by cmp.
fold_sorted [Emitter.Make_table]
fold_sorted [State_builder.Hashtbl]
fold_sorted_by_entry [FCHashtbl.S]
Iter or fold on the hashtable, respecting the order on entries given by cmp.
fold_sorted_by_value [FCHashtbl.S]
Iter or fold on the hashtable, respecting the order on entries given by cmp.
fold_state_callstack [Db.Value]
fold_stmt_state_callstack [Db.Value]
fold_succ [State_selection.S]
Iterate over the successor of a state in a selection.
fold_terminates [Annotations]
apply f to the terminates predicate if any.
fold_topset_ok [Locations.Zone]
fold_i f l acc folds l by base.
fold_topset_ok [Locations.Location_Bytes]
Fold with offsets, including in the case Top bases.
fold_true [Bitvector]
Iterates on all indexes of the bitvector with their bit set.
for_all [Rangemap.S]
for_all p m checks if all the bindings of the map satisfy the predicate p.
for_all [Map_lattice.MapSet_Lattice]
for_all p t checks if all binding of t satisfy p .
for_all [Locations.Location_Bytes]
for_all [Int_set]
for_all [Hptset.S_Basic_Compare]
for_all [Hptmap_sig.S]
for_all p m returns true if all the bindings of the map m satisfy the predicate p.
for_all [Lattice_type.Lattice_Set]
for_all2 [Rangemap.S]
for_all2 f m1 m2 returns true if and only if f k v1 v2 holds for each k present in either m1 and m2, v_i being Some (find k m_i) if k is in m_i, and None otherwise (for i=1 or i=2)
forall [Utf8_logic]
force_ast_compute [Parameter_builder]
force_brace [Printer_api.S_pp]
self#force_brace printer fmt x pretty prints x by using printer, but add some extra braces '{' and '}' which are hidden by default.
formal_args [Ast_info.Function]
Returns the list of the named formal arguments of a function.
format [Markdown]
Plain markdown content of the formatted string
formatter [Rich_text]
formatter [Datatype]
forward [History]
If possible (ie.
forward_cast [Float_interval_sig.S]
forward_comp [Float_interval_sig.S]
forward_comp_int [Ival]
four [Integer]
frama_c_destructor [Cabs2cil]
Name of the attribute used to store the function that should be called when the corresponding variable exits its scope.
frama_c_display [Service_graph]
must be set to false before output the graph in dot format and must be set to true in order to display the graph in the Frama-C GUI.
frama_c_ghost_else [Cil]
A block marked with this attribute is known to be a ghost else.
frama_c_ghost_formal [Cil]
A varinfo marked with this attribute is known to be a ghost formal.
frama_c_init_obj [Cil]
a formal marked with this attribute is known to be a pointer to an object being initialized by the current function, which can thus assign any sub-object regardless of const status.
frama_c_keep_block [Cabs2cil]
Name of the attribute inserted by the elaboration to prevent user blocks from disappearing.
frama_c_mutable [Cil]
a field struct marked with this attribute is known to be mutable, i.e.
framac_icon [Gtk_helper]
framac_libc [Fc_config]
Directory where Frama-C libc headers are.
framac_logo [Gtk_helper]
frank [Cil]
Returns a unique number representing the floating-point conversion rank.
fresh [Dotgraph]
Create a fresh node identifier
fresh_behavior_name [Annotations]
fresh_code_annotation [Logic_const]
fresh_global [Cabs2cil]
fresh_global prefix creates a variable name not clashing with any other globals and starting with prefix
fresh_predicate_id [Logic_const]
fresh_term_id [Logic_const]
from_compare [Datatype]
Must be used for equal in order to implement it by compare x y = 0 (with your own compare function).
from_filename [File]
Build a file from its name.
from_func_annots [Db.Properties.Interp.To_zone]
Entry point to get zones needed to evaluate annotations of this kf.
from_ival_size [Int_Intervals_sig]
Conversion from an ival, which represents the beginning of each interval.
from_ival_size_under [Int_Intervals_sig]
Same as from_ival_size, except that the result is an under-approximation if the ival points to too many locations
from_pred [Db.Properties.Interp.To_zone]
Entry point to get zones needed to evaluate the predicate relative to the ctx of interpretation.
from_preds [Db.Properties.Interp.To_zone]
Entry point to get zones needed to evaluate the list of predicates relative to the ctx of interpretation.
from_pretty_code [Datatype]
Must be used for pretty in order to implement it by pretty_code provided by the datatype from your own internal_pretty_code function.
from_same_fun [Db.Pdg]
from_shape [Hptmap_sig.S]
Build an entire map from another map indexed by the same keys.
from_shape [Hptset.S]
Build a set from another elt-indexed map or set.
from_shape_id [Hptmap_sig.S]
Same as from_shape (fun _ v -> v).
from_stmt_annot [Db.Properties.Interp.To_zone]
Entry point to get zones needed to evaluate an annotation on the given stmt.
from_stmt_annots [Db.Properties.Interp.To_zone]
Entry point to get zones needed to evaluate annotations of this stmt.
from_term [Db.Properties.Interp.To_zone]
Entry point to get zones needed to evaluate the term relative to the ctx of interpretation.
from_terms [Db.Properties.Interp.To_zone]
Entry point to get zones needed to evaluate the list of terms relative to the ctx of interpretation.
from_unichar [Utf8_logic]
given an unicode code point, returns the corresponding utf-8 encoding.
from_unique_name [Project]
Return a project based on unique_name.
from_zone [Db.Properties.Interp.To_zone]
Entry point to get zones needed to evaluate the zone relative to the ctx of interpretation.
fround [Fval]
fround [Floating_point]
Rounds to nearest integer, away from zero (like round() in C).
fround [Float_sig.S]
fround [Float_interval_sig.S]
fst [Lattice_type.Lattice_Product]
full [State_selection]
The selection containing all the states.
full_command [Command]
Same arguments as but returns only when execution is complete.
full_command_async [Command]
Same arguments as .
full_compare [Description]
Completes pp_compare with Property.compare
fun_allocates_visible [Filter.RemoveInfo]
fun_assign_visible [Filter.RemoveInfo]
true if the assigned value (first component of the from) is visible
fun_deps_visible [Filter.RemoveInfo]
true if the corresponding functional dependency is visible.
fun_frees_visible [Filter.RemoveInfo]
fun_get_args [Db.Value]
For this function, the result None means that default values are used for the arguments.
fun_postcond_visible [Filter.RemoveInfo]
fun_precond_visible [Filter.RemoveInfo]
fun_set_args [Db.Value]
Specify the arguments to use.
fun_use_default_args [Db.Value]
fun_variant_visible [Filter.RemoveInfo]
func [Datatype]
func2 [Datatype]
func3 [Datatype]
func4 [Datatype]
funcExitData [Dataflow2.BackwardsTransfer]
The data at function exit.
function_env [Dataflows]
fundec [Visitor_behavior.Fold]
fundec [Visitor_behavior.Iter]
fundec [Visitor_behavior.Unset]
fundec [Visitor_behavior.Set]
fundec [Visitor_behavior.Get]
fundec [Visitor_behavior.Reset]
fundec_category [Parameter_builder]
funspec [Logic_typing.Make]
funspec behaviors f prms typ spec type-checks a function contract.
funspec [Annotations]
Get the contract associated to the given function.
funspec_state [Annotations]
The state which stores all the function contracts of the program.

G
g [Wbox]
Helper to box for packing a GObj.widget.
gccMode [Cil]
gcc_x86_16 [Machdeps]
gcc_x86_32 [Machdeps]
gcc_x86_64 [Machdeps]
ge [Utf8_logic]
ge [Integer]
generic_join [Hptmap_sig.S]
Merge of two trees, parameterized by the decide function.
generic_predicate [Hptmap_sig.S]
generic_is_included e (cache_name, cache_size) ~decide_fast
          ~decide_fst ~decide_snd ~decide_both t1 t2
decides whether some relation holds between t1 and t2.
generic_symmetric_predicate [Hptmap_sig.S]
Same as generic_predicate, but for a symmetric relation.
get [Vector]
Raise Not_found if out-of-bounds.
get [Typed_parameter]
Get the parameter from the option name.
get [State_builder.Hashcons]
Projection out of hashconsing.
get [State_builder.Counter]
get [State_builder.Proxy]
Getting the state corresponding to a proxy.
get [State_builder.Array]
get [State.Local]
How to access to the current state.
get [State]
get [Property_status.Consolidation_graph]
get [Property_status.Feedback]
get [Property_status.Consolidation]
get [Property_status]
get [Plugin]
Get a plug-in from its name.
get [Parameter_sig.Specific_dir]
get [Parameter_sig.S_no_parameter]
Option value (not necessarily set on the current command line).
get [Indexer.Make]
raises Not_found.
get [Gtk_helper.Icon]
get [Globals.Functions]
get [Emitter.Usable_emitter]
Get the emitter from an usable emitter.
get [Emitter]
Get the emitter which is really able to emit something.
get [Dynamic.Parameter.Common]
get [Dynamic]
get ~plugin name ty returns the value registered with the name name, the type ty and the plug-in plugin.
get [Dotgraph.Node]
get [Db.Pdg]
Get the PDG of a function.
get [Db.From]
get [State_builder.Ref]
Get the referenced value.
get [Cabshelper.Comments]
get [Ast.UntypedFiles]
The list of untyped AST that have been parsed.
get [Ast]
Get the cil file representation.
getAlphaPrefix [Alpha]
Split the name in preparation for newAlphaName.
getCompField [Cil]
Return a named fieldinfo in compinfo, or raise Not_found
getFormalsDecl [Cil]
Get the formals of a function declaration registered with Cil.setFormalsDecl.
getReturnType [Cil]
Takes as input a function type (or a typename on it) and return its return type.
get_all [File]
Return the list of toplevel files.
get_all_block_last_stmts [Stmts_graph]
get_all_block_out_edges [Stmts_graph]
get_all_categories [Log.Messages]
returns all registered categories.
get_all_status [Db.RteGen]
get_all_stmt_last_stmts [Stmts_graph]
Find the last statements in s, meaning that if s' is in the returned statements, s' is in s statements, but a least one of its successor is not.
get_all_stmt_out_edges [Stmts_graph]
Like get_stmt_in_edges but for edges going out of s statements.
get_all_warn_categories [Log.Messages]
get_all_warn_categories_status [Log.Messages]
get_astinfo [Globals.Vars]
Linear in the number of locals and formals of the program.
get_automaton [Interpreted_automata.Compute]
Get the interpreted automaton for the given kernel_function.
get_automaton [Interpreted_automata]
Get the interpreted automaton for the given kernel_function without annotations
get_bases [Locations.Location_Bytes]
Returns the bases the location may point to.
get_behavior [Property]
get_behavior_names [Logic_utils]
get_block_in_edges [Stmts_graph]
get_block_last_stmts [Stmts_graph]
get_block_stmts [Stmts_graph]
get_bool_value_status [Db.RteGen]
get_c_ified_functions [Parameter_customize]
Function names can be modified (aka mangled) from the original source to valid C identifiers.
get_called [Kernel_function]
Returns the static call to function expr, if any.
get_category [Log.Messages]
returns the corresponding registered category or None if no such category exists.
get_comments_global [Globals]
Gets a list of comments associated to the given global.
get_comments_stmt [Globals]
Gets a list of comments associated to the given statement.
get_conjunction [Property_status.Feedback]
get_conjunction [Property_status.Consolidation]
get_conversion_tables [Ordered_stmt]
This function computes, caches, and returns the conversion tables between a stmt and an ordered_stmt, and a table mapping each ordered_stmt to a connex component number (connex component number are also sorted in topological order
get_current [History]
return the current history point, if available
get_current_selection [Project]
If an operation on a project is ongoing, then get_current_selection () returns the selection which is applied on.
get_current_source [Log]
get_current_source_view [Source_manager]
Returns the source viewer for the currently displayed tab
get_debug_keys [Log.Messages]
Returns currently active keys
get_debug_keyset [Log.Messages]
Returns currently active keys
get_definition [Kernel_function]
get_definitionloc [Cabshelper]
get_descr [State]
get_description [Alarms]
Long description of the alarm, explaining the UB it guards against.
get_dir [Parameter_sig.Specific_dir]
get_dir ?mode p returns a (local) path p, i.e.
get_divMod_status [Db.RteGen]
get_embedded_type_names [Type]
Get the list of names containing in the type represented by the given type value.
get_external [Db.INOUTKF]
Inputs/Outputs without either local or formal variables
get_file [Parameter_sig.Specific_dir]
get_file ?mode p returns a (local) path p, i.e.
get_files [Globals.FileIndex]
Get the files list containing all global C symbols.
get_finite_float_status [Db.RteGen]
get_flags [Json_compilation_database]
get_float_to_int_status [Db.RteGen]
get_fold [Parameter_category]
Fold over the elements of the given category.
get_formal_position [Kernel_function]
get_formal_position v kf is the position of v as parameter of kf.
get_formals [Kernel_function]
get_from_name [Plugin]
Get a plug-in from its name.
get_from_shortname [Plugin]
Get a plug-in from its shortname.
get_function_name [Parameter_sig.String]
returns the given argument only if it is a valid function name (see Parameter_customize.get_c_ified_functions for more information), and abort otherwise.
get_functions [Globals.FileIndex]
Global functions of the given module for the kernel user interface.
get_garbled_mix [Locations.Location_Bytes]
All the garbled mix that have been created so far, sorted by "temporal" order of emission.
get_global [Kernel_function]
For functions with a declaration and a definition, returns the definition.
get_global_annotations [Globals.FileIndex]
Global annotations of the given module for the kernel user interface
get_globals [Globals.FileIndex]
Global variables of the given module for the kernel user interface
get_id [Kernel_function]
get_id [Ast_info.Function]
get_idom [Dominators]
Immediate dominator of the statement.
get_initial_state [Db.Value]
get_initial_state_callstack [Db.Value]
get_initialized_status [Db.RteGen]
get_instance [Type.Polymorphic4]
get_instance [Type.Polymorphic3]
get_instance [Type.Function]
get_instance [Type.Polymorphic2]
get_instance [Type.Polymorphic]
get_instance ty returns the type value used to create the given monomorphic instantiation.
get_internal [Db.INOUTKF]
Inputs/Outputs with local and formal variables
get_internal_precise [Db.Operational_inputs]
More precise version of get_internal function.
get_keys [Map_lattice.MapSet_Lattice]
Returns the set of keys in t.
get_kf [Property]
get_kf_exn [Exn_flow]
returns the set of exceptions that a given kernel function might throw.
get_kinstr [Property]
get_locals [Kernel_function]
get_location [Kernel_function]
get_mem [Parameter_category]
Is the given element present in the category?
get_memAccess_status [Db.RteGen]
get_name [State]
Name of a state.
get_name [Project]
Project name.
get_name [Parameter_category]
Name of the category.
get_name [Kernel_function]
get_name [Journal]
get_name [File]
File name (not normalized).
get_name [Emitter.Usable_emitter]
get_name [Emitter]
get_name [Ast_info.Function]
get_name [Alarms]
Short name of the alarm, used to prefix the assertion in the AST.
get_naturals [Loop]
get_non_naturals [Loop]
get_operator [Cprint]
get_option [State_builder.Option_ref]
get_optional_argument [Type.Function]
get_pane_ratio [Wutil]
get_parameter [Dynamic.Parameter]
retrieve the representation of the corresponding parameter.
get_params [Globals.Functions]
get_plain_string [Parameter_sig.String]
always return the argument, even if the argument is not a function name.
get_pointerCall_status [Db.RteGen]
get_pointer_downcast_status [Db.RteGen]
get_pointer_value_status [Db.RteGen]
get_possible_values [Parameter_sig.String]
What are the acceptable values for this parameter.
get_pred_body [Logic_utils]
returns the body of the given predicate.
get_preprocessor_command [File]
Return the preprocessor command to use.
get_project [Visitor_behavior]
get_prop_basename [Property.Names]
returns the basename of the property.
get_prop_basename [Property.LegacyNames]
get_prop_name_id [Property.Names]
returns a unique name identifying the property.
get_prop_name_id [Property.LegacyNames]
get_range [Parameter_sig.Int]
What is the possible range of values for this parameter.
get_reset_selection [Parameter_state]
Selection of resettable parameters in case of copy with a visitor.
get_return_type [Kernel_function]
get_rounding_mode [Floating_point]
get_selection [Parameter_state]
Selection of all the settable parameters.
get_selection_context [Parameter_state]
Selection of all the parameters that may have an impact on some analysis.
get_session_file [Journal]
get_short_name [Alarms]
Even shorter name.
get_sid [Ast_info]
get_signedOv_status [Db.RteGen]
get_signed_downCast_status [Db.RteGen]
get_small_cardinal [Int_set]
Returns the limit above which integer sets are converted into intervals.
get_state [Logic_lexer]
get_state [Dynamic.Parameter]
retrieve the state related to the corresponding parameter.
get_state [Db.Value]
after is false by default.
get_statementloc [Cabshelper]
get_statics [Kernel_function]
Returns the list of static variables declared inside the function.
get_stmt_in_edges [Stmts_graph]
Find the entry edges that go inside s statements, meaning that if the pair (s1,s2) is in the returned information, s2 is a successor of s1 and s2 is in s statements, but s1 is not.
get_stmt_last_stmts [Stmts_graph]
Subset of get_all_stmt_last_stmts according to termination_kind.
get_stmt_state [Db.Value]
after is false by default.
get_stmt_state_callstack [Db.Value]
get_stmt_stmts [Stmts_graph]
Get the statements that compose s.
get_subgraph [State_dependency_graph.Attributes]
get_suffixes [File]
get_symbols [Globals.FileIndex]
All global C symbols of the given module.
get_termination_kind_name [Cil_printer]
get_toolbar_index [Gtk_compat]
get_type [Kernel_function]
get_type_specifier [Gui_printers]
Returns the base type for a pointer/array, otherwise t itself.
get_unique_name [State]
Unique name of a state.
get_unique_name [Project]
get_unique_name [Emitter.Usable_emitter]
get_unsignedDownCast_status [Db.RteGen]
get_unsignedOv_status [Db.RteGen]
get_value [Typed_parameter]
Get the current value of the parameter, as a string.
get_vi [Kernel_function]
get_vi [Globals.Functions]
get_vi [Ast_info.Function]
get_warn_category [Log.Messages]
get_warn_status [Log.Messages]
get_with_formals [Db.Inputs]
Inputs with formals and without local variables
get_wto [Interpreted_automata]
Extract an exit strategy from a component, i.e.
get_wto_index [Interpreted_automata.Compute]
get_wto_index [Interpreted_automata]
get_wto_index_diff [Interpreted_automata.Compute]
get_wto_index_diff [Interpreted_automata]
getident [Cabshelper]
getword [Unmarshal]
ghost_local_env [Cabs2cil]
same as empty_local_env, but sets the ghost status to the value of its argument
gimage [Widget]
global [Globals.Types]
Find the global that defines the corresponding type.
global_annotation_attributes [Cil]
Return the attributes of the global annotation, if any.
global_attributes [Cil]
Return the attributes of the global, if any.
global_state [Annotations]
The state which stores all the global annotations of the program.
globals_set_initial_state [Db.Value]
Specify the initial state to use.
globals_state [Db.Value]
Initial state used by the analysis
globals_use_default_initial_state [Db.Value]
globals_use_supplied_state [Db.Value]
glue [Markdown]
Glue fragments, typically used for combining text, block and elements.
graph [State_dependency_graph.S]
graph_attributes [State_dependency_graph.Attributes]
graph_window [Dgraph_helper]
graph_window_through_dot [Dgraph_helper]
Create a new window displaying a graph, by printing dot commands.
gt [Integer]
gui_unlocked [Gtk_helper]
This is a mutex you may use to prevent running some code while the GUI is locked.

H
h [Wbox]
w ~expand:H
had_errors [Errorloc]
Has an error been raised since the last call to Errorloc.clear_errors?
hasAttribute [Cil]
True if the named attribute appears in the attribute list.
has_code_annot [Annotations]
has_definition [Kernel_function]
has_extern_local_init [Cil]
returns true iff the given non-scoping block contains local init statements (thus of locals belonging to an outer block), either directly or within a non-scoping block or undefined sequence.labels
has_flexible_array_member [Cil]
true iff the given type is a struct whose last field is a flexible array member.
has_greater_min_bound [Ival]
has_greater_min_bound i1 i2 returns 1 if the interval i1 has a better minimum bound (i.e.
has_greater_min_bound [Float_interval_sig.S]
has_greater_min_bound f1 f2 returns 1 if the interval f1 has a better minimum bound (i.e.
has_smaller_max_bound [Ival]
has_smaller_max_bound i1 i2 returns 1 if the interval i1 has a better maximum bound (i.e.
has_smaller_max_bound [Float_interval_sig.S]
has_smaller_max_bound f1 f2 returns 1 if the interval f1 has a better maximum bound (i.e.
has_some [Extlib]
true iff its argument is Some x
has_status [Property]
Does the property has a logical status (which may be Never_tried)? False for pragma, assumes clauses and some ACSL extensions.
has_suffix [Floating_point]
Checks if the (uppercased) string ends with an explicit F|D|L suffix corresponding to the given float kind.
hash [Type]
hash [Project]
hash [Logic_lexer]
hash [Integer]
hash [Hptmap.Shape]
hash [Hook.Comparable]
hash [Float_sig.S]
hash [Float_interval_sig.S]
hash [FCHashtbl]
hash [Datatype.Make_input]
hash [Datatype.S_no_copy]
Hash function: same spec than Hashtbl.hash.
hash [Datatype.Undefined]
hash [Datatype]
hash [Bitvector]
hash [Binary_cache.Cacheable]
hash [Abstract_interp.Rel]
hash_param [FCHashtbl]
hash_predicate [Logic_utils]
hash_term [Logic_utils]
hash function compatible with is_same_term
hashcons [State_builder.Hashcons]
Injection as an hashconsed value.
hbox [Wbox]
Pack a list of boxes horizontally.
height [Rangemap.Make]
help [Plugin.S_no_log]
The group containing option -*-help.
help [Parameter_sig.Input]
A description for this option (e.g.
here_label [Logic_const]
hgroup [Wbox]
Pack a list of widgets horizontally, with all widgets stuck to the same width
hide_typename [Logic_env]
marks temporarily a typename as being a normal identifier in the logic
hilite [Pretty_source]
host_to_term_lhost [Logic_utils]
howto_marshal [State_builder.S]
howto_marshal marshal unmarshal registers a custom couple of functions (marshal, unmarshal) to be used for serialization.
href [Markdown]
Href link
hscroll [Wbox]
Same as scroll ~vpolicy:`NEVER
html_escape [Extlib]
hv [Wbox]
w ~expand:HV

I
id [Unmarshal]
Use this function when you don't want to change the value unmarshaled by input_val.
id [State_builder.Hashcons]
Id of an hashconsed value.
id [Kernel_function]
id [Hptmap_sig.S]
Bijective function.
id [Extlib]
identity function.
id [Cil_datatype.Kf]
id [Hptmap.Id_Datatype]
Identity of a key.
id [Base.Base]
id [Base]
identity [Datatype]
Must be used if you want to implement a required function by fun x ->
    x
.
idx [Qstack.Make]
iff [Utf8_logic]
ignored_recursive_call [Db.Value]
This functions returns true if the value analysis found and ignored a recursive call to this function during the analysis.
image [Markdown]
Image
image_menu_item [Gtk_helper]
calls the packing function to append a new menu item with an icon and a label.
implies [Utf8_logic]
imprecise_write_msg [Offsetmap_sig]
The message "more than N <imprecise_msg_write>.
imprecise_write_msg [Lmap_bitwise.Location_map_bitwise]
in_degree [State_topological.G]
inbound [Gtk_helper.MAKE_CUSTOM_LIST]
incr [Transitioning.Stdlib]
incr [Parameter_sig.Int]
Increment the integer.
incr [Dynamic.Parameter.Int]
increm [Cil]
Increment an expression.
increm64 [Cil]
Increment an expression.
index [Indexer.Make]
raise Not_found.
info [Datatype]
init [Transitioning.Dynlink]
init [Logic_builtin]
init [Dataflows.FORWARD_MONOTONE_PARAMETER]
The initial value for each statement.
init [Dataflows.BACKWARD_MONOTONE_PARAMETER]
The initial state after each statement.
init [Clexer]
initCIL [Cil]
Call this function to perform some initialization, and only after you have set Cil.msvcMode.
init_builtins [Cil]
initialize the C built-ins.
init_dependencies [Logic_env]
Used to postpone dependency of Lenv global tables wrt Cil_state, which is initialized afterwards.
init_from_c_files [File]
Initialize the cil file representation of the current project.
init_from_cmdline [File]
Initialize the cil file representation with the file given on the command line.
init_label [Logic_const]
init_project_from_cil_file [File]
Initialize the cil file representation with the given file for the given project from the current one.
init_project_from_visitor [File]
init_project_from_visitor prj vis initialize the cil file representation of prj.
initial [Clexer]
This is the main lexing function
inject [Map_lattice.MapSet_Lattice]
Returns the singleton map binding key to v.
inject [Locations.Zone]
inject [Locations.Location_Bytes]
inject [Lattice_type.Lattice_Base]
inject [Lattice_type.Lattice_Product]
inject [Int_Intervals_sig]
inject [Int_Base]
inject [Fval]
inject creates an abstract float interval.
inject [Float_interval_sig.S]
inject ~nan b e creates the floating-point interval b..e, plus NaN if nan is true.
inject [Lattice_type.Lattice_Set]
inject_bounds [Int_Intervals_sig]
inject_float [Locations.Location_Bytes]
inject_float [Ival]
inject_float_interval [Ival]
inject_interval [Ival]
Builds the set of integers between min and max included and congruent to rem modulo modulo.
inject_interval [Int_val]
Builds an abstraction of all integers between min and max included and congruent to rem modulo modu.
inject_itv [Int_Intervals_sig]
inject_ival [Locations.Location_Bytes]
inject_list [Int_set]
Creates a set from an integer list.
inject_periodic [Int_set]
Creates the set with integers from + k*period for k in ...
inject_range [Ival]
None means unbounded.
inject_range [Int_val]
inject_range min max returns an abstraction of all integers between min and max included.
inject_range [Int_interval]
Makes the interval of all integers between min and max.
inject_singleton [Ival]
inject_singleton [Int_val]
Returns an exact abstraction of the given integer.
inject_singleton [Int_set]
Creates the set containing only the given integer.
inject_singleton [Fval]
inject_singleton [Lattice_type.Lattice_Set]
inject_t1 [Lattice_type.Lattice_Sum]
inject_t2 [Lattice_type.Lattice_Sum]
inject_top_origin [Locations.Location_Bytes]
inject_top_origin origin p creates a top with origin origin and additional information param
inline_calls [Inline]
inline_predicate [Inline]
Inlines predicates and logic functions in a predicate.
inline_term [Inline]
inline_term ~inline term inlines in term the application of predicates and logic functions for which inline is true.
inode [Dotgraph.Node]
inode [Dotgraph]
Combinaison of fresh and node
inout_source [Kernel]
inplace [Visitor_behavior]
In-place modification.
input_string [Gtk_helper]
Copied from lablgtk GToolbox.input_string.
input_val [Unmarshal]
input_val c t Read a value from the input channel c, applying the transformations described by t.
input_val [Descr]
inset [Utf8_logic]
inset_string [Unicode]
inst_visible [Filter.RemoveInfo]
tells if the statement is visible.
instantiate [Type.Polymorphic4]
instantiate [Type.Polymorphic3]
instantiate [Type.Function]
Possibility to add a label for the parameter.
instantiate [Type.Polymorphic2]
instantiate [Type.Polymorphic]
instantiate [Logic_utils]
instantiate type variables in a logic type.
instantiate [Logic_const]
instantiate type variables in a logic type.
int [Json]
Convert Null, Int, Float, Number and String to an int.
int [Datatype]
int32 [Datatype]
int64 [Datatype]
intKindForSize [Cil]
The signed integer kind for a given size (unsigned if second argument is true).
intKindForValue [Cil]
intOfAttrparam [Cil]
intOfAttrparam a tries to const-fold a into a numeric value.
intPtrType [Cil]
int *
intType [Cil]
int
intTypeIncluded [Cil]
intTypeIncluded i1 i2 returns true iff the range of values representable in i1 is included in the one of i2
int_of_digit [Logic_lexer]
integer [Utf8_logic]
integer [Datatype]
integer [Cil]
Construct an integer of kind IInt.
integralPromotion [Cil]
performs the usual integral promotions mentioned in C reference manual.
integralPromotion [Cabs2cil]
performs the usual integral promotions mentioned in C reference manual.
integral_cast [Cabs2cil]
Raise Failure
inter [Hptset.S_Basic_Compare]
inter [Hptmap_sig.S]
Intersection of two trees, parameterized by the decide function.
inter_with_shape [Hptmap_sig.S]
inter_with_shape s m keeps only the elements of m that are also bound in the map s.
internal_pretty_code [Datatype.Make_input]
internal_pretty_code [Datatype.S_no_copy]
Same spec than pretty_code, but must take care of the precedence of the context in order to put parenthesis if required.
internal_pretty_code [Datatype.Undefined]
internal_pretty_code [Datatype]
interp_boolean [Ival]
interpret [Cparser]
interpret_character_constant [Cil]
gives the value of a char literal.
intersects [Locations.Zone]
intersects [Int_set]
intersects [Lattice_type.With_Intersects]
intersects t1 t2 returns true iff the intersection of t1 and t2 is non-empty.
intersects [Hptset.S]
intersects s1 s2 returns true if and only if s1 and s2 have an element in common
inv [Abstract_interp.Comp]
Inverse relation: a op b <==> ! (a (inv op) b).
inv_truth [Abstract_interp]
invalidStmt [Cil]
An empty statement.
invalid_part [Locations]
Overapproximation of the invalid part of a location
ip_all_of_behavior [Property]
ip_all_of_behavior kf ki active bhv builds all IP related to a behavior.
ip_allocation_of_behavior [Property]
ip_allocation_of_behavior kf ki active bhv builds IPAllocation for behavior bhv, in the spec in function kf, at statement ki, under active behaviors active
ip_assigns_of_behavior [Property]
ip_assigns_of_behavior kf ki active bhv builds IPAssigns for a contract (if not WritesAny).
ip_assigns_of_code_annot [Property]
Builds IPAssigns for a loop annotation (if not WritesAny)
ip_assumes_of_behavior [Property]
Builds the IPPredicate corresponding to assumes of a behavior.
ip_axiom [Property]
Builds an IPAxiom.
ip_complete_of_spec [Property]
ip_complete_of_spec kf ki active spec builds IPComplete of a given spec.
ip_decreases_of_spec [Property]
Builds IPDecrease of a given spec.
ip_disjoint_of_spec [Property]
ip_disjoint_of_spec kf ki active spec builds IPDisjoint of a given spec.
ip_ensures_of_behavior [Property]
Builds the IPPredicate PKEnsures corresponding to a behavior.
ip_from_of_behavior [Property]
ip_from_of_behavior kf ki active bhv builds IPFrom for a behavior (if not ReadsAny).
ip_from_of_code_annot [Property]
Builds IPFrom for a loop annotation(if not ReadsAny)
ip_global_invariant [Property]
Build an IPGlobalInvariant.
ip_lemma [Property]
Build an IPLemma.
ip_of_allocation [Property]
Builds the corresponding IPAllocation.
ip_of_assigns [Property]
Builds the corresponding IPAssigns.
ip_of_assumes [Property]
IPPredicate of a single assumes.
ip_of_behavior [Property]
ip_of_behavior kf ki activd bhv builds the IP corresponding to the behavior itself.
ip_of_code_annot [Property]
Builds all IP related to a given code annotation.
ip_of_code_annot_single [Property]
Builds the IP related to the code annotation.
ip_of_complete [Property]
ip_of_complete kf ki active complete builds IPComplete.
ip_of_decreases [Property]
Builds IPDecrease
ip_of_disjoint [Property]
ip_of_disjoint kf ki active disjoint builds IPDisjoint.
ip_of_ensures [Property]
IPPredicate of single ensures.
ip_of_extended [Property]
Extended property.
ip_of_from [Property]
Builds the corresponding IPFrom (if not FromAny)
ip_of_global_annotation [Property]
ip_of_global_annotation_single [Property]
ip_of_requires [Property]
IPPredicate of a single requires.
ip_of_spec [Property]
ip_of_spec kf ki active spec builds all IP related to a spec.
ip_of_terminates [Property]
ip_other [Property]
Create a non-standard property.
ip_post_cond_of_behavior [Property]
ip_post_cond_of_behavior kf ki active bhv builds all IP related to the post-conditions (including allocates, frees, assigns and from).
ip_post_cond_of_spec [Property]
ip_post_cond_of_spec kf ki active spec builds all IP of post-conditions related to a spec.
ip_property_instance [Property]
Build a specialization of the given property at the given function and stmt.
ip_reachable_ppt [Property]
ip_reachable_stmt [Property]
ip_requires_of_behavior [Property]
Builds the IPPredicate corresponding to requires of a behavior.
ip_terminates_of_spec [Property]
Builds IPTerminates of a given spec.
ip_type_invariant [Property]
Build an IPTypeInvariant.
irecord [Dotgraph.Node]
irecord [Dotgraph]
Create a new node from a record (combines fresh and record)
isAnyCharArrayType [Cil]
True if the argument is an array of a character type (i.e.
isAnyCharPtrType [Cil]
True if the argument is a pointer to a character type (i.e.
isAnyCharType [Cil]
True if the argument is a character type (i.e.
isArithmeticOrPointerType [Cil]
True if the argument is an arithmetic or pointer type (i.e.
isArithmeticType [Cil]
True if the argument is an arithmetic type (i.e.
isArrayType [Cil]
True if the argument is an array type
isBitfield [Cil]
Is an lvalue a bitfield?
isBoolType [Cil]
True if the argument is _Bool
isCharArrayType [Cil]
True if the argument is an array of a character type (i.e.
isCharConstPtrType [Cil]
True if the argument is a pointer to a constant character type, e.g.
isCharPtrType [Cil]
True if the argument is a pointer to a plain character type (but neither signed char nor unsigned char).
isCharType [Cil]
True if the argument is a plain character type (but neither signed char nor unsigned char).
isCompleteProgramRoot [Rmtmps]
isCompleteType [Cil]
Returns true if this is a complete type.
isConstType [Cil]
Check for "const" qualifier from the type of an l-value (do not follow pointer)
isConstant [Cil]
True if the expression is a compile-time constant
isConstantOffset [Cil]
True if the given offset contains only field names or constant indices.
isExactFloat [Cil]
True if the real constant is an exact float for the given type
isExportedRoot [Rmtmps]
isExtern [Cabshelper]
isFiniteFloat [Cil]
True if the float is finite for the kind's range
isFloatingType [Cil]
True if the argument is a floating point type.
isFunPtrType [Cil]
True if the argument is a function pointer type.
isFunctionType [Cil]
True if the argument is a function type
isGhostFormalVarDecl [Cil]
true if the given formal declaration corresponds to a ghost formal variable.
isGhostFormalVarinfo [Cil]
true if the given varinfo is a ghost formal variable.
isGhostType [Cil]
Check for "ghost" qualifier from the type of an l-value (do not follow pointer)
isInline [Cabshelper]
isInteger [Cil]
True if the given expression is a (possibly cast'ed) character or an integer constant
isIntegerConstant [Cil]
True if the expression is a compile-time integer constant
isIntegralOrPointerType [Cil]
True if the argument is an integral or pointer type.
isIntegralType [Cil]
True if the argument is an integral type (i.e.
isLogicAnyCharType [Logic_utils]
isLogicArithmeticType [Cil]
True if the argument is a logic arithmetic type (i.e.
isLogicArrayType [Logic_utils]
Predefined tests over types
isLogicBooleanType [Cil]
True if the argument is a boolean type, either integral C type or mathematical boolean one.
isLogicCType [Logic_const]
isLogicType test typ is false for pure logic types and the result of test for C types.
isLogicCharType [Logic_utils]
isLogicFloatType [Cil]
True if the argument is a floating point type.
isLogicFunPtrType [Cil]
True if the argument is the logic function pointer type.
isLogicFunctionType [Cil]
True if the argument is the logic function type.
isLogicIntegralType [Cil]
True if the argument is an integral type (i.e.
isLogicNull [Cil]
True if the given term is \null or a constant null pointer
isLogicPointer [Logic_utils]
true if the term is a pointer.
isLogicPointerType [Logic_utils]
isLogicPureBooleanType [Cil]
True if the argument is _Bool or boolean.
isLogicRealOrFloatType [Cil]
True if the argument is a C floating point type or logic 'real' type.
isLogicRealType [Cil]
True if the argument is the logic 'real' type.
isLogicType [Logic_utils]
isLogicType test typ is false for pure logic types and the result of test for C types.
isLogicVoidPointerType [Logic_utils]
isLogicVoidType [Logic_utils]
isLogicZero [Cil]
True if the term is the constant 0
isPointerType [Cil]
True if the argument is a pointer type.
isShortType [Cil]
True if the argument is a short type (i.e.
isSigned [Cil]
Returns the signedness of the given integer kind depending on the current machdep.
isSignedInteger [Cil]
isStatic [Cabshelper]
isStructOrUnionType [Cil]
True if the argument is a struct of union type
isTypeTagType [Cil]
True if the argument is the type for reified C types.
isTypedef [Cabshelper]
isUnsignedInteger [Cil]
isVariadicListType [Cil]
True if the argument denotes the type of ...
isVoidPtrType [Cil]
is the given type "void *"?
isVoidType [Cil]
is the given type "void"?
isVolatileLogicType [Cil]
Check for "volatile" qualifier from a logic type
isVolatileLval [Cil]
Check if the l-value has a volatile part
isVolatileTermLval [Cil]
Check if the l-value has a volatile part
isVolatileType [Cil]
Check for "volatile" qualifier from the type of an l-value (do not follow pointer)
isWFGhostType [Cil]
Check if the received type is well-formed according to \ghost semantics, that is once the type is not ghost anymore, \ghost cannot appear again.
isZero [Cil]
True if the given expression is a (possibly cast'ed) integer or character constant with value zero
is_C_array [Logic_utils]
true if the term denotes a C array.
is_abstract [Descr]
is_accessible [Db.Value]
is_aligned_by [Base]
is_annot_next_stmt [Logic_utils]
Does the annotation apply to the next statement (e.g.
is_any_formal_or_local [Base]
is_any_local [Base]
is_arithmetic_type [Logic_typing]
is_array_type [Logic_typing]
is_assert [Logic_utils]
is_assigns [Logic_utils]
is_attr_test [Cabshelper]
is_back_edge [Interpreted_automata.Compute]
is_back_edge [Interpreted_automata]
is_between [Kernel_function]
is_between b s1 s2 s3 returns true if the statement s2 appears strictly between s1 and s3 inside the b.bstmts list.
is_block_local [Base]
is_block_local [Ast_info]
determines if a var is local to a block.
is_boolean_type [Logic_const]
is_bottom [Locations.Zone]
is_bottom [Locations.Location_Bytes]
is_bottom [Lmap_bitwise.Location_map_bitwise]
is_bottom [Ival]
is_bottom [Bottom]
is_bottom_loc [Locations]
is_builtin [Cil]
is_builtin_logic_ctor [Logic_env]
is_builtin_logic_function [Logic_env]
is_builtin_logic_type [Logic_env]
is_c_keyword [Clexer]
true if the given string is a C keyword.
is_called [Db.Value]
is_case_label [Cil]
Return true on case and default labels, false otherwise.
is_cea_domain_function [Ast_info]
is_cea_dump_file_function [Ast_info]
is_cea_dump_function [Ast_info]
is_cea_function [Ast_info]
is_check [Logic_utils]
is_computed [State_builder.S]
Returns true iff the registered state will not change again for the given project (default is current ()).
is_computed [Db.From]
Check whether the from analysis has been performed for the given function.
is_computed [Db.Value]
Return true iff the value analysis has been done.
is_computed [Ast]
is_config_visible [Plugin]
Make visible to the end-user the -<plug-in>-config option.
is_contract [Logic_utils]
is_copy [Visitor_behavior]
true iff the behavior is a copy behavior.
is_current [Project]
Check whether the given project is the current one or not.
is_debug_key_enabled [Log.Messages]
Returns true if the given category is currently active
is_def_or_last_decl [Ast]
true if the global is the last one in the AST to introduce a given variable.
is_default [Parameter_sig.S_no_parameter]
Is the option equal to its default value?
is_default [Dynamic.Parameter.Common]
is_default_behavior [Cil]
is_definition [Kernel_function]
is_definition [Ast_info.Function]
is_dot_installed [Dotgraph]
Memoized
is_dummy [State]
is_empty [State_selection]
is_empty [State_builder.Queue]
is_empty [Rangemap.S]
Test whether a map is empty or not.
is_empty [Qstack.Make]
Test whether the stack is empty or not.
is_empty [Parameter_sig.Collection]
Is the collection empty?
is_empty [Lmap_bitwise.Location_map_bitwise]
is_empty [Indexer.Make]
is_empty [Hptset.S_Basic_Compare]
is_empty [Hptmap_sig.S]
is_empty m returns true if and only if the map m defines no bindings at all.
is_empty [History]
Does the history contain an event.
is_empty [Dynamic.Parameter.StringList]
is_empty [Dynamic.Parameter.StringSet]
is_empty [Hook.S]
Is no function already registered in the hook?
is_empty [State_builder.Set_ref]
is_empty [Bitvector]
is_empty [Bag]
is_empty_behavior [Cil]
is_empty_funspec [Cil]
is_empty_map [Lmap_sig]
is_entry_point [Kernel_function]
is_even [Integer]
is_exact [Float_sig.S]
Is the representation of floating-point numbers of a given precision exact? Should at least be false for Real.
is_exit_status [Logic_const]
true if the term is \exit_status (potentially enclosed in \at)
is_extension [Logic_env]
is_finite [Fval.F]
Returns true if the float is a finite number.
is_finite [Float_sig.S]
is_finite [Float_interval_sig.S]
is_first_stmt [Kernel_function]
is_float [Ival]
is_formal [Kernel_function]
is_formal [Base]
is_formal [Ast_info.Function]
is_formal_of_prototype [Base]
is_formal_of_prototype [Ast_info.Function]
is_formal_of_prototype v f returns true iff f is a prototype and v is one of its formal parameters.
is_formal_or_local [Kernel_function]
is_formal_or_local [Base]
is_formal_or_local [Ast_info.Function]
is_frama_c_builtin [Ast_info]
is_fresh [Visitor_behavior]
true iff the behavior provides fresh id for copied structs with id.
is_full [State_selection]
is_fully_arithmetic [Cil]
Returns true whenever the type contains only arithmetic types
is_function [Base]
is_function_type [Ast_info]
Return true iff the type of the given varinfo is a function type.
is_ghost_else [Cil]
returns true iff the given block is a ghost else block.
is_global [Base]
is_going_to_load [Cmdline]
To be call if one action is going to run after the loading stage.
is_gui [Fc_config]
Is the Frama-C GUI running?
is_impact_pragma [Logic_utils]
is_included [Origin]
is_included [Offsetmap_bitwise_sig]
is_included [Lmap_sig]
is_included [Int_set]
is_included [Float_interval_sig.S]
is_included [Lattice_type.Join_Semi_Lattice]
is first argument included in the second?
is_included [Dataflows.JOIN_SEMILATTICE]
Must verify: a is_included b <=> a join b = b.
is_included [Bottom]
is_infinite [Float_sig.S]
is_instance_of [Type.Polymorphic4]
is_instance_of [Type.Polymorphic3]
is_instance_of [Type.Function]
is_instance_of [Type.Polymorphic2]
is_instance_of [Type.Polymorphic]
is_instance_of [Logic_utils]
is_instance_of poly t1 t2 returns true if t1 can be derived from t2 by instantiating some of the type variable in poly.
is_int [Ival]
is_integral_const [Ast_info]
is_integral_logic_const [Ast_info]
is_integral_type [Logic_typing]
is_invariant [Logic_utils]
is_invisible [Parameter_customize]
Prevent the help to list the parameter.
is_isotropic [Offsetmap_lattice_with_isotropy]
Are the bits independent?
is_kw_c_mode [Logic_utils]
is_list_type [Logic_typing]
is_list_type [Logic_const]
returns true if the type is a list<t>.
is_local [Kernel_function]
is_local [Base]
is_local [Ast_info.Function]
is_logic_ctor [Logic_env]
is_logic_function [Logic_env]
tests of existence
is_logic_type [Logic_env]
is_loop_annot [Logic_utils]
is_loop_invariant [Logic_utils]
is_loop_pragma [Logic_utils]
is_loop_statement [Ast_info]
is_main [Kernel_function]
is_model_field [Logic_env]
is_modifiable_lval [Cil]
indicates whether the given lval is a modifiable lvalue in the sense of the C standard 6.3.2.1§1.
is_mutable_or_initialized [Cil]
true if the given lval is allowed to be assigned to thanks to a frama_c_init_obj or a frama_c_mutable attribute.
is_nan [Float_sig.S]
is_natural [Loop]
is_negative [Float_sig.S]
Is a number negative? Never called on NaN, but must be correct on infinities and zeros.
is_negative [Float_interval_sig.S]
is_negative f returns True iff all values in f are negative; False iff all values are positive; and Unknown otherwise.
is_non_natural [Loop]
is_non_null_expr [Ast_info]
is_not_nan [Float_interval_sig.S]
is_null [Base]
is_null_expr [Ast_info]
is_null_term [Ast_info]
is_one [Ival]
is_one [Integer]
is_permissive_ref [Parameter_customize]
if true, less checks are performed on value of arguments.
is_plain_type [Logic_const]
true if the argument is not a set type.
is_pointer_type [Logic_typing]
is_postdominator [Db.PostdominatorsTypes.Sig]
is_pragma [Logic_utils]
is_present [Plugin]
Whether a plug-in already exists.
is_property_pragma [Logic_utils]
Should this pragma be proved by plugins
is_reachable [Lmap_sig]
is_reachable [Db.Value]
is_reachable_stmt [Db.Value]
is_read_only [Base]
Is the base valid as a read/write location, or only for reading.
is_registered_category [Log.Messages]
true iff the string corresponds to a registered category
is_relationable [Locations.Location_Bytes]
is_relationable loc returns true iff loc represents a single memory location.
is_relative [Filepath]
returns true if the file is relative to base (that is, it is prefixed by base_name), or to the current working directory if no base is specified.
is_result [Logic_utils]
true if the term is \result or an offset of \result.
is_result [Logic_const]
true if the term is \result (potentially enclosed in \at)
is_return_stmt [Kernel_function]
is_rt_type_mode [Logic_utils]
is_running [Task]
Don't make the thread progress, just returns true if not terminated or not started yet
is_same_allocation [Logic_utils]
is_same_assigns [Logic_utils]
is_same_axiomatic [Logic_utils]
is_same_behavior [Logic_utils]
is_same_builtin_profile [Logic_utils]
is_same_code_annotation [Logic_utils]
is_same_constant [Logic_utils]
is_same_deps [Logic_utils]
is_same_global_annotation [Logic_utils]
is_same_identified_predicate [Logic_utils]
is_same_identified_term [Logic_utils]
is_same_impact_pragma [Logic_utils]
is_same_indcase [Logic_utils]
is_same_lexpr [Logic_utils]
is_same_lhost [Logic_utils]
is_same_list [Logic_utils]
is_same_logic_body [Logic_utils]
is_same_logic_ctor_info [Logic_utils]
is_same_logic_info [Logic_utils]
is_same_logic_label [Logic_utils]
is_same_logic_profile [Logic_utils]
is_same_logic_signature [Logic_utils]
is_same_logic_type_def [Logic_utils]
is_same_logic_type_info [Logic_utils]
is_same_loop_pragma [Logic_utils]
is_same_model_info [Logic_utils]
is_same_offset [Logic_utils]
is_same_pconstant [Logic_utils]
is_same_post_cond [Logic_utils]
is_same_pragma [Logic_utils]
is_same_predicate [Logic_utils]
is_same_predicate_node [Logic_utils]
is_same_slice_pragma [Logic_utils]
is_same_spec [Logic_utils]
is_same_term [Logic_utils]
is_same_tlval [Logic_utils]
is_same_type [Logic_utils]
is_same_value [Offsetmap_sig]
is_same_value o v is true if the offsetmap o contains a single binding to v, or is the empty offsetmap.
is_same_value [Offsetmap_bitwise_sig]
is_same_value o v is true if the offsetmap o contains a single binding to v, or is the empty offsetmap.
is_same_var [Logic_utils]
is_same_variant [Logic_utils]
is_session_visible [Plugin]
Make visible to the end-user the -<plug-in>-session option.
is_set [Parameter_sig.Specific_dir]
is_set [Dynamic.Parameter.Common]
is_set_type [Logic_typing]
is_set_type [Logic_const]
returns true if the type is a set<t>.
is_share_visible [Plugin]
Make visible to the end-user the -<plug-in>-share option.
is_signed_int_enum_pointer [Bit_utils]
true means that the type is signed.
is_single_interval [Offsetmap_sig]
is_single_interval o is true if the offsetmap o contains a single binding.
is_single_interval [Offsetmap_bitwise_sig]
is_single_interval o is true if the offsetmap o contains a single binding.
is_singleton [Int_val]
is_singleton [Hptmap_sig.S]
is_singleton m returns Some (k, d) if m is a singleton map that maps k to d.
is_singleton [Fval]
Returns true on NaN.
is_singleton [Float_interval_sig.S]
Returns true on NaN.
is_singleton_int [Ival]
is_skip [Cil]
is_slice_pragma [Logic_utils]
is_small_set [Ival]
is_small_set [Int_val]
Is an abstraction internally represented as a small integer set?
is_special_builtin [Cil]
is_stmt_invariant [Logic_utils]
is_subcategory [Log]
Sub-category checks.
is_top [Origin]
is_top [Lmap_sig]
is_top [Int_Intervals_sig]
is_top [Int_Base]
is_transient_block [Cil]
tells whether the block has been marked as transient
is_trivial_annotation [Logic_utils]
is_trivially_false [Logic_utils]
true if the predicate is Pfalse
is_trivially_true [Logic_utils]
true if the predicate is Ptrue.
is_ucn [Logic_lexer]
is_unknown [Filepath.Normalized]
is_unmarshable [Descr]
is_unrollable_ltdef [Logic_const]
is_unused_builtin [Cil]
is_valid [Locations]
Is the given location entirely valid, without any access or as a destination for a read or write access.
is_valid_offset [Base]
is_valid_offset access b offset holds iff the ival offset (expressed in bits) is completely valid for the access of base b (it only represents valid offsets for such an access).
is_variant [Logic_utils]
is_warn_category [Log.Messages]
is_weak [Base]
Is the given base a weak one (in the sens that its validity is Weak).
is_weak_validity [Base]
is_weak_validity v returns true iff v is a Weak validity.
is_wto_head [Interpreted_automata.Compute]
is_wto_head [Interpreted_automata]
is_zero [Locations.Location_Bytes]
is_zero [Ival]
is_zero [Integer]
is_zero [Int_val]
is_zero [Int_Base]
is_zero [Abstract_interp.Rel]
is_zero_comparable [Logic_utils]
true if the given term has a type for which a comparison to 0 exists (i.e.
isfinite [Floating_point]
isnan [Floating_point]
iter [Vector]
iter [Type.Obj_tbl]
iter [Type.Heterogeneous_table]
iter [Task]
Auto-flush
iter [State_topological.Make]
iter action calls action node repeatedly.
iter [State_selection.S]
Iterate over a selection.
iter [State_builder.States]
iterates a function f over all registered states.
iter [State_builder.Array]
iter [State_builder.Queue]
iter [State_builder.Weak_hashtbl]
iter [State_builder.List_ref]
iter [Rgmap]
Iter over all entries present in the map.
iter [Rangemap.S]
iter f m applies f to all bindings in map m.
iter [Qstack.Make]
Iter on all the elements from the top to the end of the stack.
iter [Property_status]
iter [Parameter_sig.Collection]
Iterate over all the elements of the collection.
iter [Offsetmap_sig]
iter f m calls f on all the intervals bound in m, in increasing order.
iter [Messages]
Iter over all stored messages.
iter [Logic_env.Logic_builtin_used]
iter [Locations.Location_Bytes.M]
iter [Lmap_sig]
iter [Journal.Reverse_binding]
iter [Int_set]
iter [Int_Intervals_sig]
May raise Error_Top
iter [Indexer.Make]
Linear.
iter [Hptset.S_Basic_Compare]
iter [Hptmap_sig.S]
iter f m applies f to all bindings of the map m.
iter [Hptmap.Shape]
iter [Globals.Functions]
iter [Globals.Vars]
iter [Emitter.Make_table]
iter [Dynamic.Parameter.StringList]
iter [Dynamic.Parameter.StringSet]
iter [Dynamic]
iter [Db.From.Callwise]
iter [Dataflow2.StmtStartData]
iter [State_builder.Set_ref]
iter [State_builder.Hashtbl]
iter [Cabshelper.Comments]
iter [Bottom]
iter [Bag]
iter [Alarms]
Iterator over all alarms and the associated annotations at some program point.
iter [Lattice_type.Lattice_Set]
iter2 [Rangemap.S]
iter2 f m1 m2 computes f k v1 v2 for each k present in either m1 or m2 (the k being presented in ascending order), v_i being Some (find k m_i) if k is in m_i, and None otherwise (for i=1 or i=2)
iterFormalsDecl [Cil]
iterate the given function on declared prototypes.
iterGlobals [Cil]
Iterate over all globals, including the global initializer
iter_all_code_annot [Annotations]
Iter on each code annotation of the program.
iter_allocates [Annotations]
Iter on the allocates of the corresponding behavior.
iter_assigns [Annotations]
Iter on the assigns of the corresponding behavior.
iter_assumes [Annotations]
Iter on the assumes of the corresponding behavior.
iter_behaviors [Annotations]
Iter on the behaviors of the given kernel function.
iter_builtin_logic_ctor [Logic_env]
iter_builtin_logic_function [Logic_env]
iter_builtin_logic_type [Logic_env]
iter_code_annot [Annotations]
Iter on each code annotation attached to the given statement.
iter_comment [Dynamic]
iter_complete [Annotations]
Iter on the complete clauses of the given kernel function.
iter_decreases [Annotations]
apply f to the decreases term if any.
iter_disjoint [Annotations]
Iter on the disjoint clauses of the given kernel function.
iter_ensures [Annotations]
Iter on the ensures of the corresponding behavior.
iter_extended [Annotations]
iter_global [Annotations]
Iter on each global annotation of the program.
iter_in_file_order [Globals.Vars]
The next four iterators iter on all global variables present in the AST, following the order in which they are declared/defined.
iter_in_file_rev_order [Globals.Vars]
iter_in_order [State_selection.S]
Iterate over a selection in a topological ordering compliant with the State Dependency Graph.
iter_nodes [Db.Pdg]
apply a given function to all the PDG nodes
iter_on_fundecs [Globals.Functions]
iter_on_plugins [Plugin]
Iterate on each registered plug-ins.
iter_on_projects [Project]
iteration on project starting with the current one.
iter_on_result [Dataflows.Simple_forward]
iter_on_result [Dataflows.Simple_backward]
iter_on_statuses [Property_status]
iter_on_strings [Locations.Location_Bytes]
iter_on_values [Offsetmap_sig]
iter_on_values f m iterates on the entire contents of m, but f receives only the value bound to each interval.
iter_requires [Annotations]
Iter on the requires of the corresponding behavior.
iter_sorted [FCHashtbl.S]
Iter on the hashtbl, but respecting the order on keys induced by cmp.
iter_sorted [Emitter.Make_table]
iter_sorted [State_builder.Hashtbl]
iter_sorted_by_entry [FCHashtbl.S]
iter_sorted_by_value [FCHashtbl.S]
iter_succ [State_topological.G]
iter_succ [State_selection.S]
Iterate over the successor of a state in a selection.
iter_terminates [Annotations]
apply f to the terminates predicate if any.
iter_true [Bitvector]
Iterates on all indexes of the bitvector with their bit set.
iter_types [Globals.Types]
Iteration on named types (typedefs, structs, unions, enums).
iter_uncurry2 [Extlib]
iter_vertex [State_topological.G]
iteri [Vector]
iteri [State_builder.Array]
iteri [Indexer.Make]
Linear.
iteri [Extlib]
Same as iter, but the function to be applied take also as argument the index of the element (starting from 0).

J
job [Task]
join [Origin]
join [Offsetmap_bitwise_sig]
join [Lmap_sig]
join [Interpreted_automata.Domain]
Merges two states coming from different paths.
join [Int_set]
join [Hptmap_sig.S]
Same as generic_merge, but we assume that decide key None (Some v) = decide key (Some v) None = v holds.
join [Float_interval_sig.S]
join [Lattice_type.Join_Semi_Lattice]
over-approximation of union
join [Dataflows.JOIN_SEMILATTICE]
Must be idempotent (join a a = a), commutative, and associative.
join [Bottom.Top]
join [Bottom]
join_and_is_included [Dataflows.JOIN_SEMILATTICE]
This function is used by the dataflow algorithm to determine if something has to be recomputed.
join_list [Bottom]

K
keepUnused [Rmtmps]
keep_file [Journal]
This function has not to be used explicitly.
kernel [Emitter]
The special emitter corresponding to the kernel.
kernel_channel_name [Log]
the reserved channel name used by the Frama-C kernel.
kernel_function [Visitor_behavior.Fold]
kernel_function [Visitor_behavior.Iter]
kernel_function [Visitor_behavior.Unset]
kernel_function [Visitor_behavior.Set]
kernel_function [Visitor_behavior.Get]
kernel_function [Visitor_behavior.Reset]
kernel_function_of_local_var_or_param_varinfo [Globals.FileIndex]
kernel_function where the local variable or formal parameter is declared.
kernel_label_name [Log]
the reserved label name used by the Frama-C kernel.
kf [Dataflows.FUNCTION_ENV]
kf_category [Parameter_builder]
kf_decl_category [Parameter_builder]
kf_def_category [Parameter_builder]
kf_of_localizable [Printer_tag]
kf_of_localizable [Pretty_source]
kf_string_category [Parameter_builder]
kfloat [Cil]
Constructs a floating point constant.
ki_of_localizable [Printer_tag]
ki_of_localizable [Pretty_source]
kind [Fval]
Classify a Cil_types.fkind as either a 32 or 64 floating-point type.
kinstr [Db.INOUT]
kinstr_of_opt_stmt [Cil_datatype.Kinstr]
kinteger [Cil]
Construct an integer of a given kind.
kinteger64 [Cil]
Construct an integer of a given kind without literal representation.
kprintf [Rich_text]
ksfprintf [Pretty_utils]
similar to Format.kfprintf, but the continuation is given the result string instead of a formatter.
kw_c_mode [Logic_utils]

L
label [Wbox]
Helper to pack a Widget.label widget using box.
label [Markdown]
Transforms a string into an anchor name, roughly following pandoc's conventions.
label [Gtk_form]
label [Dotgraph.Record]
label_visible [Filter.RemoveInfo]
tells if the label is visible.
lablgtk [Fc_config]
Name of the lablgtk version against which Frama-C has been compiled.
last [Extlib]
returns the last element of a list.
lastOffset [Cil]
Returns the last offset in the chain.
lastTermOffset [Logic_const]
Equivalent to lastOffset for terms.
later [Wutil]
Post the action on next idle.
later [Task]
The task that, when started, compute a task to continue with.
launch [Task]
Starts the server if not running yet
layout [Dotgraph]
Invoke dot command (if installed) with specified target and engine.
lconstant [Cil]
The given constant logic term
lconstant_to_constant [Logic_utils]
le [Utf8_logic]
le [Integer]
legal_dependency_cycle [Property_status]
The given properties may define a legal dependency cycle for the given emitter.
lenOfArray [Cil]
Call to compute the array length as present in the array type, to an integer.
lenOfArray64 [Cil]
length [Vector]
length [State_builder.Array]
length [Qstack.Make]
length [Integer]
b - a + 1
length [Hook.S]
Number of registered functions.
length [Dataflow2.StmtStartData]
length [State_builder.Hashtbl]
Length of the table.
length [Bag]
lex_error [Logic_lexer]
lexpr [Logic_lexer]
lexpr_eof [Logic_parser]
lhost_c_type [Logic_utils]
libdir [Fc_config]
Directory where the Frama-C kernel library is.
library_names [Fc_config]
List of linked libraries.
lightweight_transform [Translate_lightweight]
Code transformation that interprets __declspec annotations.
link [Origin]
link [Markdown]
Local links
link [Lattice_type.With_Under_Approximation]
under-approximation of union
link [Int_set]
link [Eva_lattice_type.With_Under_Approximation]
under-approximation of union
link [Dotgraph.Record]
link [Dotgraph]
Link the node sequence with attributed edges
list [Markdown]
Itemized list
list [Json]
Extract the list of an Array object.
list [Datatype]
list [Bag]
list_compare [Extlib]
Generic list comparison function, where the elements are compared with the specified function
list_first_n [Extlib]
list_first_n n l returns the first n elements of the list.
list_of_bot [Bottom]
list_of_opt [Extlib]
converts an option into a list with 0 or 1 elt.
list_slice [Extlib]
list_slice ?first ?last l is equivalent to Python's slice operator (lfirst:last): returns the range of the list between first (inclusive) and last (exclusive), starting from 0.
list_union [State_selection.S]
Union of an arbitrary number of selection (0 gives an empty selection)
lmone [Cil]
The constant logic term -1.
load [Project]
Load a file into a new project given by its name.
load [Gtk_helper.Configuration]
loadConfiguration [Cilconfig]
Load the configuration from a file
load_all [Project]
First remove all the existing project, then load all the projects from a file.
load_channel [Json]
Parses the stream until EOF.
load_file [Source_manager]
If line is 0 then the last line of the text is shown.
load_file [Json]
May also raise system exception.
load_lexbuf [Json]
Consumes the entire buffer.
load_module [Dynamic]
Load the module specification.
load_string [Json]
Parses the Json in the string.
loc [Logic_lexer]
loc [Cil_datatype.Global_annotation]
loc [Cil_datatype.Code_annotation]
loc [Cil_datatype.Stmt]
loc [Cil_datatype.Kinstr]
loc [Cil_datatype.Instr]
loc [Cil_datatype.Global]
loc_bits_to_loc_bytes [Locations]
loc_bits_to_loc_bytes_under [Locations]
loc_bottom [Locations]
loc_bytes_to_loc_bits [Locations]
loc_equal [Locations]
loc_of_base [Locations]
loc_of_link [Gui_printers]
Convert a string of the form link:locN into the location of id N.
loc_of_localizable [Printer_tag]
Might return Location.unknown
loc_of_typoffset [Locations]
loc_of_varinfo [Locations]
loc_size [Locations]
loc_to_exp [Db.Properties.Interp]
loc_to_loc [Db.Properties.Interp]
loc_to_loc_under_over [Db.Properties.Interp]
Same as Db.Properties.Interp.loc_to_loc, except that we return simultaneously an under-approximation of the term (first location), and an over-approximation (second location).
loc_to_loc_without_size [Locations]
loc_to_localizable [Pretty_source]
return the (hopefully) most precise localizable that contains the given Filepath.position.
loc_to_lval [Db.Properties.Interp]
loc_to_offset [Db.Properties.Interp]
loc_var_visible [Filter.RemoveInfo]
tells if the local variable is visible.
local_definition [Kernel_function]
local_definition f v returns the statement initializing the (defined) local variable v of f.
localizable_from_locs [Pretty_source]
Returns the lists of localizable in file at line visible in the current Locs.state.
locate_localizable [Pretty_source]
location [Property]
returns the location of the property.
loffset_contains_result [Logic_utils]
true if \result is included in the offset.
log [Log.Messages]
Generic log routine.
log [Fval]
log [Float_sig.S]
log [Float_interval_sig.S]
log10 [Fval]
log10 [Float_sig.S]
log10 [Float_interval_sig.S]
log10f [Floating_point]
log_channel [Log]
logging function to user-created channel.
log_redirector [Gtk_helper]
Redirects all strings written to the terminal and call the given function on each.
logand [Integer]
logf [Floating_point]
logicCType [Logic_utils]
logicConditionalConversion [Cabs2cil]
returns the type of the result of a logic operator applied to values of the corresponding input types.
logic_info [Visitor_behavior.Fold]
logic_info [Visitor_behavior.Iter]
logic_info [Visitor_behavior.Unset]
logic_info [Visitor_behavior.Set]
logic_info [Visitor_behavior.Get]
logic_info [Visitor_behavior.Reset]
logic_info_of_global [Annotations]
logic_type_info [Visitor_behavior.Fold]
logic_type_info [Visitor_behavior.Iter]
logic_type_info [Visitor_behavior.Unset]
logic_type_info [Visitor_behavior.Set]
logic_type_info [Visitor_behavior.Get]
logic_type_info [Visitor_behavior.Reset]
logic_var [Visitor_behavior.Fold]
logic_var [Visitor_behavior.Iter]
logic_var [Visitor_behavior.Unset]
logic_var [Visitor_behavior.Set]
logic_var [Visitor_behavior.Get]
logic_var [Visitor_behavior.Reset]
logical_consequence [Property_status]
logical_consequence e ppt list indicates that the emitter e considers that ppt is a logical consequence of the conjunction of properties list.
lognot [Integer]
logor [Integer]
logwith [Log.Messages]
Recommanded generic log routine using warn_category instead of kind.
logxor [Integer]
lone [Cil]
The constant logic term 1.
longDoubleType [Cil]
long double
longLongType [Cil]
long long
longType [Cil]
long
loop_current_label [Logic_const]
loop_entry_label [Logic_const]
loop_preds [Stmts_graph]
Split the loop predecessors into: the entry point : coming from outside the loop, the back edges. Notice that there might be nothing in the entry point when the loop is the first statement.
lowest_binding [Rangemap.Make]
lowest_binding_above [Rangemap.Make]
lt [Integer]
lval_contains_result [Logic_utils]
true if \result is included in the lval.
lval_to_loc [Db.Value]
lval_to_loc_state [Db.Value]
lval_to_loc_with_deps [Db.Value]
lval_to_loc_with_deps_state [Db.Value]
lval_to_offsetmap [Db.Value]
lval_to_offsetmap_state [Db.Value]
lval_to_precise_loc_state [Db.Value]
lval_to_precise_loc_with_deps_state [Db.Value]
lval_to_term_lval [Logic_utils]
lval_to_zone [Db.Value]
lval_to_zone_state [Db.Value]
Does not emit alarms.
lval_to_zone_with_deps_state [Db.Value]
lval_to_zone_with_deps_state state ~for_writing ~deps lv computes res_deps, zone_lv, exact, where res_deps are the memory zones needed to evaluate lv in state joined with deps.
lzero [Cil]
The constant logic term zero.

M
machdep_macro [File]
machdep_macro machine returns the name of a macro __FC_MACHDEP_XXX so that the preprocessor can select std lib definition consistent with the selected machdep.
major_version [Fc_config]
Frama-C major version number.
make [Warning_manager]
Build a new widget for storing the warnings.
make [Source_viewer]
Build a new source viewer.
make [Source_manager]
make [Project_skeleton.Make_setter]
make [Int_val]
As inject_interval, but also checks that min and max are congruent to rem modulo modu.
make [Int_interval]
Makes the interval of all integers between min and max and congruent to rem modulo modu.
make [Filetree]
Create a file tree packed in the given tree_view.
makeFormalVar [Cil]
Make a formal variable for a function declaration.
makeFormalsVarDecl [Cil]
creates a new varinfo for the parameter of a prototype.
makeGlobalVar [Cil]
Make a global variable.
makeLocalVar [Cil]
Make a local variable and add it to a function's slocals and to the given block (only if insert = true, which is the default).
makeTempVar [Cil]
Make a temporary variable and add it to a function's slocals.
makeVarinfo [Cil]
Make a varinfo.
makeZeroInit [Cil]
Make a initializer for zero-ing a data type
make_formatter [Gtk_helper]
Build a formatter that redirects its output to the given buffer.
make_loc [Locations]
make_logic_info [Cil_const]
Create a fresh logical (global) variable giving its name and type.
make_logic_info_local [Cil_const]
Create a new local logic variable given its name.
make_logic_var [Cil_const]
Create a fresh logical variable giving its name and type.
make_logic_var_formal [Cil_const]
Create a new formal logic variable
make_logic_var_global [Cil_const]
Create a new global logic variable
make_logic_var_kind [Cil_const]
Create a fresh logical variable giving its name, type and origin.
make_logic_var_local [Cil_const]
Create a new local logic variable
make_logic_var_quant [Cil_const]
Create a new quantified logic variable
make_marker_attributes [GSourceView]
make_set_type [Logic_const]
converts a type into the corresponding set type if needed.
make_string_list [Gtk_helper]
make_tag [Gtk_helper]
make_temp_logic_var [Cil]
Make a temporary variable to use in annotations
make_text_page [Gtk_helper]
Insert a GText.view in a new page of the notebook with the given title, at position pos if specified, or last if not.
make_type [Datatype.Hashtbl]
make_type_list_of [Logic_const]
make_type_list_of t returns the type list<t>.
make_unique_name [Project_skeleton.Make_setter]
make_unique_name [Extlib]
make_unique_name mem s returns (0, s) when (mem s)=false otherwise returns (n,new_string) such that new_string is derived from (s,sep,start) and (mem new_string)=false and n<>0
make_view_column [Gtk_helper.MAKE_CUSTOM_LIST]
map [Vector]
Result is shrunk.
map [Task]
map [State_builder.Option_ref]
map [Rangemap.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 [Qstack.Make]
Replace in-place all the elements of the stack by mapping the old one.
map [Offsetmap_bitwise_sig]
map [Map_lattice.MapSet_Lattice]
map [Lmap_bitwise.Location_map_bitwise]
map [Int_set]
map [Hptmap_sig.S]
map f m returns the map obtained by composing the map m with the function f; that is, the map $k\mapsto f(m(k))$.
map [Bag]
map' [Hptmap_sig.S]
Same as map, except if f k v returns None.
map2 [Offsetmap_bitwise_sig]
See the documentation of function Offsetmap_sig.map2_on_values.
map2 [Lmap_bitwise.Location_map_bitwise]
'map'-like function between two interval maps, implemented as a simultaneous descent in both maps.
map2_on_values [Offsetmap_sig]
map2_on_values cache decide join m1 m2 applies join pointwise to all the elements of m1 and m2 and builds the resulting map.
mapGlobals [Cil]
Map over all globals, including the global initializer and change things in place
mapNoCopy [Cil]
Like map but try not to make a copy of the list
mapNoCopyList [Cil]
Like map but each call can return a list.
map_on_values [Offsetmap_sig]
map_on_values f m  creates the map derived from m by applying f to each interval.
map_reduce [Int_set]
map_under_info [Cil]
Map some function on underlying expression if Info or else on expression
mapi [Vector]
Result is shrunk.
mapi [Rangemap.S]
Same as Map.S.map, but the function receives as arguments both the key and the associated value for each binding of the map.
mapi [Extlib]
Same as map, but the function to be applied take also as argument the index of the element (starting from 0).
mapii [Rangemap.S]
Same as Map.S.mapi, but the function also returns a new key.
marger [Pretty_utils]
Create an empty marger
mark [Design.Feedback]
offset is the offset of the character in the source buffer.
mark_as_changed [Ast]
call this function whenever you've made some changes in place inside the AST
mark_as_computed [State_builder.S]
Indicate that the registered state will not change again for the given project (default is current ()).
mark_as_computed [Db.Value]
Indicate that the value analysis has been done already.
mark_as_computed [Ast]
mark_as_grown [Ast]
call this function whenever you have added something to the AST, without modifying the existing nodes
max [Transitioning.Stdlib]
max [Integer]
max [Int_set]
Returns the highest integer of a set.
max_binding [Rangemap.S]
Same as Map.S.min_binding, but returns the largest binding of the given map.
max_binding [Hptmap_sig.S]
max_bit_address [Bit_utils]
max_bit_size [Bit_utils]
max_byte_address [Bit_utils]
max_byte_size [Bit_utils]
max_cpt [Extlib]
max_cpt t1 t2 returns the maximum of t1 and t2 wrt the total ordering induced by tags creation.
max_float [Transitioning.Float]
max_int [Transitioning.Stdlib]
max_int [Ival]
A None result means the argument is unbounded.
max_int [Int_val]
Returns the highest integer represented by an abstraction.
max_int64 [Integer]
max_signed_number [Cil]
Returns the maximal value representable in a signed integer type of the given size (in bits)
max_single_precision_float [Floating_point]
max_unsigned_number [Cil]
Returns the maximal value representable in a unsigned integer type of the given size (in bits)
max_valid_absolute_address [Base]
Bounds for option absolute-valid-range
may [State_builder.Option_ref]
may [Extlib]
may f v applies f to x if v = Some(x)
may_map [Extlib]
may_map f ?dft x applies f to the value of x if exists.
may_reach [Locations.Location_Bytes]
may_reach base loc is true if base might be accessed from loc.
meet [Origin]
meet [Lattice_type.With_Under_Approximation]
under-approximation of intersection
meet [Int_set]
meet [Fval]
meet [Eva_lattice_type.With_Under_Approximation]
under-approximation of intersection
mem [Type.Obj_tbl]
mem [State_selection]
mem [State_builder.Weak_hashtbl]
mem x returns true if there is at least one instance of x in the table, false otherwise.
mem [Rangemap.S]
mem x m returns true if m contains a binding for x, and false otherwise.
mem [Qstack.Make]
Return true if the data exists in the stack and false otherwise.
mem [Parameter_sig.Multiple_map]
mem [Logic_env.Logic_builtin_used]
mem [Parameter_sig.Map]
mem [Parameter_sig.Set]
Does the given element belong to the set?
mem [Int_set]
mem i s is true iff the set s contains the integer i.
mem [Int_interval]
mem i t returns true iff the integer i is in the interval t.
mem [Indexer.Make]
Log complexity.
mem [Hptset.S_Basic_Compare]
mem [Hptmap_sig.S]
mem k m returns true if k is bound in m, and false otherwise.
mem [Emitter.Make_table]
mem [Dataflow2.StmtStartData]
mem [State_builder.Set_ref]
mem [State_builder.Hashtbl]
mem [Bitvector]
mem [Lattice_type.Lattice_Set]
mem_base [Locations.Zone]
mem_base b m returns true if b is associated to something or topified in t, and false otherwise.
mem_builtin [Db.Value]
returns whether there is an abstract function registered by Db.Value.register_builtin with the given name.
mem_project [Datatype.Make_input]
mem_project [Datatype.S_no_copy]
mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.
mem_project [Datatype.Undefined]
mem_project [Datatype]
memo [State_builder.Option_ref]
Memoization.
memo [FCHashtbl.S]
memo tbl k f returns the binding of k in tbl.
memo [State_builder.Hashtbl]
Memoization.
memory_footprint_var_name [Binary_cache]
menu [Gtk_form]
menubar [Menu_manager]
merge [State_builder.Weak_hashtbl]
merge x returns an instance of x found in the table if any, or else adds x and return x.
merge [Rangemap.S]
merge f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.
merge [Property_status]
merge old new registers properties in new which are not in old and removes properties in old which are not in new.
merge [Mergecil]
merge [Lmap_sig]
merge ~into t adds all binding from t into into.
merge [Hptmap_sig.S]
Merge of two trees, parameterized by a merge function.
merge [Binary_cache.Arity_Three]
merge [Binary_cache.Arity_Two]
merge [Binary_cache.Arity_One]
merge [Binary_cache.Symmetric_Binary_Predicate]
merge [Binary_cache.Binary_Predicate]
merge [Binary_cache.Symmetric_Binary]
merge [Hptset.S]
merge_allocation [Logic_utils]
merge allocation: take the one that is defined and select an arbitrary one if both are, emitting a warning unless both are syntactically the same.
merge_assigns [Logic_utils]
merge assigns: take the one that is defined and select an arbitrary one if both are, emitting a warning unless both are syntactically the same.
merge_assigns [Ast_info]
Returns the assigns of an unguarded behavior.
merge_assigns_from_complete_bhvs [Ast_info]
merge_assigns_from_spec [Ast_info]
It is a shortcut for merge_assigns_from_complete_bhvs
    spec.spec_complete_behaviors spec.spec_behavior
.
merge_behaviors [Logic_utils]
merge_distinct_bits [Offsetmap_lattice_with_isotropy]
Merge the bits of the two given values, that span disjoint bit ranges by construction.
merge_funspec [Logic_utils]
merge_funspec ?oldloc oldspec newspec merges newspec into oldspec.
merge_neutral_element [Offsetmap_lattice_with_isotropy]
Value that can be passed to Offsetmap_lattice_with_isotropy.merge_distinct_bits as the starting value.
merge_opt [Extlib]
merge f k a b returns None if both a and b are None, Some a' (resp. b' if b (resp a) is None and a (resp. b) is Some, f k a' b' if both a and b are Some It is mainly intended to be used with Map.merge
message [Rich_text]
Buffer contents, with its formatting tags.
messages [Plugin.S_no_log]
The group containing options -*-debug and -*-verbose.
min [Transitioning.Stdlib]
min [Integer]
min [Int_set]
Returns the smallest integer of a set.
min_and_max [Ival]
Returns the minimal and maximal integers represented by an ival.
min_and_max [Int_val]
Returns the smallest and highest integers represented by an abstraction.
min_and_max [Int_interval]
Returns the bounds of the given interval.
min_and_max [Float_interval_sig.S]
Returns the bounds of the float interval, (or None if the argument is exactly NaN), and a boolean indicating the possibility that the value may be NaN.
min_and_max_float [Ival]
returns the bounds of the float interval, (or None if the argument is exactly NaN), and a boolean indicating the possibility that the value may be NaN.
min_binding [Rangemap.S]
Return the smallest binding of the given map (with respect to the Ord.compare ordering), or raise Not_found if the map is empty.
min_binding [Hptmap_sig.S]
min_denormal [Floating_point]
min_int [Transitioning.Stdlib]
min_int [Ival]
A None result means the argument is unbounded.
min_int [Int_val]
Returns the smallest integer represented by an abstraction.
min_int64 [Integer]
min_max_r_mod [Ival]
min_max_rem_modu [Int_val]
Returns min, max, rem, modu such that for all integers i represented by the given abstraction, i satisfies min ≤ i ≤ max and i ≅ rem modu.
min_max_rem_modu [Int_interval]
Returns the bounds and the modulo of the given interval.
min_signed_number [Cil]
Returns the smallest value representable in a signed integer type of the given size (in bits)
min_single_precision_denormal [Floating_point]
min_valid_absolute_address [Base]
minor_version [Fc_config]
Frama-C minor version number.
minus [Utf8_logic]
minus_one [Ival]
The lattice element that contains only the integer -1.
minus_one [Integer]
minus_one [Int_val]
minus_one [Int_set]
minus_one [Int_Base]
minus_zero [Fval]
missingFieldDecl [Cabshelper]
missingFieldName [Cil]
This is a constant used as the name of an unnamed bitfield.
mkAddrOf [Cil]
Make an AddrOf.
mkAddrOfAndMark [Cabs2cil]
Applies mkAddrOf after marking variable whose address is taken.
mkAddrOfVi [Cil]
Creates an expression corresponding to "&v".
mkAddrOrStartOf [Cil]
Like mkAddrOf except if the type of lval is an array then it uses StartOf.
mkAttrAnnot [Cil]
returns the complete name for an attribute annotation.
mkBinOp [Cil]
makes a binary operation and performs const folding.
mkBinOp_safe_ptr_cmp [Cil]
same as Cil.mkBinOp, but performs a systematic cast (unless one of the arguments is 0) of pointers into uintptr_t during comparisons, making such operation defined even if the pointers do not share the same base.
mkBlock [Cil]
Construct a block with no attributes, given a list of statements
mkBlockNonScoping [Cil]
Construct a non-scoping block, i.e.
mkCast [Cil]
Like Cil.mkCastT but uses typeOf to get oldt
mkCastT [Cil]
Construct a cast when having the old type of the expression.
mkCompInfo [Cil_const]
Creates a (potentially recursive) composite type.
mkEmptyStmt [Cil]
Returns an empty statement (of kind Instr).
mkFor [Cil]
Make a for loop for(start; guard; next) { ...
mkForIncr [Cil]
Make a for loop for(i=start; i<past; i += incr) { ...
mkLoop [Cil]
Make a loop.
mkMem [Cil]
Make a Mem, while optimizing AddrOf.
mkPureExpr [Cil]
Create an instruction as above, enclosed in a block of a single (Instr) statement, which will be the scope of the fresh variable holding the value of the expression.
mkPureExprInstr [Cil]
Create an instruction equivalent to a pure expression.
mkStmt [Cil]
Construct a statement, given its kind.
mkStmtCfg [Cil]
mkStmtCfgBlock [Cil]
Construct a block with no attributes, given a list of statements and wrap it into the Cfg.
mkStmtOneInstr [Cil]
Construct a statement consisting of just one instruction See Cil.mkStmt for the signification of the optional args.
mkString [Cil]
Make an expression that is a string constant (of pointer type)
mkTermMem [Cil]
Equivalent to mkMem for terms.
mk_asm_templates [Cabshelper]
mk_behavior [Cil]
mk_behavior [Cabshelper]
mk_cast [Logic_utils]
creates a logic cast if required, with some automatic simplifications being performed automatically.
mk_cast [Logic_typing.Make]
mk_ctx_func_contrat [Db.Properties.Interp.To_zone]
To build an interpretation context relative to function contracts.
mk_ctx_stmt_annot [Db.Properties.Interp.To_zone]
To build an interpretation context relative to statement annotations.
mk_ctx_stmt_contrat [Db.Properties.Interp.To_zone]
To build an interpretation context relative to statement contracts.
mk_fun [Extlib]
Build a reference to an uninitialized function
mk_labeled_fun [Extlib]
To be used to initialized a reference over a labeled function.
mk_logic_AddrOf [Logic_utils]
creates an AddrOf from a TLval.
mk_logic_StartOf [Logic_utils]
creates a TStartOf from an TLval.
mk_logic_pointer_or_StartOf [Logic_utils]
creates either a TStartOf or the corresponding TLval.
mkassign [Ast_info]
mkassign_statement [Ast_info]
mkdir [Extlib]
mkdir ?parents name perm creates directory name with permission perm.
ml_name [Type]
model_annot [Logic_typing.Make]
model_fields [Annotations]
returns the model fields attached to a given type (either directly or because the type is a typedef of something that has model fields.
model_info [Visitor_behavior.Fold]
model_info [Visitor_behavior.Iter]
model_info [Visitor_behavior.Unset]
model_info [Visitor_behavior.Set]
model_info [Visitor_behavior.Get]
model_info [Visitor_behavior.Reset]
module_name [Type.Polymorphic4_input]
module_name [Type.Polymorphic3_input]
module_name [Type.Polymorphic2_input]
module_name [Type.Polymorphic_input]
The name of the built module.
module_name [Kernel.Input_with_arg]
module_name [Datatype.Functor_info]
Must be a valid OCaml module name corresponding to the module name you are defining by applying the functor.
mone [Cil]
-1
most_negative_single_precision_float [Floating_point]
move_at_end [Qstack.Make]
Move the element x at the end of the stack s.
move_at_top [Qstack.Make]
Move the element x at the top of the stack s.
msvcMode [Cprint]
msvcMode [Cil]
msvc_x86_64 [Machdeps]
mul [Ival]
mul [Integer]
mul [Int_val]
mul [Int_set]
mul [Int_interval]
mul [Float_sig.S]
mul [Float_interval_sig.S]
must_recompute_cfg [File]
must_recompute_cfg f must be called by code transformation hooks when they modify statements in function f.
mutex [Task]

N
name [Type.Polymorphic4_input]
name [Type.Polymorphic3_input]
name [Type.Polymorphic2_input]
name [Type.Polymorphic_input]
How to build a name for each monomorphic instance of the type value from the underlying type.
name [Type]
name [State_builder.Info]
Name of the internal state.
name [State_builder.S]
name [Datatype.Make_input]
Unique name for this datatype.
name [Datatype.S_no_copy]
Unique name of the datatype.
name [Dataflow2.BackwardsTransfer]
For debugging purposes, the name of the analysis
name [Dataflow2.ForwardsTransfer]
For debugging purposes, the name of the analysis
name [Cmdline.Group]
nan [Float_interval_sig.S]
The NaN singleton
narrow [Origin]
narrow [Offsetmap_sig.Make_Narrow]
Over-approximation of the intersection of abstract values, without considering (bitwise) reinterpretations.
narrow [Lmap_sig.Make_Narrow]
narrow [Lattice_type.With_Narrow]
over-approximation of intersection
narrow [Int_set]
narrow [Float_interval_sig.S]
narrow [Eva_lattice_type.With_Narrow]
over-approximation of intersection
narrow [Bottom.Top]
narrow [Bottom]
narrow_reinterpret [Offsetmap_sig.Make_Narrow]
Variant of the function above that bitwise-reinterprets values before performing the intersection (in order to get normal forms).
nativeint [Datatype]
nb_errors [Messages]
nb_messages [Messages]
Number of stored warning messages, error messages, or all messages.
nb_stmts [Dataflows.FUNCTION_ENV]
nb_warnings [Messages]
nearest_common_ancestor [Dominators]
Finds the statement lowest in the function that dominates all the statements in the list passed as argument.
nearest_elt_ge [Datatype.Set]
nearest_elt_le [Datatype.Set]
need_cast [Cil]
true if both types are not equivalent.
neg [Utf8_logic]
neg [Integer]
neg [Int_val]
Negation of an integer abstraction.
neg [Int_set]
neg [Int_interval]
neg [Int_Base]
neg [Float_sig.S]
neg [Float_interval_sig.S]
neg_infinity [Float_interval_sig.S]
neg_int [Ival]
Negation of an integer ival.
neg_min_denormal [Floating_point]
neg_min_single_precision_denormal [Floating_point]
negative_integers [Ival]
The lattice element that contains exactly the negative or null integers
negative_integers [Int_val]
All negative integers, including 0.
neq [Utf8_logic]
never_any_project [Datatype]
Must be used for mem_project if values of your type does never contain any project.
never_write [Journal]
never_write name f returns a closure g observationally equal to f except that trying to write a call to g in the journal is an error.
newAlphaName [Alpha]
Create a new name based on a given name.
new_acsl_extension [Logic_const]
creates a new acsl_extension with a fresh id.
new_channel [Log]
new_code_annotation [Logic_const]
creates a code annotation with a fresh id.
new_exp [Cil]
creates an expression with a fresh id
new_file_type [File]
new_file_type suffix func funcname registers a new type of files (with corresponding suffix) as recognized by Frama-C through func.
new_identified_term [Logic_const]
creates a new identified term with a fresh id
new_machdep [File]
new_machdep name module registers a new machdep name as recognized by Frama-C through The usual uses is Cmdline.run_after_loading_stage
      (fun () -> File.new_machdep "my_machdep" my_machdep_implem)
new_predicate [Logic_const]
creates a new identified predicate with a fresh id.
new_raw_id [Cil_const]
Generate a new ID.
newline [Errorloc]
Call this function to announce a new line
next [State_builder.Counter]
Increments the counter and returns a fresh value
next [Cil_const.Eid]
next [Cil_const.Sid]
next [Cil_const.Vid]
next_float [Fval.F]
First double strictly above the argument.
next_float [Float_sig.S]
First value above the argument in the given precision.
nextafter [Floating_point]
nextafterf [Floating_point]
nextident [Cabshelper]
no_category [Parameter_customize]
Prevent a collection parameter to use categories and the extension '+', and '-' mechanism.
no_element_of_string [Parameter_sig.Builder]
no_op_coerce [Cil]
no_op_coerce typ term is true iff converting term to typ does not modify its value.
no_results [Db.Value]
Returns true if the user has requested that no results should be recorded for this function.
node [Dotgraph.Node]
node [Dotgraph]
Set attributes to node
node_default [Dotgraph]
Set default node attributes
node_key [Db.Pdg]
non_bottom [Bottom]
none [Parameter_sig.Collection_category]
The category '@none'
nop [Task]
The task that immediately returns unit
nop [Extlib]
Do nothing.
nop [Cmdline]
normalisation [Kernel]
normalization_parameters [Kernel]
All the normalization options that influence the AST (in particular, changing one will reset the AST entirely.contents
normalize [Filepath]
Returns an absolute path leading to the given file.
not_yet_implemented [Logic_interp.To_zone]
not_yet_implemented [Log.Messages]
raises FeatureRequest but does not send any message.
notify [Log]
Send an event over the associated listeners.
nth [Qstack.Make]
null [Unmarshal]
recursive values cannot be completely formed at the time they are passed to their transformation function.
null [Pretty_utils]
Prints nothing.
null [Log]
Prints nothing.
null [Base]
null_set [Base]
Set containing only the base Base.null.
nullprintf [Pretty_utils]
Discards the message and returns unit.
nullprintf [Log]
Discards the message and returns unit.
number_to_color [Extlib]
numeric_coerce [Logic_utils]
numeric_coerce typ t returns a term with the same value as t and of type typ.

O
o_loc_of_stmt [Property]
create a Loc_contract or Loc_stmt depending on the kinstr.
ocaml_wflags [Fc_config]
Warning flags used when compiling Frama-C.
ocamlc [Fc_config]
Name of the bytecode compiler.
ocamlopt [Fc_config]
Name of the native compiler.
of_array [Vector]
Makes a copy.
of_array [Json]
of_bool [Json]
of_c_logic_var [Base]
Must only be called on logic variables that have a C type
of_fields [Json]
of_float [Json]
of_float [Integer]
of_float [Fval.F]
fails on NaNs, but allows infinities.
of_float [Float_sig.S]
Converts a caml float into a floating-point number of the given precision.
of_int [Json]
of_int [Ival]
of_int [Integer]
of_int32 [Integer]
of_int64 [Ival]
of_int64 [Integer]
of_lexing_loc [Cil_datatype.Location]
of_lexing_pos [Cil_datatype.Position]
of_list [State_selection]
The selection containing only the given list of states.
of_list [Offsetmap_sig]
from_list fold c size creates an offsetmap by applying the iterator fold to the container c, the elements of c being supposed to be of size size.
of_list [Json]
of_list [Hptset.S_Basic_Compare]
of_pack [Structural_descr]
of_singleton_string [Parameter_sig.String_datatype_with_collections]
If a single string can be mapped to several elements.
of_string [Parameter_sig.Multiple_value_datatype]
of_string [Parameter_sig.Value_datatype]
key is the key associated to this value, while prev is the previous value associated to this key (if any).
of_string [Parameter_sig.String_datatype_with_collections]
of_string [Parameter_sig.String_datatype]
of_string [Json]
of_string [Integer]
of_string [Datatype.Filepath]
of_string [Filepath.Normalized]
of_string s converts s into a normalized path.
of_string_exp [Base]
of_structural [Descr]
Type descriptor from the structural descriptor.
of_type [Descr]
Type descriptor from the type value.
of_varinfo [Base]
off [Parameter_sig.Bool]
Set the boolean to false.
off [Dynamic.Parameter.Bool]
Set the parameter to false.
off_progress [Db]
Unregister the daemon.
offset_to_term_offset [Logic_utils]
old_gtk_compat [Gtk_helper]
Catch exception Not_found and do nothing
old_label [Logic_const]
on [Wutil]
on [Project]
on p f x sets the current project to p, computes f x then restores the current project.
on [Parameter_sig.Bool]
Set the boolean to true.
on [Dynamic.Parameter.Bool]
Set the parameter to true.
on_bool [Gtk_helper]
Pack a check button
on_combo [Gtk_helper]
Pack a string-selector
on_current_history [History]
on_current_history () returns a closure at such that at f will execute f in a context in which the history will be the one relevant when on_current_history was executed.
on_idle [Task]
Typically modified by GUI.
on_int [Gtk_helper]
Pack a spin button.
on_progress [Db]
on_progress ?debounced ?on_delayed trigger registers trigger as new daemon to be executed on each Db.yield.
on_server_activity [Task]
Idle server callback
on_server_start [Task]
On-start server callback
on_server_stop [Task]
On-stop server callback
on_server_wait [Task]
On-wait server callback (all tasks are scheduled)
on_singleton [Hptmap_sig.S]
on_singleton f m returns f k d if m is a singleton map that maps k to d.
on_string [Gtk_helper]
Pack a string chooser
on_string_completion [Gtk_helper]
on_string_set [Gtk_helper]
Pack a string-set chooser
once [Wutil_once]
once [Wutil]
once [Bitvector]
return true if unset, then set the bit.
one [Ival]
The lattice element that contains only the integer 1.
one [Integer]
one [Int_val]
one [Int_set]
one [Int_Base]
one [Cil]
1
oneret [Oneret]
Make sure that there is only one Return statement in the whole body.
onethousand [Integer]
only_codependencies [State_selection.S]
The selection containing all the co-dependencies of the given state (but not this state itself).
only_dependencies [State_selection.S]
The selection containing all the dependencies of the given state (but not this state itself).
open_dot [Dotgraph]
open_in_external_viewer [Gtk_helper]
Opens file in an external viewer, optionally centered on line line (if supported by the viewer).
optMapNoCopy [Cil]
same as mapNoCopy for options
opt_bind [Extlib]
opt_bind f x returns None if x is None and f y if is Some y (monadic bind)
opt_compare [Extlib]
opt_conv [Extlib]
opt_conv default v returns default if v is None and a if v is Some a
opt_equal [Extlib]
opt_filter [Extlib]
opt_fold [Extlib]
opt_hash [Extlib]
opt_if [Extlib]
opt_if cond v returns Some v if cond is true and None otherwise
opt_map [Extlib]
opt_of_list [Extlib]
converts a list with 0 or 1 element into an option.
option [Datatype]
option_name [Parameter_sig.S_no_parameter]
Name of the option on the command-line
option_name [Parameter_sig.Input]
The name of the option
optlabel_func [Datatype]
optlabel_func lab dft ty1 ty2 is equivalent to func ~label:(lab, Some dft) ty1 ty2
osizeof [Bit_utils]
osizeof ty is the size of ty in bytes.
osizeof_pointed [Bit_utils]
output [Parameter_sig.With_output]
To be used by the plugin to output the results of the option in a controlled way.
output [Kernel.CodeOutput]
output_graph [Service_graph.S]
output_to_dot [Interpreted_automata.UnrollUnnatural]
output_to_dot [Interpreted_automata.Compute]
output_to_dot [Interpreted_automata]
overlaps [Locations]
Is there a possibly non-empty intersection between two given locations? If partial is true, returns true if the two locations may be overlapping without being equal.
overlaps [Ival]
overlaps [Int_val]

P
p_abstract [Structural_descr]
Equivalent to pack Abstract
p_bool [Structural_descr]
p_float [Structural_descr]
p_int [Structural_descr]
p_int32 [Structural_descr]
p_int64 [Structural_descr]
p_nativeint [Structural_descr]
p_string [Structural_descr]
p_unit [Structural_descr]
pack [Structural_descr]
Pack a structural descriptor in order to embed it inside another one.
pack [Descr]
packed_descr [Fval.F]
packed_descr [Float_sig.S]
packed_descr [Float_interval_sig.S]
packed_descr [Datatype.S_no_copy]
Packed version of the descriptor.
pair [Datatype]
pallocable [Logic_const]
\allocable
pand [Logic_const]
&&
pandoc [Markdown]
Creates a document from a list of elements and optional metadatas.
pands [Logic_const]
Folds && over a list of predicates.
panel [Wbox]
Helper to create a full featured window: ~top is layout as a toolbar, left and right as sidebars, and bottom as a status bar.
papp [Logic_const]
application of predicate
par [Type]
par context myself fmt pp puts parenthesis around the verbatim prints by pp according to the precedence myself of the verbatim and to the precedence context of the caller of the pretty printer.
par [Markdown]
Single Paragraph element
par_ty_name [Type]
par_ty_name f ty puts parenthesis around the name of the ty iff f ty is true.
param_visible [Filter.RemoveInfo]
tells if the n-th formal parameter is visible.
parameter [Parameter_sig.S]
parameters [Parameter_sig.Builder]
parse [Frontc]
the main command to parse a file.
parse [Floating_point]
parse s parses s and returns the parsed float and its kind (single, double or long double precision) according to its suffix, if any.
parseInt [Cil]
Convert a string representing a C integer literal to an expression.
parseIntExp [Cil]
parseIntLogic [Cil]
parse_error [Errorloc]
Parse errors are usually fatal, but their reporting is sometimes delayed until the end of the current parsing phase.
parse_float [Logic_utils]
Parse the given string as a float or real logic constant.
parse_from_location [Logic_lexer]
parsing [Kernel]
partition [Wto.Make]
Implements Bourdoncle "Efficient chaotic iteration strategies with widenings" algorithm to compute a WTO.
partition [Rangemap.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 [Hptset.S_Basic_Compare]
partition [Bag]
partitionAttributes [Cil]
Partition the attributes into classes:name attributes, function type, and type attributes
paste_offsetmap [Lmap_sig]
paste_offsetmap ~from ~dst_loc ~size ~exact m copies from, which is supposed to be exactly size bits, and pastes them at dst_loc in m.
paste_slice [Offsetmap_sig]
pat [Logic_const]
\at
pdangling [Logic_const]
\dangling
peepHole1 [Cil]
Similar to peepHole2 except that the optimization window consists of one statement, not two
peepHole2 [Cil]
A peephole optimizer that processes two adjacent statements and possibly replaces them both.
pexists [Logic_const]
\exists
pfalse [Logic_const]
\false
pforall [Logic_const]
\forall
pfreeable [Logic_const]
\freeable
pfresh [Logic_const]
\fresh(pt,size)
pgcd [Integer]
pgcd v 0 == pgcd 0 v == abs v.
pi [Utf8_logic]
pi [Fval]
Real representation of \pi.
pif [Logic_const]
? :
piff [Logic_const]
<==>
pimplies [Logic_const]
==>
pinitialized [Logic_const]
\initialized
place_paned [Gtk_helper]
Sets the position of the paned widget to the given ratio
plain [Markdown]
Plain markdown
plain_or_set [Logic_const]
plain_or_set f t applies f to t or to the type of elements of t if it is a set type.
play [Db.Main]
Run all the Frama-C analyses.
plet [Logic_const]
local binding
plugin_dir [Fc_config]
Directory where the Frama-C dynamic plug-ins are.
plugin_path [Fc_config]
The coma-separated concatenation of plugin_dir.
plugin_subpath [Plugin]
Use the given string as the sub-directory in which the plugin files will be installed (ie.
plus_zero [Fval.F]
plus_zero [Fval]
pnot [Logic_const]
pobject_pointer [Logic_const]
\object_pointer
pointed_type [Ast_info]
pointer_comparable [Logic_utils]
\pointer_comparable
pold [Logic_const]
\old
pool [Task]
pop_attr_test [Cabshelper]
pop_context [Lexerhack]
pop_context [Clexer]
Remove all names added in this context
pop_state [Logic_lexer]
popcount [Integer]
por [Logic_const]
||
pors [Logic_const]
Folds || over a list of predicates.
port [Dotgraph]
Create a port to a node, and returns the associated pseudo-node so you can link an edge to it.
pos_infinity [Float_interval_sig.S]
The infinities singleton
positive_integers [Ival]
The lattice element that contains exactly the positive or null integers
positive_integers [Int_val]
All positive integers, including 0.
possible_value_of_integral_const [Ast_info]
possible_value_of_integral_expr [Ast_info]
possible_value_of_integral_logic_const [Ast_info]
possible_value_of_integral_term [Ast_info]
post_label [Logic_const]
post_state [Dataflows.Simple_forward]
This function calls transfer_stmt on the result of pre_state.
post_state [Dataflows.Simple_backward]
post_state_env [Logic_typing]
enter a given post-state and put \result in the env.
pow [Float_sig.S]
pow [Float_interval_sig.S]
power_int_positive_int [Integer]
Exponentiation
powf [Floating_point]
pp [Json]
pp_abs [Datatype.Filepath]
pp_abs [Filepath.Normalized]
Pretty-prints the normalized (absolute) path.
pp_acsl_extension [Cil_types_debug]
pp_acsl_extension_kind [Cil_types_debug]
pp_all_warn_categories_status [Log.Messages]
pp_allocation [Printer_api.S_pp]
pp_allocation [Cil_types_debug]
pp_array [Pretty_utils]
pretty prints an array.
pp_assigns [Printer_api.S_pp]
pp_assigns [Cil_types_debug]
pp_attr [Dotgraph]
pp_attr [Cabs_debug]
pp_attribute [Printer_api.S_pp]
pp_attribute [Cil_types_debug]
pp_attributes [Printer_api.S_pp]
pp_attributes [Cil_types_debug]
pp_attrparam [Printer_api.S_pp]
pp_attrparam [Cil_types_debug]
pp_attrs [Cabs_debug]
pp_behavior [Printer_api.S_pp]
pp_behavior [Cil_types_debug]
pp_bhv [Description]
prints nothing for default behavior, and " for 'b'" otherwise
pp_bin [Integer]
Print binary format.
pp_bin_op [Cabs_debug]
pp_binop [Printer_api.S_pp]
pp_binop [Cil_types_debug]
pp_bits [Bitvector]
0b...
pp_bitsSizeofTyp [Cil_types_debug]
pp_bitsSizeofTypCache [Cil_types_debug]
pp_block [Printer_api.S_pp]
pp_block [Markdown]
pp_block [Cil_types_debug]
pp_block [Cabs_debug]
pp_block_element [Markdown]
pp_blocklist [Pretty_utils]
pp_bool [Cil_types_debug]
pp_builtin_logic_info [Printer_api.S_pp]
pp_builtin_logic_info [Cil_types_debug]
pp_cabsloc [Cabs_debug]
pp_catch_binder [Cil_types_debug]
pp_category [Log.Messages]
pretty-prints a category.
pp_char [Cil_types_debug]
pp_cil_function [Cil_types_debug]
pp_close_block [Pretty_utils]
pp_close_stag [Transitioning.Format]
pp_code_annotation [Printer_api.S_pp]
pp_code_annotation [Cil_types_debug]
pp_code_annotation_node [Cil_types_debug]
pp_compare [Description]
Computes a partial order compatible with pretty printing
pp_compinfo [Printer_api.S_pp]
pp_compinfo [Cil_types_debug]
pp_cond [Pretty_utils]
pp_cond cond f s pretty-prints s if cond is true and the optional pr_false, which defaults to nothing, otherwise
pp_const [Cabs_debug]
pp_constant [Printer_api.S_pp]
pp_constant [Cil_types_debug]
pp_context_from_file [Errorloc]
prints the line identified by the position, together with ctx lines of context before and after.
pp_custom_tree [Cil_types_debug]
pp_cvspec [Cabs_debug]
pp_decl_type [Cabs_debug]
pp_decreases [Printer_api.S_pp]
pp_def [Cabs_debug]
pp_deps [Cil_types_debug]
pp_dump [Json]
without formatting
pp_edge [Dotgraph]
-> b
pp_element [Markdown]
pp_elements [Markdown]
pp_enum_item [Cabs_debug]
pp_enuminfo [Cil_types_debug]
pp_enumitem [Cil_types_debug]
pp_exp [Printer_api.S_pp]
pp_exp [Cil_types_debug]
pp_exp [Cil_descriptive_printer]
pp_exp [Cabs_debug]
pp_exp_info [Cil_types_debug]
pp_exp_node [Cil_types_debug]
pp_exp_node [Cabs_debug]
pp_extended [Printer_api.S_pp]
pp_extended_asm [Cil_types_debug]
pp_fail [Datatype]
Must be used for internal_pretty_code if this pretty-printer must fail only when called.
pp_field [Printer_api.S_pp]
pp_field_group [Cabs_debug]
pp_field_groups [Cabs_debug]
pp_fieldinfo [Cil_types_debug]
pp_file [Printer_api.S_pp]
pp_file [Cil_types_debug]
pp_file [Cabs_debug]
pp_filepath_position [Cil_types_debug]
pp_fkind [Printer_api.S_pp]
pp_fkind [Cil_types_debug]
pp_float [Cil_types_debug]
pp_flowlist [Pretty_utils]
pp_for [Description]
prints nothing or " for 'b1,...,bn'"
pp_for_clause [Cabs_debug]
pp_from [Printer_api.S_pp]
pp_from [Cil_types_debug]
pp_from_file [Command]
pp_from_file fmt file dumps the content of file into the fmt.
pp_full_assigns [Printer_api.S_pp]
first parameter is the introducing keyword (e.g.
pp_fun_spec [Cabs_debug]
pp_funbehavior [Cil_types_debug]
pp_fundec [Printer_api.S_pp]
pp_fundec [Cil_types_debug]
pp_funspec [Printer_api.S_pp]
pp_funspec [Cil_types_debug]
pp_get_formatter_stag_functions [Transitioning.Format]
pp_global [Printer_api.S_pp]
pp_global [Cil_types_debug]
pp_global_annotation [Printer_api.S_pp]
pp_global_annotation [Cil_types_debug]
pp_hex [Integer]
Print hexadecimal format.
pp_identified_predicate [Printer_api.S_pp]
pp_identified_predicate [Cil_types_debug]
pp_identified_term [Printer_api.S_pp]
pp_identified_term [Cil_types_debug]
pp_idpred [Description]
prints the "'<labels>'" or the "(<location>)" of the predicate
pp_ikind [Printer_api.S_pp]
pp_ikind [Cil_types_debug]
pp_impact_pragma [Cil_types_debug]
pp_init [Printer_api.S_pp]
pp_init [Cil_types_debug]
pp_init_exp [Cabs_debug]
pp_init_name [Cabs_debug]
pp_init_name_group [Cabs_debug]
pp_initinfo [Printer_api.S_pp]
pp_initinfo [Cil_types_debug]
pp_initwhat [Cabs_debug]
pp_inline [Markdown]
pp_instr [Printer_api.S_pp]
pp_instr [Cil_types_debug]
pp_int [Cil_types_debug]
pp_int64 [Cil_types_debug]
pp_integer [Cil_types_debug]
pp_items [Pretty_utils]
Prints a collection of elements, with the possibility of aligning titles with each others.
pp_iter [Pretty_utils]
pretty prints any structure using an iterator on it.
pp_iter2 [Pretty_utils]
pretty prints any map-like structure using an iterator on it.
pp_kernel_function [Cil_types_debug]
pp_kinstr [Description]
prints nothing for global, or " at <stmt>"
pp_kinstr [Cil_types_debug]
pp_label [Printer_api.S_pp]
pp_label [Cil_types_debug]
pp_labels [Cabs_debug]
pp_lexing_position [Cil_types_debug]
pp_lhost [Cil_types_debug]
pp_list [Pretty_utils]
pretty prints a list.
pp_list [Cil_types_debug]
pp_local [Description]
completely local printer
pp_localisation [Cil_types_debug]
pp_localized [Description]
prints more-or-less localized property
pp_location [Printer_api.S_pp]
pp_location [Cil_types_debug]
pp_logic_body [Cil_types_debug]
pp_logic_builtin_label [Printer_api.S_pp]
pp_logic_builtin_label [Cil_types_debug]
pp_logic_constant [Printer_api.S_pp]
pp_logic_constant [Cil_types_debug]
pp_logic_ctor_info [Printer_api.S_pp]
pp_logic_ctor_info [Cil_types_debug]
pp_logic_info [Printer_api.S_pp]
pp_logic_info [Cil_types_debug]
pp_logic_label [Printer_api.S_pp]
pp_logic_label [Cil_types_debug]
pp_logic_real [Cil_types_debug]
pp_logic_type [Printer_api.S_pp]
pp_logic_type [Cil_types_debug]
pp_logic_type_def [Cil_types_debug]
pp_logic_type_info [Printer_api.S_pp]
pp_logic_type_info [Cil_types_debug]
pp_logic_var [Printer_api.S_pp]
pp_logic_var [Cil_types_debug]
pp_logic_var_kind [Cil_types_debug]
pp_loop_allocation [Printer_api.S_pp]
pp_loop_assigns [Printer_api.S_pp]
pp_loop_from [Printer_api.S_pp]
pp_loop_pragma [Cil_types_debug]
pp_lval [Printer_api.S_pp]
pp_lval [Cil_types_debug]
pp_lval [Cil_descriptive_printer]
pp_mach [Cil_types_debug]
pp_margin [Pretty_utils]
Prints a text with margins wrt to marger.
pp_ml_name [Type]
pp_model_field [Printer_api.S_pp]
pp_model_info [Printer_api.S_pp]
pp_model_info [Cil_types_debug]
pp_name [Cabs_debug]
pp_name_group [Cabs_debug]
pp_named [Description]
prints the name of a named logic structure (if any), separated by ','.
pp_node [Dotgraph]
pp_offset [Printer_api.S_pp]
pp_offset [Cil_types_debug]
pp_open_block [Pretty_utils]
pp_open_stag [Transitioning.Format]
pp_opt [Pretty_utils]
pretty-prints an optional value.
pp_option [Cil_types_debug]
pp_pair [Pretty_utils]
pp_pair ?pre ?sep ?suf pp_a pp_b (a,b) pretty prints the pair (a,b), using the pretty printers pp_a and pp_b, with optional prefix/separator/suffix, whose default values are: pre: open a box, sep: print a comma character, suf: close a box.
pp_pair [Cil_types_debug]
pp_pandoc [Markdown]
pp_pos [Filepath]
Pretty-prints a position, in the format file:line.
pp_post_cond [Printer_api.S_pp]
pp_pragma [Cil_types_debug]
pp_predicate [Printer_api.S_pp]
pp_predicate [Cil_types_debug]
pp_predicate_node [Printer_api.S_pp]
pp_predicate_node [Cil_types_debug]
pp_print_option [Transitioning.Format]
pp_print_string_fill [Pretty_utils]
transforms every space in a string in breakable spaces.
pp_property [Description]
prints an identified property
pp_quantifiers [Cil_types_debug]
pp_raw_stmt [Cabs_debug]
pp_ref [Cil_types_debug]
pp_region [Description]
prints message "nothing" or the "'<names>'" or the "(<location>)" of the relation
pp_relation [Printer_api.S_pp]
pp_relation [Cil_types_debug]
pp_set_formatter_stag_functions [Transitioning.Format]
pp_short_extended [Printer_api.S_pp]
pp_single_name [Cabs_debug]
pp_slice_pragma [Cil_types_debug]
pp_spec [Cil_types_debug]
pp_spec [Cabs_debug]
pp_spec_elem [Cabs_debug]
pp_stmt [Printer_api.S_pp]
pp_stmt [Description]
prints "<instruction>" or "<instruction> (<file,line>)"
pp_stmt [Cil_types_debug]
pp_stmt [Cabs_debug]
pp_stmtkind [Cil_types_debug]
pp_storage [Printer_api.S_pp]
pp_storage [Cil_types_debug]
pp_storage [Cabs_debug]
pp_string [Cil_types_debug]
pp_term [Printer_api.S_pp]
pp_term [Cil_types_debug]
pp_term_lhost [Printer_api.S_pp]
pp_term_lhost [Cil_types_debug]
pp_term_lval [Printer_api.S_pp]
pp_term_lval [Cil_types_debug]
pp_term_node [Cil_types_debug]
pp_term_offset [Printer_api.S_pp]
pp_term_offset [Cil_types_debug]
pp_termination_kind [Cil_types_debug]
pp_text [Markdown]
pp_thisloc [Cil]
Pretty-print (Cil.CurrentLoc.get ())
pp_to_file [Command]
pp_to_file file pp runs pp on a formatter that writes into file.
pp_trail [Pretty_utils]
pretty-prints its contents inside an '(** ...
pp_tuple3 [Cil_types_debug]
pp_tuple4 [Cil_types_debug]
pp_tuple5 [Cil_types_debug]
pp_typ [Printer_api.S_pp]
pp_typ [Gui_printers]
Same as Printer.pp_typ, except that the type is output between Format tags @{<link:typN>}, that are recognized by the GUI.
pp_typ [Cil_types_debug]
pp_typ_unfolded [Gui_printers]
Pretty-prints a type, unfolding it once if it is a typedef, enum, struct or union.
pp_typeSpecifier [Cabs_debug]
pp_typeinfo [Cil_types_debug]
pp_un_op [Cabs_debug]
pp_unop [Printer_api.S_pp]
pp_unop [Cil_types_debug]
pp_variant [Printer_api.S_pp]
pp_variant [Cil_types_debug]
pp_varinfo [Printer_api.S_pp]
pp_varinfo [Cil_types_debug]
pp_varname [Printer_api.S_pp]
pp_warn_category [Log.Messages]
pp_with_col [Cil_datatype.Position]
ppc_32 [Machdeps]
ppcm [Integer]
ppcm v 0 == ppcm 0 v == 0.
pre_label [Logic_const]
pre_register [File]
Register some file as source file before command-line files
pre_state [Dataflows.Simple_forward]
pre_state [Dataflows.Simple_backward]
This function calls transfer_stmt on the result of post_state.
precondition [Ast_info]
Builds the precondition from b_assumes and b_requires clauses.
precondition_at_call [Statuses_by_call]
property_at_call kf p stmt returns the property corresponding to the status of the precondition p at the call stmt.
pred [Integer]
pred_of_id_pred [Logic_const]
extract a named predicate for an identified predicate.
predicate [Logic_typing.Make]
predicate [Db.Properties.Interp]
predicate_of_identified_predicate [Logic_utils]
prefix [Dotgraph.Node]
Set node prefix.
prefix [Cabs2cil]
Check that s starts with the prefix p.
prel [Logic_const]
Binary relation.
prepareCFG [Cfg]
This function converts all Break, Switch, Default and Continue Cil_types.stmtkinds and Cil_types.labels into Ifs and Gotos, giving the function body a very CFG-like character.
prepare_cil_file [File]
prepare_from_c_files [File]
Initialize the AST of the current project according to the current filename list.
prepare_tables [Logic_env]
Prepare all internal tables before their uses: clear all tables except builtins.
preprocess_extension [Logic_env]
preprocessor [Fc_config]
Name of the default command to call the preprocessor.
preprocessor_is_gnu_like [Fc_config]
whether the default preprocessor accepts the same options as gcc (i.e.
preprocessor_keep_comments [Fc_config]
true if the default preprocessor selected during compilation is able to keep comments (hence ACSL annotations) in its output.
preprocessor_supported_arch_options [Fc_config]
architecture-related options (e.g.
pretty [Tr_offset]
pretty [Task]
pretty [State_selection.S]
Display a selection.
pretty [Rich_text]
Pretty-print the message onto the given formatter, with the tags.
pretty [Property_status.Feedback]
pretty [Offsetmap_bitwise_sig]
pretty [Locations]
pretty [Lmap_sig]
pretty [Journal.Reverse_binding]
pretty [Interpreted_automata.UnrollUnnatural.G]
pretty [Integer]
pretty [Hptmap.Shape]
pretty [Fval.F]
pretty [Floating_point]
pretty [Float_sig.S]
pretty [Float_interval_sig.S]
pretty [Db.INOUTKF]
pretty [Db.Pdg]
For debugging...
pretty [Db.From]
pretty [Db.Value]
pretty [Datatype.Make_input]
pretty [Datatype.S_no_copy]
Pretty print each value in an user-friendly way.
pretty [Datatype.Undefined]
pretty [Datatype]
pretty [Dataflows.JOIN_SEMILATTICE]
Display the contents of an element of the lattice.
pretty [Dataflow2.BackwardsTransfer]
Pretty-print the state
pretty [Dataflow2.ForwardsTransfer]
Pretty-print the state.
pretty [Filepath.Normalized]
Pretty-print a path according to these rules: relative filenames are kept, except for leading './', which are stripped;, absolute filenames are relativized if their prefix is included in the current working directory; also, symbolic names are resolved, i.e. the result may be prefixed by known aliases (e.g. FRAMAC_SHARE). See Filepath.add_symbolic_dir for more details. Therefore, the result of this function may not designate a valid name in the filesystem and must ONLY be used to pretty-print information; it must NEVER to be converted back to a filepath later.
pretty [Filepath]
DEPRECATED: use Normalized.to_pretty_string instead.
pretty [Bottom]
pretty [Bitvector]
Bit vector, as blocs of 8-bits separated by space, first bits to last bits from left to right.
pretty [Abstract_interp.Rel]
pretty_addr [Base]
pretty_addr fmt base pretty-prints the name of base on fmt, with a leading ampersand if it is a variable
pretty_as_reason [Origin]
Pretty-print because of <origin> if the origin is not Unknown, or nothing otherwise
pretty_ast [File]
Print the project CIL file on the given Formatter.
pretty_bits [Bit_utils]
Pretty prints a range of bits in a type for the user.
pretty_code [Datatype.S_no_copy]
Pretty print each value in an ML-like style: the result must be a valid OCaml expression.
pretty_code [Datatype]
pretty_comp [Abstract_interp.Comp]
pretty_component [Wto.Make]
pretty_debug [Property]
Internal use only.
pretty_debug [Offsetmap_bitwise_sig]
pretty_debug [Map_lattice.MapSet_Lattice]
pretty_debug [Locations.Zone]
pretty_debug [Lmap_sig]
pretty_debug [Lmap_bitwise.Location_map_bitwise]
pretty_debug [Ival]
pretty_debug [Hptmap.V]
pretty_debug [Hptset.S]
pretty_diff [Lmap_sig]
pretty_edge [Interpreted_automata]
pretty_english [Locations]
pretty_filter [Lmap_sig]
pretty_filter m z pretties only the part of m that correspond to the bases present in z
pretty_generic [Offsetmap_sig]
pretty_generic [Offsetmap_bitwise_sig]
pretty_generic_printer [Lmap_bitwise.Location_map_bitwise]
pretty_key [Db.Pdg]
Pretty print information on a node key
pretty_kind [Fval]
pretty_line [Cil_datatype.Location]
Prints only the line of the location
pretty_long [Cil_datatype.Location]
Pretty the location under the form file <f>, line <l>, without the full-path to the file.
pretty_machdep [File]
Prints the associated machdep, or the current one in current project by default.
pretty_node [Db.Pdg]
Pretty print information on a node : with short=true, only the id of the node is printed..
pretty_normal [Fval.F]
pretty_normal [Floating_point]
pretty_parameter [Emitter.Usable_emitter]
Pretty print the parameter (given by its name) with its value.
pretty_partition [Wto.Make]
pretty_predicate_kind [Property]
pretty_sid [Cil_datatype.Stmt]
Pretty print the sid of the statement
pretty_state [Db.Value]
pretty_transition [Interpreted_automata]
pretty_typ [Offsetmap_lattice_with_isotropy]
pretty_typ [Int_Intervals_sig]
Pretty-printer that supposes the intervals are subranges of a C type, and use the type to print nice offsets
pretty_validity [Base]
pretty_witness [State_selection.S]
Display a selection in a more concise form.
prev_float [Fval.F]
First double strictly below the argument.
prev_float [Float_sig.S]
First value below the argument in the given precision.
prevent [Journal]
prevent f x applies x to f without printing anything in the journal, even if f is journalized.
printComments [Cprint]
printCounters [Cprint]
printFile [Cprint]
printLn [Cprint]
printLnComment [Cprint]
print_assigns [Logic_print]
print_attribute [Cprint]
print_attributes [Cprint]
print_block [Cprint]
print_code_annot [Logic_print]
print_constant [Logic_print]
print_decl [Logic_print]
print_decl [Cprint]
print_def [Cprint]
print_defs [Cprint]
print_delayed [Log]
Direct printing on output.
print_dot [Db.PostdominatorsTypes.Sig]
Print a representation of the postdominators in a dot file whose name is basename.function_name.dot.
print_enum_items [Cprint]
print_expression [Cprint]
print_expression_level [Cprint]
print_field [Cprint]
print_field_group [Cprint]
print_fields [Cprint]
print_file [Command]
Properly flush and close the channel and re-raise exceptions
print_global [Cil_printer]
Is the given global displayed by the pretty-printer.
print_help [Parameter_sig.S_no_parameter]
Print the help of the parameter in the given formatter as it would be printed on the command line by -<plugin>-help.
print_init_expression [Cprint]
print_init_name [Cprint]
print_init_name_group [Cprint]
print_lexpr [Logic_print]
print_logic_type [Logic_print]
First arguments prints the name of identifier declared with the corresponding type (None for pure type.
print_name [Cprint]
print_name_group [Cprint]
print_on_output [Log]
Direct printing on output.
print_onlytype [Cprint]
print_params [Cprint]
print_quantifiers [Logic_print]
print_single_name [Cprint]
print_spec [Logic_print]
print_specifiers [Cprint]
print_statement [Cprint]
print_struct_name_attr [Cprint]
print_type_annot [Logic_print]
print_type_spec [Cprint]
print_typedef [Logic_print]
print_variant [Logic_print]
printf [Log.Messages]
Outputs the formatted message on stdout.
printf [Dotgraph]
Low-level routine to directly write material in the dot file
println [Dotgraph]
Low-level routine to directly write material with an end-of-line ("\n") in the dot file
private_ops [State]
product [Extlib]
product f l1 l2 applies f to all the pairs of an elt of l1 and an element of l2.
product_fold [Extlib]
product f acc l1 l2 is similar to fold_left f acc l12 with l12 the list of all pairs of an elt of l1 and an elt of l2
progress [Task]
Make the thread progress and return true if still running
progress [Db]
This function should be called from time to time by all analysers taking time.
project [Lattice_type.Lattice_Base]
project [Kernel]
project [Int_Base]
project [Lattice_type.Lattice_Set]
project_float [Ival]
Should be used only when we know it is a float
project_float [Fval]
project_int [Ival]
project_int [Int_val]
Projects a singleton abstraction into an integer.
project_set [Int_Intervals_sig]
May raise Error_Top.
project_singleton [Int_Intervals_sig]
project_small_set [Ival]
project_small_set [Int_val]
property_kind_and_node [Description]
Returns separately the kind and the node of a property.
pseparated [Logic_const]
\separated
ptrue [Logic_const]
\true
push [History]
Add the element to the current history; clears the forward history, and push the old current element to the past history.
push [Dotgraph]
Register a continuation to be executed later.
pushGlobal [Cil]
CIL keeps the types at the beginning of the file and the variables at the end of the file.
push_attr_test [Cabshelper]
push_context [Lexerhack]
push_context [Clexer]
Start a context
pvalid [Logic_const]
\valid
pvalid_function [Logic_const]
\valid_function
pvalid_index [Logic_const]
\valid_index: requires index having integer type or set of integers
pvalid_range [Logic_const]
\valid_range: requires bounds having integer type
pvalid_read [Logic_const]
\valid_read
pxor [Logic_const]
^^

Q
quadruple [Datatype]
queue [Datatype]

R
raised [Task]
The task that immediately fails with an exception
range [Rich_text]
Sub-string with range.
range_covers_whole_type [Int_Intervals_sig]
Does the interval cover the entire range of bits that are valid for the given type.
range_loc [Cil]
Returns a location that ranges over the two locations in arguments.
range_selector [Gtk_helper]
rank [Dotgraph]
Layout nodes at the same rank
rank [Cil]
Returns a unique number representing the integer conversion rank.
rawfile [Markdown]
Get the content of a file as raw markdown.
reachable_stmts [Stmts_graph]
reachable_stmts kf stmt returns the transitive closure of the successors of stmt in kf.
reactive_buffer [Design]
This function creates a reactive buffer for the given list of globals.
read16s [Unmarshal]
read16u [Unmarshal]
read32s [Unmarshal]
read32u [Unmarshal]
read64s [Unmarshal]
read64u [Unmarshal]
read8s [Unmarshal]
read8u [Unmarshal]
read_file [Command]
Properly close the channel and re-raise exceptions
read_lines [Command]
Iter over all text lines in the file
readblock [Unmarshal]
readblock_rev [Unmarshal]
real [Utf8_logic]
record [Dotgraph.Node]
record [Dotgraph]
Define the node to be a record
recursive_pack [Structural_descr]
Pack a recursive descriptor.
redirect [Gtk_helper]
Redirect the given formatter to the given buffer
reduce_bit [Int_interval]
reduce_by_cond [Db.Value]
reduce_multichar [Cil]
gives the value of a wide char literal.
reduce_sign [Int_interval]
refresh [Visitor_behavior]
Makes fresh copies of the mutable structures and provides fresh id for the structures that have ids.
refresh [Gtk_form]
refresh_code_annotation [Logic_const]
set a fresh id to an existing code annotation
refresh_gui [Gtk_helper]
Process some pending events in the main Glib loop.
refresh_identified_term [Logic_const]
Gives a new id to an existing term.
refresh_local_name [Cil]
if needed, rename the given varinfo so that its vname does not clash with the one of a local or formal variable of the given function.
refresh_predicate [Logic_const]
Gives a new id to an existing predicate.
refresh_spec [Logic_const]
set fresh id to properties of an existing funspec
register [Type]
register ?closure ~name ~ml_name descr reprs registers a new type value.
register [Property_status]
Register the given property.
register [Log.Messages]
Local registry for listeners.
register [Lattice_messages]
Register a new emitter for a message.
register [Journal]
register name ty ~comment ~is_dyn v journalizes the value v of type ty with the name name.
register [Gtk_helper.Icon]
register ~name ~file registers the kind Custom name associated to the filename file.
register [Gtk_form]
register [Globals.Functions]
register [Dynamic]
register ~plugin name ty v registers v with the name name, the type ty and the plug-in plugin.
register [Db]
Plugins must register values with this function.
register [Alarms]
Register the given alarm on the given statement.
registerAlphaName [Alpha]
Register a name with an alpha conversion table to ensure that when later we call newAlphaName we do not end up generating this one
registerAttribute [Cil]
Add a new attribute with a specified class
register_after_global_load_hook [Project]
register_after_load_hook f adds a hook called just after loading *all projects**.
register_after_load_hook [Project]
register_after_load_hook f adds a hook called just after loading *each project**: if n projects are on disk, the same hook will be called n times (one call by project).
register_after_set_current_hook [Project]
register_after_set_current_hook f adds a hook on function Project.set_current.
register_allocated_var [Base]
Allocated variables are variables not present in the source of the program, but instead created through dynamic allocation.
register_before_load_hook [Project]
register_before_load_hook f adds a hook called just before loading *each project** (more precisely, the project exists and but is empty while the hook is applied): if n projects are on disk, the same hook will be called n times (one call by project).
register_before_remove_hook [Project]
register_before_remove_hook f adds a hook called just before removing a project.
register_behavior [Acsl_extension]
register_behavior name ~preprocessor typer ~visitor ~printer ~short_printer status registers new ACSL extension to be used in function contracts with name name.
register_behavior_extension [Logic_typing]
register_behavior_extension name status f registers a typing function f to be used to type function contract clause with name name.
register_behavior_extension [Cil_printer]
register_behavior_extension [Cil]
Indicates how an extended behavior clause is supposed to be visited.
register_builtin [Db.Value]
!register_builtin name ?replace ?typ f registers an abstract function f to use everytime a C function named name of type typ is called in the program.
register_category [Log.Messages]
register a new debugging/verbose category.
register_code_annot [Acsl_extension]
Registers extension for code annotation to be evaluated at _current_ program point.
register_code_annot_extension [Logic_typing]
register an extension for code annotation to be evaluated at _current_ program point.
register_code_annot_extension [Cil_printer]
register_code_annot_next_both [Acsl_extension]
Registers extension both for code and loop annotations.
register_code_annot_next_both_extension [Logic_typing]
register an extension both for code and loop annotations.
register_code_annot_next_loop [Acsl_extension]
Registers extension for loop annotation.
register_code_annot_next_loop_extension [Logic_typing]
register an extension for loop annotation.
register_code_annot_next_stmt [Acsl_extension]
Registers extension for code annotation to be evaluated for the _next_ statement.
register_code_annot_next_stmt_extension [Logic_typing]
register an extension for code annotation to be evaluated for the _next_ statement.
register_code_transformation_category [File]
Adds a new category of code transformation
register_compute [Db]
register_conditional_side_effect_hook [Cabs2cil]
new hook called when an expression with side-effect is evaluated conditionally (RHS of && or ||, 2nd and 3rd term of ?:).
register_create_hook [Project]
register_create_hook f adds a hook on function create: each time a new project p is created, f p is applied.
register_custom [Unmarshal]
register_different_decl_hook [Cabs2cil]
new hook called when a definition has a compatible but not strictly identical prototype than its declaration The hook takes as argument the old and new varinfo.
register_extension [Design]
Register an extension to the main GUI.
register_for_loop_all_hook [Cabs2cil]
new hook that will be called when processing a for loop.
register_for_loop_body_hook [Cabs2cil]
new hook that will called when processing a for loop.
register_for_loop_incr_hook [Cabs2cil]
new hook that will be called when processing a for loop.
register_for_loop_init_hook [Cabs2cil]
new hook that will be called when processing a for loop.
register_for_loop_test_hook [Cabs2cil]
new hook that will be called when processing a for loop.
register_global [Acsl_extension]
Registers extension for global annotation.
register_global_extension [Logic_typing]
register an extension for global annotation.
register_global_extension [Cil_printer]
register_guarded_compute [Db]
register_ignore_pure_exp_hook [Cabs2cil]
register_ignore_side_effect_hook [Cabs2cil]
new hook called when side-effects are dropped.
register_implicit_prototype_hook [Cabs2cil]
new hook called when an implicit prototype is generated.
register_incompatible_decl_hook [Cabs2cil]
new hook called when two conflicting declarations are found.
register_key [Hook.S_ordered]
register_local_func_hook [Cabs2cil]
new hook called when encountering a definition of a local function.
register_locking_machinery [Gtk_helper]
Add hooks to the locking mechanism of the GUI.
register_loop_annot_extension [Cil_printer]
register_memory_var [Base]
Memory variables are variables not present in the source of the program.
register_new_global_hook [Cabs2cil]
Hook called when a new global is created.
register_property_add_hook [Property_status]
add an hook that will be called for any newly registered property
register_property_remove_hook [Property_status]
Add and hook that will be called each time a property is removed.
register_reset_extension [Design]
Register a function to be called whenever the main GUI reset method is called.
register_shallow_attribute [Cil_printer]
Register an attribute that will never be pretty printed.
register_stmt [Kernel_function]
Register a new statement in a kernel function, with the list of blocks that contain the statement (innermost first).
register_tag_handlers [Log.Messages]
register_todo_after_clear [Project]
Register an action performed just after clearing a project.
register_todo_before_clear [Project]
Register an action performed just before clearing a project.
register_warn_category [Log.Messages]
registered_builtins [Db.Value]
Returns a list of the pairs (name, builtin) registered via register_builtin.
rehash [Datatype.Make_input]
How to rehashconsed values.
rehash [Datatype.Undefined]
reinterpret_as_float [Ival]
Bitwise reinterpretation of the given value as a float of the given kind.
reinterpret_as_int [Ival]
Bitwise reinterpretation of the given value, of size size, as an integer of the given signedness (and size).
relativize [Filepath]
relativize base_name file_name returns a relative path name of file_name w.r.t.
remove [State_builder.Weak_hashtbl]
remove x removes from the table one instance of x.
remove [Rangemap.S]
remove x m returns a map containing the same bindings as m, except for x which is unbound in the returned map.
remove [Qstack.Make]
Remove an element from the stack.
remove [Property_status]
Remove the property deeply.
remove [Project]
Default project is current ().
remove [Int_set]
Removes an integer from a set.
remove [Indexer.Make]
Log complexity.
remove [Hptset.S_Basic_Compare]
remove [Hptmap_sig.S]
remove k m returns the map m deprived from any binding involving k.
remove [Globals.Functions]
Removes the given varinfo, which must have already been removed from the AST.
remove [Globals.Vars]
Removes the given varinfo, which must have already been removed from the AST.
remove [Emitter.Make_table]
remove [Dynamic.Parameter.StringList]
remove [Dynamic.Parameter.StringSet]
remove [State_builder.Set_ref]
remove [State_builder.Hashtbl]
remove [Alarms]
Remove the alarms and the associated annotations emitted by the given emitter.
removeAttribute [Cil]
Remove an attribute previously registered.
removeFormalsDecl [Cil]
remove a binding from the table.
removeOffset [Cil]
Remove ONE offset from the end of an offset sequence.
removeOffsetLval [Cil]
Remove ONE offset from the end of an lvalue.
removeUnused [Rmtmps]
remove_allocates [Annotations]
Remove the corresponding allocation clause.
remove_assigns [Annotations]
Remove the corresponding assigns clause.
remove_assumes [Annotations]
Remove an assumes clause from the spec of the given function.
remove_base [Lmap_sig]
Removes the base if it is present.
remove_base [Lmap_bitwise.Location_map_bitwise]
remove_behavior [Annotations]
Remove a behavior attached to a function.
remove_behavior_components [Annotations]
remove all the component of a behavior, but keeps the name (so as to avoid issues with disjoint/complete clauses).
remove_code_annot [Annotations]
Remove a code annotation attached to a statement.
remove_codependencies [State_dependency_graph.S]
Remove an edge in graph from each state of the list to the state onto.
remove_complete [Annotations]
Remove a complete behaviors clause attached to a function.
remove_decreases [Annotations]
Remove the decreases clause attached to a function.
remove_dependencies [State_dependency_graph.S]
Remove an edge in graph from the given state to each state of the list.
remove_disjoint [Annotations]
Remove a disjoint behaviors clause attached to a function.
remove_ensures [Annotations]
Remove a post-condition from the spec of the given function.
remove_escaping_locals [Locations.Location_Bytes]
remove_escaping_locals is_local v removes from v the information associated with bases for which is_local returns true.
remove_exn [Exn_flow]
transforms functions that may throw into functions returning a union type composed of the normal return or one of the exceptions.
remove_extended [Annotations]
remove_global [Annotations]
Remove a global annotation.
remove_global_annotations [Globals.FileIndex]
remove_logic_coerce [Logic_utils]
Removes TLogic_coerce at head of term.
remove_logic_ctor [Logic_env]
removes the given logic constructor.
remove_logic_function [Logic_env]
removes all overloaded bindings to a given symbol.
remove_logic_info_gen [Logic_env]
remove_logic_info_gen is_same_profile li removes a specific logic info among all the overloaded ones.
remove_logic_type [Logic_env]
remove_logic_type s removes the definition of logic type s.
remove_model_field [Logic_env]
remove_requires [Annotations]
Remove a requires clause from the spec of the given function.
remove_tag [Gtk_helper]
remove_term_offset [Logic_utils]
remove_term_offset o returns o without its last offset and this last offset.
remove_terminates [Annotations]
Remove the terminates clause attached to a function.
remove_typename [Logic_env]
removes latest typename status associated to a given identifier
remove_unused_labels [Rmtmps]
removes unused labels for which is_removable is true.
remove_variables [Lmap_sig]
remove_whole [Rangemap.Make]
reorder_ast [File]
reorder globals so that all uses of an identifier are preceded by its declaration.
reorder_custom_ast [File]
replace [Hptmap_sig.S]
replace f k m returns a map whose bindings are all bindings in m, except for the key k which is: removed from the map if f o = None, bound to v' if f o = Some v' where o is (Some v) if k is bound to v in m, or None if k is not bound in m.
replace [Extlib]
replace cmp x l replaces the first element y of l such that cmp x y is true by x.
replace [Dataflow2.StmtStartData]
replace [State_builder.Hashtbl]
Add a new binding.
replace_by_declaration [Globals.Functions]
Note: if the varinfo is already registered and bound to a definition, the definition will be erased only if vdefined is false.
replace_by_definition [Globals.Functions]
TODO: do not take a funspec as argument
replace_call_precondition [Statuses_by_call]
replace_for_call pre stmt pre_at_call states that pre_at_call is the property corresponding to the status of pre at call stmt.
reprs [Type.Polymorphic4_input]
reprs [Type.Polymorphic3_input]
reprs [Type.Polymorphic2_input]
reprs [Type.Polymorphic_input]
How to make the representant of each monomorphic instance of the polymorphic type value from an underlying representant.
reprs [Type]
Not usable in the "no-obj" mode
reprs [Datatype.Make_input]
Must be non-empty.
reprs [Datatype.S_no_copy]
List of representants of the descriptor.
res_call_visible [Filter.RemoveInfo]
tells if the lvalue of the call has to be visible
reset [Gtk_helper.Configuration]
reset_once_flag [Messages]
Reset the once flag of pretty-printers.
reset_typenames [Logic_env]
erases all the typename status
resize [Vector]
Low-level interface.
resize [Bitvector]
A copy of the bitvector up-to or down-to n bits.
restore [Project.Undo]
restore [Journal]
Restore a previously saved journal.
result [Log.Messages]
Results of analysis.
result_visible [Filter.RemoveInfo]
tells if the function returns something or if the result is void.
return [Task]
The task that immediately returns a result
return [Descr]
Similar to Unmarshal.Return, but safe.
return [Command]
returns_void [Kernel_function]
rmUnusedInlines [Rmtmps]
rmUnusedStatic [Rmtmps]
rm_asserts [Db.Value]
round_down_to_r [Integer]
round_down_to_r m r modu is the largest number n such that n<=m and n = r modulo modu
round_to_precision [Float_sig.S]
Rounds a number to a given precision.
round_to_single_precision_float [Fval]
round_to_single_precision_float [Floating_point]
round_up_to_r [Integer]
round_up_to_r m r modu is the smallest number n such that n>=m and n = r modulo modu
rt_type_mode [Logic_utils]
run [Task]
Runs one single task in the background.
run [Dotgraph]
Flushes all pending continuations.
run [Db.Toplevel]
Run a Frama-C toplevel playing the game given in argument (in particular, applying the argument runs the analyses).
run_after_configuring_stage [Cmdline]
Register an action to be executed at the end of the configuring stage.
run_after_early_stage [Cmdline]
Register an action to be executed at the end of the early stage.
run_after_exiting_stage [Cmdline]
Register an action to be executed at the end of the exiting stage.
run_after_extended_stage [Cmdline]
Register an action to be executed at the end of the extended stage.
run_after_loading_stage [Cmdline]
Register an action to be executed at the end of the loading stage.
run_after_setting_files [Cmdline]
Register an action to be executed just after setting the files put on the command line.
run_ai_analysis [Db.Security]
Only run the analysis by abstract interpretation.
run_during_extending_stage [Cmdline]
Register an action to be executed during the extending stage.
run_slicing_analysis [Db.Security]
Only run the security slicing pre-analysis.
run_whole_analysis [Db.Security]
Run all the security analysis.

S
safe_at_exit [Extlib]
Register function to call with Pervasives.at_exit, but only for non-child process (fork).
safe_remove [Extlib]
Tries to delete a file and never fails.
safe_remove_dir [Extlib]
save [Project]
Save a given project in a file.
save [Journal]
Save the current state of the journal for future restoration.
save [Gtk_helper.Configuration]
saveConfiguration [Cilconfig]
Save the configuration in a file.
save_all [Project]
Save all the projects in a file.
save_buffer [Json]
save_channel [Json]
save_file [Json]
save_formatter [Json]
save_paned_ratio [Gtk_helper]
Saves the current ratio of the panel associated to the given key.
save_string [Json]
saveload [Kernel]
scalar_term_to_boolean [Logic_utils]
Compare the given term with the constant 0 (of the appropriate type) to return the result of the comparison e <> 0 as a boolean term.
scalar_term_to_predicate [Logic_utils]
Compare the given term with the constant 0 (of the appropriate type) to return the result of the comparison e <> 0.
scale [Ival]
scale f v returns the interval of elements x * f for x in v.
scale [Int_val]
scale f v returns an abstraction of the integers f * x for all x in v.
scale [Int_set]
scale [Int_interval]
scale_div [Ival]
scale_div ~pos:false f v is an over-approximation of the set of elements x c_div f for x in v.
scale_div [Int_val]
scale_div f v is an over-approximation of the elements x / f for all elements x in v.
scale_div [Int_set]
scale_div [Int_interval]
scale_div_under [Ival]
scale_div_under ~pos:false f v is an under-approximation of the set of elements x c_div f for x in v.
scale_div_under [Int_val]
Under-approximation of the division.
scale_div_under [Int_interval]
scale_int_base [Ival]
scale_rem [Ival]
scale_rem ~pos:false f v is an over-approximation of the set of elements x c_rem f for x in v.
scale_rem [Int_val]
Over-approximation of the remainder of the division.
scale_rem [Int_set]
scale_rem [Int_interval]
scharPtrType [Cil]
scharType [Cil]
scheduled [Task]
Number of scheduled process
scroll [Wbox]
default policy is AUTOMATIC
section [Markdown]
Adds a H1 header with the given title on top of the given elements.
select_file [Source_manager]
Selection by page filename
select_file [Gtk_helper]
Launches a standard gtk file chooser window and returns the name of the selected file.
select_name [Source_manager]
Selection by page title
selected_localizable [History]
selected_localizable () returns the localizable currently selected, or None if nothing or an entire global is selected.
selection_locked [Source_manager]
Prevents the filetree callback from resetting the selected line when it was selected via a click in the original source viewer.
self [State_builder.Hashcons]
self [State_builder.Counter]
self [State_builder.Queue]
self [State_builder.S]
The kind of the registered state.
self [Property_status]
The state which stores the computed status.
self [Property.Names]
self [Property.LegacyNames]
self [Messages]
Internal state of stored messages
self [Logic_env.Logic_builtin_used]
self [Kernel_function]
self [Hptset.Make]
self [Hptmap_sig.S]
self [Globals.Syntactic_search]
self [Globals.FileIndex]
The state kind corresponding to the table of global C symbols.
self [Globals.Functions]
self [Globals.Vars]
self [Emitter.Make_table]
self [Emitter]
self [Db.Pdg]
self [Db.Security]
self [Db.RteGen]
self [Db.From]
self [Db.Value]
Internal state of the value analysis from projects viewpoint.
self [Cil_datatype.Varinfo.Hptset]
self [Cil_datatype.Stmt.Hptset]
self [Cabshelper.Comments]
self [Ast.UntypedFiles]
self [Ast]
The state kind associated to the cil AST.
self [Alarms]
selfFormalsDecl [Cil]
state of the table associating formals to each prototype.
selfMachine [Cil]
selfMachine_is_computed [Cil]
whether current project has set its machine description.
self_external [Db.INOUTKF]
self_internal [Db.INOUTKF]
self_with_formals [Db.Inputs]
sentinel [Binary_cache.Result]
sentinel [Binary_cache.Cacheable]
separateStorageModifiers [Cil]
Separate out the storage-modifier name attributes
separate_if_succs [Cil]
Provided s is a if, separate_if_succs s splits the successors of s according to the truth value of the condition.
separate_switch_succs [Cil]
Provided s is a switch, separate_switch_succs s returns the subset of s.succs that correspond to the Case labels of s, and a "default statement" that either corresponds to the Default label, or to the syntactic successor of s if there is no default label.
seq [Kernel]
sequence [Task]
sequence t k first runs t.
server [Task]
Creates a server of commands.
set [Vector]
Raise Not_found if out-of-bounds.
set [State_builder.Array]
set [State.Local]
How to change the current state.
set [Parameter_sig.Specific_dir]
Sets the plugin <specific-dir> directory (without creating it).
set [Parameter_sig.S_no_parameter]
Set the option.
set [Gtk_helper.Configuration]
Set a configuration element, with a key.
set [Dynamic.Parameter.Common]
set [State_builder.Ref]
Change the referenced value.
set [Bitvector]
set [Ast.UntypedFiles]
Should not be used by casual users.
setConfiguration [Cilconfig]
Set a configuration element, with a key.
setCurrentFile [Errorloc]
setCurrentLine [Errorloc]
setCurrentWorkingDirectory [Errorloc]
This function is used especially when the preprocessor has generated linemarkers in the output that let us know the current working directory at the time of preprocessing (option -fworking-directory for GNU CPP).
setDoAlternateConditional [Cabs2cil]
If called, sets a flag so that translation of conditionals does not result in forward ingoing gotos (from the if-branch to the else-branch).
setDoTransformWhile [Cabs2cil]
If called, sets a flag so that continue in while loops get transformed into forward gotos, like it is already done in do-while and for loops.
setFormals [Cil]
Update the formals of a fundec and make sure that the function type has the same information.
setFormalsDecl [Cil]
Update the formals of a function declaration from its identifier and its type.
setFunctionType [Cil]
Set the types of arguments and results as given by the function type passed as the second argument.
setFunctionTypeMakeFormals [Cil]
Set the type of the function and make formal arguments for them
setMSVCMode [Frontc]
setMaxId [Cil]
Update the smaxid after you have populated with locals and formals (unless you constructed those using Cil.makeLocalVar or Cil.makeTempVar.
setReturnType [Cil]
setReturnTypeVI [Cil]
Change the return type of the function passed as 1st argument to be the type passed as 2nd argument.
setTypeAttrs [Cil]
Sets the attributes of the type to the given list.
set_bold_font [Wutil]
set_bold_font [Gtk_compat.Pango]
makes the font bold.
set_bool [Gtk_helper.Configuration]
Sets a ConfigBool
set_cmdline_stage [Parameter_customize]
Set the stage where the option corresponding to the parameter is recognized.
set_conversion [Logic_const]
set_conversion ty1 ty2 returns a set type as soon as ty1 and/or ty2 is a set.
set_current [Project]
Set the current project with the given one.
set_default [Parameter_sig.Collection_category]
Modify the '@default' category.
set_default_initialization [Ast]
set_echo [Log]
Turns echo on or off.
set_enabled [Wutil]
set_entry_point [Globals]
set_entry_point name lib sets Kernel.MainFunction to name and Kernel.LibEntry to lib.
set_extension_handler [Logic_typing]
Used to setup references related to the handling of ACSL extensions.
set_extension_handler [Logic_env]
Used to setup references related to the handling of ACSL extensions.
set_file [Ast]
set_float [Gtk_helper.Configuration]
Sets a ConfigFloat
set_font [Wutil]
set_forward [History]
Replaces the forward history with the given elements.
set_group [Parameter_customize]
Affect a group to the parameter.
set_initial_location [Logic_lexer]
set_int [Gtk_helper.Configuration]
Sets a ConfigInt
set_keep_current [Project]
set_keep_current b keeps the current project forever (even after the end of the current Project.on) iff b is true.
set_length [State_builder.Array]
set_list [Gtk_helper.Configuration]
set_ml_name [Type]
set_module_load_path [Dynamic]
Sets the load path for modules in FRAMAC_PLUGIN, prepending it with path.
set_monospace [Wutil]
set_name [Type]
set_name [State]
Set the name of the given state.
set_name [Project_skeleton.Make_setter]
set_name [Project]
Set the name of the given project.
set_name [Journal]
set_name name changes the filename into the journal is generated.
set_negative_option_help [Parameter_customize]
For boolean parameters, set the help message of the negative option generating automatically.
set_negative_option_name [Parameter_customize]
For boolean parameters, set the name of the negative option generating automatically from the positive one (the given option name).
set_optional_help [Parameter_customize]
Concatenate an additional description just after the default one.
set_output [Log]
This function has the same parameters as Format.make_formatter.
set_output_dependencies [Parameter_sig.With_output]
Set the dependencies for the output of the option.
set_pane_ratio [Wutil]
set_possible_values [Parameter_sig.String]
Set what are the acceptable values for this parameter.
set_printer [Printer_api.S]
Set the current pretty-printer, typically to a printer previously obtained through Printer_api.S.current_printer.
set_procs [Task]
Adjusts the maximum number of running process.
set_range [Parameter_sig.Int]
Set what is the possible range of values for this parameter.
set_range [Bitvector]
set_round_downward [Floating_point]
set_round_nearest_even [Floating_point]
set_round_toward_zero [Floating_point]
set_round_upward [Floating_point]
set_rounding_mode [Floating_point]
set_small_cardinal [Int_set]
Sets the limit above which integer sets are converted into intervals.
set_small_font [Wutil]
set_small_font [Gtk_compat.Pango]
makes the font smaller.
set_tooltip [Wutil]
set_unset_option_help [Parameter_customize]
For string collection parameters, gives the help message for the corresponding unset option.
set_unset_option_name [Parameter_customize]
For string collection parameters, set the name of an option that will remove elements from the set.
set_vid [Cil_const]
set the vid to a fresh number.
set_visible [Wutil]
set_warn_status [Log.Messages]
setup_all_preconditions_proxies [Statuses_by_call]
setup_all_preconditions_proxies kf is equivalent to calling setup_precondition_proxy on all the requires of kf.
setup_precondition_proxy [Statuses_by_call]
setup_precondition_proxy kf p creates a new property for p at each syntactic call site of kf, representing the status of p at this particular call.
sfprintf [Pretty_utils]
Equivalent to Format.asprintf.
shape [Locations.Zone]
Misc
shape [Locations.Location_Bytes.M]
shape [Lmap_sig]
Shape of the map.
shape [Lmap_bitwise.Location_map_bitwise]
shape [Hptmap_sig.S]
Export the map as a value suitable for functions Hptmap_sig.S.inter_with_shape and Hptmap_sig.S.from_shape
shape [Hptset.S]
Export the shape of the set.
share [Wutil]
share [Task]
New instance of shared task.
shared [Task]
Build a shareable task.
shared_icon [Widget]
shift [Locations.Location_Bytes]
shift_bits [Offsetmap_lattice_with_isotropy]
Left-shift the given value, of size size, by offset bits.
shift_left [Ival]
shift_left [Integer]
shift_left [Int_val]
shift_right [Ival]
shift_right [Integer]
shift_right [Int_val]
shift_right_logical [Integer]
shift_under [Locations.Location_Bytes]
Over- and under-approximation of shifting the value by the given Ival.
short_pretty [Property]
output a meaningful name for the property (e.g.
show [Launcher]
Display the Frama-C launcher.
show_current [History]
Redisplay the current history point, if available.
shrink [Vector]
Low-level interface.
shrink [Rich_text]
Resize the buffer to roughly fit its actual content.
sidebar [Wbox]
The first list is packed to the top of the sidebar.
signof_typeof_lval [Bit_utils]
sin [Float_sig.S]
sin [Float_interval_sig.S]
sinf [Floating_point]
single_interval_value [Offsetmap_sig]
single_interval_value o returns Some v if o contains a single interval, to which v is bound, and None otherwise.
single_interval_value [Offsetmap_bitwise_sig]
single_interval_value o returns Some v if o contains a single interval, to which v is bound, and None otherwise.
singleton [State_selection]
The selection containing only the given state.
singleton [Rangemap.S]
singleton x y returns the one-element map that contains a binding y for x.
singleton [Qstack.Make]
Create a new qstack with a single element.
singleton [Hptset.S_Basic_Compare]
singleton [Hptmap_sig.S]
singleton k d returns a map whose only binding is from k to d.
singleton [Float_interval_sig.S]
singleton f creates the singleton interval f, without NaN.
singleton [Bag]
singleton_one [Locations.Location_Bytes]
the set containing only the value 1
singleton_zero [Locations.Location_Bytes]
the set containing only the value for to the C expression 0
sixteen [Integer]
size [Vector]
Same as length
size [Task]
Auto-flush.
size [State_builder.Info_with_size]
Initial size for the hash table.
size [Rich_text]
size [Indexer.Make]
Number of elements in the collection.
sizeOf [Cil]
The size of a type, in bytes.
size_from_validity [Offsetmap_sig]
size_from_validity v returns the size to be used when creating a new offsetmap for a base with validity v.
size_from_validity [Offsetmap_bitwise_sig]
size_from_validity v returns the size to be used when creating a new offsetmap for a base with validity v.
sizeof [Bit_utils]
sizeof ty is the size of ty in bits.
sizeof_lval [Bit_utils]
sizeof_pointed [Bit_utils]
sizeof_pointed_lval [Bit_utils]
sizeof_vid [Bit_utils]
sizeofchar [Bit_utils]
sizeof(char) in bits
sizeofpointer [Bit_utils]
sizeof(char* ) in bits
sleep [Db]
Pauses the currently running process for the specified time, in milliseconds.
snd [Lattice_type.Lattice_Product]
sort [Bag]
The returned list preserves duplicates and order of equals elements.
sort_unique [Extlib]
Same as List.sort , but also remove duplicates.
source [Property]
returns the location of the property, if not unknown.
source [Log]
source_files_chooser [Gtk_helper]
Open a dialog box for choosing C source files and performing an action on them.
spawn [Task]
Schedules a task on the server.
spawn_command [Gtk_helper]
Launches the given command and calls the given function when the process terminates.
spec [Logic_parser]
spec [Logic_lexer]
spinner [Gtk_form]
split [Wbox]
split [Map_lattice.MapSet_Lattice]
split key t is equivalent to find key t, add key bottom t.
split [Locations.Location_Bytes]
splitArrayAttributes [Cil]
given some attributes on an array type, split them into those that belong to the type of the elements of the array (currently, qualifiers such as const and volatile), and those that must remain on the array, in that order
splitFunctionType [Cil]
Given a function type split it into return type, arguments, is_vararg and attributes.
splitFunctionTypeVI [Cil]
split_category [Log]
Split a category specification into its constituants.
sqrt [Float_sig.S]
sqrt [Float_interval_sig.S]
sqrtf [Floating_point]
stag_of_string [Transitioning.Format]
startParsing [Errorloc]
Call this function to start parsing.
startsWith [Cil]
sm: return true if the first is a prefix of the second string
state [Cil_printer]
state_stack [Logic_lexer]
statement [Db.INOUT]
status [Task]
The task that immediately finishes with provided status
status_feedback [Description]
User-friendly description of property statuses.
stmt [Visitor_behavior.Fold]
stmt [Visitor_behavior.Iter]
stmt [Visitor_behavior.Unset]
stmt [Visitor_behavior.Set]
stmt [Visitor_behavior.Get]
stmt [Visitor_behavior.Reset]
stmtFallsThrough [Cabs2cil]
returns true if the given statement can fall through the next syntactical one.
stmt_can_reach [Stmts_graph]
stmt_can_reach kf s1 s2 is true iff the control flow can reach s2 starting at s1 in function kf.
stmt_can_reach_filtered [Stmts_graph]
Just like stmt_can_reach but uses a function to filter the nodes of the graph it operates on.
stmt_in_loop [Kernel_function]
stmt_in_loop kf stmt is true iff stmt strictly occurs in a loop of kf.
stmt_is_in_cycle [Stmts_graph]
stmt_is_in_cycle s is true iff s is reachable through a non trivial path starting at s.
stmt_is_in_cycle_filtered [Stmts_graph]
Just like stmt_is_in_cycle but uses a function to filter the nodes of the graph it operates on.
stmt_of_instr_list [Cil]
if the list has 2 elements or more, it will return a block with bscoping=false
stmt_postdominators [Db.PostdominatorsTypes.Sig]
stmt_start [Pretty_source]
Offset at which the current statement starts in the buffer corresponding to state, _without_ ACSL assertions/contracts, etc.
str [Descr]
string [Rich_text]
string [Json]
Convert Null, Int, Float, Number and String to a string.
string [Datatype]
string_del_prefix [Extlib]
string_del_prefix ~strict p s returns None if p is not a prefix of s and Some s1 iff s=p^s1.
string_del_suffix [Extlib]
string_del_suffix ~strict suf s returns Some s1 when s = s1 ^ suf and None of suf is not a suffix of s.
string_of_c_rounding_mode [Floating_point]
string_of_stag [Transitioning.Format]
string_prefix [Extlib]
string_prefix ~strict p s returns true if and only if p is a prefix of the string s.
string_selector [Gtk_helper]
string_split [Extlib]
string_split s i returns the beginning of s up to char i-1 and the end of s starting from char i+1
string_suffix [Extlib]
string_suffix ~strict suf s returns true iff suf is a suffix of string s.
stripCasts [Cil]
Removes casts from this expression, but ignores casts within other expression constructs.
stripCastsAndInfo [Cil]
Removes casts and info wrappers and return underlying expression
stripCastsButLastInfo [Cil]
Removes casts and info wrappers,except last info wrapper, and return underlying expression
stripInfo [Cil]
Removes info wrappers and return underlying expression
stripTermCasts [Cil]
Equivalent to stripCasts for terms.
strip_underscore [Extlib]
remove underscores at the beginning and end of a string.
structural_descr [Type.Polymorphic4_input]
structural_descr [Type.Polymorphic3_input]
structural_descr [Type.Polymorphic2_input]
structural_descr [Type.Polymorphic_input]
How to build the structural descriptor for each monomorphic instance.
structural_descr [Type]
structural_descr [Datatype.Hashtbl_with_descr]
structural_descr [Datatype.Make_input]
structural_descr [Datatype.Undefined]
sub [Rich_text]
Similar to Buffer.sub
sub [Integer]
sub [Float_sig.S]
sub [Float_interval_sig.S]
sub [Abstract_interp.Rel]
sub_abs [Abstract_interp.Rel]
sub_int [Ival]
sub_int_under [Ival]
sub_pointer [Locations.Location_Bytes]
Subtracts the offsets of two locations.
sub_pointwise [Locations.Location_Bytes]
Subtracts the offsets of two locations loc1 and loc2.
subdiv_float_interval [Fval]
Raise Can_not_subdiv if it can't be subdivided
subdivide [Ival]
Subdivisions into two intervals
subdivide [Int_val]
Splits an abstraction into two abstractions.
subdivide [Int_set]
subdivide [Int_interval]
subdivide [Float_interval_sig.S]
Subdivides an interval of a given precision into two intervals.
subgraph [Dotgraph]
The continuation shall add the graph content in the dot file.
subsections [Markdown]
subsections header body returns a list of elements where the body's headers have been increased by one (i.e.
subset [Hptset.S_Basic_Compare]
subsets [Extlib]
subsets k l computes the combinations of k elements from list l.
substring [Rich_text]
succ [Transitioning.Stdlib]
succ [Integer]
swap [Extlib]
Swap arguments.
sym [Abstract_interp.Comp]
Opposite relation: a op b <==> b (sym op) a.
symmetric_binary_predicate [Hptmap_sig.S]
Same as binary_predicate, but for a symmetric relation.
sync [Task]
Schedules a task such that only one can run simultaneously for a given mutex.
sys_single_precision_of_string [Floating_point]

T
t_abstract [Structural_descr]
t_array [Unmarshal]
t_array [Structural_descr]
t_bool [Unmarshal]
t_bool [Structural_descr]
t_bool [Descr]
t_float [Unmarshal]
t_float [Structural_descr]
t_float [Descr]
t_hashtbl_changedhashs [Unmarshal]
t_hashtbl_unchanged_hashs [Structural_descr]
t_hashtbl_unchangedhashs [Unmarshal]
t_int [Unmarshal]
t_int [Structural_descr]
t_int [Descr]
t_int32 [Unmarshal]
t_int32 [Structural_descr]
t_int32 [Descr]
t_int64 [Unmarshal]
t_int64 [Structural_descr]
t_int64 [Descr]
t_list [Unmarshal]
t_list [Structural_descr]
t_list [Descr]
Type descriptor for lists.
t_map_unchanged_compares [Structural_descr]
t_map_unchangedcompares [Unmarshal]
t_nativeint [Unmarshal]
t_nativeint [Structural_descr]
t_nativeint [Descr]
t_option [Unmarshal]
t_option [Structural_descr]
t_option [Descr]
Type descriptor for options.
t_pair [Descr]
Type descriptor for pairs (2-tuples).
t_queue [Unmarshal]
t_queue [Structural_descr]
t_queue [Descr]
Type descriptor for queues.
t_record [Unmarshal]
t_record [Structural_descr]
t_record [Descr]
Type descriptor for records (the length of the array must be equal to the number of fields in the record).
t_ref [Unmarshal]
t_ref [Structural_descr]
t_ref [Descr]
Type descriptor for references.
t_ref [Datatype]
t_set_unchanged_compares [Structural_descr]
t_set_unchangedcompares [Unmarshal]
t_string [Unmarshal]
t_string [Structural_descr]
t_string [Descr]
t_sum [Structural_descr]
t_tuple [Unmarshal]
t_tuple [Structural_descr]
t_tuple [Descr]
Type descriptor for tuples of any range (the length of the array range is the range of the tuple).
t_unit [Unmarshal]
t_unit [Structural_descr]
t_unit [Descr]
t_unknown [Structural_descr]
taddrof [Logic_const]
&
tags_at [Rich_text]
Returns the list of tags at the given position.
tat [Logic_const]
\at
tcast [Logic_const]
cast to the given C type
temp_dir_cleanup_at_exit [Extlib]
temp_file_cleanup_at_exit [Extlib]
Similar to Filename.temp_file except that the temporary file will be deleted at the end of the execution (see above), unless debug is set to true, in which case a message with the name of the kept file will be printed.
term [Logic_typing.Make]
type-checks a term.
term [Logic_const]
returns a anonymous term of the given type.
term [Db.Properties.Interp]
term_lval [Db.Properties.Interp]
term_lval_to_lval [Db.Properties.Interp]
term_lvals_of_term [Ast_info]
term_of_exp_info [Cil]
Constructs a term from a term node and an expression information
term_offset_to_offset [Db.Properties.Interp]
term_to_exp [Db.Properties.Interp]
term_to_lval [Db.Properties.Interp]
terminated [Task]
Number of terminated process
terminates [Annotations]
If any, get the terminates clause of the contract associated to the given function.
text [Markdown]
Text Block
the [Extlib]
theMachine [Cil]
Current machine description
thirtytwo [Integer]
thread [Task]
time [Command]
Compute the elapsed time with Sys.time.
tint [Logic_const]
integer constant
tinteger [Logic_const]
integer constant
tinteger_s64 [Logic_const]
integer constant
tlogic_coerce [Logic_const]
coercion to the given logic type
to_annot [Alarms]
Conversion of an alarm to a code_annotation, without any registration.
to_array [Vector]
Makes a copy.
to_float [Transitioning.Q]
to_float [Integer]
to_float [Fval.F]
to_float [Float_sig.S]
Converts a floating-point number of single or double precision into a caml float.
to_int [Integer]
to_int32 [Integer]
to_int64 [Integer]
to_lexing_loc [Cil_datatype.Location]
to_lexing_pos [Cil_datatype.Position]
to_list [State_selection.S]
Convert a selection into a list of states.
to_list [Int_set]
Returns the set as an integer list.
to_list [Bottom]
Conversion functions.
to_ordered [Ordered_stmt]
Conversion functions between stmt and ordered_stmt.
to_ordered [Dataflows.FUNCTION_ENV]
to_pretty_string [Filepath.Normalized]
to_pretty_string p returns p prettified, that is, a relative path-like string.
to_result_from_pred [Db.Properties.Interp]
Does the interpretation of the predicate rely on the interpretation of the term result?
to_stmt [Ordered_stmt]
to_stmt [Dataflows.FUNCTION_ENV]
to_string [Pretty_utils]
pretty-prints the supplied value into a string.
to_string [Parameter_sig.Multiple_value_datatype]
to_string [Parameter_sig.Value_datatype]
key is the key associated to this value.
to_string [Parameter_sig.String_datatype_with_collections]
to_string [Parameter_sig.String_datatype]
to_string [Integer]
to_utf8 [Wutil]
to_varinfo [Base]
todo [Task]
Specialized version of later.
token [Logic_lexer]
told [Logic_const]
\old
toolbar [Wbox]
The first list is packed to the left side of the toolbar.
toolbar [Menu_manager]
toolmenubar [Menu_manager]
top [Utf8_logic]
top [Qstack.Make]
Return the top element of the stack.
top [Origin]
top [Map_lattice.MapSet_Lattice]
top [Map_lattice.Value]
top [Lmap_sig]
top [Int_Base]
top [Fval]
top [Float_interval_sig.S]
Top interval for a given precision, including infinite and NaN values.
top [Lattice_type.With_Top]
largest element
top_finite [Float_interval_sig.S]
The interval of all finite values in the given precision.
top_float [Locations.Location_Bytes]
top_float [Ival]
top_int [Locations.Location_Bytes]
top_opt [Lattice_type.With_Top_Opt]
optional largest element
top_single_precision_float [Locations.Location_Bytes]
top_single_precision_float [Ival]
top_string [Unicode]
top_with_origin [Locations.Location_Bytes]
Completely imprecise value.
topify_arith_origin [Locations.Location_Bytes]
Topifying of values, in case of imprecise accesses
topify_leaf_origin [Locations.Location_Bytes]
topify_merge_origin [Locations.Location_Bytes]
topify_misaligned_read_origin [Locations.Location_Bytes]
topify_with_origin [Offsetmap_lattice_with_isotropy]
Force a value to be isotropic, when a loss of imprecision occurs.
topify_with_origin [Locations.Location_Bytes]
topify_with_origin_kind [Locations.Location_Bytes]
toplevel_attr [Cil_datatype.Typ]
returns the attributes associated to the toplevel type, without adding attributes from compinfo, enuminfo or typeinfo.
trace_event [Gtk_helper]
Trace all events on stderr for the given object.
track_garbled_mix [Locations.Location_Bytes]
trange [Logic_const]
.. of integers
transfer [Interpreted_automata.Domain]
Transfer function for transitions: computes the state after the transition from the state before.
transfer_if_from_guard [Dataflows]
transfer_if_from_guard implements FORWARD_MONOTONE_PARAMETER.transfer_stmt for the If statement, given a function transfer_guard.
transfer_stmt [Dataflows.FORWARD_MONOTONE_PARAMETER]
transfer_stmt s state must returns a list of pairs in which the first element is a statement s' in s.succs, and the second element a value that will be joined with the current result for before s'.
transfer_stmt [Dataflows.BACKWARD_MONOTONE_PARAMETER]
transfer_stmt s state must implement the transfer function for s.
transfer_switch_from_guard [Dataflows]
Same as Dataflows.transfer_if_from_guard, but for a Switch statement.
transform [Lattice_type.Lattice_Base]
transform [Descr]
Similar to Unmarshal.Transform, but safe.
transform_category [Ghost_cfg]
transform_category [Ghost_accesses]
transform_category [Exn_flow]
category of the code transformation above.
transform_category [Destructors]
category of the transformation.
transform_element [Logic_const]
transform_element f t is the same as set_conversion (plain_or_set f t) t
transient_block [Cil]
Mark the given block as candidate to be flattened into its parent block, after returning from its visit.
translate_history_elt [History]
try to translate the history_elt of one project to the current one
translate_old_label [Logic_utils]
transforms \old and \at(,Old) into \at(,L) for L a label pointing to the given statement, creating one if needed.
treal [Logic_const]
real constant
treal_zero [Logic_const]
real zero
treat_constructor_as_func [Cil]
treat_constructor_as_func action v f args kind loc calls action with the parameters corresponding to the call to f, of kind kind, initializing v with arguments args.
tresult [Logic_const]
\result
trim [Rich_text]
Range of non-blank leading and trailing characters.
trim_by_validity [Tr_offset]
trim_by_validity ?origin offsets size validity reduces offsets so that all accesses to offsets+(0..size-1) are valid according to validity.
triple [Datatype]
trunc [Fval]
trunc [Floating_point]
Rounds to integer, toward zero (like trunc() in C).
trunc [Float_sig.S]
trunc [Float_interval_sig.S]
truncateInteger64 [Cil]
Represents an integer as for a given kind.
truncate_to_integer [Floating_point]
Raises Float_Non_representable_as_Int64 if the float value cannot be represented as an Int64 or as an unsigned Int64.
try_finally [Extlib]
tstring [Logic_const]
string constant
tuning_parameters [Emitter.Usable_emitter]
tuning_parameters [Emitter]
tvar [Logic_const]
variable
two [Integer]
two_power [Integer]
Computes 2^n
two_power_32 [Integer]
two_power_64 [Integer]
two_power_of_int [Integer]
Computes 2^n
ty [Type.Abstract]
ty [State_selection]
Type value representing State_selection.t.
ty [Datatype.Ty]
typ_of_link [Gui_printers]
Convert a string of the form link:typN into a type.
typeAddAttributes [Cil]
Add some attributes to a type
typeAttr [Cil]
Returns the attributes of a type.
typeAttrs [Cil]
Returns all the attributes contained in a type.
typeDeepDropAllAttributes [Cil]
Remove any attribute appearing somewhere in the fully expanded version of the type.
typeDeepDropAttributes [Cil]
Remove attributes whose name appears in the first argument that are present anywhere in the fully expanded version of the type.
typeForInsertedCast [Cabs2cil]
Like typeForInsertedVar, but for casts.
typeForInsertedVar [Cabs2cil]
A hook into the code that creates temporary local vars.
typeHasAttribute [Cil]
Does the type have the given attribute.
typeHasAttributeDeep [Cil]
typeHasAttributeMemoryBlock [Cil]
typeHasAttributeMemoryBlock attr t is true iff at least one component of an object of type t has attribute attr.
typeHasQualifier [Cil]
Does the type have the given qualifier.
typeOf [Cil]
Compute the type of an expression.
typeOfInit [Cil]
Compute the type of an initializer
typeOfLhost [Cil]
Compute the type of an lhost (with no offset)
typeOfLval [Cil]
Compute the type of an lvalue
typeOfTermLval [Cil]
Equivalent to typeOfLval for terms.
typeOf_array_elem [Cil]
Returns the type of the array elements of the given type.
typeOf_pointed [Cil]
Returns the type pointed by the given type.
typeOffset [Cil]
Compute the type of an offset from a base type
typeRemoveAllAttributes [Cil]
same as above, but remove any existing attribute from the type.
typeRemoveAttributes [Cil]
Remove all attributes with the given names from a type.
typeRemoveAttributesDeep [Cil]
Same as typeRemoveAttributes, but recursively removes the given attributes from inner types as well.
typeTermOffset [Cil]
Equivalent to typeOffset for terms.
type_annot [Logic_typing.Make]
type_binop [Logic_typing]
Arithmetic binop conversion.
type_of_array_elem [Logic_typing]
type_of_element [Logic_const]
returns the type of elements of a set type.
type_of_field [Logic_typing.Make]
type_of_list_elem [Logic_typing]
type_of_list_elem [Logic_const]
returns the type of elements of a list type.
type_of_pointed [Logic_typing]
type_of_set_elem [Logic_typing]
type_rel [Logic_typing]
Relation operators conversion
type_remove_attributes_for_c_cast [Cil]
Remove all attributes relative to const, volatile and restrict attributes when building a C cast
type_remove_attributes_for_logic_type [Cil]
Remove all attributes relative to const, volatile and restrict attributes when building a logic cast
type_remove_qualifier_attributes [Cil]
Remove all attributes relative to const, volatile and restrict attributes
type_remove_qualifier_attributes_deep [Cil]
remove also qualifiers under Ptr and Arrays
typeinfo [Visitor_behavior.Fold]
typeinfo [Visitor_behavior.Iter]
typeinfo [Visitor_behavior.Unset]
typeinfo [Visitor_behavior.Set]
typeinfo [Visitor_behavior.Get]
typeinfo [Visitor_behavior.Reset]
typename_status [Logic_env]
returns the typename status of the given identifier.
typeof [Base]
Type of the memory block that starts from the given base.

U
ucharPtrType [Cil]
ucharType [Cil]
uint16_t [Cil]
Any unsigned integer type of size 16 bits.
uint32_t [Cil]
Any unsigned integer type of size 32 bits.
uint64_t [Cil]
Any unsigned integer type of size 64 bits.
uintPtrType [Cil]
unsigned int *
uintType [Cil]
unsigned int
ulist [Bag]
ulongLongType [Cil]
unsigned long long
ulongType [Cil]
unsigned long
umap [Bag]
unamed [Logic_const]
makes a predicate with no name.
uncurry [Extlib]
undefined [Datatype]
Must be used if you don't want to implement a required function.
undoAlphaChanges [Alpha]
Undo the changes to a table
unescape [Logic_typing]
unicode_char [Logic_lexer]
union [Utf8_logic]
union [State_selection.S]
Union of two selections.
union [Hptset.S_Basic_Compare]
union_string [Unicode]
uniqueVarNames [Cil]
Assign unique names to local variables.
unique_name_from_name [State]
unit [Datatype]
unknown [Cil_datatype.Location]
unknown [Cil_datatype.Position]
unknown [Filepath.Normalized]
Unknown filepath, used as 'dummy' for Datatype.Filepath.
unmarshable [Descr]
Descriptor for unmarshallable types.
unrollType [Cil]
Unroll a type until it exposes a non TNamed.
unrollTypeDeep [Cil]
Unroll all the TNamed in a type (even under type constructors such as TPtr, TFun or TArray.
unroll_ltdef [Logic_const]
expands logic type definitions only.
unroll_transform [Unroll_loops]
unroll_type [Logic_utils]
expands logic type definitions.
unroll_unnatural_loop [Interpreted_automata.UnrollUnnatural]
unsafeSetFormalsDecl [Cil]
replace formals of a function declaration with the given list of varinfo.
unsafe_pack [Structural_descr]
unsafe_set [Kernel.LibEntry]
Not for casual users.
unsafe_set [Kernel.MainFunction]
unsignedVersionOf [Cil]
Give the unsigned kind corresponding to any integer kind
update [Vector]
Set value at index.
update [Structural_descr.Recursive]
update [Offsetmap_sig]
update ?origin ~validity ~exact ~offsets ~size v m writes v, of size size, each offsets in m; m must be of the size implied by validity.
update [Indexer.Make]
update x y t replaces x by y and returns the range a..b of modified indices.
update_file_loc [Logic_lexer]
update_imprecise_everywhere [Offsetmap_sig]
update_everywhere ~validity o v m computes the offsetmap resulting from imprecisely writing v potentially anywhere where m is valid according to validity.
update_line_loc [Logic_lexer]
update_newline_loc [Logic_lexer]
update_printer [Printer_api.S]
Register a pretty-printer extension.
update_under [Offsetmap_sig]
Same as Offsetmap_sig.update, except that no over-approximation on the set of offsets or on the value written occurs.
update_var_type [Cil]
Changes the type of a varinfo and of its associated logic var if any.
update_variable_validity [Base]
Update the corresponding fields of the variable validity.
url [Markdown]
URL links
use [Parameter_category]
use s c indicates that the state s depends on the category c.
useConfigurationBool [Cilconfig]
useConfigurationFloat [Cilconfig]
useConfigurationInt [Cilconfig]
Looks for an integer configuration element, and if it is found, it uses the given function.
useConfigurationList [Cilconfig]
useConfigurationString [Cilconfig]
use_bool [Gtk_helper.Configuration]
use_float [Gtk_helper.Configuration]
use_int [Gtk_helper.Configuration]
Looks for an integer configuration element, and if it is found, it is given to the given function.
use_list [Gtk_helper.Configuration]
use_spec_instead_of_definition [Db.Value]
To be called by derived analyses to determine if they must use the body of the function (if available), or only its spec.
use_string [Gtk_helper.Configuration]
using_default_cpp [Fc_config]
whether the preprocessor command is the one defined at configure time or the result of taking a CPP environment variable, in case it differs from the configure-time command.

V
v [Wbox]
w ~expand:V
valid_behaviors [Db.Value]
valid_cardinal_zero_or_one [Locations]
Is the valid part of the location bottom or a singleton?
valid_intersects [Locations.Zone]
Assuming that z1 and z2 only contain valid bases, valid_intersects z1 z2 returns true iff z1 and z2 have a valid intersection.
valid_offset [Base]
Computes all offsets that may be valid for an access of base t.
valid_part [Locations]
Overapproximation of the valid part of the given location.
valid_range [Base]
valid_range v returns Invalid_range if v is Invalid, Valid_range None if v is Empty, or Valid_range (Some (mn, mx)) otherwise, where mn and mx are the minimum and maximum (possibly) valid bounds of v.
validity [Base]
validity_from_size [Base]
validity_from_size size returns Empty if size is zero, or Known (0, size-1) if size > 0.
validity_from_type [Base]
valueOfDigit [Cabshelper]
value_of_integral_const [Ast_info]
value_of_integral_expr [Ast_info]
value_of_integral_logic_const [Ast_info]
var [Cil]
Makes an lvalue out of a given variable
var_is_in_scope [Kernel_function]
var_is_in_scope kf stmt vi returns true iff the local variable vi is syntactically visible from statement stmt in function kf.
variable_term [Ast_info]
varinfo [Visitor_behavior.Fold]
varinfo [Visitor_behavior.Iter]
varinfo [Visitor_behavior.Unset]
varinfo [Visitor_behavior.Set]
varinfo [Visitor_behavior.Get]
varinfo [Visitor_behavior.Reset]
varinfo_of_link [Gui_printers]
Convert a string of the form link:vidN into the varinfo of vid N.
varinfo_of_localizable [Printer_tag]
varinfo_of_localizable [Pretty_source]
varname [Datatype.Make_input]
varname [Datatype.S_no_copy]
A good prefix name to use for an OCaml variable of this type.
varname [Datatype.Undefined]
varname [Datatype]
vbox [Wbox]
Pack a list of boxes vertically.
verbose_atleast [Log.Messages]
verify [Log.Messages]
If the first argument is true, return true and do nothing else, otherwise, send the message on the fatal channel and return false.
verify_assigns_froms [Db.Value]
For internal use only.
version [Fc_config]
Frama-C Version identifier.
version [Cprint]
version_and_codename [Fc_config]
Frama-C version and codename.
vertex [Service_graph.S]
vertex_attributes [State_dependency_graph.Attributes]
vertex_name [State_dependency_graph.Attributes]
vgroup [Wbox]
Pack a list of widgets vertically, with all widgets stuck to the same width
vi [Cil_datatype.Kf]
visit [Rich_text]
Visit the message, with depth-first recursion on tags.
visitCabsAttributes [Cabsvisit]
visitCabsBlock [Cabsvisit]
visitCabsDeclType [Cabsvisit]
Visits a decl_type.
visitCabsDefinition [Cabsvisit]
visitCabsExpression [Cabsvisit]
visitCabsFile [Cabsvisit]
visitCabsName [Cabsvisit]
visitCabsSpecifier [Cabsvisit]
visitCabsStatement [Cabsvisit]
visitCabsTypeSpecifier [Cabsvisit]
visitCilAllocates [Cil]
visitCilAllocation [Cil]
visitCilAnnotation [Cil]
visitCilAssigns [Cil]
visitCilAttributes [Cil]
Visit a list of attributes
visitCilBehavior [Cil]
visitCilBehaviors [Cil]
visitCilBlock [Cil]
Visit a block
visitCilCodeAnnotation [Cil]
visitCilDeps [Cil]
visitCilEnumInfo [Cil]
visitCilExpr [Cil]
visitCilExtended [Cil]
visit an extended clause of a behavior.
visitCilFile [Cil]
Same thing, but the result is ignored.
visitCilFileCopy [Cil]
Visit a file.
visitCilFileSameGlobals [Cil]
A visitor for the whole file that does not *physically* change the globals (but maybe changes things inside the globals through side-effects).
visitCilFrees [Cil]
visitCilFrom [Cil]
visitCilFunction [Cil]
Visit a function definition
visitCilFunspec [Cil]
visitCilGlobal [Cil]
Visit a global
visitCilIdPredicate [Cil]
visitCilIdTerm [Cil]
visit identified_term.
visitCilInit [Cil]
Visit an initializer, pass also the global to which this belongs and the offset.
visitCilInitOffset [Cil]
Visit an initializer offset
visitCilInstr [Cil]
Visit an instruction
visitCilLocal_init [Cil]
Visit a local initializer (with the local being initialized).
visitCilLogicInfo [Cil]
visitCilLogicType [Cil]
visitCilLogicVarDecl [Cil]
visitCilLogicVarUse [Cil]
visitCilLval [Cil]
Visit an lvalue
visitCilModelInfo [Cil]
visitCilOffset [Cil]
Visit an lvalue or recursive offset
visitCilPredicate [Cil]
visitCilPredicateNode [Cil]
visitCilPredicates [Cil]
visitCilStmt [Cil]
Visit a statement
visitCilTerm [Cil]
visitCilTermLhost [Cil]
visitCilTermLval [Cil]
visit term_lval.
visitCilTermOffset [Cil]
visitCilType [Cil]
Visit a type
visitCilVarDecl [Cil]
Visit a variable declaration
visitFramacAllocation [Visitor]
visitFramacAnnotation [Visitor]
visitFramacAssigns [Visitor]
visitFramacAttributes [Visitor]
Visit a list of attributes
visitFramacBehavior [Visitor]
visitFramacBehaviors [Visitor]
visitFramacBlock [Visitor]
Visit a block
visitFramacCodeAnnotation [Visitor]
visitFramacDeps [Visitor]
visitFramacExpr [Visitor]
Visit an expression
visitFramacExtended [Visitor]
visitFramacFile [Visitor]
Same thing, but the result is ignored.
visitFramacFileCopy [Visitor]
Visit a file.
visitFramacFileSameGlobals [Visitor]
A visitor for the whole file that does not change the globals (but maybe changes things inside the globals).
visitFramacFrom [Visitor]
visitFramacFunction [Visitor]
Visit a function definition.
visitFramacFunspec [Visitor]
visitFramacGlobal [Visitor]
Visit a global.
visitFramacIdPredicate [Visitor]
visitFramacIdTerm [Visitor]
visit identified_term.
visitFramacInit [Visitor]
Visit an initializer, pass also the global to which this belongs and the offset.
visitFramacInitOffset [Visitor]
Visit an initializer offset
visitFramacInstr [Visitor]
Visit an instruction
visitFramacKf [Visitor]
Visit a kernel_function.
visitFramacLogicInfo [Visitor]
visitFramacLogicType [Visitor]
visitFramacLogicVarDecl [Visitor]
Visit a logic variable declaration
visitFramacLval [Visitor]
Visit an lvalue
visitFramacModelInfo [Visitor]
visitFramacOffset [Visitor]
Visit an lvalue or recursive offset
visitFramacPredicate [Visitor]
visitFramacPredicateNode [Visitor]
visitFramacPredicates [Visitor]
visitFramacStmt [Visitor]
Visit a statement
visitFramacTerm [Visitor]
visitFramacTermLhost [Visitor]
visitFramacTermLval [Visitor]
visitFramacTermOffset [Visitor]
visitFramacType [Visitor]
Visit a type
visitFramacVarDecl [Visitor]
Visit a variable declaration
voidConstPtrType [Cil]
void const *
voidPtrType [Cil]
void *
voidType [Cil_const]
voidType [Cil]
void
vscroll [Wbox]
Same as scroll ~volicy:`NEVER

W
w [Wbox]
Helper to box for packing a widget.
wait [Task]
Blocks until termination.
waiting [Task]
All task scheduled and server is waiting for termination
warning [Wutil]
warning [Log.Messages]
Hypothesis and restrictions.
wcharlist_of_string [Logic_typing]
widen [Offsetmap_sig]
widen wh m1 m2 performs a widening step on m2, assuming that m1 was the previous state.
widen [Lmap_sig]
widen [Interpreted_automata.Domain]
widen v1 v2 must returns None if v2 is included in v1.
widen [Float_interval_sig.S]
widen [Lattice_type.With_Widening]
widen h t1 t2 is an over-approximation of join t1 t2.
widen_down [Float_sig.S]
widen_up [Float_sig.S]
widen_up f returns a value strictly larger than f, such that successive applications of widen_up converge rapidly to infinity.
window [Gtk_compat]
with_codependencies [State_selection.S]
The selection containing the given state and all its co-dependencies.
with_dependencies [State_selection.S]
The selection containing the given state and all its dependencies.
with_error [Log.Messages]
with_error f fmt calls f in the same condition as logwith.
with_failure [Log.Messages]
with_failure f fmt calls f in the same condition as logwith.
with_null [Pretty_utils]
Discards the message and call the continuation.
with_null [Log]
Discards the message and call the continuation.
with_progress [Db]
with_progress ?debounced ?on_delayed trigger job data executes the given job on data while registering trigger as temporary (debounced) daemon.
with_result [Log.Messages]
with_result f fmt calls f in the same condition as logwith.
with_unfold_precond [Printer_tag.S_pp]
with_warning [Log.Messages]
with_warning f fmt calls f in the same condition as logwith.
without_annot [Printer_api.S_pp]
without_annot printer fmt x pretty prints x by using printer, without pretty-printing its function contracts and code annotations.
without_unicode [Kernel.Unicode]
Execute the given function as if the option -unicode was not set.
wkey_acsl_extension [Kernel]
wkey_acsl_float_compare [Kernel]
wkey_annot_error [Kernel]
error in annotation.
wkey_cert_exp_10 [Kernel]
wkey_cert_exp_46 [Kernel]
wkey_cert_msc_38 [Kernel]
wkey_check_volatile [Kernel]
wkey_cmdline [Kernel]
Command-line related warning, e.g.
wkey_decimal_float [Kernel]
wkey_drop_unused [Kernel]
wkey_ghost_already_ghost [Kernel]
ghost element is qualified with \ghost while this is already the case by default
wkey_ghost_bad_use [Kernel]
error in ghost code
wkey_implicit_conv_void_ptr [Kernel]
wkey_implicit_function_declaration [Kernel]
wkey_incompatible_pointer_types [Kernel]
wkey_incompatible_types_call [Kernel]
wkey_int_conversion [Kernel]
wkey_jcdb [Kernel]
wkey_missing_spec [Kernel]
wkey_name [Log.Messages]
returns the warning category name as a string.
wkey_no_proto [Kernel]
write [Journal]
write () writes the content of the journal into the file set by set_name (or in "frama_c_journal.ml" by default); without clearing the journal.
write_file [Command]
Properly close the channel and re-raise exceptions
wto_index_diff [Wto_statement]
wto_index_diff [Interpreted_automata.Compute]
wto_index_diff [Interpreted_automata]
wto_index_diff_of_stmt [Wto_statement]
wto_index_of_stmt [Wto_statement]
wto_of_kf [Wto_statement]

X
x86_16 [Machdeps]
x86_32 [Machdeps]
x86_64 [Machdeps]
x_or [Utf8_logic]
xor [Extlib]
exclusive-or.

Y
yield [Db]
Trigger all registered daemons (debounced).

Z
zero [Ival]
The lattice element that contains only the integer 0.
zero [Integer]
zero [Int_val]
zero [Int_set]
zero [Int_Base]
zero [Cil]
0
zero [Abstract_interp.Rel]
zero_or_one [Locations.Location_Bytes]
zero_or_one [Ival]
The lattice element that contains only the integers 0 and 1.
zero_or_one [Int_val]
zero_or_one [Int_set]
zeros [Fval]
Both positive and negative zero
zone_of_varinfo [Locations]