($) [Extlib] |
Composition.
|
(>>!) [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_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] | |
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.Make_without_cardinal] | |
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 [Indexer.Make] |
Log complexity.
|
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 [Set.S] | add x s returns a set containing all elements of s ,
plus x .
|
add [Fval] | |
add [FCSet.S_Basic_Compare] | add x s returns a set containing all elements of s ,
plus x .
|
add [FCMap.S] | add x y m returns a map containing the same bindings as
m , plus a binding of x to y .
|
add [Emitter.Make_table] | |
add [Dynamic.Parameter.StringList] | |
add [Dynamic.Parameter.StringSet] | |
add [Datatype.Sub_caml_weak_hashtbl] | |
add [Dataflow2.StmtStartData] | |
add [Dataflow.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_2_32 [Integer] | |
add_2_64 [Integer] | |
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_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_buffer [FCBuffer] | add_buffer b1 b2 appends the current contents of buffer b2
at the end of buffer b1 .
|
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_bytes [FCBuffer] | add_string b s appends the string s at the end of the buffer b .
|
add_call_fun [Db.Slicing.Request] |
change every call to any
to_call source or specialisation
in order to call the source function to_call in caller
|
add_call_min_fun [Db.Slicing.Request] |
For each call to
to_call in caller such so that, at least, it
will be visible at the end, ie.
|
add_call_slice [Db.Slicing.Request] |
change every call to any
to_call source or specialisation in order
to call to_call in caller .
|
add_channel [FCBuffer] | add_channel b ic n reads at most n characters from the
input channel ic and stores them at the end of buffer b .
|
add_char [FCBuffer] | add_char b c appends the character c at the end of the buffer b .
|
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] |
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_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_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_or_bottom [Map_Lattice.Make_without_cardinal] | |
add_persistent_cmdline [Db.Slicing.Request] |
Add persistent selection from the command line.
|
add_persistent_selection [Db.Slicing.Request] |
Add a persistent selection request to all slices (already existing or
created later) of a function to the project requests.
|
add_requires [Annotations] |
Add new requires clauses into the given behavior.
|
add_result [Logic_typing] |
add
\result in the environment.
|
add_selection [Db.Slicing.Request] |
Add a selection request to all slices (existing)
of a function to the project requests.
|
add_selection_internal [Db.Slicing.Request] |
Internally used to add a selection request to the project requests.
|
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 [Ival] |
Addition of an integer ival with an integer.
|
add_slice_selection_internal [Db.Slicing.Request] |
Internally used to add a selection request for a function slice
to the project requests.
|
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 [FCBuffer] | add_string b s appends the string s at the end of the buffer b .
|
add_subbytes [FCBuffer] | add_substring b s ofs len takes len characters from offset
ofs in byte sequence s and appends them at the end of the buffer b .
|
add_substitute [FCBuffer] | add_substitute b f s appends the string pattern s at the end
of the buffer b with substitution.
|
add_substring [FCBuffer] | add_substring b s ofs len takes len characters from offset
ofs in string s and appends them at the end of the buffer b .
|
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_to_selects_internal [Db.Slicing.Select] | |
add_type [Lexerhack] | |
add_type [Clexer] |
Add a new string as a type name
|
add_typename [Logic_env] |
marks an identifier as being a typename in the logic
|
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] |
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_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_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.
|
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.
|
anisotropic_cast [Offsetmap_lattice_with_isotropy] |
Convert the given value so 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] | |
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_Generic] | |
apply2 [Lattice_type.Lattice_Set_Generic] | |
apply_after_computed [Ast] |
Apply the given hook just after building the AST.
|
apply_all [Db.Slicing.Request] |
Apply all slicing requests.
|
apply_all_internal [Db.Slicing.Request] |
Internally used to apply all slicing requests.
|
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_next_internal [Db.Slicing.Request] |
Internally used to apply the first slicing request of the project list
and remove it from the list.
|
apply_once [State_builder] | apply_once name dep f returns a closure applying f only once and the
state internally used.
|
apply_set [Ival] | |
apply_set_unary [Ival] | |
apply_tag [Gtk_helper] | |
arch_bigendian [Unmarshal] | |
arch_sixtyfour [Unmarshal] | |
areCompatibleTypes [Cabs2cil] |
Check 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.
|
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)
|
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 ).
|
ast_dependencies [Parameter_builder] | |
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 [Fval] |
Returns atan2(y,x).
|
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.
|
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_comp_float_left [Ival] |
Same as
Ival.backward_comp_int_left , except that the arguments should now
be floating-point values.
|
backward_comp_int_left [Ival] | backward_comp_int op l r reduces l into l' so that
l' op r holds.
|
backward_comp_left [Fval] | backward_comp op allroundingmodes fkind f1 f2 attempts to reduce
f1 into f1' so that the relation f1' op f2 holds.
|
backward_mult_int_left [Ival] | |
band [Bitvector] | |
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] | |
big_endian_merge_bits [Offsetmap_lattice_with_isotropy] | |
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.
|
bindings [FCMap.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.
|
bitsSizeOfInt [Cil] | |
bits_of_float32 [Fval] | |
bits_of_float64 [Fval] | |
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_not [Ival] | |
bitwise_not_size [Ival] |
bitwise negation on a finite integer type.
|
bitwise_op2 [Bitvector] | |
bitwise_op3 [Bitvector] | |
bitwise_op4 [Bitvector] | |
bitwise_or [Ival] | |
bitwise_xor [Ival] | |
blit [FCBuffer] | Buffer.blit src srcoff dst dstoff len copies len characters from
the current contents of the buffer src , starting at offset srcoff
to dst , starting at character dstoff .
|
blit_buffer [FCBuffer] |
Similar to
blit , but copies to a buffer, and allows the destination
buffer to grow, that is, dstoff + len can be larger than the length of
dst .
|
blit_subbytes [FCBuffer] |
Same as
blit_buffer , but copies from bytes to a buffer.
|
blit_substring [FCBuffer] |
Same as
blit_buffer , but copies from a string to a buffer.
|
blockInit [Cabs2cil] |
Returns a block of statements equivalent to the initialization
init
applied to lvalue lval of type typ .
|
blockInitializer [Cabs2cil] | |
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.
|
bool [Json] |
Extract
True and False only.
|
bool [Datatype] | |
boolean [Utf8_logic] | |
boolean_type [Logic_const] | |
bor [Bitvector] | |
bot_of_list [Bottom] |
Conversion functions.
|
bottom [Origin] | |
bottom [Map_Lattice.Make_without_cardinal] | |
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
|
box [Wbox] |
Generic packing.
|
breakpoint [Project.Undo] | |
bs_identifier [Logic_lexer] | |
buffer [Source_viewer] | |
build_cil_file [Filter.F] | |
build_zones [Db.Scope] | |
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_rem [Ival] | |
c_rem [Integer] |
Remainder of the truncated division towards 0 (like in C99)
|
cabslu [Cabshelper] | |
cache_size [Binary_cache] |
Size of the caches.
|
cached_fold [Map_Lattice.Make_without_cardinal] | |
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_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.
|
capitalize_ascii [Transitioning.String] | |
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 [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 [Set.S] |
Return the number of elements of a set.
|
cardinal [FCSet.S_Basic_Compare] |
Return the number of elements of a set.
|
cardinal [FCMap.S] |
Return the number of bindings of a map.
|
cardinal_estimate [Ival] | cardinal_estimate v size returns an estimation of the cardinal
of v , knowing that v fits in size bits.
|
cardinal_is_less_than [Ival] |
Same than cardinal_less_than but just return if it is the case.
|
cardinal_less_than [Map_Lattice.Make] |
the cardinal of a map
m is the sum of the cardinals of the
values bound to a key in m
|
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 [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_less_than [Ival] | cardinal_less_than t n returns the cardinal of t is this cardinal
is at most n .
|
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 [Map_Lattice.Make] | |
cardinal_zero_or_one [Locations.Location_Bytes] | |
cardinal_zero_or_one [Locations] |
Is the location bottom or a singleton?
|
cardinal_zero_or_one [Lattice_type.With_Cardinal_One] | |
cardinal_zero_or_one [Ival] | |
cardinal_zero_or_one [Int_Base] | |
cast [Ival] | |
cast [Integer] | |
cast_double [Ival] | |
cast_float [Ival] | |
cast_float_to_double_inverse [Fval] | cast_float_to_double_inverse d return all possible float32 f such that
(double)f = d .
|
cast_float_to_int [Ival] | |
cast_float_to_int_inverse [Ival] |
integer
|
cast_int_to_float [Ival] | |
cast_int_to_float_inverse [Ival] |
integer
|
catch [Command] | |
category [Asm_contracts] |
the corresponding code transformation category.
|
ceil [Fval] | |
ceilf [Fval] | |
cfgFun [Cfg] |
Compute a control flow graph for fd.
|
change_slicing_level [Db.Slicing.Project] |
change the slicing level of this function
(see the
-slicing-level option documentation to know the meaning of the
number)
|
change_varinfo_name [Cil_const] | change_varinfo_name vi name changes the name of vi to name .
|
channel_redirector [Gtk_helper] |
Redirects all strings written to the file descriptor
and call the given function on each.
|
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
|
check [Gtk_form] | |
check [Abstract_interp.Rel] | |
check_asserts [Db.Scope] |
Print how many assertions could be removed based on the previous
analysis (
get_prop_scope_at_stmt ) and return the annotations
that can be removed.
|
check_ast [Filecheck] |
Visits the given AST (defaults to the AST of the current project)
to check whether it is consistent.
|
check_join_assert [Map_Lattice.Make_without_cardinal] | |
check_sequences [Undefined_sequence] | |
childrenBehavior [Cil] | |
choose [Rangemap.S] |
Return one binding of the given map, or raise
Not_found if
the map is empty.
|
choose [Set.S] |
Return one element of the given set, or raise
Not_found if
the set is empty.
|
choose [FCSet.S_Basic_Compare] |
Return one element of the given set, or raise
Not_found if
the set is empty.
|
choose [FCMap.S] |
Return one binding of the given map, or raise
Not_found if
the map is empty.
|
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 [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 [FCBuffer] |
Empty the buffer.
|
clear [Dynamic.Parameter.Common] | |
clear [Hook.S] |
Clear the hook.
|
clear [Dataflow2.StmtStartData] | |
clear [Dataflow.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 [Map_Lattice.Make_without_cardinal] | |
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 [Cil_datatype] | |
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_predicate [Cil] |
Bind all free variables with an universal quantifier
|
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.
|
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.
|
combinePredecessors [Dataflow.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.
|
combineStmtStartData [Dataflow.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
|
combineSuccessors [Dataflow.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 .
|
compFullName [Cil] |
Get the full name of a comp, including the 'struct' or 'union' prefix
|
compare [Type] | |
compare [Project] | |
compare [Origin.LocationSetLattice] | |
compare [Map_Lattice.Make_without_cardinal] | |
compare [Json] |
Pervasives
|
compare [Integer] | |
compare [Indexer.Elt] | |
compare [Hook.Comparable] | |
compare [Set.S] |
Total ordering between sets.
|
compare [Fval.F] | |
compare [Fval] | |
compare [FCSet.S_Basic_Compare] |
Total ordering between sets.
|
compare [FCMap.S] |
Total ordering between maps.
|
compare [Db.Slicing.Mark] |
A total ordering function similar to the generic structural
comparison function
compare .
|
compare [Datatype.Make_input] | |
compare [Datatype.S_no_copy] |
Comparison: same spec than
Pervasives.compare .
|
compare [Datatype.Undefined] | |
compare [Datatype] | |
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_max [Fval] | |
compare_max_float [Ival] | compare_min_int m1 m2 returns 1 if the int interval m1 has a
better min bound (i.e.
|
compare_max_int [Ival] | |
compare_max_min [Ival] |
In the results of
min_int and max_int , None represents the
corresponding infinity.
|
compare_min [Fval] | |
compare_min_float [Ival] | compare_min_float m1 m2 returns 1 if the float interval m1 has a
better min bound (i.e.
|
compare_min_int [Ival] | compare_max_int m1 m2 returns 1 if the int interval m1 has a
better max bound (i.e.
|
compare_min_max [Ival] | |
compare_term [Logic_utils] |
comparison compatible with is_same_term
|
compatibleTypes [Cabs2cil] |
Check that the two given types are compatible (C99, 6.2.7), and
return their composite type.
|
compilation_unit_names [Config] |
List of names of all kernel compilation units.
|
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.Constant_Propagation] |
Propagate constant into the functions given by the parameters (in the
same way that
Db.Constant_Propagation.get .
|
compute [Db.RteGen] | |
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 [Dataflow.Backwards] |
Fill in the T.stmtStartData, given a number of initial statements to start
from (the sinks for the backwards data flow).
|
compute [Dataflow.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.
|
computeFirstPredecessor [Dataflow.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_pragmas [Db.Impact] |
Compute the impact analysis from the impact pragma in the program.
|
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 [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_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.
|
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.
|
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 [Fval] | |
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_non_zero [Ival] | |
contains_result [Logic_utils] |
true if \result is included in the term
|
contains_single_elt [Hptset.S] | |
contains_zero [Ival] | |
contains_zero [Fval] | |
contents [FCBuffer] |
Return a copy of the current contents of the buffer.
|
convFile [Cabs2cil] | |
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 [Dataflow.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] |
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_slice [Db.Slicing.Request] |
Copy the input slice.
|
copy_visit [Cil] |
Makes fresh copies of the mutable structures.
|
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 [Fval] | |
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 [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 [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 [FCBuffer] | create n returns a fresh buffer, initially empty.
|
create [Emitter] | Emitter.create name kind ~correctness ~tuning creates a new emitter with
the given name.
|
create [Db.Slicing.Slice] |
Used to get an empty slice (nothing selected) related to a
function.
|
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_modu [Ival] | |
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_printer [Printer_api.S] |
Returns the current pretty-printer, with all the extensions added
using
Printer_api.S.update_printer .
|
currentloc_singleton [Origin.LocationSetLattice] | |
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 [Config] |
Directory where architecture independent files are.
|
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 [Dataflow.BackwardsTransfer] |
Whether to turn on debugging
|
debug [Dataflow.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.
|
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_slice_names [Db.Slicing.Project] | |
default_vertex_attributes [State_dependency_graph.Attributes] | |
default_widen_hints [Ival.Widen_Hints] | |
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.
|
diff [State_selection.S] |
Difference between two selections.
|
diff [Map_Lattice.Make_without_cardinal] | |
diff [Locations.Location_Bytes] |
Over-approximation of difference.
|
diff [Lattice_type.With_Diff] | diff t1 t2 is an over-approximation of t1-t2 .
|
diff [Set.S] |
Set difference.
|
diff [Fval] | |
diff [FCSet.S_Basic_Compare] |
Set difference.
|
diff_if_one [Map_Lattice.Make] | |
diff_if_one [Locations.Location_Bytes] |
Over-approximation of difference.
|
diff_if_one [Lattice_type.With_Diff_One] | diff_of_one t1 t2 is an over-approximation of t1-t2 .
|
digest [Type] | |
dir [Parameter_sig.Specific_dir] | dir ~error () returns the specific directory name, if
any.
|
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 [Integer] |
Euclidean division (that returns a positive rem)
|
div [Fval] | |
div_rem [Integer] | div_rem a b returns (pos_div a b, pos_rem a b)
|
divexact [Integer] |
Faster, but produces correct results only when b evenly divides a.
|
dkey [Project_skeleton.Output] | |
doEdge [Dataflow2.ForwardsTransfer] |
what to do when following the edge between the two given statements.
|
doEdge [Dataflow.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.
|
doGuard [Dataflow.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 .
|
doInstr [Dataflow.BackwardsTransfer] |
The (backwards) transfer function for an instruction.
|
doInstr [Dataflow.ForwardsTransfer] |
The (forwards) transfer function for an instruction (which is englobed
by the given statement).
|
doStmt [Dataflow2.BackwardsTransfer] |
The (backwards) transfer function for a branch.
|
doStmt [Dataflow2.ForwardsTransfer] |
The (forwards) transfer function for a statement.
|
doStmt [Dataflow.BackwardsTransfer] |
The (backwards) transfer function for a branch.
|
doStmt [Dataflow.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] | |
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_precond [Db.RteGen] | |
do_rte [Db.RteGen] | |
do_tooltip [Gtk_helper] |
Add the given tooltip to the given widget.
|
do_track_garbled_mix [Locations.Location_Bytes] | |
docAlphaTable [Alpha] |
Split the name in preparation for newAlphaName.
|
dominates [Dominators] | dominates a b tells whether a dominates b .
|
dot [Config] |
Dot command name.
|
doubleType [Cil] |
double
|
double_precision_of_string [Floating_point] | |
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 [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
|
dyn_set [Db.Slicing.Select] |
For dynamic type checking and journalization.
|
dyn_t [Db.Slicing.Slice] |
For dynamic type checking and journalization.
|
dyn_t [Db.Slicing.Select] |
For dynamic type checking and journalization.
|
dyn_t [Db.Slicing.Mark] |
For dynamic type checking and journalization.
|
dynamic [Descr] |
Similar to
Unmarshal.Dynamic .
|
E | |
e [Hptmap.Comp_unused] | |
echo [Log] |
Display an event of the terminal, unless echo has been turned off.
|
edge_attributes [State_dependency_graph.Attributes] | |
eight [Integer] | |
element_type [Ast_info] | |
elements [Leftistheap.Make] |
the returned list is not sorted
|
elements [Set.S] |
Return the list of all elements of the given set.
|
elements [FCSet.S_Basic_Compare] |
Return the list of all elements of the given set.
|
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] | |
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 [Leftistheap.Make] | |
empty [Lattice_type.Lattice_Set_Generic] | |
empty [Indexer.Make] | |
empty [Hptmap_sig.S] |
the empty map
|
empty [Set.S] |
The empty set.
|
empty [FCSet.S_Basic_Compare] |
The empty set.
|
empty [FCMap.S] |
The empty map.
|
empty [Bag] | |
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_selects [Db.Slicing.Select] |
Empty selection.
|
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.
|
end_user [Emitter] |
The special emitter corresponding to the end-user.
|
endline [Logic_lexer] | |
enlarge_1ulp [Fval] |
enlarge the bounds of the interval by one ulp.
|
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] | |
enumerate_bits [Locations] | |
enumerate_bits_under [Locations] | |
enumerate_valid_bits [Locations] | |
enumerate_valid_bits_under [Locations] | |
eq [Utf8_logic] | |
equal [Type] | |
equal [Qstack.DATA] | |
equal [Project] | |
equal [Parameter_sig.S_no_parameter] | |
equal [Map_Lattice.Make_without_cardinal] | |
equal [Json] |
Pervasives
|
equal [Integer] | |
equal [Hook.Comparable] | |
equal [Set.S] | equal s1 s2 tests whether the sets s1 and s2 are
equal, that is, contain equal elements.
|
equal [Fval.F] |
Those functions distinguish -0.
|
equal [FCSet.S_Basic_Compare] | equal s1 s2 tests whether the sets s1 and s2 are
equal, that is, contain equal elements.
|
equal [FCMap.S] | equal cmp m1 m2 tests whether the maps m1 and m2 are
equal, that is, contain equal keys and associate them with
equal data.
|
equal [Datatype.Make_input] | |
equal [Datatype.S_no_copy] |
Equality: same spec than
Pervasives.(=) .
|
equal [Datatype.Undefined] | |
equal [Datatype] | |
equal [Bottom] | |
equal [Bitvector] | |
equal [Binary_cache.Cacheable] | |
equal [Abstract_interp.Rel] | |
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.
|
exists [Utf8_logic] | |
exists [Rangemap.S] | exists p m checks if at least one binding of the map
satisfy the predicate p .
|
exists [Lattice_type.Lattice_Set_Generic] | |
exists [Parameter_sig.Set] |
Is there some element satisfying the given predicate?
|
exists [Hptmap_sig.S] | for_all p m returns true if at least one binding of the map m satisfies
the predicate p .
|
exists [Set.S] | exists p s checks if at least one element of
the set satisfies the predicate p .
|
exists [FCSet.S_Basic_Compare] | exists p s checks if at least one element of
the set satisfies the predicate p .
|
exists [FCMap.S] | exists p m checks if at least one binding of the map
satisfy the predicate p .
|
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] | |
exp [Fval] | |
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 [Fval] | |
expf [Floating_point] | |
explodeStringToInts [Cabshelper] | |
expr [Db.Inputs] | |
expr_to_kernel_function [Db.Value] | |
expr_to_kernel_function_state [Db.Value] | |
expr_to_term [Logic_utils] |
translates a C expression into an "equivalent" logical term.
|
expr_to_term_coerce [Logic_utils] |
same as
Logic_utils.expr_to_term , except that if the new term has an arithmetic
type, it is automatically coerced into real (or integer for integral types).
|
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 (==)
|
extract [Db.Slicing.Project] |
Build a new
Db.Project.t from all Slice.t of a project.
|
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_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_min [Leftistheap.Make] |
runs in O(log n)
|
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.
|
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.
|
file [Parameter_sig.Specific_dir] | file basename returns the complete filename of a file stored in dir .
|
file [Logic_preprocess] | |
file [Logic_lexer] | |
file [Cparser] | |
filename [Command] | |
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 [Lattice_type.Lattice_Set_Generic] | |
filter [Indexer.Make] |
Linear.
|
filter [Hptmap_sig.S] | filter f t keep only the bindings of m whose key verify f .
|
filter [Set.S] | filter p s returns the set of all elements in s
that satisfy predicate p .
|
filter [FCSet.S_Basic_Compare] | filter p s returns the set of all elements in s
that satisfy predicate p .
|
filter [FCMap.S] | filter p m returns the map with all the bindings in m
that satisfy predicate p .
|
filter [Bag] | |
filterAttributes [Cil] |
Retains attributes with the given name
|
filterStmt [Dataflow2.BackwardsTransfer] |
Whether to put this predecessor block in the worklist.
|
filterStmt [Dataflow.BackwardsTransfer] |
Whether to put this predecessor block in the worklist.
|
filterStmt [Dataflow.ForwardsTransfer] |
Whether to put this statement in the worklist.
|
filter_base [Map_Lattice.Make_without_cardinal] |
Over-approximation of the filter (in the case
Top Top )
|
filter_base [Locations.Zone] | filter_base can't raise Error_Top since it filters bases of Top .
|
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_loc [Locations] | |
filter_map [Extlib] | |
filter_map' [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 [Parameter_sig.Map] |
Search a given key in the 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.Make_without_cardinal] | |
find [Locations.Zone] | |
find [Locations.Location_Bytes.M] | |
find [Locations.Location_Bytes] |
Destructuring
|
find [Lmap_sig] | |
find [Lmap_bitwise.Location_map_bitwise] | |
find [Journal.Reverse_binding] | |
find [Hptmap_sig.S] | |
find [Gtk_helper.Configuration] |
Find a configuration elements, given a key.
|
find [Globals.FileIndex] |
All global C symbols for valviewer.
|
find [Globals.Vars] | |
find [Set.S] | find x s returns the element of s equal to x (according
to Ord.compare ), or raise Not_found if no such element
exists.
|
find [FCSet.S_Basic_Compare] | find x s returns the element of s equal to x (according
to Ord.compare ), or raise Not_found if no such element
exists.
|
find [FCMap.S] | find x m returns the current binding of x in m ,
or raises Not_found if no such binding exists.
|
find [Emitter.Make_table] | |
find [Db.From.Callwise] | |
find [Db.Value] | |
find [Dataflow2.StmtStartData] | |
find [Dataflow.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_inputs_nodes [Db.Pdg] |
Get the nodes corresponding to all inputs.
|
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
|
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_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_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_englobing_kf [Kernel_function] | |
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] |
Same as
Gtk_helper.Configuration.find_int .
|
find_from_astinfo [Globals.Vars] | |
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
|
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_type [Logic_env] | |
find_lonely_binding [Map_Lattice.Make] |
if there is only one binding
k -> v in map m (that is, only one key
k and cardinal_zero_or_one v ), returns the pair k,v .
|
find_lonely_binding [Locations.Location_Bytes] |
if there is only one binding
b -> 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.Make_without_cardinal] |
if there is only one key
k in map m , then returns the pair k,v
where v is the value associated to k .
|
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 [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.Make_without_cardinal] | |
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_stmts [Dataflow] | |
find_string [Gtk_helper.Configuration] |
Same as
Gtk_helper.Configuration.find_int .
|
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_utf8 [Logic_lexer] | |
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
|
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] | |
floorf [Fval] | |
flush [Wutil] | |
flush [Task] |
Clean all terminated tasks
|
fmod [Fval] |
Returns fmod(x,y).
|
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 [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 [Leftistheap.Make] |
elements are presented in an arbitrary order
|
fold [Lattice_type.Lattice_Set_Generic] | |
fold [Json] |
Fold over all fields of the object.
|
fold [Int_Intervals_sig] |
Iterators
|
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 [Set.S] | fold f s a computes (f xN ... (f x2 (f x1 a))...) ,
where x1 ... xN are the elements of s , in increasing order.
|
fold [FCSet.S_Basic_Compare] | fold f s a computes (f xN ... (f x2 (f x1 a))...) ,
where x1 ... xN are the elements of s , in increasing order.
|
fold [FCMap.S] | fold f m a computes (f kN dN ... (f k1 d1 a)...) ,
where k1 ... kN are the keys of all bindings in m
(in increasing order), and d1 ... dN are the associated data.
|
fold [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 [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 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 [Map_Lattice.Make_without_cardinal] | |
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 [Map_Lattice.Make] | |
fold_enum [Locations.Location_Bytes] | fold_enum f loc acc enumerates the locations in acc , and passes
them to f .
|
fold_enum [Lattice_type.With_Enumeration] |
Fold on the elements of the value one by one if possible.
|
fold_enum [Ival] |
Iterate on every value of the ival.
|
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_i [Map_Lattice.Make_without_cardinal] | fold_i f m acc folds f on the bindings in m .
|
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_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_left [State_builder.Array] | |
fold_left [State_builder.List_ref] | |
fold_left [Bag] | |
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_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_selects_internal [Db.Slicing.Select] | |
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_split [Ival] | |
fold_split [Fval] |
no splitting occurs if the integer argument is less than 2
|
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 [Map_Lattice.Make_without_cardinal] | |
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.
|
fold_visitor_compinfo [Cil] | |
fold_visitor_enuminfo [Cil] | |
fold_visitor_enumitem [Cil] | |
fold_visitor_fieldinfo [Cil] | |
fold_visitor_fundec [Cil] | |
fold_visitor_kernel_function [Cil] | |
fold_visitor_logic_info [Cil] | |
fold_visitor_logic_type_info [Cil] | |
fold_visitor_logic_var [Cil] | |
fold_visitor_model_info [Cil] | |
fold_visitor_stmt [Cil] | |
fold_visitor_typeinfo [Cil] | |
fold_visitor_varinfo [Cil] | fold_visitor_varinfo vis f folds f over each pair of varinfo registered
in vis .
|
for_all [Rangemap.S] | for_all p m checks if all the bindings of the map satisfy
the predicate p .
|
for_all [Lattice_type.Lattice_Set_Generic] | |
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 [Set.S] | for_all p s checks if all elements of the set
satisfy the predicate p .
|
for_all [FCSet.S_Basic_Compare] | for_all p s checks if all elements of the set
satisfy the predicate p .
|
for_all [FCMap.S] | for_all p m checks if all the bindings of the map
satisfy the predicate p .
|
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] | self#force_brace printer fmt x pretty prints x by using printer ,
but add some extra braces '{' and '}' which are hidden by default.
|
force_dir [Parameter_sig.Specific_dir] |
For functions below: if
force_dir is true: if error is false , then
creates the directory if it does not exist (or raises No_dir if the
directory cannot be created).
|
force_float [Ival] |
Reinterpret the given value as a float of the given kind.
|
formal_args [Ast_info.Function] |
Returns the list of the named formal arguments of a function.
|
formatter [Datatype] | |
forward [History] |
If possible (ie.
|
forward_comp [Fval] | |
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_keep_block [Cabs2cil] |
Name of the attribute inserted by the elaboration to prevent user blocks
from disappearing.
|
framac_icon [Gtk_helper] | |
framac_logo [Gtk_helper] | |
frank [Cil] |
Returns a unique number representing the floating-point conversion rank.
|
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_nodes [Db.Impact] |
Compute the impact analysis of the given set of PDG nodes,
that come from the given function.
|
from_num_id [Db.Slicing.Slice] | |
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_stmt [Db.Impact] |
Compute the impact analysis of the given statement.
|
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_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).
|
froundf [Fval] |
Single-precision versions
|
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.
|
funcExitData [Dataflow.BackwardsTransfer] |
The data at function exit.
|
function_env [Dataflows] | |
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 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.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 [Db.Occurrence] |
Return the occurrences of the given varinfo.
|
get [Db.Sparecode] |
Remove in each function what isn't used to compute its outputs,
or its annotations when
select_annot is true,
or its slicing pragmas when select_slice_pragmas is true.
|
get [Db.Pdg] |
Get the PDG of a function.
|
get [Db.Constant_Propagation] |
Propagate constant into the functions given by name.
|
get [Db.Users] | |
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] | |
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 .
|
getGlobInit [Cil] |
Get the global initializer and create one if it does not already exist.
|
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 [Db.Slicing.Slice] |
Get all slices related to a function.
|
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_astinfo [Globals.Vars] |
Linear in the number of locals and formals of the program.
|
get_bases [Map_Lattice.Make_without_cardinal] | |
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_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_called_funcs [Db.Slicing.Slice] |
To get the source functions called by the statement of a slice.
|
get_called_slice [Db.Slicing.Slice] |
To get the slice directly called by the statement of a slice.
|
get_callers [Db.Slicing.Slice] |
Get the slices having direct calls to a slice.
|
get_category [Log.Messages] |
returns all registered categories (including sub-categories)
corresponding to a given string
|
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_compinfo [Cil] | |
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_data_scope_at_stmt [Db.Scope] | |
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_defs [Db.Scope] | |
get_defs_with_type [Db.Scope] | |
get_descr [State] | |
get_description [Alarms] |
Long description of the alarm, explaining the UB it guards against.
|
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_enuminfo [Cil] | |
get_enumitem [Cil] | |
get_external [Db.INOUTKF] |
Inputs/Outputs without either local or formal variables
|
get_fieldinfo [Cil] | |
get_files [Globals.FileIndex] |
Get the files list containing all
global C symbols.
|
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_from_src_func [Db.Slicing.Mark] |
The mark
m related to all statements of a source function kf .
|
get_function [Db.Slicing.Slice] |
To get the function related to a slice
|
get_function [Db.Slicing.Select] |
The function related to an internal selection.
|
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_fundec [Cil] | |
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_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_kernel_function [Cil] | |
get_kf [Property] | |
get_kf_exn [Exn_flow] |
returns the set of exceptions that a given kernel function might throw.
|
get_kinstr [Property] | |
get_last_result [Db.Occurrence] | |
get_locals [Kernel_function] | |
get_location [Kernel_function] | |
get_logic_info [Cil] | |
get_logic_type_info [Cil] | |
get_logic_var [Cil] | |
get_mark_from_formal [Db.Slicing.Slice] |
Get the mark from the formal of a function.
|
get_mark_from_label [Db.Slicing.Slice] |
Get the mark value of a label.
|
get_mark_from_local_var [Db.Slicing.Slice] |
Get the mark value of local variable.
|
get_mark_from_stmt [Db.Slicing.Slice] |
Get the mark value of a statement.
|
get_mem [Parameter_category] |
Is the given element present in the category?
|
get_memAccess_status [Db.RteGen] | |
get_model_info [Cil] | |
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.
|
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_num_id [Db.Slicing.Slice] | |
get_operator [Cprint] | |
get_option [State_builder.Option_ref] | |
get_optional_argument [Type.Function] | |
get_original_compinfo [Cil] | |
get_original_enuminfo [Cil] | |
get_original_enumitem [Cil] | |
get_original_fieldinfo [Cil] | |
get_original_fundec [Cil] | |
get_original_kernel_function [Cil] | |
get_original_logic_info [Cil] | |
get_original_logic_type_info [Cil] | |
get_original_logic_var [Cil] | |
get_original_model_info [Cil] | |
get_original_stmt [Cil] | |
get_original_typeinfo [Cil] | |
get_original_varinfo [Cil] |
retrieve the original representative of a given copy of a varinfo
in the current state of the visitor.
|
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_possible_values [Parameter_sig.String] |
What are the acceptable values for this parameter.
|
get_precond_status [Db.RteGen] | |
get_pred_body [Logic_utils] |
returns the body of the given predicate.
|
get_preprocessor_command [File] |
Return the preprocessor command to use.
|
get_prop_basename [Property.Names] |
returns the basename of the property.
|
get_prop_name_id [Property.Names] |
returns a unique name identifying the property.
|
get_prop_scope_at_stmt [Db.Scope] |
compute the set of statements where the given annotation has the same
value as before the given stmt.
|
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 [Ival] |
Value of option -ilevel
|
get_state [Logic_lexer] | |
get_state [Dynamic.Parameter] |
retrieve the state related to the corresponding parameter.
|
get_state [Db.Value] | |
get_statementloc [Cabshelper] | |
get_stmt [Cil] | |
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] | |
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_type [Kernel_function] | |
get_type_specifier [Gui_printers] |
Returns the base type for a pointer/array, otherwise
t itself.
|
get_typeinfo [Cil] | |
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_user_mark_from_inputs [Db.Slicing.Slice] |
Get a mark that is the merged user inputs marks of the slice
|
get_value [Typed_parameter] |
Get the current value of the parameter, as a string.
|
get_varinfo [Cil] |
retrieve the representative of a given varinfo in the current
state of the visitor
|
get_vi [Kernel_function] | |
get_vi [Globals.Functions] | |
get_vi [Ast_info.Function] | |
get_with_formals [Db.Inputs] |
Inputs with formals and without local variables
|
get_zones [Db.Scope] | |
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_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] | |
graph [State_dependency_graph.S] | |
graph_attributes [State_dependency_graph.Attributes] | |
graph_window [Gtk_helper] |
Create a new window displaying a graph.
|
graph_window_through_dot [Gtk_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_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_finite [Fval] | has_finite f returns true iff f contains at least one finite
element.
|
has_persistent_selection [Db.Slicing.Project] |
return
true iff the source function has persistent selection
|
has_some [Extlib] | true iff its argument is Some x
|
hash [Type] | |
hash [Project] | |
hash [Map_Lattice.Make_without_cardinal] | |
hash [Logic_lexer] | |
hash [Integer] | |
hash [Hook.Comparable] | |
hash [Fval] | |
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_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] |
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_host [Logic_utils] | |
howto_marshal [State_builder.S] | howto_marshal marshal unmarshal registers a custom couple of
functions (marshal, unmarshal) to be used for serialization.
|
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 [Map_Lattice.Key] | |
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 -> .
|
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.
|
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 [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 [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.Make_without_cardinal] | |
inject [Locations.Zone] | |
inject [Locations.Location_Bytes] | |
inject [Lattice_type.Lattice_Set_Generic] | |
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_bounds [Int_Intervals_sig] | |
inject_f [Fval] |
Equivalent to
inject_r_f , but ignores the boolean not_finite .
|
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_itv [Int_Intervals_sig] | |
inject_ival [Locations.Location_Bytes] | |
inject_map [Map_Lattice.Make_without_cardinal] | |
inject_r [Fval] |
Alias for
inject_r_f Float64 .
|
inject_r_f [Fval] | inject_r_f creates an abstract float interval.
|
inject_range [Ival] | None means unbounded.
|
inject_singleton [Lattice_type.Lattice_Set_Generic] | |
inject_singleton [Ival] | |
inject_singleton [Fval] | |
inject_t1 [Lattice_type.Lattice_Sum] | |
inject_t2 [Lattice_type.Lattice_Sum] | |
inject_top [Ival] | inject_top min max r m checks min , max , r and m for consistency
as arguments of the Top constructor
and returns the lattice element of integers equal to r modulo m
between min and max (which may be a Set if there are few of these).
|
inject_top_origin [Locations.Location_Bytes] | inject_top_origin origin p creates a top with origin origin
and additional information param
|
inplace_visit [Cil] |
In-place modification.
|
input_val [Unmarshal] | input_val c t
Read a value from the input channel c , applying the transformations
described by t .
|
input_val [Descr] | |
insert [Leftistheap.Make] |
runs in O(log n)
|
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.
|
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 [Hptmap_sig.S] |
Intersection of two trees, parameterized by the
decide function.
|
inter [Set.S] |
Set intersection.
|
inter [FCSet.S_Basic_Compare] |
Set intersection.
|
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 [Map_Lattice.Make_without_cardinal] | |
intersects [Locations.Zone] | |
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_result [Abstract_interp.Comp] |
Given a result
r for an operation op , inv_result r is
the result that would have been obtained for inv op .
|
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_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.
|
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?
|
isCharArrayType [Cil] |
True if the argument is an array of a character type
(i.e.
|
isCharPtrType [Cil] |
True if the argument is a pointer to a character type
(i.e.
|
isCharType [Cil] |
True if the argument is a character type (i.e.
|
isCompleteProgramRoot [Rmtmps] | |
isCompleteType [Cil] |
Returns true if this is a complete type.
|
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.
|
isDefaultRoot [Rmtmps] | |
isExportedRoot [Rmtmps] | |
isExtern [Cabshelper] | |
isFloatingType [Cil] |
True if the argument is a floating point type
|
isFunctionType [Cil] |
True if the argument is a function type.
|
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.
|
isLogicArithmeticType [Cil] |
True if the argument is a logic arithmetic type (i.e.
|
isLogicArrayType [Logic_utils] |
Predefined tests over types
|
isLogicCharType [Logic_utils] | |
isLogicFloatType [Cil] |
True if the argument is a floating point 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] | |
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"?
|
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_a_zero [Fval] | is_a_zero f returns true iff f ⊆ -0.0,+0.0
|
is_abstract [Descr] | |
is_accessible [Db.Value] | |
is_addr [Db.Slicing.Mark] |
The element is used to compute the address of a selected data.
|
is_aligned_by [Base] | |
is_already_selected_internal [Db.Slicing.Request] |
Return true when the requested selection is already selected into the
slice.
|
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_block_local [Base] | |
is_block_local [Ast_info] |
determines if a var is local to a block.
|
is_boolean_type [Logic_const] | |
is_bottom [Map_Lattice.Make_without_cardinal] | |
is_bottom [Locations.Zone] | |
is_bottom [Locations.Location_Bytes] | |
is_bottom [Lmap_bitwise.Location_map_bitwise] | |
is_bottom [Ival] | |
is_bottom [Db.Slicing.Mark] | true iff the mark is empty: it is the only case where the
associated element is invisible.
|
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.Slicing.Project] |
Return
true iff the source function is called (even indirectly via
transitivity) from a Slice.t .
|
is_called [Db.Value] | |
is_case_label [Cil] |
Return
true on case and default labels, false otherwise.
|
is_cea_dump_file_function [Ast_info] | |
is_cea_dump_function [Ast_info] | |
is_cea_function [Ast_info] | |
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_behavior [Cil] |
true iff the behavior is a copy behavior.
|
is_ctrl [Db.Slicing.Mark] |
The element is used to control the program point of a selected
data.
|
is_current [Project] |
Check whether the given project is the current one or not.
|
is_data [Db.Slicing.Mark] |
The element is used to compute selected data.
|
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_directly_called_internal [Db.Slicing.Project] |
Return
true if the source function is directly (even via pointer
function) called from a Slice.t .
|
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 [Leftistheap.Make] |
runs in O(1)
|
is_empty [Indexer.Make] | |
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 [Set.S] |
Test whether a set is empty or not.
|
is_empty [FCSet.S_Basic_Compare] |
Test whether a set is empty or not.
|
is_empty [FCMap.S] |
Test whether a map is empty or not.
|
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_exit_status [Logic_const] | true if the term is \exit_status (potentially enclosed in \at)
|
is_extension [Logic_utils] | |
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_behavior [Cil] |
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_global [Base] | |
is_going_to_load [Cmdline] |
To be call if one action is going to run after the loading stage.
|
is_gui [Config] |
Is the Frama-C GUI running?
|
is_impact_pragma [Logic_utils] | |
is_included [Origin] | |
is_included [Offsetmap_bitwise_sig] | |
is_included [Map_Lattice.Make_without_cardinal] | |
is_included [Lmap_sig] | |
is_included [Lattice_type.Join_Semi_Lattice] |
is first argument included in the second?
|
is_included [Fval] | |
is_included [Dataflows.JOIN_SEMILATTICE] |
Must verify: a is_included b <=> a join b = b.
|
is_included [Bottom] | |
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_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 set<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_model_field [Logic_env] | |
is_natural [Loop] | |
is_non_natural [Loop] | |
is_non_null_expr [Ast_info] | |
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_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 strictly relative to
base
(that is, it is prefixed by base ), or to the present working directory
if no base is specified.
|
is_request_empty_internal [Db.Slicing.Request] |
Internally used to know if internal requests are pending.
|
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_rt_type_mode [Logic_utils] | |
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 [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 [Hptmap_sig.S] | is_singleton m returns Some (k, d) if m is a singleton map
that maps k to d .
|
is_singleton [Fval] | |
is_singleton_int [Ival] | |
is_skip [Cil] | |
is_slice_pragma [Logic_utils] | |
is_spare [Db.Slicing.Mark] |
Smallest visible mark.
|
is_special_builtin [Cil] | |
is_stmt_invariant [Logic_utils] | |
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_unmarshable [Descr] | |
is_unused_builtin [Cil] | |
is_valid [Locations] |
Is the given location entirely valid, as the destination of a write
operation if
for_writing is true, as the destination of a read
otherwise.
|
is_valid_offset [Base] | is_valid_offset ~for_writing size b offset checks that offset
(expressed in bits) plus size bits is valid in b .
|
is_variant [Logic_utils] | |
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_zero [Locations.Location_Bytes] | |
is_zero [Ival] | |
is_zero [Integer] | |
is_zero [Int_Base] | |
is_zero [Fval] | |
is_zero [Abstract_interp.Rel] | |
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 [Lattice_type.Lattice_Set_Generic] | |
iter [Journal.Reverse_binding] | |
iter [Int_Intervals_sig] |
May raise
Error_Top
|
iter [Indexer.Make] |
Linear.
|
iter [Hptmap_sig.S] | iter f m applies f to all bindings of the map m .
|
iter [Globals.Functions] | |
iter [Globals.Vars] | |
iter [Set.S] | iter f s applies f in turn to all elements of s .
|
iter [FCSet.S_Basic_Compare] | iter f s applies f in turn to all elements of s .
|
iter [FCMap.S] | iter f m applies f to all bindings in map m .
|
iter [Emitter.Make_table] | |
iter [Dynamic.Parameter.StringList] | |
iter [Dynamic.Parameter.StringSet] | |
iter [Dynamic] | |
iter [Db.From.Callwise] | |
iter [Dataflow2.StmtStartData] | |
iter [Dataflow.StmtStartData] | |
iter [State_builder.Set_ref] | |
iter [State_builder.Hashtbl] | |
iter [Cabshelper.Comments] | |
iter [Bag] | |
iter [Alarms] |
Iterator over all alarms and the associated annotations at some program
point.
|
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_selects_internal [Db.Slicing.Select] | |
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] | |
iter_visitor_compinfo [Cil] | |
iter_visitor_enuminfo [Cil] | |
iter_visitor_enumitem [Cil] | |
iter_visitor_fieldinfo [Cil] | |
iter_visitor_fundec [Cil] | |
iter_visitor_kernel_function [Cil] | |
iter_visitor_logic_info [Cil] | |
iter_visitor_logic_type_info [Cil] | |
iter_visitor_logic_var [Cil] | |
iter_visitor_model_info [Cil] | |
iter_visitor_stmt [Cil] | |
iter_visitor_typeinfo [Cil] | |
iter_visitor_varinfo [Cil] | iter_visitor_varinfo vis f iterates f over each pair of
varinfo registered in vis .
|
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 [Map_Lattice.Make_without_cardinal] | |
join [Lmap_sig] | |
join [Lattice_type.Join_Semi_Lattice] |
over-approximation of union
|
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 [Fval] | |
join [Dataflows.JOIN_SEMILATTICE] |
Must be idempotent (join a a = a), commutative, and associative.
|
join [Bottom.Top] | |
join [Bottom] | |
join_and_is_included [Map_Lattice.Make_without_cardinal] | |
join_and_is_included [Lattice_type.Join_Semi_Lattice] |
Do both ops simultaneously
|
join_and_is_included [Dataflows.JOIN_SEMILATTICE] |
This function is used by the dataflow algorithm to determine if
something has to be recomputed.
|
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_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 [Pretty_source] | |
kf_string_category [Parameter_builder] | |
kfloat [Cil] |
Constructs a floating point constant.
|
ki_of_localizable [Pretty_source] | |
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.
|
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 [Gtk_form] | |
label_visible [Filter.RemoveInfo] |
tells if the label is visible.
|
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.
|
launch [Task] |
Starts the server if not running yet
|
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 [FCBuffer] |
Return the number of characters currently contained in the buffer.
|
length [Hook.S] |
Number of registered functions.
|
length [Dataflow2.StmtStartData] | |
length [Dataflow.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 [Config] |
Directory where the Frama-C kernel library is.
|
library_names [Config] |
List of linked libraries.
|
lightweight_transform [Translate_lightweight] |
Code transformation that interprets __declspec annotations.
|
link [Map_Lattice.Make_without_cardinal] | |
link [Lattice_type.With_Under_Approximation] |
under-approximation of union
|
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_of_bot [Bottom] | |
list_of_opt [Extlib] |
converts an option into a list with 0 or 1 elt.
|
list_union [State_selection.S] |
Union of an arbitrary number of selection (0 gives an empty selection)
|
little_endian_merge_bits [Offsetmap_lattice_with_isotropy] | |
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_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
Lexing.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.
|
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] | |
log10 [Fval] |
All three functions may raise
Fval.Non_finite .
|
log10f [Fval] | |
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 [Fval] | |
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_of_global [Annotations] | |
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] | |
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.
|
lowercase_ascii [Transitioning.Char] | |
lowercase_ascii [Transitioning.String] | |
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.
|
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 [Filetree] |
Create a file tree packed in the given tree_view.
|
make [Db.Slicing.Mark] |
To construct a mark such as
(is_ctrl result, is_data result, isaddr result) = ,
(is_bottom result) = false and
(is_spare result) = not (~ctrl || ~data || ~addr) .
|
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_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 [Lmap_bitwise.Location_map_bitwise] | |
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 [Set.S] | map f s is the set whose elements are f a0 ,f a1 ...
|
map [FCMap.S] | map f m returns a map with same domain as m , where the
associated value a of all bindings of m has been
replaced by the result of the application of f to a .
|
map [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_i [Map_Lattice.Make_without_cardinal] | |
map_i [Locations.Zone] | |
map_offsets [Map_Lattice.Make_without_cardinal] | |
map_on_values [Offsetmap_sig] | map_on_values f m creates the map derived from m by applying f to
each interval.
|
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 [FCMap.S] |
Same as
FCMap.S.map , but the function receives as arguments both the
key and the associated value for each binding of the map.
|
mapi [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 [Integer] | |
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_binding [FCMap.S] |
Same as
FCMap.S.min_binding , but returns the largest binding
of the given map.
|
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_elt [Set.S] |
Same as
Set.S.min_elt , but returns the largest element of the
given set.
|
max_elt [FCSet.S] |
Same as , but returns the largest element of the
given set.
|
max_int [Ival] |
A
None result means the argument is unbounded.
|
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 [Map_Lattice.Make_without_cardinal] | |
meet [Lattice_type.With_Under_Approximation] |
under-approximation of intersection
|
meet [Fval] | |
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 [Parameter_sig.Map] | |
mem [Logic_env.Logic_builtin_used] | |
mem [Lattice_type.Lattice_Set_Generic] | |
mem [Parameter_sig.Set] |
Does the given element belong to the set?
|
mem [Indexer.Make] |
Log complexity.
|
mem [Hptmap_sig.S] | mem k m returns true if k is bound in m , and false otherwise.
|
mem [Set.S] | mem x s tests whether x belongs to the set s .
|
mem [FCSet.S_Basic_Compare] | mem x s tests whether x belongs to the set s .
|
mem [FCMap.S] | mem x m returns true if m contains a binding for x ,
and false otherwise.
|
mem [Emitter.Make_table] | |
mem [Dataflow2.StmtStartData] | |
mem [Dataflow.StmtStartData] | |
mem [State_builder.Set_ref] | |
mem [State_builder.Hashtbl] | |
mem [Bitvector] | |
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 [Datatype.Hashtbl] | memo tbl k f returns the binding of k in tbl .
|
memo [State_builder.Hashtbl] |
Memoization.
|
memo_compinfo [Cil] | |
memo_enuminfo [Cil] | |
memo_enumitem [Cil] | |
memo_fieldinfo [Cil] | |
memo_fundec [Cil] | |
memo_kernel_function [Cil] | |
memo_logic_info [Cil] | |
memo_logic_type_info [Cil] | |
memo_logic_var [Cil] | |
memo_model_info [Cil] | |
memo_stmt [Cil] | |
memo_typeinfo [Cil] | |
memo_varinfo [Cil] |
finds a binding in new project for the given varinfo, creating one
if it does not already exists.
|
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 [Leftistheap.Make] |
runs in O(log max(n1, n2))
|
merge [Hptmap_sig.S] |
Merge of two trees, parameterized by a merge function.
|
merge [FCMap.S] | merge f m1 m2 computes a map whose keys is a subset of keys of m1
and of m2 .
|
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 .
|
merge_behaviors [Logic_utils] | |
merge_funspec [Logic_utils] | merge_funspec oldspec newspec merges newspec into oldspec .
|
merge_internal [Db.Slicing.Select] |
The function related to an internal selection.
|
merge_neutral_element [Offsetmap_lattice_with_isotropy] |
Value that can be passed to
Offsetmap_lattice_with_isotropy.little_endian_merge_bits or
Offsetmap_lattice_with_isotropy.big_endian_merge_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
|
merge_slices [Db.Slicing.Request] |
Build a new slice which marks is a merge of the two given slices.
|
messages [Plugin.S] |
The group containing options -*-debug and -*-verbose.
|
min [Leftistheap.Make] |
runs in O(1)
|
min [Integer] | |
min_and_max [Ival] | |
min_and_max [Fval] | |
min_and_max_float [Ival] | |
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_binding [FCMap.S] |
Return the smallest binding of the given map
(with respect to the
Ord.compare ordering), or raise
Not_found if the map is empty.
|
min_denormal [Floating_point] | |
min_elt [Set.S] |
Return the smallest element of the given set
(with respect to the
Ord.compare ordering), or raise
Not_found if the set is empty.
|
min_elt [FCSet.S] |
Return the smallest element of the given set
(with respect to the
Ord.compare ordering), or raise
Not_found if the set is empty.
|
min_int [Ival] |
A
None result means the argument is unbounded.
|
min_int64 [Integer] | |
min_max_r_mod [Ival] | |
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] | |
minus [Utf8_logic] | |
minus_one [Ival] |
The lattice element that contains only the integer -1.
|
minus_one [Integer] | |
minus_one [Int_Base] | |
minus_one_one [Fval] | |
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.
|
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] |
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) { ...
|
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.
|
mkWhile [Cil] |
Make a while loop.
|
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] | |
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.
|
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 [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 [Fval] | |
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 [Dataflow.BackwardsTransfer] |
For debugging purposes, the name of the analysis
|
name [Dataflow.ForwardsTransfer] |
For debugging purposes, the name of the analysis
|
name [Cmdline.Group] | |
narrow [Origin] | |
narrow [Offsetmap_sig.Make_Narrow] |
Over-approximation of the intersection of abstract values, without
considering (bitwise) reinterpretations.
|
narrow [Map_Lattice.Make_without_cardinal] | |
narrow [Lmap_sig.Make_Narrow] | |
narrow [Lattice_type.With_Narrow] |
over-approximation of intersection
|
narrow [Fval] | |
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).
|
native_div [Integer] | |
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 [FCSet.S] | nearest_elt_ge v s returns the smallest element of s that is
bigger or equal to v .
|
nearest_elt_le [FCSet.S] | nearest_elt_le v s returns the largest element of s that is
smaller or equal to v .
|
need_cast [Cil] | true if both types are not equivalent.
|
neg [Utf8_logic] | |
neg [Integer] | |
neg [Int_Base] | |
neg [Fval] | |
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
|
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_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
|
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.Vid] | |
next [Cil.Eid] | |
next [Cil.Sid] | |
next_after [Fval] |
Equivalent to the
nextafter/nextafterf functions in C.
|
next_float [Fval.F] |
First double strictly above the argument.
|
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_results [Db.Value] |
Returns
true if the user has requested that no results should
be recorded for this function.
|
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] | |
normalization_parameters [Kernel] |
All the normalization options that influence the AST (in particular,
changing one will reset the AST entirely
|
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] | |
nth [FCBuffer] |
get the n-th character of the buffer.
|
null [Unmarshal] |
recursive values cannot be completely formed at the time
they are passed to their transformation function.
|
null [Log] |
Prints nothing.
|
null [Base] | |
null_set [Base] |
Set containing only the base
Base.null .
|
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 | |
ocamlc [Config] |
Name of the bytecode compiler.
|
ocamlopt [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] |
Converts from a floating-point value.
|
of_float [Fval.F] |
fails on NaNs, but allows infinities.
|
of_int [Json] | |
of_int [Ival] | |
of_int [Integer] | |
of_int32 [Integer] | |
of_int64 [Ival] | |
of_int64 [Integer] | |
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 [Leftistheap.Make] | |
of_list [Json] | |
of_list [Set.S] | of_list l creates a set from a list of elements.
|
of_list [FCSet.S_Basic_Compare] | of_list l creates a set from a list of elements.
|
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_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 .
|
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_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 [Bitvector] |
return
true if unset, then set the bit.
|
one [Ival] |
The lattice element that contains only the integer 1.
|
one [Integer] | |
one [Int_Base] | |
one [Cil] |
1
|
oneret [Oneret] | |
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_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_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_buffer [FCBuffer] | output_buffer oc b writes the current contents of buffer b
on the output channel oc .
|
output_graph [Service_graph.S] | |
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 [Fval] | |
packed_descr [Datatype.S_no_copy] |
Packed version of the descriptor.
|
pair [Datatype] | |
pallocable [Logic_const] |
\allocable
|
pand [Logic_const] |
&&
|
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_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.
|
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_from_location [Logic_lexer] | |
parse_kind [Floating_point] | |
partially_overlaps [Locations.Location_Bytes] |
Is there a possibly-non empty intersection between the two supplied
locations, assuming they have size
size
|
partially_overlaps [Ival] | |
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 [Set.S] | partition p s returns a pair of sets (s1, s2) , where
s1 is the set of all the elements of s that satisfy the
predicate p , and s2 is the set of all the elements of
s that do not satisfy p .
|
partition [FCSet.S_Basic_Compare] | partition p s returns a pair of sets (s1, s2) , where
s1 is the set of all the elements of s that satisfy the
predicate p , and s2 is the set of all the elements of
s that do not satisfy p .
|
partition [FCMap.S] | partition p m returns a pair of maps (m1, m2) , where
m1 contains all the bindings of s that satisfy the
predicate p , and m2 is the map with all the bindings of
s that do not satisfy p .
|
partition [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 .
|
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_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 [Config] |
Directory where the Frama-C dynamic plug-ins are.
|
plugin_path [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.
|
pnot [Logic_const] | |
pointed_type [Ast_info] | |
pointer_comparable [Logic_utils] |
\pointer_comparable
|
points_to_valid_string [Logic_utils] |
\points_to_valid_string
|
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.
|
pos_div [Integer] |
Euclidean division.
|
pos_rem [Integer] |
Remainder of the Euclidean division (always positive)
|
pos_rem [Abstract_interp.Rel] | |
positive_integers [Ival] |
The lattice element that contains exactly the positive or null integers
|
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 [Fval] |
Returns pow(x,y).
|
power_int_positive_int [Integer] | |
powf [Fval] |
Single-precision version of pow.
|
powf [Floating_point] | |
pp [Json] | |
pp_acsl_extension [Cil_types_debug] | |
pp_acsl_extension_kind [Cil_types_debug] | |
pp_allocation [Printer_api.S] | |
pp_allocation [Cil_types_debug] | |
pp_array [Pretty_utils] |
pretty prints an array.
|
pp_assigns [Printer_api.S] | |
pp_assigns [Cil_types_debug] | |
pp_attr [Cabs_debug] | |
pp_attribute [Printer_api.S] | |
pp_attribute [Cil_types_debug] | |
pp_attributes [Printer_api.S] | |
pp_attributes [Cil_types_debug] | |
pp_attrparam [Printer_api.S] | |
pp_attrparam [Cil_types_debug] | |
pp_attrs [Cabs_debug] | |
pp_behavior [Printer_api.S] | |
pp_behavior [Cil_types_debug] | |
pp_bhv [Description] |
prints nothing for default behavior, and " for 'b'" otherwise
|
pp_bin_op [Cabs_debug] | |
pp_binop [Printer_api.S] | |
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_block [Cil_types_debug] | |
pp_block [Cabs_debug] | |
pp_blocklist [Pretty_utils] | |
pp_bool [Cil_types_debug] | |
pp_builtin_logic_info [Cil_types_debug] | |
pp_cabsloc [Cabs_debug] | |
pp_catch_binder [Cil_types_debug] | |
pp_char [Cil_types_debug] | |
pp_cil_function [Cil_types_debug] | |
pp_close_block [Pretty_utils] | |
pp_code_annotation [Printer_api.S] | |
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 [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_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_def [Cabs_debug] | |
pp_deps [Cil_types_debug] | |
pp_enum_item [Cabs_debug] | |
pp_enuminfo [Cil_types_debug] | |
pp_enumitem [Cil_types_debug] | |
pp_exp [Printer_api.S] | |
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_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_field_group [Cabs_debug] | |
pp_field_groups [Cabs_debug] | |
pp_fieldinfo [Cil_types_debug] | |
pp_file [Printer_api.S] | |
pp_file [Cil_types_debug] | |
pp_file [Cabs_debug] | |
pp_fkind [Printer_api.S] | |
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_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] |
first parameter is the introducing keyword (e.g.
|
pp_fun_spec [Cabs_debug] | |
pp_funbehavior [Cil_types_debug] | |
pp_fundec [Cil_types_debug] | |
pp_funspec [Printer_api.S] | |
pp_funspec [Cil_types_debug] | |
pp_global [Printer_api.S] | |
pp_global [Cil_types_debug] | |
pp_global_annotation [Printer_api.S] | |
pp_global_annotation [Cil_types_debug] | |
pp_identified_predicate [Printer_api.S] | |
pp_identified_predicate [Cil_types_debug] | |
pp_identified_term [Printer_api.S] | |
pp_identified_term [Cil_types_debug] | |
pp_idpred [Description] |
prints the "'<labels>'" or the "(<location>)" of the predicate
|
pp_ikind [Printer_api.S] | |
pp_ikind [Cil_types_debug] | |
pp_impact_pragma [Cil_types_debug] | |
pp_init [Printer_api.S] | |
pp_init [Cil_types_debug] | |
pp_init_exp [Cabs_debug] | |
pp_init_name [Cabs_debug] | |
pp_init_name_group [Cabs_debug] | |
pp_initinfo [Cil_types_debug] | |
pp_initwhat [Cabs_debug] | |
pp_instr [Printer_api.S] | |
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_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_location [Cil_types_debug] | |
pp_logic_body [Cil_types_debug] | |
pp_logic_constant [Cil_types_debug] | |
pp_logic_ctor_info [Cil_types_debug] | |
pp_logic_info [Cil_types_debug] | |
pp_logic_label [Printer_api.S] | |
pp_logic_label [Cil_types_debug] | |
pp_logic_real [Cil_types_debug] | |
pp_logic_type [Printer_api.S] | |
pp_logic_type [Cil_types_debug] | |
pp_logic_type_def [Cil_types_debug] | |
pp_logic_type_info [Cil_types_debug] | |
pp_logic_var [Printer_api.S] | |
pp_logic_var [Cil_types_debug] | |
pp_logic_var_kind [Cil_types_debug] | |
pp_loop_allocation [Printer_api.S] | |
pp_loop_assigns [Printer_api.S] | |
pp_loop_from [Printer_api.S] | |
pp_loop_pragma [Cil_types_debug] | |
pp_lval [Printer_api.S] | |
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_model_info [Printer_api.S] | |
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_offset [Printer_api.S] | |
pp_offset [Cil_types_debug] | |
pp_open_block [Pretty_utils] | |
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_post_cond [Printer_api.S] | |
pp_pragma [Cil_types_debug] | |
pp_predicate [Printer_api.S] | |
pp_predicate [Cil_types_debug] | |
pp_predicate_node [Printer_api.S] | |
pp_predicate_node [Cil_types_debug] | |
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_relation [Cil_types_debug] | |
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_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_storage [Cil_types_debug] | |
pp_storage [Cabs_debug] | |
pp_string [Cil_types_debug] | |
pp_term [Printer_api.S] | |
pp_term [Cil_types_debug] | |
pp_term_lhost [Cil_types_debug] | |
pp_term_lval [Printer_api.S] | |
pp_term_lval [Cil_types_debug] | |
pp_term_node [Cil_types_debug] | |
pp_term_offset [Printer_api.S] | |
pp_term_offset [Cil_types_debug] | |
pp_termination_kind [Cil_types_debug] | |
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_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_unop [Cil_types_debug] | |
pp_variant [Printer_api.S] | |
pp_variant [Cil_types_debug] | |
pp_varinfo [Printer_api.S] | |
pp_varinfo [Cil_types_debug] | |
pp_varname [Printer_api.S] | |
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 [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.stmtkind s and Cil_types.label s
into If s and Goto s, giving the function body a very CFG-like character.
|
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.
|
preprocessor [Config] |
Name of the default command to call the preprocessor.
|
preprocessor_is_gnu_like [Config] |
whether the default preprocessor accepts the same options as gcc
(i.e.
|
preprocessor_keep_comments [Config] | true if the default preprocessor selected during compilation is
able to keep comments (hence ACSL annotations) in its output.
|
preprocessor_supported_arch_options [Config] |
architecture-related options (e.g.
|
pretty [Tr_offset] | |
pretty [Task] | |
pretty [State_selection.S] |
Display a selection.
|
pretty [Property_status.Feedback] | |
pretty [Offsetmap_bitwise_sig] | |
pretty [Map_Lattice.Make_without_cardinal] | |
pretty [Locations] | |
pretty [Lmap_sig] | |
pretty [Journal.Reverse_binding] | |
pretty [Integer] | |
pretty [Fval.F] | |
pretty [Fval] | |
pretty [Floating_point] | |
pretty [Filepath] |
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
present 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.
|
pretty [Db.INOUTKF] | |
pretty [Db.Slicing.Request] |
For debugging...
|
pretty [Db.Slicing.Slice] |
For debugging...
|
pretty [Db.Slicing.Select] |
For debugging...
|
pretty [Db.Slicing.Mark] |
For debugging...
|
pretty [Db.Slicing.Project] |
For debugging...
|
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 [Dataflow.BackwardsTransfer] |
Pretty-print the state
|
pretty [Dataflow.ForwardsTransfer] |
Pretty-print the state.
|
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 [Offsetmap_bitwise_sig] | |
pretty_debug [Map_Lattice.Make_without_cardinal] | |
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_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_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_overflow [Fval] |
This pretty-printer does not display -FLT_MAX and FLT_MAX as interval
bounds.
|
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_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.
|
pretty_zones [Db.Scope] | |
prev_float [Fval.F] |
First double strictly below the argument.
|
prevent [Journal] | prevent f x applies x to f without printing anything in the
journal, even if f is journalized.
|
print [Db.Report] | |
printComments [Cprint] | |
printCounters [Cprint] | |
printFile [Cprint] | |
printLn [Cprint] | |
printLnComment [Cprint] | |
print_all [Db.Occurrence] |
Print all the occurrence of each variable declarations.
|
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.Slicing.Project] |
Print a representation of the slicing project (call graph)
in a dot file which name is the given string.
|
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_extracted_project [Db.Slicing.Project] |
Print the extracted project when "-slice-print" is set.
|
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 .
|
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 [Db] |
This function should be called from time to time by all analysers taking
time.
|
project [Lattice_type.Lattice_Set_Generic] | |
project [Lattice_type.Lattice_Base] | |
project [Int_Base] | |
project_float [Ival] | |
project_float [Fval] | |
project_int [Ival] | |
project_set [Int_Intervals_sig] |
May raise
Error_Top .
|
project_singleton [Int_Intervals_sig] | |
propagate_user_marks [Db.Slicing.Request] |
Apply pending request then propagate user marks to callers
recursively then apply pending requests
|
pseparated [Logic_const] |
\separated
|
psubtype [Logic_const] |
subtype relation
|
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.
|
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_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 [Cil] |
Returns a unique number representing the integer
conversion rank.
|
reachable_stmts [Stmts_graph] | reachable_stmts kf stmt returns the transitive closure of the successors
of stmt in kf .
|
reachedStatement [Dataflow.Forwards] | |
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] | |
recursive_pack [Structural_descr] |
Pack a recursive descriptor.
|
redirect [Gtk_helper] |
Redirect the given formatter to the given buffer
|
reduce_by_cond [Db.Value] | |
reduce_multichar [Cil] |
gives the value of a wide char literal.
|
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 predicate
|
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
|
refresh_visit [Cil] |
Makes fresh copies of the mutable structures and provides fresh id
for the structures that have ids.
|
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_extension [Logic_typing] | register_behavior_extension name f registers a typing function f to
be used to type clause with name name .
|
register_behavior_extension [Cil_printer] |
Register a pretty-printer used for behavior extension.
|
register_behavior_extension [Cil] |
Indicates how an extended behavior clause is supposed to be visited.
|
register_builtin [Db.Value] | !register_builtin name ?replace f registers an abstract function f
to use everytime a C function named name is called in the program.
|
register_category [Log.Messages] |
register a new debugging/verbose category.
|
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 [Logic_utils] |
register a given name as a clause name for extended contract.
|
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_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_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.
|
registered_builtins [Db.Value] |
Returns a list of the pairs (name, builtin_sig) registered via
register_builtin .
|
rehash [Datatype.Make_input] |
How to rehashconsed values.
|
rehash [Datatype.Undefined] | |
relativize [Filepath] | relativize base file returns a (strict) relative path of file
w.r.t.
|
rem [Integer] |
Remainder of the Euclidean division (always positive)
|
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 [Indexer.Make] |
Log complexity.
|
remove [Hptmap_sig.S] | remove k m returns the map m deprived from any binding involving
k .
|
remove [Set.S] | remove x s returns a set containing all elements of s ,
except x .
|
remove [FCSet.S_Basic_Compare] | remove x s returns a set containing all elements of s ,
except x .
|
remove [FCMap.S] | remove x m returns a map containing the same bindings as
m , except for x which is unbound in the returned map.
|
remove [Emitter.Make_table] | |
remove [Dynamic.Parameter.StringList] | |
remove [Dynamic.Parameter.StringSet] | |
remove [Db.Slicing.Slice] |
Remove the slice from the project.
|
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.
|
removeUnusedTemps [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] | |
remove_logic_function [Logic_env] |
removing
|
remove_logic_type [Logic_env] | |
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_uncalled [Db.Slicing.Slice] |
Remove the uncalled slice from the project.
|
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 [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 [Dataflow.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
|
reserve_name_id [Property.Names] |
returns the name that should be returned by the function
get_prop_name_id if the given property has name as basename.
|
reset [FCBuffer] |
Empty the buffer and deallocate the internal byte sequence holding the
buffer contents, replacing it with the initial internal byte sequence
of length
n that was allocated by Buffer.create n .
|
reset_behavior_compinfo [Cil] | |
reset_behavior_enuminfo [Cil] | |
reset_behavior_enumitem [Cil] | |
reset_behavior_fieldinfo [Cil] | |
reset_behavior_fundec [Cil] | |
reset_behavior_kernel_function [Cil] | |
reset_behavior_logic_info [Cil] | |
reset_behavior_logic_type_info [Cil] | |
reset_behavior_model_info [Cil] | |
reset_behavior_stmt [Cil] | |
reset_behavior_typeinfo [Cil] | |
reset_behavior_varinfo [Cil] |
resets the internal tables used by the given visitor_behavior.
|
reset_logic_var [Cil] | |
reset_once_flag [Messages] |
Reset the
once flag of pretty-printers.
|
reset_slice [Db.Slicing.Project] | |
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.Scope] |
Same analysis than
check_asserts but mark the assertions as proven.
|
rm_unused_globals [Db.Sparecode] |
Remove unused global types and variables from the given project
(the current one if no project given).
|
round_down_to_r [Integer] | |
round_down_to_zero [Integer] | |
round_to_single_precision_float [Fval] | |
round_to_single_precision_float [Floating_point] | |
round_up_to_r [Integer] | |
rt_type_mode [Logic_utils] | |
run [Task] |
Runs one single task in the background.
|
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.
|
running [Task] | |
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_paned_ratio [Gtk_helper] |
Saves the current ratio of the panel associated to the given key.
|
save_string [Json] | |
scale [Ival] | scale f v returns the interval of elements x * f for x in v .
|
scale_div [Ival] | scale_div ~pos:false f v is an over-approximation of the set of
elements x / f for x in v .
|
scale_div_under [Ival] | scale_div_under ~pos:false f v is an under-approximation of the
set of elements x / f for x in v .
|
scale_int_base [Ival] | |
scale_rem [Ival] | scale_rem ~pos:false f v is an over-approximation of the set of
elements x mod f for x in v .
|
scharPtrType [Cil] | |
scharType [Cil] | |
scheduled [Task] |
Number of scheduled process
|
select_decl_var_internal [Db.Slicing.Select] | |
select_entry_point_internal [Db.Slicing.Select] | |
select_file [Source_manager] |
Selection by page filename
|
select_func_annots [Db.Slicing.Select] |
To select the annotations related to a function.
|
select_func_calls_into [Db.Slicing.Select] |
To select every calls to the given function without the selection of
its inputs/outputs.
|
select_func_calls_to [Db.Slicing.Select] |
To select every calls to the given function, i.e.
|
select_func_lval [Db.Slicing.Select] |
To select lvalues (given as a string) related to a function.
|
select_func_lval_rw [Db.Slicing.Select] |
To select rw accesses to lvalues (given as a string) related to a function.
|
select_func_return [Db.Slicing.Select] |
To select the function result (returned value).
|
select_func_zone [Db.Slicing.Select] |
To select an output zone related to a function.
|
select_label_internal [Db.Slicing.Select] | |
select_min_call_internal [Db.Slicing.Select] |
Internally used to select a statement call without its
inputs/outputs so that it doesn't select the statements computing the
inputs of the called function as
select_stmt_internal would do.
|
select_modified_output_zone_internal [Db.Slicing.Select] |
Internally used to select the statements that modify the
given zone considered as in output.
|
select_name [Source_manager] |
Selection by page title
|
select_pdg_nodes [Db.Slicing.Select] | |
select_pdg_nodes_internal [Db.Slicing.Select] |
Internally used to select PDG nodes : if
is_ctrl_mark m ,
propagate ctrl_mark on ctrl dependencies of the statement, if is_addr_mark m ,
propagate addr_mark on addr dependencies of the statement, if is_data_mark m ,
propagate data_mark on data dependencies of the statement, mark the node with a spare_mark and propagate so that
the dependencies that were not selected yet will be marked spare.
|
select_return_internal [Db.Slicing.Select] | |
select_stmt [Db.Slicing.Select] |
To select a statement.
|
select_stmt_annot [Db.Slicing.Select] |
To select the annotations related to a statement.
|
select_stmt_annots [Db.Slicing.Select] |
To select the annotations related to a statement.
|
select_stmt_ctrl [Db.Slicing.Select] |
To select a statement reachability.
|
select_stmt_ctrl_internal [Db.Slicing.Select] |
Internally used to select a statement reachability :
Only propagate a ctrl_mark on the statement control dependencies.
|
select_stmt_internal [Db.Slicing.Select] |
Internally used to select a statement : if
is_ctrl_mark m ,
propagate ctrl_mark on ctrl dependencies of the statement, if is_addr_mark m ,
propagate addr_mark on addr dependencies of the statement, if is_data_mark m ,
propagate data_mark on data dependencies of the statement, mark the node with a spare_mark and propagate so that
the dependencies that were not selected yet will be marked spare.
When the statement is a call, its functional inputs/outputs are
also selected (The call is still selected even it has no output).
When the statement is a composed one (block, if, etc...),
all the sub-statements are selected.
|
select_stmt_lval [Db.Slicing.Select] |
To select lvalues (given as string) related to a statement.
|
select_stmt_lval_rw [Db.Slicing.Select] |
To select rw accesses to lvalues (given as string) related to a statement.
|
select_stmt_pred [Db.Slicing.Select] |
To select a predicate value related to a statement.
|
select_stmt_term [Db.Slicing.Select] |
To select a predicate value related to a statement.
|
select_stmt_zone [Db.Slicing.Select] |
To select a zone value related to a statement.
|
select_stmt_zone_internal [Db.Slicing.Select] |
Internally used to select a zone value at a program point.
|
select_zone_at_end_internal [Db.Slicing.Select] |
Internally used to select a zone value at the end of a function.
|
select_zone_at_entry_point_internal [Db.Slicing.Select] |
Internally used to select a zone value at the beginning of a function.
|
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 [Messages] |
Internal state of stored messages
|
self [Logic_env.Logic_builtin_used] | |
self [Kernel_function] | |
self [Hptset.Make] | |
self [Hptmap_sig.S] | |
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.Slicing] |
Internal state of the slicing tool from project viewpoints.
|
self [Db.Occurrence] | |
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.
|
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.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] |
If normalize is false,
setCurrentFile ~normalize:false path
accepts path as the current file "as is".
|
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_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_compinfo [Cil] | |
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_enuminfo [Cil] | |
set_enumitem [Cil] | |
set_fieldinfo [Cil] | |
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_fundec [Cil] | |
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_kernel_function [Cil] | |
set_length [State_builder.Array] | |
set_list [Gtk_helper.Configuration] | |
set_logic_info [Cil] | |
set_logic_type_info [Cil] | |
set_logic_var [Cil] | |
set_ml_name [Type] | |
set_model_info [Cil] | |
set_modes [Db.Slicing] | |
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_orig_compinfo [Cil] | |
set_orig_enuminfo [Cil] | |
set_orig_enumitem [Cil] | |
set_orig_fieldinfo [Cil] | |
set_orig_fundec [Cil] | |
set_orig_kernel_function [Cil] | |
set_orig_logic_info [Cil] | |
set_orig_logic_type_info [Cil] | |
set_orig_logic_var [Cil] | |
set_orig_model_info [Cil] | |
set_orig_stmt [Cil] | |
set_orig_typeinfo [Cil] | |
set_orig_varinfo [Cil] |
change the reference of a given new varinfo in the current
state of the visitor.
|
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_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_font [Wutil] | |
set_stmt [Cil] | |
set_tooltip [Wutil] | |
set_typeinfo [Cil] | |
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_varinfo [Cil] |
change the representative of a given varinfo in the current
state of the visitor.
|
set_vid [Cil_const] |
set the vid to a fresh number.
|
set_visible [Wutil] | |
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_left [Ival] | |
shift_left [Integer] | |
shift_right [Ival] | |
shift_right [Integer] | |
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.
|
sidebar [Wbox] |
The first list is packed to the top of the sidebar.
|
signof_typeof_lval [Bit_utils] | |
sin [Fval] | |
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.
|
single_precision_of_string [Floating_point] | |
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 [Hptmap_sig.S] | singleton k d returns a map whose only binding is from k to d .
|
singleton [Set.S] | singleton x returns the one-element set containing only x .
|
singleton [FCSet.S_Basic_Compare] | singleton x returns the one-element set containing only x .
|
singleton [FCMap.S] | singleton x y returns the one-element map that contains a binding y
for x .
|
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 [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
|
small_nums [Integer] | |
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_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 [Map_Lattice.Make_without_cardinal] | |
split [Locations.Location_Bytes] | |
split [Hptmap_sig.S] | |
split [Set.S] | split x s returns a triple (l, present, r) , where
l is the set of elements of s that are
strictly less than x ;
r is the set of elements of s that are
strictly greater than x ;
present is false if s contains no element equal to x ,
or true if s contains an element equal to x .
|
split [FCSet.S_Basic_Compare] | split x s returns a triple (l, present, r) , where
l is the set of elements of s that are
strictly less than x ;
r is the set of elements of s that are
strictly greater than x ;
present is false if s contains no element equal to x ,
or true if s contains an element equal to x .
|
split [FCMap.S] | split x m returns a triple (l, data, r) , where
l is the map with all the bindings of m whose key
is strictly less than x ;
r is the map with all the bindings of m whose key
is strictly greater than x ;
data is None if m contains no binding for x ,
or Some v if m binds v to x .
|
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_slice [Db.Slicing.Request] |
Copy the input slice to have one slice for each call of the original
slice and generate requests in order to call them.
|
sqrt [Fval] | |
sqrtf [Fval] | |
sqrtf [Floating_point] | |
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] | |
static_gui_plugins [Config] |
GUI of plug-ins statically linked within Frama-C.
|
static_plugins [Config] |
Plug-ins statically linked within Frama-C.
|
status [Task] |
The task that immediately finishes with provided status
|
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 [Dataflow.BackwardsTransfer] |
Must return
true if there is a path in the control-flow graph of the
function from the first statement to the second.
|
stmt_can_reach [Dataflow.ForwardsTransfer] |
Must return
true if there is a path in the control-flow graph of the
function from the first statement to the second.
|
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 [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_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 .
|
string_to_float_lconstant [Logic_utils] |
Parse the given string as a float logic constant, taking into account
the fact that the constant may not be exactly representable.
|
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
|
stripConstLocalType [Cil] |
Strip const attribute from the type.
|
stripInfo [Cil] |
Removes info wrappers and return underlying expression
|
stripTermCasts [Cil] |
Equivalent to
stripCasts for terms.
|
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 [Integer] | |
sub [Fval] | |
sub [FCBuffer] | Buffer.sub b off len returns (a copy of) the bytes from the
current contents of the buffer b starting at offset off of
length len bytes.
|
sub [Abstract_interp.Rel] | |
sub_abs [Abstract_interp.Rel] | |
sub_bytes [FCBuffer] |
Same as
sub but return a byte sequence instead of a string.
|
sub_int [Ival] | |
sub_int_under [Ival] | |
sub_pointwise [Locations.Location_Bytes] |
Subtracts the offsets of two locations
loc1 and loc2 .
|
subdiv_float_interval [Ival] | |
subdiv_float_interval [Fval] | |
subdiv_int [Ival] | |
subset [Set.S] | subset s1 s2 tests whether the set s1 is a subset of
the set s2 .
|
subset [FCSet.S_Basic_Compare] | subset s1 s2 tests whether the set s1 is a subset of
the set s2 .
|
subsets [Extlib] | subsets k l computes the combinations of k elements from list l .
|
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] |
&
|
tat [Logic_const] |
\at
|
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] | |
terminate_process [Extlib] |
Terminate a process id.
|
terminated [Task] |
Number of terminated process
|
terminates [Annotations] |
If any, get the terminates clause of the contract associated to the given
function.
|
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_bytes [FCBuffer] |
Return a copy of the current contents of the buffer.
|
to_float [Integer] | |
to_float [Fval.F] | |
to_int [Integer] | |
to_int64 [Integer] | |
to_list [State_selection.S] |
Convert a selection into a list of states.
|
to_num [Integer] | |
to_ordered [Ordered_stmt] |
Conversion functions between stmt and ordered_stmt.
|
to_ordered [Dataflows.FUNCTION_ENV] | |
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] | |
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 [Qstack.Make] |
Return the top element of the stack.
|
top [Origin] | |
top [Map_Lattice.Make_without_cardinal] | |
top [Lmap_sig] | |
top [Lattice_type.With_Top] |
largest element
|
top [Int_Base] | |
top [Fval] | |
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_single_precision_float [Fval] | |
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.
|
trange [Logic_const] | .. of integers
|
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 [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_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).
|
truncate [FCBuffer] | truncate b c truncates the length of b to be no larger than c .
|
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.
|
truncf [Fval] | |
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] | |
two_power_64 [Integer] | |
two_power_of_int [Integer] | |
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.
|
typ_to_logic_type [Logic_utils] |
C type to logic type, with implicit conversion for arithmetic types.
|
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] |
Does the type or one of its subtypes have the given attribute.
|
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.
|
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
|
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.
|
uncapitalize_ascii [Transitioning.String] | |
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] | |
union [State_selection.S] |
Union of two selections.
|
union [Set.S] |
Set union.
|
union [FCSet.S_Basic_Compare] |
Set union.
|
uniqueVarNames [Cil] |
Assign unique names to local variables.
|
unique_name_from_name [State] | |
unit [Datatype] | |
unknown [Cil_datatype.Location] | |
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_transform [Unroll_loops] | |
unroll_type [Logic_utils] |
expands logic type definitions.
|
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.
|
uppercase_ascii [Transitioning.Char] | |
uppercase_ascii [Transitioning.String] | |
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] |
Same as
Gtk_helper.Configuration.use_int .
|
use_float [Gtk_helper.Configuration] |
Same as
Gtk_helper.Configuration.use_int .
|
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] |
Same as
Gtk_helper.Configuration.use_int .
|
using_default_cpp [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.
|
usleep [Extlib] |
Unix function that sleep for
n microseconds.
|
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_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
|
variable_term [Ast_info] | |
varinfo_of_link [Gui_printers] |
Convert a string of the form
link:vidN into the varinfo of vid N .
|
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 [Cprint] | |
version [Config] |
Frama-C Version identifier.
|
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] | |
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 change the globals (but maybe
changes things inside the globals).
|
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
|
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 [Map_Lattice.Make] | |
widen [Lmap_sig] | |
widen [Lattice_type.With_Widening] | widen h t1 t2 is an over-approximation of join t1 t2 .
|
widen [Fval] | |
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_failure [Log.Messages] | |
with_log [Log.Messages] | |
with_log_channel [Log] |
logging function to user-created channel.
|
with_null [Log] |
Discards the message and call the continuation.
|
with_result [Log.Messages] | |
with_warning [Log.Messages] | |
without_annot [Printer_api.S] | 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.
|
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_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.
|
Z | |
zero [Ival] |
The lattice element that contains only the integer 0.
|
zero [Integer] | |
zero [Int_Base] | |
zero [Fval.F] | |
zero [Fval] | |
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.
|
zeros [Fval] |
Both positive and negative zero
|
zone_of_varinfo [Locations] |