($) [Extlib] | Composition. |
(>>!) [Task] |
|
(>>-) [Bottom.Type] | This monad propagates the `Bottom value if needed. |
(>>-:) [Bottom.Type] | Use this monad if the following function returns a simple value. |
(>>=) [Task] |
|
(>>>) [Task] |
|
(>>?) [Task] |
|
__ocaml_lex_chr_rec [Logic_lexer] | |
__ocaml_lex_comment_rec [Logic_lexer] | |
__ocaml_lex_endline_rec [Logic_lexer] | |
__ocaml_lex_file_rec [Logic_lexer] | |
__ocaml_lex_hash_rec [Logic_lexer] | |
__ocaml_lex_tables [Logic_lexer] | |
__ocaml_lex_token_rec [Logic_lexer] | |
A | |
abort [Log.Messages] | user error stopping the plugin. |
abs [Integer] | |
abs [Float_sig.S] | |
abs [Float_interval_sig.S] | |
accept_c_comments_into_acsl_spec [Logic_lexer] | |
access [Db.From] | |
access [Db.Value] | |
access_expr [Db.Value] | |
access_location [Db.Value] | |
adapt_filename [Extlib] | Ensure that the given filename has the extension "cmo" in bytecode and "cmxs" in native |
add [Vector] | Element will be added at index |
add [Type.Obj_tbl] | |
add [Type.Ty_tbl] | |
add [Type.Heterogeneous_table] |
|
add [Task] | Auto-flush |
add [State_builder.Queue] | |
add [State_builder.Weak_hashtbl] |
|
add [State_builder.List_ref] | |
add [Rgmap] | Returns a new map with the added entry. |
add [Rangemap.S] |
|
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 [Map_lattice.MapSet_Lattice] |
|
add [Logic_env.Logic_builtin_used] | |
add [Logic_builtin] | |
add [Locations.Location_Bytes] |
|
add [Journal.Binding] |
|
add [Integer] | |
add [Indexer.Make] | Log complexity. |
add [Hptmap_sig.S] |
|
add [Globals.Functions] | TODO: remove this function and replace all calls by: |
add [Globals.Vars] | |
add [Float_sig.S] | |
add [Float_interval_sig.S] | |
add [FCSet.S_Basic_Compare] |
|
add [FCMap.S] |
|
add [Emitter.Make_table] | |
add [Dynamic.Parameter.StringList] | |
add [Dynamic.Parameter.StringSet] | |
add [Datatype.Sub_caml_weak_hashtbl] | |
add [Dataflow2.StmtStartData] | |
add [State_builder.Set_ref] | |
add [State_builder.Hashtbl] | Add a new binding. |
add [Cabshelper.Comments] | |
add [Bag] | |
add [Abstract_interp.Rel] | |
addAttribute [Cil] | Add an attribute. |
addAttributes [Cil] | Add a list of attributes. |
addOffset [Cil] |
|
addOffsetLval [Cil] | Add an offset at the end of an lvalue. |
addTermOffset [Logic_const] | Equivalent to |
addTermOffsetLval [Logic_const] | Equivalent to |
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 |
add_allocates_nothing_funspec [Allocates] | Adds |
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 [Lmap_bitwise.Location_map_bitwise] | |
add_base_value [Lmap_sig] | Creates the offsetmap described by |
add_behaviors [Annotations] | Add new behaviors into the given contract. |
add_binding [Lmap_sig] |
|
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_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_channel [FCBuffer] |
|
add_char [Sanitizer] | |
add_char [Rich_text] | Buffer-like |
add_char [FCBuffer] |
|
add_check [Annotations] | Add a checking assertion attached to the given statement. |
add_code_annot [Annotations] | Add a new code annotation attached to the given statement. |
add_code_transformation_after_cleanup [File] | Same as above, but the hook is applied after clean up. |
add_code_transformation_before_cleanup [File] |
|
add_codependencies [State_dependency_graph.S] | Add an edge in |
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 |
add_dependency [Hook.S_ordered] |
|
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_function_name_transformation [Parameter_customize] | Adds a mangling operation to allow writing user-friendly function names on command-line. |
add_global [Annotations] | Add a new global annotation into the program. |
add_group [Plugin.S_no_log] | Create a new group inside the plug-in. |
add_hook_on_remove [Emitter.Make_table] | Register a hook to be applied whenever a binding is removed from the table. |
add_hook_on_update [State_builder.S] | Add an hook which is applied each time (just before) the project library changes the local value of the state. |
add_hook_on_update [State] | Add an hook which is applied each time the project library changes the local value of the state. |
add_hook_on_update [Ast] | Apply the given hook each time the reference to the AST is updated, including on a project switch. |
add_identifier [Lexerhack] | |
add_identifier [Clexer] | Add a new string as a variable name |
add_int [Ival] | Addition of two integer (ie. |
add_int_under [Ival] | Underapproximation of the same operation |
add_list [Sanitizer] | Separated with |
add_listener [Log] | Register a hook that is called each time an event is emitted. |
add_logic_ctor [Logic_env] | |
add_logic_function [Logic_utils] | add a logic function in the environment. |
add_logic_function_gen [Logic_env] | add_logic_function_gen takes as argument a function eq_logic_info which decides whether two logic_info are identical. |
add_logic_info [Logic_typing.Lenv] | |
add_logic_label [Logic_typing.Lenv] | |
add_logic_type [Logic_env] | |
add_margin [Pretty_utils] | Updates the marger with new text dimension. |
add_model_field [Logic_env] | |
add_monotonic_state [Ast] | indicates that the given state (which must depend on Ast.self) is robust against additions to the AST, that is, it will be able to compute information on the new nodes whenever needed. |
add_offset_lval [Logic_typing] | |
add_once [Journal.Binding] | Same as function |
add_plugin_output_aliases [Plugin.S_no_log] | Adds aliases to the options -plugin-help, -plugin-verbose, -plugin-log, -plugin-msg-key, and -plugin-warn-key. |
add_requires [Annotations] | Add new requires clauses into the given behavior. |
add_result [Logic_typing] | add |
add_sep [Sanitizer] | Adds |
add_set_hook [Parameter_sig.S_no_parameter] | Add a hook to be called after the function |
add_singleton_int [Ival] | Addition of an integer ival with an integer. |
add_special_builtin [Cil] | register a new special built-in function |
add_special_builtin_family [Cil] | register a new family of special built-in functions. |
add_state [State_dependency_graph] | |
add_string [Sanitizer] | |
add_string [Rich_text] | Buffer-like |
add_string [FCBuffer] |
|
add_subbytes [FCBuffer] |
|
add_substitute [FCBuffer] |
|
add_substring [Rich_text] | Buffer-like |
add_substring [FCBuffer] |
|
add_symbolic_dir [Filepath] |
|
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] |
|
add_type [Lexerhack] | |
add_type [Clexer] | Add a new string as a type name |
add_type_var [Logic_typing.Lenv] | |
add_typename [Logic_env] | marks an identifier as being a typename in the logic |
add_update_hook [Parameter_sig.S_no_parameter] | Add a hook to be called when the value of the parameter changes (by
calling |
add_var [Logic_typing.Lenv] | |
add_var [Logic_typing] | adds a given variable in local environment. |
add_whole [Rangemap.Make] | |
addi [Vector] | Return index of added (last) element. |
address_of_value [Extlib] | |
all [Parameter_sig.Collection_category] | The '@all' category. |
all [Bottom] | |
all_addr_dpds [Db.Pdg] | Similar to |
all_call_preconditions_at [Statuses_by_call] |
|
all_ctrl_dpds [Db.Pdg] | Similar to |
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 |
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] |
|
allow_return_collapse [Cabs2cil] | Given a call |
analysis_options [Kernel] | |
anisotropic_cast [Offsetmap_lattice_with_isotropy] | Optionnally change the representation of the given value, under the
assumption that it fits in |
annot [Logic_typing.Make] | |
annot [Logic_parser] | |
annot [Logic_lexer] | |
annot_char [Clexer] | The character to recognize logic formulae in comments |
annotate_kf [Db.RteGen] | Generates RTE for a single function. |
annotation_visible [Filter.RemoveInfo] | tells if the annotation, attached to the given statement is visible. |
anonCompFieldName [Cabs2cil] | |
app_under_info [Cil] | Apply some function on underlying expression if Info or else on expression |
appears_in_expr [Cil] | |
append [Warning_manager] | Append a new message warning. |
append [Bag] | |
append_after [Parameter_sig.List] | append a list at the end of the current state |
append_after [Dynamic.Parameter.StringList] | |
append_before [Parameter_sig.List] | append a list in front of the current state |
append_before [Dynamic.Parameter.StringList] | |
append_here_label [Logic_typing] | appends the Here label in the environment |
append_init_label [Logic_typing] | appends the "Init" label in the environment |
append_old_and_post_labels [Logic_typing] | append the Old and Post labels in the environment |
append_pre_label [Logic_typing] | appends the "Pre" label in the environment |
apply [Logic_env.Builtins] | adds all requested objects in the environment. |
apply [Hook.S] | Apply all the functions of the hook on the given parameter. |
apply1 [Lattice_type.Lattice_Set] | |
apply2 [Lattice_type.Lattice_Set] | |
apply_after_computed [Ast] | Apply the given hook just after building the AST. |
apply_hooks_on_remove [Emitter.Make_table] | This function must be called on each binding which is removed from the
table without directly calling the function |
apply_once [State_builder] |
|
apply_set [Ival] | |
apply_set_unary [Ival] | |
apply_tag [Gtk_helper] | |
arch_bigendian [Unmarshal] | |
arch_sixtyfour [Unmarshal] | |
areCompatibleTypes [Cabs2cil] |
|
are_consistent [Structural_descr] | Not symmetrical: check that the second argument is a correct refinement of the first one. |
are_preconds_unfolded [Pretty_source] | |
arg_name [Parameter_sig.Input_with_arg] | A standard name for the argument which may be used in the description. |
argsToList [Cil] | Obtain the argument list ([] if None) |
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 [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] |
|
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 |
assigns_outputs_to_locations [Db.Value] | Evaluation of the left part of |
assigns_outputs_to_zone [Db.Value] | Evaluation of the left part of |
assoc [Json] | Extract the list of an |
assoc_opt [Transitioning.List] | 4.05 |
assq_opt [Transitioning.List] | 4.05 |
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 [Float_sig.S] | |
atan2 [Float_interval_sig.S] | |
atan2f [Floating_point] | |
attr [Cil_datatype.Global_annotation] | attributes tied to the global annotation. |
attr [Cil_datatype.Global] | |
attributeClass [Cil] | Return the class of an attributes. |
attributeName [Cil] | Returns the name of an attribute. |
automatically_proven [Property_status] | Is the status of the given property only automatically handled by the kernel? |
auxiliary_kf_stmt_state [Kernel_function] | |
B | |
back [History] | If possible, go back one step in the history. |
back_edges [Loop] | Statements that are the origin of a back-edge to a natural loop. |
backward_add [Float_interval_sig.S] | |
backward_cast [Float_interval_sig.S] | |
backward_cast_double_to_real [Fval] | |
backward_cast_float_to_double [Fval] |
|
backward_comp_float_left_false [Ival] | Same as |
backward_comp_float_left_true [Ival] | |
backward_comp_int_left [Ival] |
|
backward_comp_left_false [Float_interval_sig.S] |
|
backward_comp_left_true [Float_interval_sig.S] |
|
backward_is_finite [Float_interval_sig.S] | |
backward_is_not_nan [Float_interval_sig.S] | |
backward_mult_int_left [Ival] | |
backward_sub [Float_interval_sig.S] | |
band [Bitvector] | |
base_access [Locations] | Conversion into a base access, with the size information. |
behavior_assumes [Ast_info] | Builds the conjunction of the |
behavior_names_of_stmt_in_kf [Annotations] | |
behavior_postcondition [Ast_info] | Builds the postcondition from |
behavior_precondition [Ast_info] | Builds the precondition from |
behaviors [Annotations] | Get the behaviors clause of the contract associated to the given function. |
beq [Bitvector] | |
billion_one [Integer] | |
binary_predicate [Hptmap_sig.S] | Same functionality as |
bincopy [Command] |
|
bind [Task] |
|
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 |
bitsOffset [Cil] | Give a type of a base and an offset, returns the number of bits from the base address and the width (also expressed in bits) for the subobject denoted by the offset. |
bitsSizeOf [Cil] | The size of a type, in bits. |
bitsSizeOfBitfield [Cil] | Returns the size of the given type, in bits. |
bitsSizeOfInt [Cil] | |
bits_of_float32_list [Float_interval_sig.S] | Bitwise reinterpretation of a floating-point interval of single precision into consecutive ranges of integers. |
bits_of_float64_list [Float_interval_sig.S] | Bitwise reinterpretation of a floating-point interval of double precision into consecutive ranges of integers. |
bits_of_max_double [Floating_point] | binary representation of -DBL_MAX and DBL_MAX as 64 bits signed integers |
bits_of_max_float [Floating_point] | binary representation of -FLT_MAX and FLT_MAX as 32 bits signed integers |
bits_of_most_negative_double [Floating_point] | |
bits_of_most_negative_float [Floating_point] | |
bits_sizeof [Base] | |
bitwise_and [Ival] | |
bitwise_not [Ival] | |
bitwise_op2 [Bitvector] | |
bitwise_op3 [Bitvector] | |
bitwise_op4 [Bitvector] | |
bitwise_or [Ival] | |
bitwise_signed_not [Ival] | |
bitwise_unsigned_not [Ival] | |
bitwise_xor [Ival] | |
blit [FCBuffer] |
|
blit_buffer [FCBuffer] | Similar to |
blit_subbytes [FCBuffer] | Same as |
blit_substring [FCBuffer] | Same as |
block_from_unspecified_sequence [Cil] | creates a block with empty attributes from an unspecified sequence. |
block_of_local [Ast_info] |
|
blocks_closed_by_edge [Kernel_function] |
|
blocks_opened_by_edge [Kernel_function] |
|
bnot [Bitvector] | |
body_visible [Filter.RemoveInfo] | tells if the body of a function definition is visible. |
bool [Json] | Extract |
bool [Datatype] | |
boolean [Utf8_logic] | |
boolean_type [Logic_const] | |
bor [Bitvector] | |
bot_of_list [Bottom] | |
bottom [Utf8_logic] | |
bottom [Origin] | |
bottom [Map_lattice.MapSet_Lattice] | |
bottom [Map_lattice.Value] | |
bottom [Lmap_sig] | Every location is associated to the value |
bottom [Dataflows.JOIN_SEMILATTICE] | Must verify that forall a, join a bottom = a. |
bottom [Lattice_type.Bounded_Join_Semi_Lattice] | smallest element |
bottom_string [Unicode] | |
box [Wbox] | Generic packing. |
bprintf [Rich_text] | |
breakpoint [Project.Undo] | |
bs_identifier [Logic_lexer] | |
buffer [Source_viewer] | |
build_cil_file [Filter.F] | |
build_wto [Interpreted_automata.Compute] | Extract an exit strategy from a component, i.e. |
build_wto_index_table [Interpreted_automata.Compute] | Compute the index table from a wto |
builtinLoc [Cil] | This is used as the location of the prototypes of builtin functions. |
builtin_states [Logic_env] | |
builtin_types_as_typenames [Logic_env] | marks builtin logical types as logical typenames for the logic lexer. |
button [Gtk_form] | |
bxor [Bitvector] | |
bytesAlignOf [Cil] | The minimum alignment (in bytes) for a type. |
bytesSizeOf [Cil] | The size of a type, in bytes. |
bytesSizeOfInt [Cil] | Returns the number of bytes (resp. |
C | |
c_div [Integer] | Truncated division towards 0 (like in C99). |
c_div_rem [Integer] |
|
c_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.MapSet_Lattice] | |
cached_fold [Locations.Zone] | |
cached_fold [Locations.Location_Bytes] | Cached version of |
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 |
called_info [Filter.RemoveInfo] |
|
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] | 4.03 |
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 [Hptmap_sig.S] |
|
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_is_less_than [Ival] | Same than cardinal_less_than but just return if it is the case. |
cardinal_less_than [Locations.Location_Bytes] |
|
cardinal_less_than [Lattice_type.With_Enumeration] | Raises |
cardinal_less_than [Ival] |
|
cardinal_zero_or_one [Offsetmap_sig] | Returns |
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 [Integer] | |
cast_float_to_float [Ival] | Cast the given float to the given size. |
cast_float_to_int [Ival] | Casts the given float into an integer. |
cast_float_to_int_inverse [Ival] | floating-point |
cast_int_to_float [Ival] | |
cast_int_to_float [Float_interval_sig.S] | |
cast_int_to_float_inverse [Ival] | integer |
cast_int_to_int [Ival] | |
catch [Command] | |
category [Asm_contracts] | the corresponding code transformation category. |
ceil [Fval] | |
ceil [Float_sig.S] | |
ceil [Float_interval_sig.S] | |
cfgFun [Cfg] | Compute a control flow graph for fd. |
change_varinfo_name [Cil_const] |
|
char [Datatype] | |
charConstPtrType [Cil] | char const * |
charConstToInt [Cil] | Given the character c in a (CChr c), sign-extend it to 32 bits. |
charConstToIntConstant [Cil] | |
charPtrType [Cil] | char * |
charType [Cil] | char |
char_at [Rich_text] | |
check [Gtk_form] | |
check [Abstract_interp.Rel] | |
check_ast [Filecheck] | Visits the given AST (defaults to the AST of the current project) to check whether it is consistent. |
check_sequences [Undefined_sequence] | |
checks [Kernel] | |
childrenBehavior [Cil] | |
choose [Rangemap.S] | Return one binding of the given map, or raise |
choose [FCSet.S_Basic_Compare] | Return one element of the given set, or raise |
choose [FCMap.S] | Return one binding of the given map, or raise |
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_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 |
clear [Sanitizer] | |
clear [Qstack.Make] | Remove all the elements of a stack. |
clear [Project] | Clear the given project. |
clear [Pretty_source.Locs] | |
clear [Parameter_sig.S_no_parameter] | Set the option to its default value, that is the value if |
clear [Gtk_helper.Icon] | Reloads the builtin icons from the theme specified in the configuration. |
clear [FCBuffer] | Empty the buffer. |
clear [Dynamic.Parameter.Common] | |
clear [Hook.S] | Clear the hook. |
clear [Dataflow2.StmtStartData] | |
clear [State_builder.Ref] | Reset the reference to its default value. |
clear [State_builder.Hashtbl] | Clear the table. |
clear [Bitvector] | |
clear [Binary_cache.Arity_Three] | |
clear [Binary_cache.Arity_Two] | |
clear [Binary_cache.Arity_One] | |
clear [Binary_cache.Symmetric_Binary_Predicate] | |
clear [Binary_cache.Binary_Predicate] | |
clear [Binary_cache.Symmetric_Binary] | |
clearCFGinfo [Cfg] | clear the sid, succs, and preds fields of each statement in a function |
clearConfiguration [Cilconfig] | Clear all configuration data |
clearFileCFG [Cfg] | clear the sid (except when clear_id is explicitly set to false), succs, and preds fields of each statement. |
clear_all [Project] | Clear all the projects: all the internal states of all the projects are
now empty (wrt the action registered with
|
clear_breakpoint [Project.Undo] | |
clear_caches [Offsetmap_sig] | Clear the caches local to this module. |
clear_caches [Offsetmap_bitwise_sig] | Clear the caches local to this module. |
clear_caches [Lmap_sig] | Clear the caches local to this module. |
clear_caches [Lmap_bitwise.Location_map_bitwise] | Clear the caches local to this module. |
clear_caches [Hptmap_sig.S] | Clear all the persistent caches used internally by the functions of this module. |
clear_caches [Hptset.S] | Clear all the caches used internally by the functions of this module. |
clear_errors [Errorloc] | |
clear_funspec [Logic_utils] | Reset the given funspec to empty. |
clear_garbled_mix [Locations.Location_Bytes] | Clear the information on created garbled mix. |
clear_last_decl [Ast] | reset the mapping between a varinfo and the last global introducing it. |
clear_sid_info [Kernel_function] | removes any information related to statements in kernel functions. |
clear_some_projects [State.Local] |
|
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 |
cmp_ieee [Float_sig.S] | IEEE comparison: do not distinguish between -0.0 and 0.0. |
code_annot [Logic_typing.Make] |
|
code_annot [Db.Properties.Interp] | |
code_annot [Annotations] | Get all the code annotations attached to the given statement. |
code_annot_emitter [Annotations] | Same as |
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. |
codename [Config] | Frama-C version codename. |
collapse [Abstract_interp.Collapse] | |
collections [Parameter_state] | |
combinePredecessors [Dataflow2.ForwardsTransfer] | Take some old data for the given statement, and some new data for the same point. |
combineStmtStartData [Dataflow2.BackwardsTransfer] | When the analysis reaches the start of a block, combine the old data with the one we have just computed. |
combineSuccessors [Dataflow2.BackwardsTransfer] | Take the data from two successors and combine it |
command [Task] | Immediately launch a system-process. |
command [Command] | Same arguments as . |
command_async [Command] | Same arguments as . |
comment [Logic_lexer] | |
common_block [Kernel_function] |
|
compFullName [Cil] | Get the full name of a comp, including the 'struct' or 'union' prefix |
compare [Type] | |
compare [Transitioning.Stdlib] | |
compare [Project] | |
compare [Json] | Pervasives |
compare [Integer] | |
compare [Indexer.Elt] | |
compare [Hook.Comparable] | |
compare [Fval.F] | |
compare [Float_sig.S] | Comparison that distinguishes -0.0 and 0.0. |
compare [Float_interval_sig.S] | |
compare [FCSet.S_Basic_Compare] | Total ordering between sets. |
compare [FCMap.S] | Total ordering between maps. |
compare [Datatype.Make_input] | |
compare [Datatype.S_no_copy] | Comparison: same spec than |
compare [Datatype.Undefined] | |
compare [Datatype] | |
compare [Filepath.Normalized] | Compares normalized paths |
compare [Bitvector] | |
compare [Abstract_interp.Rel] | |
compareConstant [Cil] |
|
compare_basic [Extlib] | Use this function instead of |
compare_ignore_case [Extlib] | Case-insensitive string comparison. |
compare_predicate [Logic_utils] | |
compare_pretty [Filepath.Normalized] | Compares prettified (i.e. |
compare_term [Logic_utils] | comparison compatible with is_same_term |
compilation_unit_names [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 |
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 |
compute [Service_graph.S] | |
compute [Exn_flow] | computes the information if not already done. |
compute [Db.INOUTKF] | |
compute [Db.RteGen] | Same result as having |
compute [Db.PostdominatorsTypes.Sig] | |
compute [Db.From] | |
compute [Db.Value] | Compute the value analysis using the entry point of the current project. |
compute [Dataflow2.Backwards] | Fill in the T.stmtStartData, given a number of initial statements to start from (the sinks for the backwards data flow). |
compute [Dataflow2.Forwards] | Fill in the T.stmtStartData, given a number of initial statements to start from. |
compute [Ast] | Enforce the computation of the AST. |
computeFileCFG [Cfg] | Compute the CFG for an entire file, by calling cfgFun on each function. |
computeFirstPredecessor [Dataflow2.ForwardsTransfer] |
|
compute_all [Db.From] | |
compute_all_calldeps [Db.From] | |
compute_strategy [Dataflow2.Forwards] | Same as compute but using a given strategy, instead of the default strategy computed by the Wto module. |
compute_worklist [Dataflow2.Forwards] | Same as compute but using only a working list of statements instead of iterating on a weak topological ordering. |
concat [Bitvector] |
|
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] |
|
condition_truth_value [Db.Value] | Provided |
config_bool [Gtk_helper.Configuration] | |
config_float [Gtk_helper.Configuration] | |
config_int [Gtk_helper.Configuration] | |
config_string [Gtk_helper.Configuration] | |
config_values [Gtk_helper.Configuration] | The |
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 |
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 [Float_interval_sig.S] | |
contains_addresses_of_any_locals [Locations.Location_Bytes] |
|
contains_addresses_of_locals [Locations.Location_Bytes] |
|
contains_nan [Float_interval_sig.S] | |
contains_neg_infinity [Float_interval_sig.S] | |
contains_neg_zero [Float_interval_sig.S] | |
contains_non_zero [Ival] | |
contains_non_zero [Float_interval_sig.S] | |
contains_plus_zero [Fval] | |
contains_pos_infinity [Float_interval_sig.S] | |
contains_pos_zero [Float_interval_sig.S] | |
contains_result [Logic_utils] | true if \result is included in the term |
contains_single_elt [Hptset.S] | |
contains_zero [Ival] | contains the zero value (including -0. |
contents [Sanitizer] | |
contents [Rich_text] | Similar to |
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 [Command] |
|
copy [Datatype.S] | Deep copy: no possible sharing between |
copyCompInfo [Cil] | Makes a shallow copy of a |
copyVarinfo [Cil] | Make a shallow copy of a |
copy_and_rename [Parameter_category] |
|
copy_exp [Cil] | performs a deep copy of an expression (especially, avoid eid sharing). |
copy_offsetmap [Lmap_sig] |
|
copy_slice [Offsetmap_sig] |
|
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 [Float_sig.S] | |
cos [Float_interval_sig.S] | |
cosf [Floating_point] | |
count [State_builder.Weak_hashtbl] | Length of the table. |
create [Vector] | |
create [Type.Obj_tbl] | |
create [Type.Ty_tbl] | |
create [Type.Heterogeneous_table] |
|
create [Structural_descr.Recursive] | |
create [State_builder.Proxy] |
|
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 [State] | |
create [Sanitizer] | |
create [Rich_text] | Create a buffer. |
create [Rangemap.S] | |
create [Qstack.Make] | Create a new empty stack. |
create [Project] | Create a new project with the given name and attach it after the existing projects (so the current project, if existing, is unchanged). |
create [Printer_tag.Tag] | |
create [Pretty_source.Locs] | |
create [Parameter_category] |
|
create [Offsetmap_sig] |
|
create [Offsetmap_bitwise_sig] |
|
create [FCBuffer] |
|
create [Emitter] |
|
create [Datatype.Sub_caml_weak_hashtbl] | |
create [Bitvector] | Create a vector of |
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 |
create_by_copy_hook [Project] | Register a hook to call at the end of |
create_isotropic [Offsetmap_sig] | Same as |
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 |
create_set [Bitvector] | Create a vector of |
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 |
currentLoc [Errorloc] | |
currentLoc [Clexer] | |
current_loc [Origin.LocationLattice] | |
current_printer [Printer_api.S] | Returns the current pretty-printer, with all the extensions added
using |
custom [Logic_typing.Make] | |
custom_list [Gtk_helper.MAKE_CUSTOM_LIST] | |
custom_related_nodes [Db.Pdg] |
|
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. |
datadirs [Config] | Directories where architecture independent files are in order of priority. |
debug [Log.Messages] | Debugging information dedicated to Plugin developers. |
debug [Dataflow2.BackwardsTransfer] | Whether to turn on debugging |
debug [Dataflow2.ForwardsTransfer] | Whether to turn on debugging |
debug_atleast [Log.Messages] | |
decide_fast_inclusion [Hptmap_sig.S] | Function suitable for the |
decide_fast_intersection [Hptmap_sig.S] | Function suitable for the |
declare_markers [Design.Feedback] | Declares the icons used for the property status bullets, as marks in the left-margin of the source buffer. |
decreases [Annotations] | If any, get the decrease clause of the contract associated to the given function. |
def_or_last_decl [Ast] |
|
default [Parameter_sig.Collection_category] | The '@default' category. |
default [Lmap_bitwise.With_default] | |
default [Gtk_helper.Icon] | |
default [Cmdline.Group] | |
default_behavior_name [Cil] | |
default_edge_attributes [State_dependency_graph.Attributes] | |
default_icon [Widget] | |
default_msg_keys [Plugin] | Debug message keys set by default for the plugin. |
default_vertex_attributes [State_dependency_graph.Attributes] | |
default_widen_hints [Ival.Widen_Hints] | |
default_widen_hints [Float_sig.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 |
deprecated [Log.Messages] |
|
descr [Datatype.S_no_copy] | Datatype descriptor. |
diff [State_selection.S] | Difference between two selections. |
diff [Locations.Location_Bytes] | Over-approximation of difference. |
diff [Lattice_type.With_Diff] |
|
diff [FCSet.S_Basic_Compare] | Set difference. |
diff_if_one [Locations.Location_Bytes] | Over-approximation of difference. |
diff_if_one [Lattice_type.With_Diff_One] |
|
diff_with_shape [Hptmap_sig.S] |
|
digest [Type] | |
dir [Parameter_sig.Specific_dir] |
|
direct_addr_dpds [Db.Pdg] | Similar to |
direct_addr_uses [Db.Pdg] | Similar to |
direct_array_size [Ast_info] | |
direct_ctrl_dpds [Db.Pdg] | Similar to |
direct_ctrl_uses [Db.Pdg] | Similar to |
direct_data_dpds [Db.Pdg] | Similar to |
direct_data_uses [Db.Pdg] | Similar to |
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 |
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 [Float_sig.S] | |
div [Float_interval_sig.S] | |
dkey [Project_skeleton.Output] | |
dkey_alpha [Kernel] | |
dkey_alpha_undo [Kernel] | |
dkey_asm_contracts [Kernel] | |
dkey_ast [Kernel] | |
dkey_check [Kernel] | |
dkey_comments [Kernel] | |
dkey_compilation_db [Kernel] | |
dkey_dataflow [Kernel] | |
dkey_dataflow_scc [Kernel] | |
dkey_dominators [Kernel] | |
dkey_emitter [Kernel] | |
dkey_emitter_clear [Kernel] | |
dkey_exn_flow [Kernel] | |
dkey_file_annot [Kernel] | |
dkey_file_print_one [Kernel] | |
dkey_file_transform [Kernel] | |
dkey_filter [Kernel] | |
dkey_globals [Kernel] | |
dkey_kf_blocks [Kernel] | |
dkey_linker [Kernel] | |
dkey_linker_find [Kernel] | |
dkey_loops [Kernel] | |
dkey_name [Log.Messages] | returns the category name as a string. |
dkey_parser [Kernel] | |
dkey_pp [Kernel] | |
dkey_print_attrs [Kernel] | |
dkey_print_bitfields [Kernel] | |
dkey_print_builtins [Kernel] | |
dkey_print_logic_coercions [Kernel] | |
dkey_print_logic_types [Kernel] | |
dkey_print_sid [Kernel] | |
dkey_print_unspecified [Kernel] | |
dkey_print_vid [Kernel] | |
dkey_prop_status [Kernel] | |
dkey_prop_status_emit [Kernel] | |
dkey_prop_status_graph [Kernel] | |
dkey_prop_status_merge [Kernel] | |
dkey_prop_status_reg [Kernel] | |
dkey_referenced [Kernel] | |
dkey_rmtmps [Kernel] | |
dkey_task [Kernel] | |
dkey_typing_cast [Kernel] | |
dkey_typing_chunk [Kernel] | |
dkey_typing_global [Kernel] | |
dkey_typing_init [Kernel] | |
dkey_typing_pragma [Kernel] | |
dkey_ulevel [Kernel] | |
dkey_visitor [Kernel] | |
doEdge [Dataflow2.ForwardsTransfer] | what to do when following the edge between the two given statements. |
doGuard [Dataflow2.ForwardsTransfer] | Generate the successors |
doInstr [Dataflow2.BackwardsTransfer] | The (backwards) transfer function for an instruction. |
doInstr [Dataflow2.ForwardsTransfer] | The (forwards) transfer function for an instruction, internally
called by |
doStmt [Dataflow2.BackwardsTransfer] | The (backwards) transfer function for a branch. |
doStmt [Dataflow2.ForwardsTransfer] | The (forwards) transfer function for a statement. |
doVisit [Cil] |
|
doVisitList [Cil] | same as above, but can return a list of nodes |
do_all_rte [Db.RteGen] | Generates all possible RTE for a given function. |
do_iterate [Parameter_customize] | Ensure that |
do_not_iterate [Parameter_customize] | Prevent |
do_not_journalize [Parameter_customize] | Prevent journalization of the parameter. |
do_not_projectify [Parameter_customize] | Prevent projectification of the parameter: its state is shared by all the existing projects. |
do_not_reset_on_copy [Parameter_customize] | Prevents resetting the parameter to its default value when creating a project from a copy visitor. |
do_not_save [Parameter_customize] | Prevent serialization of the parameter. |
do_rte [Db.RteGen] | Generates all possible RTE except pre-conditions for a given function. |
do_tooltip [Gtk_helper] | Add the given tooltip to the given widget. |
do_track_garbled_mix [Locations.Location_Bytes] | |
dominates [Dominators] |
|
dot [Config] | Dot command name. |
doubleType [Cil] | double |
dropAttribute [Cil] | Remove all attributes with the given name. |
dropAttributes [Cil] | Remove all attributes with names appearing in the string list. |
dummy [State] | A dummy state. |
dummy [Project_skeleton] | |
dummy [Kernel_function] | |
dummy [Emitter] | |
dummy [Datatype.Filepath] | |
dummy [Cil_datatype.Varinfo] | |
dummy [Cil_datatype.Exp] | |
dummyFile [Cil] | A dummy file |
dummyInstr [Cil] | A instr to serve as a placeholder |
dummyStmt [Cil] | A statement consisting of just |
dummy_exp [Cil] | creates an expression with a dummy id. |
dummy_state_on_disk [State] | |
dummy_unique_name [State] | |
dump [State_dependency_graph.Dot] | |
dump [State_dependency_graph] | |
dump [Property_status.Consolidation_graph] | |
dump_messages [Messages] | Dump stored messages to standard channels |
dynamic [Descr] | Similar to |
E | |
e [Hptmap.Comp_unused] | |
e [Fval] | Real representation of \e. |
e_div [Integer] | Euclidean division (that returns a positive rem). |
e_div_rem [Integer] |
|
e_loc_of_stmt [Property] | create a Loc_contract or Loc_stmt depending on the kinstr. |
e_rem [Integer] | Remainder of the Euclidean division (always positive). |
e_rem [Abstract_interp.Rel] | |
echo [Log] | Display an event of the terminal, unless echo has been turned off. |
edge_attributes [State_dependency_graph.Attributes] | |
eight [Integer] | |
element_type [Ast_info] | |
elements [Leftistheap.Make] | the returned list is not sorted |
elements [FCSet.S_Basic_Compare] | Return the list of all elements of the given set. |
elements [Bag] | Might have |
elt [Bag] | |
emit [Property_status] |
|
emit [Lattice_messages] | Emit a message. |
emit_and_get [Property_status] | Like |
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 [Indexer.Make] | |
empty [Hptmap_sig.S] | the empty map |
empty [FCSet.S_Basic_Compare] | The empty set. |
empty [FCMap.S] | The empty map. |
empty [Bag] | |
empty [Lattice_type.Lattice_Set] | |
emptyFunction [Cil] | Make an empty function |
emptyFunctionFromVI [Cil] | Make an empty function from an existing global varinfo. |
empty_funspec [Cil] | |
empty_local_env [Cabs2cil] | an empty local environment. |
empty_map [Lmap_sig] | Empty map. |
empty_map [Lmap_bitwise.Location_map_bitwise] | |
empty_size_cache [Cil] | Create a fresh size cache with |
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] | |
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] |
|
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 [Json] | Pervasives |
equal [Integer] | |
equal [Hook.Comparable] | |
equal [Fval.F] | Those functions distinguish -0. |
equal [Float_interval_sig.S] | |
equal [FCSet.S_Basic_Compare] |
|
equal [FCMap.S] |
|
equal [Datatype.Make_input] | |
equal [Datatype.S_no_copy] | Equality: same spec than |
equal [Datatype.Undefined] | |
equal [Datatype] | |
equal [Filepath.Normalized] | |
equal [Bottom] | |
equal [Bitvector] | |
equal [Binary_cache.Cacheable] | |
equal [Abstract_interp.Rel] | |
equal_component [Wto.Make] | |
equal_partition [Wto.Make] | |
error [Task] | Extract error message form exception |
error [Log.Messages] | user error: syntax/typing error, bad expected input, etc. |
escape_char [Escape] | escape various constructs in accordance with C lexical rules |
escape_string [Escape] | |
escape_underscores [Pretty_utils] | |
escape_wchar [Escape] | |
escape_wstring [Escape] | |
eval_expr [Db.Value] | |
eval_expr_with_state [Db.Value] | |
eval_lval [Db.Value] | |
eval_predicate [Db.Value.Logic] | Evaluate the given predicate in the given states for the Pre and Here ACSL labels. |
evar [Cil] | Creates an expr representing the variable. |
evt_category [Log] | Split an event category into its constituants. |
exists [Utf8_logic] | |
exists [Rangemap.S] |
|
exists [Map_lattice.MapSet_Lattice] |
|
exists [Locations.Location_Bytes] | |
exists [Parameter_sig.Set] | Is there some element satisfying the given predicate? |
exists [Hptmap_sig.S] |
|
exists [FCSet.S_Basic_Compare] |
|
exists [FCMap.S] |
|
exists [Lattice_type.Lattice_Set] | |
exists2 [Rangemap.S] |
|
existsType [Cil] | Scans a type by applying the function on all elements. |
exit_kw_c_mode [Logic_utils] | |
exit_rt_type_mode [Logic_utils] | |
exit_strategy [Interpreted_automata.Compute] | Output the automaton in dot format |
exit_strategy [Interpreted_automata] | Output the automaton in dot format |
exp [Fval] | |
exp [Float_sig.S] | |
exp [Float_interval_sig.S] | |
expToAttrParam [Cil] | Convert an expression into an attrparam, if possible. |
exp_info_of_term [Cil] | Extracts term information in an expression information |
expand_to_path [Gtk_helper] | |
expf [Floating_point] | |
explodeStringToInts [Cabshelper] | |
expr [Db.Inputs] | |
expr_to_kernel_function [Db.Value] | |
expr_to_kernel_function_state [Db.Value] | |
expr_to_predicate [Logic_utils] | same as , but the result is a predicate. |
expr_to_term [Logic_utils] | translates a C expression into an "equivalent" logical term. |
expr_to_term_coerce [Logic_utils] | |
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 |
extension_category [Logic_env] | |
extract [Db.Pdg] | Pretty print pdg into a dot file. |
extract_bits [Offsetmap_lattice_with_isotropy] | Extract the bits between |
extract_bits [Ival] | Extract bits from |
extract_bits [Integer] | |
extract_contract [Logic_utils] | |
extract_free_logicvars_from_predicate [Cil] | extract |
extract_free_logicvars_from_term [Cil] | extract |
extract_labels_from_annot [Cil] | extract |
extract_labels_from_pred [Cil] | extract |
extract_labels_from_term [Cil] | extract |
extract_loop_pragma [Logic_utils] | |
extract_min [Leftistheap.Make] | runs in O(log n) |
extract_stmts_from_labels [Cil] | extract |
extract_varinfos_from_exp [Cil] | extract |
extract_varinfos_from_lval [Cil] | extract |
F | |
f [Hptmap.Comp_unused] | |
failed [Task] | The task that immediately fails by raising a |
failure [Log.Messages] | internal error of the plug-in. |
fast_equal [Rangemap.Value] |
|
fatal [Log.Messages] | internal error of the plug-in. |
fc_local_static [Cabs2cil] | Name of the attribute used to indicate that a given static variable has a local syntactic scope (despite a global lifetime). |
fct_info [Filter.RemoveInfo] | This function will be called for each function of the source program. |
fct_name [Filter.RemoveInfo] | useful when we want to have several functions in the result for one source function. |
feedback [Log.Messages] | Progress and feedback. |
field [Json] | Lookup a field in an object. |
file [Parameter_sig.Specific_dir] |
|
file [Logic_preprocess] | |
file [Logic_lexer] | |
file [Cparser] | |
filename [Command] | |
fill [Journal.Reverse_binding] | |
filter [Rangemap.S] |
|
filter [Qstack.Make] | Return all data of the stack satisfying the specified predicate. |
filter [Indexer.Make] | Linear. |
filter [Hptmap_sig.S] |
|
filter [FCSet.S_Basic_Compare] |
|
filter [FCMap.S] |
|
filter [Bag] | |
filter [Lattice_type.Lattice_Set] | |
filterAttributes [Cil] | Retains attributes with the given name |
filterStmt [Dataflow2.BackwardsTransfer] | Whether to put this predecessor block in the worklist. |
filter_base [Locations.Zone] |
|
filter_base [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 |
filter_keys [Map_lattice.MapSet_Lattice] | |
filter_map [Extlib] | |
filter_map' [Extlib] | Combines |
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] |
|
find [Vector] | Default exception is |
find [Type.Obj_tbl] | |
find [Type.Ty_tbl] | |
find [Type.Heterogeneous_table] |
|
find [State_builder.States] | |
find [State_builder.Weak_hashtbl] |
|
find [Rgmap] | Find the tightest entry containing the specified range. |
find [Rangemap.S] |
|
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.MapSet_Lattice] |
|
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] |
|
find [Globals.Vars] | |
find [FCSet.S_Basic_Compare] |
|
find [FCMap.S] |
|
find [Emitter.Make_table] | |
find [Db.From.Callwise] | |
find [Db.Value] | |
find [Dataflow2.StmtStartData] | |
find [State_builder.Hashtbl] | Return the current binding of the given key. |
find [Alarms] | |
findAttribute [Cil] | Returns the list of parameters associated to an attribute. |
findConfiguration [Cilconfig] | Find a configuration elements, given a key. |
findConfigurationBool [Cilconfig] | |
findConfigurationFloat [Cilconfig] | |
findConfigurationInt [Cilconfig] | Like findConfiguration but extracts the integer |
findConfigurationList [Cilconfig] | |
findConfigurationString [Cilconfig] | |
findOrCreateFunc [Cil] | Find a function or function prototype with the given name in the file. |
find_all [State_builder.Weak_hashtbl] |
|
find_all [Rgmap] | Find all entries containing the specified range. |
find_all [Project] | Find all projects with the given name. |
find_all [State_builder.Hashtbl] | Return the list of all data associated with the given key. |
find_all_enclosing_blocks [Kernel_function] | same as above, but returns all enclosing blocks, starting with the innermost one. |
find_all_enclosing_blocks [Globals] | |
find_all_inputs_nodes [Db.Pdg] | Get the nodes corresponding to all inputs. |
find_all_labels [Kernel_function] | returns all labels present in a given function. |
find_all_logic_functions [Logic_env] | |
find_all_model_fields [Logic_env] | returns all model fields of the same name. |
find_base [Lmap_sig] | |
find_base_or_default [Lmap_sig] | Same as |
find_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_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_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_decl_by_name [Globals.Functions] | |
find_decl_var_node [Db.Pdg] | Get the node corresponding the declaration of a local variable or a formal parameter. |
find_def [FCHashtbl.S] | |
find_def_by_name [Globals.Functions] | |
find_def_stmt [Cil] |
|
find_default_behavior [Cil] | |
find_default_requires [Cil] | |
find_defining_kf [Kernel_function] | Finds the kernel function defining the given varinfo as a local or a formal. |
find_deps_no_transitivity [Db.From] | |
find_deps_no_transitivity_state [Db.From] | |
find_deps_term_no_transitivity_state [Db.From] | |
find_enclosing_block [Kernel_function] | |
find_enclosing_block [Globals] | |
find_enclosing_loop [Kernel_function] |
|
find_enclosing_stmt_in_block [Kernel_function] |
|
find_englobing_kf [Kernel_function] | |
find_englobing_kf [Globals] | |
find_entry_point_node [Db.Pdg] | Find the node that represent the entry point of the function, i.e. |
find_enum_tag [Globals.Types] | Find an enum constant from its name in the AST. |
find_field_offset [Cabs2cil] | returns the offset (can be more than one field in case of unnamed members) corresponding to the first field matching the condition. |
find_first_stmt [Kernel_function] | Find the first statement in a kernel function. |
find_first_stmt [Globals] | |
find_float [Gtk_helper.Configuration] | Same as |
find_from_astinfo [Globals.Vars] | Finds a variable from its |
find_from_sid [Kernel_function] | |
find_fun_postcond_nodes [Db.Pdg] | Similar to |
find_fun_precond_nodes [Db.Pdg] | Similar to |
find_fun_variant_nodes [Db.Pdg] | Similar to |
find_imprecise [Offsetmap_sig] |
|
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_scope [Globals.Syntactic_search] |
|
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 |
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 |
find_location_nodes_at_end [Db.Pdg] | Same than |
find_location_nodes_at_stmt [Db.Pdg] | Find the nodes that define the value of the location at the given program point. |
find_logic_cons [Logic_env] | cons is a logic function with no argument. |
find_logic_ctor [Logic_env] | |
find_logic_info [Logic_typing.Lenv] | |
find_logic_label [Logic_typing.Lenv] | |
find_logic_type [Logic_env] | |
find_lonely_binding [Map_lattice.MapSet_Lattice_with_cardinality] | If |
find_lonely_binding [Map_lattice.Map_Lattice_with_cardinality] | If |
find_lonely_binding [Locations.Location_Bytes] | if there is only one binding |
find_lonely_key [Map_lattice.MapSet_Lattice] | If |
find_lonely_key [Map_lattice.Map_Lattice] | If |
find_lonely_key [Map_lattice.Map_Lattice_with_cardinality] | If |
find_lonely_key [Locations.Zone] | |
find_lonely_key [Locations.Location_Bytes] | if there is only one base |
find_lv_plus [Db.Value] | returns the list of all decompositions of |
find_model_field [Logic_env] |
|
find_next_true [Bitvector] |
|
find_offset [Bit_utils] |
|
find_opt [Transitioning.List] | 4.05 |
find_opt [FCMap.S] |
|
find_opt [FCHashtbl.S] | |
find_opt [Extlib] |
|
find_or_bottom [Map_lattice.Map_Lattice] |
|
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
|
find_stmt_node [Db.Pdg] | Get the node corresponding to the statement. |
find_stmts [Dataflow2] | |
find_string [Gtk_helper.Configuration] | Same as |
find_syntactic_callsites [Kernel_function] |
|
find_top_input_node [Db.Pdg] | |
find_type [Globals.Types] | Find a type from its name in the AST. |
find_type_var [Logic_typing.Lenv] | |
find_utf8 [Logic_lexer] | |
find_var [Logic_typing.Lenv] | |
finish [Clexer] | |
finishParsing [Errorloc] | Call this function to finish parsing and close the input channel |
fire [Wutil] | |
fitsInInt [Cil] | True if the integer fits within the kind's range |
flatten [Wto] | |
flatten_transient_sub_blocks [Cil] |
|
float [Json] | Convert |
float [Datatype] | |
floatKindForSize [Cil] | The float kind for a given size. |
floatType [Cil] | float |
float_zeros [Ival] | The lattice element containing exactly -0. |
floor [Fval] | |
floor [Float_sig.S] | |
floor [Float_interval_sig.S] | |
flush [Wutil] | |
flush [Task] | Clean all terminated tasks |
fmod [Float_sig.S] | |
fmod [Float_interval_sig.S] | |
fmodf [Floating_point] | |
fold [Type.Heterogeneous_table] | |
fold [Transitioning.Stack] | 4.03 |
fold [State_topological.Make] |
|
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 [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 |
fold [Offsetmap_bitwise_sig] | |
fold [Map_lattice.MapSet_Lattice] | |
fold [Locations.Location_Bytes.M] | |
fold [Lmap_sig] | |
fold [Lmap_bitwise.Location_map_bitwise] | The following fold_* functions, as well as |
fold [Leftistheap.Make] | elements are presented in an arbitrary order |
fold [Json] | Fold over all fields of the object. |
fold [Int_Intervals_sig] | Iterators |
fold [Hptmap_sig.S] |
|
fold [Globals.Functions] | |
fold [Globals.Vars] | |
fold [FCSet.S_Basic_Compare] |
|
fold [FCMap.S] |
|
fold [Emitter.Make_table] | |
fold [State_builder.Set_ref] | |
fold [State_builder.Hashtbl] | |
fold [Cabshelper.Comments] | |
fold [Alarms] | Folder over all alarms and the associated annotations at some program point. |
fold [Lattice_type.Lattice_Set] | |
fold [Abstract_interp.Int] | Fold the function on the value between |
fold2 [Rangemap.S] |
|
fold2_join_heterogeneous [Locations.Zone] | |
fold2_join_heterogeneous [Hptmap_sig.S] |
|
fold2_join_heterogeneous [Hptset.S] | |
foldGlobals [Cil] | Fold over all globals, including the global initializer |
foldLeftCompound [Cil] | Fold over the list of initializers in a Compound (not also the nested ones). |
fold_all_code_annot [Annotations] | Fold on each code annotation of the program. |
fold_allocates [Annotations] | Fold on the allocates of the corresponding behavior. |
fold_assigns [Annotations] | Fold on the assigns of the corresponding behavior. |
fold_assumes [Annotations] | Fold on the assumes of the corresponding behavior. |
fold_base [Lmap_bitwise.Location_map_bitwise] | |
fold_bases [Locations.Zone] |
|
fold_bases [Locations.Location_Bytes] | Fold on all the bases of the location, including |
fold_behaviors [Annotations] | Fold on the behaviors of the given kernel function. |
fold_between [Offsetmap_sig] |
|
fold_code_annot [Annotations] | Fold on each code annotation attached to the given statement. |
fold_complete [Annotations] | Fold on the complete clauses of the given kernel function. |
fold_decreases [Annotations] | apply f to the decreases term if any. |
fold_disjoint [Annotations] | Fold on the disjoint clauses of the given kernel function. |
fold_ensures [Annotations] | Fold on the ensures of the corresponding behavior. |
fold_enum [Locations.Location_Bytes] |
|
fold_enum [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_fuse_same [Lmap_bitwise.Location_map_bitwise] | Same behavior as |
fold_global [Annotations] | Fold on each global annotation of the program. |
fold_heads [Wto] | |
fold_i [Locations.Zone] |
|
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_bounds [Ival] | Given |
fold_int_decrease [Ival] | Iterate on the integer values of the ival in decreasing order. |
fold_itv [Offsetmap_bitwise_sig] | See documentation of |
fold_join_itvs [Offsetmap_bitwise_sig] |
|
fold_join_zone [Lmap_bitwise.Location_map_bitwise] |
|
fold_keys [Map_lattice.MapSet_Lattice] | |
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 |
fold_preconds_at_callsite [Pretty_source] | |
fold_range [Rangemap.Make] | |
fold_requires [Annotations] | Fold on the requires of the corresponding behavior. |
fold_rev [Hptmap_sig.S] |
|
fold_right [State_builder.Array] | |
fold_right [Bag] | |
fold_sorted [FCHashtbl.S] | Fold on the hashtbl, but respecting the order on keys induced
by |
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 |
fold_sorted_by_value [FCHashtbl.S] | Iter or fold on the hashtable, respecting the order on entries
given by |
fold_state_callstack [Db.Value] | |
fold_stmt_state_callstack [Db.Value] | |
fold_succ [State_selection.S] | Iterate over the successor of a state in a selection. |
fold_terminates [Annotations] | apply f to the terminates predicate if any. |
fold_topset_ok [Locations.Zone] |
|
fold_topset_ok [Locations.Location_Bytes] | Fold with offsets, including in the case |
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] |
|
for_all [Rangemap.S] |
|
for_all [Map_lattice.MapSet_Lattice] |
|
for_all [Locations.Location_Bytes] | |
for_all [Hptmap_sig.S] |
|
for_all [FCSet.S_Basic_Compare] |
|
for_all [FCMap.S] |
|
for_all [Lattice_type.Lattice_Set] | |
for_all2 [Rangemap.S] |
|
forall [Utf8_logic] | |
force_ast_compute [Parameter_builder] | |
force_brace [Printer_api.S_pp] |
|
force_dir [Parameter_sig.Specific_dir] | For functions below: if |
formal_args [Ast_info.Function] | Returns the list of the named formal arguments of a function. |
formatter [Rich_text] | |
formatter [Datatype] | |
forward [History] | If possible (ie. |
forward_cast [Float_interval_sig.S] | |
forward_comp [Float_interval_sig.S] | |
forward_comp_int [Ival] | |
four [Integer] | |
frama_c_destructor [Cabs2cil] | Name of the attribute used to store the function that should be called when the corresponding variable exits its scope. |
frama_c_display [Service_graph] | must be set to |
frama_c_init_obj [Cil] | a formal marked with this attribute is known to be a pointer to an object being initialized by the current function, which can thus assign any sub-object regardless of const status. |
frama_c_keep_block [Cabs2cil] | Name of the attribute inserted by the elaboration to prevent user blocks from disappearing. |
frama_c_mutable [Cil] | a field struct marked with this attribute is known to be mutable, i.e. |
framac_icon [Gtk_helper] | |
framac_libc [Config] | Directory where Frama-C libc headers are. |
framac_logo [Gtk_helper] | |
frank [Cil] | Returns a unique number representing the floating-point conversion rank. |
fresh_behavior_name [Annotations] | |
fresh_code_annotation [Logic_const] | |
fresh_global [Cabs2cil] |
|
fresh_predicate_id [Logic_const] | |
fresh_term_id [Logic_const] | |
from_compare [Datatype] | Must be used for |
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 |
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_pred [Db.Properties.Interp.To_zone] | Entry point to get zones needed to evaluate the |
from_preds [Db.Properties.Interp.To_zone] | Entry point to get zones needed to evaluate the list of
|
from_pretty_code [Datatype] | Must be used for |
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 |
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
|
from_term [Db.Properties.Interp.To_zone] | Entry point to get zones needed to evaluate the |
from_terms [Db.Properties.Interp.To_zone] | Entry point to get zones needed to evaluate the list of |
from_unique_name [Project] | Return a project based on |
from_zone [Db.Properties.Interp.To_zone] | Entry point to get zones needed to evaluate the |
fround [Fval] | |
fround [Floating_point] | Rounds to nearest integer, away from zero (like round() in C). |
fround [Float_sig.S] | |
fround [Float_interval_sig.S] | |
fst [Lattice_type.Lattice_Product] | |
full [State_selection] | The selection containing all the states. |
full_command [Command] | Same arguments as but returns only when execution is complete. |
full_command_async [Command] | Same arguments as . |
full_compare [Description] | Completes |
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 |
fun_postcond_visible [Filter.RemoveInfo] | |
fun_precond_visible [Filter.RemoveInfo] | |
fun_set_args [Db.Value] | Specify the arguments to use. |
fun_use_default_args [Db.Value] | |
fun_variant_visible [Filter.RemoveInfo] | |
func [Datatype] | |
func2 [Datatype] | |
func3 [Datatype] | |
func4 [Datatype] | |
funcExitData [Dataflow2.BackwardsTransfer] | The data at function exit. |
function_env [Dataflows] | |
fundec_category [Parameter_builder] | |
funspec [Logic_typing.Make] |
|
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 |
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 |
generic_predicate [Hptmap_sig.S] |
|
generic_symmetric_predicate [Hptmap_sig.S] | Same as |
get [Vector] | Raise |
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 [Db.Sparecode] | Remove in each function what isn't used to compute its outputs,
or its annotations when |
get [Db.Pdg] | Get the PDG of a function. |
get [Db.From] | |
get [State_builder.Ref] | Get the referenced value. |
get [Cabshelper.Comments] | |
get [Ast.UntypedFiles] | The list of untyped AST that have been parsed. |
get [Ast] | Get the cil file representation. |
getAlphaPrefix [Alpha] | Split the name in preparation for newAlphaName. |
getCompField [Cil] | Return a named fieldinfo in compinfo, or raise Not_found |
getFormalsDecl [Cil] | Get the formals of a function declaration registered with
|
getReturnType [Cil] | Takes as input a function type (or a typename on it) and return its return type. |
get_all [File] | Return the list of toplevel files. |
get_all_block_last_stmts [Stmts_graph] | |
get_all_block_out_edges [Stmts_graph] | |
get_all_categories [Log.Messages] | returns all registered categories. |
get_all_status [Db.RteGen] | |
get_all_stmt_last_stmts [Stmts_graph] | Find the last statements in |
get_all_stmt_out_edges [Stmts_graph] | Like |
get_all_warn_categories [Log.Messages] | |
get_all_warn_categories_status [Log.Messages] | |
get_astinfo [Globals.Vars] | Linear in the number of locals and formals of the program. |
get_automaton [Interpreted_automata.Compute] | Get the interpreted automaton for the given kernel_function. |
get_automaton [Interpreted_automata] | Get the interpreted automaton for the given kernel_function without annotations |
get_bases [Locations.Location_Bytes] | Returns the bases the location may point to. |
get_behavior [Property] | |
get_behavior_names [Logic_utils] | |
get_block_in_edges [Stmts_graph] | |
get_block_last_stmts [Stmts_graph] | |
get_block_stmts [Stmts_graph] | |
get_bool_value_status [Db.RteGen] | |
get_c_ified_functions [Parameter_customize] | Function names can be modified (aka mangled) from the original source to valid C identifiers. |
get_called [Kernel_function] | Returns the static call to function |
get_category [Log.Messages] | returns the corresponding registered category or |
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 |
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_source [Log] | |
get_current_source_view [Source_manager] | Returns the source viewer for the currently displayed tab |
get_debug_keys [Log.Messages] | Returns currently active keys |
get_debug_keyset [Log.Messages] | Returns currently active keys |
get_definition [Kernel_function] | |
get_definitionloc [Cabshelper] | |
get_descr [State] | |
get_description [Alarms] | Long description of the alarm, explaining the UB it guards against. |
get_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 |
get_finite_float_status [Db.RteGen] | |
get_flags [Json_compilation_database] | |
get_float_to_int_status [Db.RteGen] | |
get_fold [Parameter_category] | Fold over the elements of the given category. |
get_formal_position [Kernel_function] |
|
get_formals [Kernel_function] | |
get_from_name [Plugin] | Get a plug-in from its name. |
get_from_shortname [Plugin] | Get a plug-in from its shortname. |
get_function_name [Parameter_sig.String] | returns the given argument only if it is a valid function name
(see |
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_initialized_status [Db.RteGen] | |
get_instance [Type.Polymorphic4] | |
get_instance [Type.Polymorphic3] | |
get_instance [Type.Function] | |
get_instance [Type.Polymorphic2] | |
get_instance [Type.Polymorphic] |
|
get_internal [Db.INOUTKF] | Inputs/Outputs with local and formal variables |
get_internal_precise [Db.Operational_inputs] | More precise version of |
get_kernel_function [Cil] | |
get_keys [Map_lattice.MapSet_Lattice] | Returns the set of keys in |
get_kf [Property] | |
get_kf_exn [Exn_flow] | returns the set of exceptions that a given kernel function might throw. |
get_kinstr [Property] | |
get_locals [Kernel_function] | |
get_location [Kernel_function] | |
get_logic_info [Cil] | |
get_logic_type_info [Cil] | |
get_logic_var [Cil] | |
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 (not normalized). |
get_name [Emitter.Usable_emitter] | |
get_name [Emitter] | |
get_name [Ast_info.Function] | |
get_name [Alarms] | Short name of the alarm, used to prefix the assertion in the AST. |
get_naturals [Loop] | |
get_non_naturals [Loop] | |
get_operator [Cprint] | |
get_option [State_builder.Option_ref] | |
get_optional_argument [Type.Function] | |
get_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_pane_ratio [Wutil] | |
get_parameter [Dynamic.Parameter] | retrieve the representation of the corresponding parameter. |
get_params [Globals.Functions] | |
get_plain_string [Parameter_sig.String] | always return the argument, even if the argument is not a function name. |
get_pointerCall_status [Db.RteGen] | |
get_possible_values [Parameter_sig.String] | What are the acceptable values for this parameter. |
get_pred_body [Logic_utils] | returns the body of the given predicate. |
get_preprocessor_command [File] | Return the preprocessor command to use. |
get_prop_basename [Property.Names] | returns the basename of the property. |
get_prop_basename [Property.LegacyNames] | |
get_prop_name_id [Property.Names] | returns a unique name identifying the property. |
get_prop_name_id [Property.LegacyNames] | |
get_range [Parameter_sig.Int] | What is the possible range of values for this parameter. |
get_reset_selection [Parameter_state] | Selection of resettable parameters in case of copy with a visitor. |
get_return_type [Kernel_function] | |
get_rounding_mode [Floating_point] | |
get_selection [Parameter_state] | Selection of all the settable parameters. |
get_selection_context [Parameter_state] | Selection of all the parameters that may have an impact on some analysis. |
get_session_file [Journal] | |
get_short_name [Alarms] | Even shorter name. |
get_sid [Ast_info] | |
get_signedOv_status [Db.RteGen] | |
get_signed_downCast_status [Db.RteGen] | |
get_small_cardinal [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_statics [Kernel_function] | Returns the list of static variables declared inside the function. |
get_stmt [Cil] | |
get_stmt_in_edges [Stmts_graph] | Find the entry edges that go inside |
get_stmt_last_stmts [Stmts_graph] | Subset of |
get_stmt_state [Db.Value] | |
get_stmt_state_callstack [Db.Value] | |
get_stmt_stmts [Stmts_graph] | Get the statements that compose |
get_subgraph [State_dependency_graph.Attributes] | |
get_suffixes [File] | |
get_symbols [Globals.FileIndex] | All global C symbols of the given module. |
get_termination_kind_name [Cil_printer] | |
get_toolbar_index [Gtk_compat] | |
get_type [Kernel_function] | |
get_type_specifier [Gui_printers] | Returns the base type for a pointer/array, otherwise |
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_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_warn_category [Log.Messages] | |
get_warn_status [Log.Messages] | |
get_with_formals [Db.Inputs] | Inputs with formals and without local variables |
get_wto [Interpreted_automata] | Extract an exit strategy from a component, i.e. |
get_wto_index [Interpreted_automata.Compute] | |
get_wto_index [Interpreted_automata] | |
get_wto_index_diff [Interpreted_automata.Compute] | |
get_wto_index_diff [Interpreted_automata] | |
getident [Cabshelper] | |
getword [Unmarshal] | |
ghost_local_env [Cabs2cil] | same as |
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 [Dgraph_helper] | |
graph_window_through_dot [Dgraph_helper] | Create a new window displaying a graph, by printing dot commands. |
gt [Integer] | |
gui_unlocked [Gtk_helper] | This is a mutex you may use to prevent running some code while the GUI is locked. |
H | |
h [Wbox] |
|
had_errors [Errorloc] | Has an error been raised since the last call to |
hasAttribute [Cil] | True if the named attribute appears in the attribute list. |
has_code_annot [Annotations] | |
has_extern_local_init [Cil] | returns |
has_flexible_array_member [Cil] |
|
has_greater_min_bound [Ival] |
|
has_greater_min_bound [Float_interval_sig.S] |
|
has_smaller_max_bound [Ival] |
|
has_smaller_max_bound [Float_interval_sig.S] |
|
has_some [Extlib] |
|
has_status [Property] | Does the property has a logical status (which may be Never_tried)? False for pragma, assumes clauses and some ACSL extensions. |
hash [Type] | |
hash [Project] | |
hash [Logic_lexer] | |
hash [Integer] | |
hash [Hook.Comparable] | |
hash [Float_sig.S] | |
hash [Float_interval_sig.S] | |
hash [FCHashtbl] | |
hash [Datatype.Make_input] | |
hash [Datatype.S_no_copy] | Hash function: same spec than |
hash [Datatype.Undefined] | |
hash [Datatype] | |
hash [Bitvector] | |
hash [Binary_cache.Cacheable] | |
hash [Abstract_interp.Rel] | |
hash_param [FCHashtbl] | |
hash_predicate [Logic_utils] | |
hash_term [Logic_utils] | hash function compatible with is_same_term |
hashcons [State_builder.Hashcons] | Injection as an hashconsed value. |
hbox [Wbox] | Pack a list of boxes horizontally. |
height [Rangemap.Make] | |
help [Plugin.S_no_log] | The group containing option -*-help. |
help [Parameter_sig.Input] | A description for this option (e.g. |
here_label [Logic_const] | |
hgroup [Wbox] | Pack a list of widgets horizontally, with all widgets stuck to the same width |
hide_typename [Logic_env] | marks temporarily a typename as being a normal identifier in the logic |
hilite [Pretty_source] | |
host_to_term_host [Logic_utils] | |
howto_marshal [State_builder.S] |
|
hscroll [Wbox] | Same as |
html_escape [Extlib] | |
hv [Wbox] |
|
I | |
id [Unmarshal] | Use this function when you don't want to change the value unmarshaled by input_val. |
id [State_builder.Hashcons] | Id of an hashconsed value. |
id [Kernel_function] | |
id [Hptmap_sig.S] | Bijective function. |
id [Extlib] | identity function. |
id [Cil_datatype.Kf] | |
id [Hptmap.Id_Datatype] | Identity of a key. |
id [Base.Base] | |
id [Base] | |
identity [Datatype] | Must be used if you want to implement a required function by |
idx [Qstack.Make] | |
iff [Utf8_logic] | |
ignored_recursive_call [Db.Value] | This functions returns true if the value analysis found and ignored a recursive call to this function during the analysis. |
image_menu_item [Gtk_helper] | calls the packing function to append a new menu item with an icon and a label. |
implies [Utf8_logic] | |
imprecise_write_msg [Offsetmap_sig] | The message "more than N <imprecise_msg_write>. |
imprecise_write_msg [Lmap_bitwise.Location_map_bitwise] | |
in_degree [State_topological.G] | |
inbound [Gtk_helper.MAKE_CUSTOM_LIST] | |
incr [Transitioning.Stdlib] | |
incr [Parameter_sig.Int] | Increment the integer. |
incr [Dynamic.Parameter.Int] | |
increm [Cil] | Increment an expression. |
increm64 [Cil] | Increment an expression. |
index [Indexer.Make] | raise Not_found. |
info [Datatype] | |
init [Transitioning.Dynlink] | |
init [Logic_builtin] | |
init [Dataflows.FORWARD_MONOTONE_PARAMETER] | The initial value for each statement. |
init [Dataflows.BACKWARD_MONOTONE_PARAMETER] | The initial state after each statement. |
init [Clexer] | |
initCIL [Cil] | Call this function to perform some initialization, and only after you have
set |
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] |
|
initial [Clexer] | This is the main lexing function |
inject [Map_lattice.MapSet_Lattice] | Returns the singleton map binding |
inject [Locations.Zone] | |
inject [Locations.Location_Bytes] | |
inject [Lattice_type.Lattice_Base] | |
inject [Lattice_type.Lattice_Product] | |
inject [Int_Intervals_sig] | |
inject [Int_Base] | |
inject [Fval] |
|
inject [Float_interval_sig.S] |
|
inject [Lattice_type.Lattice_Set] | |
inject_bounds [Int_Intervals_sig] | |
inject_float [Locations.Location_Bytes] | |
inject_float [Ival] | |
inject_float_interval [Ival] | |
inject_interval [Ival] | Builds the set of integers between |
inject_itv [Int_Intervals_sig] | |
inject_ival [Locations.Location_Bytes] | |
inject_range [Ival] |
|
inject_singleton [Ival] | |
inject_singleton [Fval] | |
inject_singleton [Lattice_type.Lattice_Set] | |
inject_t1 [Lattice_type.Lattice_Sum] | |
inject_t2 [Lattice_type.Lattice_Sum] | |
inject_top_origin [Locations.Location_Bytes] |
|
inline_calls [Inline] | |
inline_predicate [Inline] | Inlines predicates and logic functions in a predicate. |
inline_term [Inline] |
|
inout_source [Kernel] | |
inplace_visit [Cil] | In-place modification. |
input_string [Gtk_helper] | Copied from lablgtk |
input_val [Unmarshal] |
|
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. |
instantiate [Logic_const] | instantiate type variables in a logic type. |
int [Json] | Convert |
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] |
|
intPtrType [Cil] | int * |
intType [Cil] | int |
intTypeIncluded [Cil] |
|
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 |
inter [FCSet.S_Basic_Compare] | Set intersection. |
inter_with_shape [Hptmap_sig.S] |
|
internal_pretty_code [Datatype.Make_input] | |
internal_pretty_code [Datatype.S_no_copy] | Same spec than |
internal_pretty_code [Datatype.Undefined] | |
internal_pretty_code [Datatype] | |
interp_boolean [Ival] | |
interpret [Cparser] | |
interpret_character_constant [Cil] | gives the value of a char literal. |
intersects [Locations.Zone] | |
intersects [Lattice_type.With_Intersects] |
|
intersects [Hptset.S] |
|
inv [Abstract_interp.Comp] | Inverse relation: |
inv_truth [Abstract_interp] | |
invalidStmt [Cil] | An empty statement. |
invalid_part [Locations] | Overapproximation of the invalid part of a location |
ip_all_of_behavior [Property] |
|
ip_allocation_of_behavior [Property] |
|
ip_assigns_of_behavior [Property] |
|
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_decreases_of_spec [Property] | Builds IPDecrease of a given spec. |
ip_disjoint_of_spec [Property] |
|
ip_ensures_of_behavior [Property] | Builds the IPPredicate PKEnsures corresponding to a behavior. |
ip_from_of_behavior [Property] |
|
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_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_decreases [Property] | Builds IPDecrease |
ip_of_disjoint [Property] |
|
ip_of_ensures [Property] | IPPredicate of single ensures. |
ip_of_extended [Property] | Extended property. |
ip_of_from [Property] | Builds the corresponding IPFrom (if not FromAny) |
ip_of_global_annotation [Property] | |
ip_of_global_annotation_single [Property] | |
ip_of_requires [Property] | IPPredicate of a single requires. |
ip_of_spec [Property] |
|
ip_of_terminates [Property] | |
ip_other [Property] | Create a non-standard property. |
ip_post_cond_of_behavior [Property] |
|
ip_post_cond_of_spec [Property] |
|
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. |
isAnyCharArrayType [Cil] | True if the argument is an array of a character type (i.e. |
isAnyCharPtrType [Cil] | True if the argument is a pointer to a character type (i.e. |
isAnyCharType [Cil] | True if the argument is a character type (i.e. |
isArithmeticOrPointerType [Cil] | True if the argument is an arithmetic or pointer type (i.e. |
isArithmeticType [Cil] | True if the argument is an arithmetic type (i.e. |
isArrayType [Cil] | True if the argument is an array type |
isBitfield [Cil] | Is an lvalue a bitfield? |
isBoolType [Cil] | True if the argument is |
isCharArrayType [Cil] | True if the argument is an array of a character type (i.e. |
isCharConstPtrType [Cil] | True if the argument is a pointer to a constant character type, e.g. |
isCharPtrType [Cil] | True if the argument is a pointer to a plain character type
(but neither |
isCharType [Cil] | True if the argument is a plain character type
(but neither |
isCompleteProgramRoot [Rmtmps] | |
isCompleteType [Cil] | Returns true if this is a complete type. |
isConstType [Cil] | Check for |
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. |
isExportedRoot [Rmtmps] | |
isExtern [Cabshelper] | |
isFloatingType [Cil] | True if the argument is a floating point type. |
isFunPtrType [Cil] | True if the argument is a function pointer type. |
isFunctionType [Cil] | True if the argument is a function type |
isInline [Cabshelper] | |
isInteger [Cil] | True if the given expression is a (possibly cast'ed) character or an integer constant |
isIntegerConstant [Cil] | True if the expression is a compile-time integer constant |
isIntegralOrPointerType [Cil] | True if the argument is an integral or pointer type. |
isIntegralType [Cil] | True if the argument is an integral type (i.e. |
isLogicAnyCharType [Logic_utils] | |
isLogicArithmeticType [Cil] | True if the argument is a logic arithmetic type (i.e. |
isLogicArrayType [Logic_utils] | Predefined tests over types |
isLogicBooleanType [Cil] | True if the argument is a boolean type, either integral C type or mathematical boolean one. |
isLogicCType [Logic_const] |
|
isLogicCharType [Logic_utils] | |
isLogicFloatType [Cil] | True if the argument is a floating point type. |
isLogicFunPtrType [Cil] | True if the argument is the logic function pointer type. |
isLogicFunctionType [Cil] | True if the argument is the logic function type. |
isLogicIntegralType [Cil] | True if the argument is an integral type (i.e. |
isLogicNull [Cil] | True if the given term is |
isLogicPointer [Logic_utils] |
|
isLogicPointerType [Logic_utils] | |
isLogicPureBooleanType [Cil] | True if the argument is |
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] |
|
isLogicVoidPointerType [Logic_utils] | |
isLogicVoidType [Logic_utils] | |
isLogicZero [Cil] | True if the term is the constant 0 |
isPointerType [Cil] | True if the argument is a pointer type. |
isShortType [Cil] | True if the argument is a short type (i.e. |
isSigned [Cil] | Returns the signedness of the given integer kind depending on the current machdep. |
isSignedInteger [Cil] | |
isStatic [Cabshelper] | |
isStructOrUnionType [Cil] | True if the argument is a struct of union type |
isTypeTagType [Cil] | True if the argument is the type for reified C types. |
isTypedef [Cabshelper] | |
isUnsignedInteger [Cil] | |
isVariadicListType [Cil] | True if the argument denotes the type of ... |
isVoidPtrType [Cil] | is the given type "void *"? |
isVoidType [Cil] | is the given type "void"? |
isVolatileLogicType [Cil] | Check for |
isVolatileLval [Cil] | Check if the l-value has a volatile part |
isVolatileTermLval [Cil] | Check if the l-value has a volatile part |
isVolatileType [Cil] | Check for |
isZero [Cil] | True if the given expression is a (possibly cast'ed) integer or character constant with value zero |
is_C_array [Logic_utils] |
|
is_abstract [Descr] | |
is_accessible [Db.Value] | |
is_aligned_by [Base] | |
is_any_formal_or_local [Base] | |
is_any_local [Base] | |
is_arithmetic_type [Logic_typing] | |
is_array_type [Logic_typing] | |
is_assert [Logic_utils] | |
is_assigns [Logic_utils] | |
is_attr_test [Cabshelper] | |
is_back_edge [Interpreted_automata.Compute] | |
is_back_edge [Interpreted_automata] | |
is_between [Kernel_function] |
|
is_block_local [Base] | |
is_block_local [Ast_info] | determines if a var is local to a block. |
is_boolean_type [Logic_const] | |
is_bottom [Locations.Zone] | |
is_bottom [Locations.Location_Bytes] | |
is_bottom [Lmap_bitwise.Location_map_bitwise] | |
is_bottom [Ival] | |
is_bottom [Bottom] | |
is_bottom_loc [Locations] | |
is_builtin [Cil] | |
is_builtin_logic_ctor [Logic_env] | |
is_builtin_logic_function [Logic_env] | |
is_builtin_logic_type [Logic_env] | |
is_c_keyword [Clexer] |
|
is_called [Db.Value] | |
is_case_label [Cil] | Return |
is_cea_domain_function [Ast_info] | |
is_cea_dump_file_function [Ast_info] | |
is_cea_dump_function [Ast_info] | |
is_cea_function [Ast_info] | |
is_check [Logic_utils] | |
is_computed [State_builder.S] | Returns |
is_computed [Db.From] | Check whether the from analysis has been performed for the given function. |
is_computed [Db.Value] | Return |
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_current [Project] | Check whether the given project is the current one or not. |
is_debug_key_enabled [Log.Messages] | Returns |
is_def_or_last_decl [Ast] |
|
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_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 [History] | Does the history contain an event. |
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_exact [Float_sig.S] | Is the representation of floating-point numbers of a given precision
exact? Should at least be false for |
is_exit_status [Logic_const] |
|
is_extension [Logic_env] | |
is_finite [Fval.F] | Returns true if the float is a finite number. |
is_finite [Float_sig.S] | |
is_finite [Float_interval_sig.S] | |
is_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_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 |
is_function [Base] | |
is_function_type [Ast_info] | Return |
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 [Lmap_sig] | |
is_included [Lattice_type.Join_Semi_Lattice] | is first argument included in the second? |
is_included [Float_interval_sig.S] | |
is_included [Dataflows.JOIN_SEMILATTICE] | Must verify: a is_included b <=> a join b = b. |
is_included [Bottom] | |
is_infinite [Float_sig.S] | |
is_instance_of [Type.Polymorphic4] | |
is_instance_of [Type.Polymorphic3] | |
is_instance_of [Type.Function] | |
is_instance_of [Type.Polymorphic2] | |
is_instance_of [Type.Polymorphic] | |
is_instance_of [Logic_utils] |
|
is_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 |
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_modifiable_lval [Cil] | indicates whether the given lval is a modifiable lvalue in the sense of the C standard 6.3.2.1§1. |
is_mutable_or_initialized [Cil] |
|
is_nan [Float_sig.S] | |
is_natural [Loop] | |
is_negative [Float_sig.S] | Is a number negative? Never called on NaN, but must be correct on infinities and zeros. |
is_negative [Float_interval_sig.S] |
|
is_non_natural [Loop] | |
is_non_null_expr [Ast_info] | |
is_not_nan [Float_interval_sig.S] | |
is_null [Base] | |
is_null_expr [Ast_info] | |
is_null_term [Ast_info] | |
is_one [Ival] | |
is_one [Integer] | |
is_permissive_ref [Parameter_customize] | if |
is_plain_type [Logic_const] |
|
is_pointer_type [Logic_typing] | |
is_postdominator [Db.PostdominatorsTypes.Sig] | |
is_pragma [Logic_utils] | |
is_present [Plugin] | Whether a plug-in already exists. |
is_property_pragma [Logic_utils] | Should this pragma be proved by plugins |
is_reachable [Lmap_sig] | |
is_reachable [Db.Value] | |
is_reachable_stmt [Db.Value] | |
is_read_only [Base] | Is the base valid as a read/write location, or only for reading. |
is_registered_category [Log.Messages] | true iff the string corresponds to a registered category |
is_relationable [Locations.Location_Bytes] |
|
is_relative [Filepath] | returns true if the file is relative to |
is_result [Logic_utils] | true if the term is \result or an offset of \result. |
is_result [Logic_const] |
|
is_rt_type_mode [Logic_utils] | |
is_running [Task] | Don't make the thread progress, just returns |
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 [Offsetmap_bitwise_sig] |
|
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 |
is_share_visible [Plugin] | Make visible to the end-user the -<plug-in>-share option. |
is_signed_int_enum_pointer [Bit_utils] |
|
is_single_interval [Offsetmap_sig] |
|
is_single_interval [Offsetmap_bitwise_sig] |
|
is_singleton [Hptmap_sig.S] |
|
is_singleton [Fval] | Returns |
is_singleton [Float_interval_sig.S] | Returns |
is_singleton_int [Ival] | |
is_skip [Cil] | |
is_slice_pragma [Logic_utils] | |
is_special_builtin [Cil] | |
is_stmt_invariant [Logic_utils] | |
is_subcategory [Log] | Sub-category checks. |
is_top [Origin] | |
is_top [Lmap_sig] | |
is_top [Int_Intervals_sig] | |
is_top [Int_Base] | |
is_transient_block [Cil] | tells whether the block has been marked as transient |
is_trivial_annotation [Logic_utils] | |
is_trivially_false [Logic_utils] |
|
is_trivially_true [Logic_utils] |
|
is_unmarshable [Descr] | |
is_unrollable_ltdef [Logic_const] | |
is_unused_builtin [Cil] | |
is_valid [Locations] | Is the given location entirely valid, without any access or as a destination for a read or write access. |
is_valid_offset [Base] |
|
is_variant [Logic_utils] | |
is_warn_category [Log.Messages] | |
is_weak [Base] | Is the given base a weak one (in the sens that its validity is |
is_weak_validity [Base] |
|
is_wto_head [Interpreted_automata.Compute] | |
is_wto_head [Interpreted_automata] | |
is_zero [Locations.Location_Bytes] | |
is_zero [Ival] | |
is_zero [Integer] | |
is_zero [Int_Base] | |
is_zero [Abstract_interp.Rel] | |
is_zero_comparable [Logic_utils] |
|
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 [State_selection.S] | Iterate over a selection. |
iter [State_builder.States] | iterates a function |
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 [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 [Messages] | Iter over all stored messages. |
iter [Logic_env.Logic_builtin_used] | |
iter [Locations.Location_Bytes.M] | |
iter [Lmap_sig] | |
iter [Journal.Reverse_binding] | |
iter [Int_Intervals_sig] | May raise |
iter [Indexer.Make] | Linear. |
iter [Hptmap_sig.S] |
|
iter [Globals.Functions] | |
iter [Globals.Vars] | |
iter [FCSet.S_Basic_Compare] |
|
iter [FCMap.S] |
|
iter [Emitter.Make_table] | |
iter [Dynamic.Parameter.StringList] | |
iter [Dynamic.Parameter.StringSet] | |
iter [Dynamic] | |
iter [Db.From.Callwise] | |
iter [Dataflow2.StmtStartData] | |
iter [State_builder.Set_ref] | |
iter [State_builder.Hashtbl] | |
iter [Cabshelper.Comments] | |
iter [Bag] | |
iter [Alarms] | Iterator over all alarms and the associated annotations at some program point. |
iter [Lattice_type.Lattice_Set] | |
iter2 [Rangemap.S] |
|
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_requires [Annotations] | Iter on the requires of the corresponding behavior. |
iter_sorted [FCHashtbl.S] | Iter on the hashtbl, but respecting the order on keys induced
by |
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] |
|
iteri [Vector] | |
iteri [State_builder.Array] | |
iteri [Indexer.Make] | Linear. |
iteri [Extlib] | Same as iter, but the function to be applied take also as argument the index of the element (starting from 0). |
J | |
job [Task] | |
join [Origin] | |
join [Offsetmap_bitwise_sig] | |
join [Lmap_sig] | |
join [Lattice_type.Join_Semi_Lattice] | over-approximation of union |
join [Hptmap_sig.S] | Same as |
join [Float_interval_sig.S] | |
join [Dataflows.JOIN_SEMILATTICE] | Must be idempotent (join a a = a), commutative, and associative. |
join [Bottom.Top] | |
join [Bottom] | |
join_and_is_included [Dataflows.JOIN_SEMILATTICE] | This function is used by the dataflow algorithm to determine if something has to be recomputed. |
join_list [Bottom] | |
K | |
keepUnused [Rmtmps] | |
keep_file [Journal] | This function has not to be used explicitly. |
kernel [Emitter] | The special emitter corresponding to the kernel. |
kernel_channel_name [Log] | the reserved channel name used by the Frama-C kernel. |
kernel_function_of_local_var_or_param_varinfo [Globals.FileIndex] | kernel_function where the local variable or formal parameter is declared. |
kernel_label_name [Log] | the reserved label name used by the Frama-C kernel. |
kf [Dataflows.FUNCTION_ENV] | |
kf_category [Parameter_builder] | |
kf_decl_category [Parameter_builder] | |
kf_def_category [Parameter_builder] | |
kf_of_localizable [Printer_tag] | |
kf_of_localizable [Pretty_source] | |
kf_string_category [Parameter_builder] | |
kfloat [Cil] | Constructs a floating point constant. |
ki_of_localizable [Printer_tag] | |
ki_of_localizable [Pretty_source] | |
kind [Fval] | Classify a |
kinstr [Db.INOUT] | |
kinstr_of_opt_stmt [Cil_datatype.Kinstr] | |
kinteger [Cil] | Construct an integer of a given kind. |
kinteger64 [Cil] | Construct an integer of a given kind without literal representation. |
kprintf [Rich_text] | |
ksfprintf [Pretty_utils] | similar to Format.kfprintf, but the continuation is given the result string instead of a formatter. |
kw_c_mode [Logic_utils] | |
L | |
label [Wbox] | Helper to pack a |
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 |
later [Wutil] | Post the action on next idle. |
later [Task] | The task that, when started, compute a task to continue with. |
launch [Task] | Starts the server if not running yet |
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 [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 [Origin] | |
link [Lattice_type.With_Under_Approximation] | under-approximation of union |
list [Json] | Extract the list of an |
list [Datatype] | |
list [Bag] | |
list_compare [Extlib] | Generic list comparison function, where the elements are compared with the specified function |
list_first_n [Extlib] |
|
list_of_bot [Bottom] | |
list_of_opt [Extlib] | converts an option into a list with 0 or 1 elt. |
list_slice [Extlib] |
|
list_union [State_selection.S] | Union of an arbitrary number of selection (0 gives an empty selection) |
lmone [Cil] | The constant logic term -1. |
load [Project] | Load a file into a new project given by its name. |
load [Gtk_helper.Configuration] | |
loadConfiguration [Cilconfig] | Load the configuration from a file |
load_all [Project] | First remove all the existing project, then load all the projects from a file. |
load_channel [Json] | Parses the stream until EOF. |
load_file [Source_manager] | If |
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 |
loc_of_localizable [Printer_tag] | Might return |
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 |
loc_to_loc_without_size [Locations] | |
loc_to_localizable [Pretty_source] | return the (hopefully) most precise localizable that contains the given Filepath.position. |
loc_to_lval [Db.Properties.Interp] | |
loc_to_offset [Db.Properties.Interp] | |
loc_var_visible [Filter.RemoveInfo] | tells if the local variable is visible. |
localizable_from_locs [Pretty_source] | Returns the lists of localizable in |
locate_localizable [Pretty_source] | |
location [Property] | returns the location of the property. |
loffset_contains_result [Logic_utils] | true if \result is included in the offset. |
log [Log.Messages] | Generic log routine. |
log [Fval] | |
log [Float_sig.S] | |
log [Float_interval_sig.S] | |
log10 [Fval] | |
log10 [Float_sig.S] | |
log10 [Float_interval_sig.S] | |
log10f [Floating_point] | |
log_channel [Log] | logging function to user-created channel. |
log_redirector [Gtk_helper] | Redirects all strings written to the terminal and call the given function on each. |
logand [Integer] | |
logf [Floating_point] | |
logicCType [Logic_utils] | |
logicConditionalConversion [Cabs2cil] | returns the type of the result of a logic operator applied to values of the corresponding input types. |
logic_info_of_global [Annotations] | |
logical_consequence [Property_status] |
|
lognot [Integer] | |
logor [Integer] | |
logwith [Log.Messages] | Recommanded generic log routine using |
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] | 4.03 |
lowercase_ascii [Transitioning.String] | 4.03 |
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] |
|
lzero [Cil] | The constant logic term zero. |
M | |
machdep_macro [File] |
|
major_version [Config] | Frama-C major version number. |
make [Warning_manager] | Build a new widget for storing the warnings. |
make [Source_viewer] | Build a new source viewer. |
make [Source_manager] | |
make [Project_skeleton.Make_setter] | |
make [Filetree] | Create a file tree packed in the given tree_view. |
makeFormalVar [Cil] | Make a formal variable for a function declaration. |
makeFormalsVarDecl [Cil] | creates a new varinfo for the parameter of a prototype. |
makeGlobalVar [Cil] | Make a global variable. |
makeLocalVar [Cil] | Make a local variable and add it to a function's slocals and to the given block (only if insert = true, which is the default). |
makeTempVar [Cil] | Make a temporary variable and add it to a function's slocals. |
makeVarinfo [Cil] | Make a varinfo. |
makeZeroInit [Cil] | Make a initializer for zero-ing a data type |
make_formatter [Gtk_helper] | Build a formatter that redirects its output to the given buffer. |
make_loc [Locations] | |
make_logic_info [Cil_const] | Create a fresh logical (global) variable giving its name and type. |
make_logic_info_local [Cil_const] | Create a new local logic variable given its name. |
make_logic_var [Cil_const] | Create a fresh logical variable giving its name and type. |
make_logic_var_formal [Cil_const] | Create a new formal logic variable |
make_logic_var_global [Cil_const] | Create a new global logic variable |
make_logic_var_kind [Cil_const] | Create a fresh logical variable giving its name, type and origin. |
make_logic_var_local [Cil_const] | Create a new local logic variable |
make_logic_var_quant [Cil_const] | Create a new quantified logic variable |
make_marker_attributes [GSourceView] | |
make_set_type [Logic_const] | converts a type into the corresponding set type if needed. |
make_string_list [Gtk_helper] | |
make_tag [Gtk_helper] | |
make_temp_logic_var [Cil] | Make a temporary variable to use in annotations |
make_text_page [Gtk_helper] | Insert a GText.view in a new page of the notebook with the given title,
at position |
make_type [Datatype.Hashtbl] | |
make_type_list_of [Logic_const] |
|
make_unique_name [Project_skeleton.Make_setter] | |
make_unique_name [Extlib] |
|
make_view_column [Gtk_helper.MAKE_CUSTOM_LIST] | |
map [Vector] | Result is shrunk. |
map [Task] | |
map [State_builder.Option_ref] | |
map [Rangemap.S] |
|
map [Qstack.Make] | Replace in-place all the elements of the stack by mapping the old one. |
map [Offsetmap_bitwise_sig] | |
map [Map_lattice.MapSet_Lattice] | |
map [Lmap_bitwise.Location_map_bitwise] | |
map [Hptmap_sig.S] |
|
map [FCMap.S] |
|
map [Bag] | |
map' [Hptmap_sig.S] | Same as |
map2 [Offsetmap_bitwise_sig] | See the documentation of function |
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] |
|
mapGlobals [Cil] | Map over all globals, including the global initializer and change things in place |
mapNoCopy [Cil] | Like map but try not to make a copy of the list |
mapNoCopyList [Cil] | Like map but each call can return a list. |
map_on_values [Offsetmap_sig] |
|
map_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 |
mapi [FCMap.S] | Same as |
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 |
marger [Pretty_utils] | Create an empty marger |
mark [Design.Feedback] |
|
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 |
mark_as_computed [Db.Value] | Indicate that the value analysis has been done already. |
mark_as_computed [Ast] | |
mark_as_grown [Ast] | call this function whenever you have added something to the AST, without modifying the existing nodes |
max [Transitioning.Stdlib] | |
max [Integer] | |
max_binding [Rangemap.S] | Same as |
max_binding [Hptmap_sig.S] | |
max_binding [FCMap.S] | Same as |
max_bit_address [Bit_utils] | |
max_bit_size [Bit_utils] | |
max_byte_address [Bit_utils] | |
max_byte_size [Bit_utils] | |
max_cpt [Extlib] |
|
max_elt [FCSet.S] | Same as , but returns the largest element of the given set. |
max_int [Ival] | A |
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_map [Extlib] |
|
may_reach [Locations.Location_Bytes] |
|
meet [Origin] | |
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 [Rangemap.S] |
|
mem [Qstack.Make] | Return |
mem [Parameter_sig.Multiple_map] | |
mem [Parameter_sig.Map] | |
mem [Logic_env.Logic_builtin_used] | |
mem [Parameter_sig.Set] | Does the given element belong to the set? |
mem [Indexer.Make] | Log complexity. |
mem [Hptmap_sig.S] |
|
mem [FCSet.S_Basic_Compare] |
|
mem [FCMap.S] |
|
mem [Emitter.Make_table] | |
mem [Dataflow2.StmtStartData] | |
mem [State_builder.Set_ref] | |
mem [State_builder.Hashtbl] | |
mem [Bitvector] | |
mem [Lattice_type.Lattice_Set] | |
mem_base [Locations.Zone] |
|
mem_builtin [Db.Value] | returns whether there is an abstract function registered by
|
mem_project [Datatype.Make_input] | |
mem_project [Datatype.S_no_copy] |
|
mem_project [Datatype.Undefined] | |
mem_project [Datatype] | |
memo [State_builder.Option_ref] | Memoization. |
memo [FCHashtbl.S] |
|
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 [Rangemap.S] |
|
merge [Property_status] |
|
merge [Mergecil] | |
merge [Lmap_sig] |
|
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 [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_behaviors [Logic_utils] | |
merge_distinct_bits [Offsetmap_lattice_with_isotropy] | Merge the bits of the two given values, that span disjoint bit ranges by construction. |
merge_funspec [Logic_utils] |
|
merge_neutral_element [Offsetmap_lattice_with_isotropy] | Value that can be passed to |
merge_opt [Extlib] |
|
message [Rich_text] | Buffer contents, with its formatting tags. |
messages [Plugin.S_no_log] | The group containing options -*-debug and -*-verbose. |
min [Transitioning.Stdlib] | |
min [Leftistheap.Make] | runs in O(1) |
min [Integer] | |
min_and_max [Ival] | Returns the minimal and maximal integers represented by an ival. |
min_and_max [Float_interval_sig.S] | Returns the bounds of the float interval, (or None if the argument is exactly NaN), and a boolean indicating the possibility that the value may be NaN. |
min_and_max_float [Ival] | returns the bounds of the float interval, (or None if the argument is exactly NaN), and a boolean indicating the possibility that the value may be NaN. |
min_binding [Rangemap.S] | Return the smallest binding of the given map (with respect to the
|
min_binding [Hptmap_sig.S] | |
min_binding [FCMap.S] | Return the smallest binding of the given map
(with respect to the |
min_denormal [Floating_point] | |
min_elt [FCSet.S] | Return the smallest element of the given set
(with respect to the |
min_int [Ival] | A |
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] | |
minor_version [Config] | Frama-C minor version number. |
minus [Utf8_logic] | |
minus_one [Ival] | The lattice element that contains only the integer -1. |
minus_one [Integer] | |
minus_one [Int_Base] | |
minus_zero [Fval] | |
missingFieldDecl [Cabshelper] | |
missingFieldName [Cil] | This is a constant used as the name of an unnamed bitfield. |
mkAddrOf [Cil] | Make an AddrOf. |
mkAddrOfAndMark [Cabs2cil] | Applies |
mkAddrOfVi [Cil] | Creates an expression corresponding to "&v". |
mkAddrOrStartOf [Cil] | Like mkAddrOf except if the type of lval is an array then it uses StartOf. |
mkAttrAnnot [Cil] | returns the complete name for an attribute annotation. |
mkBinOp [Cil] | makes a binary operation and performs const folding. |
mkBinOp_safe_ptr_cmp [Cil] | same as |
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 |
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 |
mkFor [Cil] | Make a for loop for(start; guard; next) { ... |
mkForIncr [Cil] | Make a for loop for(i=start; i<past; i += incr) { ... |
mkLoop [Cil] | Make a loop. |
mkMem [Cil] | Make a Mem, while optimizing AddrOf. |
mkPureExpr [Cil] | Create an instruction as above, enclosed in a block
of a single ( |
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 |
mkString [Cil] | Make an expression that is a string constant (of pointer type) |
mkTermMem [Cil] | Equivalent to |
mk_behavior [Cil] | |
mk_behavior [Cabshelper] | |
mk_cast [Logic_utils] | creates a logic cast if required, with some automatic simplifications being performed automatically. |
mk_cast [Logic_typing.Make] | |
mk_ctx_func_contrat [Db.Properties.Interp.To_zone] | To build an interpretation context relative to function contracts. |
mk_ctx_stmt_annot [Db.Properties.Interp.To_zone] | To build an interpretation context relative to statement annotations. |
mk_ctx_stmt_contrat [Db.Properties.Interp.To_zone] | To build an interpretation context relative to statement contracts. |
mk_fun [Extlib] | Build a reference to an uninitialized function |
mk_labeled_fun [Extlib] | To be used to initialized a reference over a labeled function. |
mk_logic_AddrOf [Logic_utils] | creates an AddrOf from a TLval. |
mk_logic_StartOf [Logic_utils] | creates a TStartOf from an TLval. |
mk_logic_pointer_or_StartOf [Logic_utils] | creates either a TStartOf or the corresponding TLval. |
mkassign [Ast_info] | |
mkassign_statement [Ast_info] | |
mkdir [Extlib] |
|
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 [Kernel.Input_with_arg] | |
module_name [Datatype.Functor_info] | Must be a valid OCaml module name corresponding to the module name you are defining by applying the functor. |
mone [Cil] | -1 |
most_negative_single_precision_float [Floating_point] | |
move_at_end [Qstack.Make] | Move the element |
move_at_top [Qstack.Make] | Move the element |
msvcMode [Cprint] | |
msvcMode [Cil] | |
msvc_x86_64 [Machdeps] | |
mul [Ival] | |
mul [Integer] | |
mul [Float_sig.S] | |
mul [Float_interval_sig.S] | |
must_recompute_cfg [File] |
|
mutex [Task] | |
N | |
name [Type.Polymorphic4_input] | |
name [Type.Polymorphic3_input] | |
name [Type.Polymorphic2_input] | |
name [Type.Polymorphic_input] | How to build a name for each monomorphic instance of the type value from the underlying type. |
name [Type] | |
name [State_builder.Info] | Name of the internal state. |
name [State_builder.S] | |
name [Datatype.Make_input] | Unique name for this datatype. |
name [Datatype.S_no_copy] | Unique name of the datatype. |
name [Dataflow2.BackwardsTransfer] | For debugging purposes, the name of the analysis |
name [Dataflow2.ForwardsTransfer] | For debugging purposes, the name of the analysis |
name [Cmdline.Group] | |
nan [Float_interval_sig.S] | The NaN singleton |
narrow [Origin] | |
narrow [Offsetmap_sig.Make_Narrow] | Over-approximation of the intersection of abstract values, without considering (bitwise) reinterpretations. |
narrow [Lmap_sig.Make_Narrow] | |
narrow [Lattice_type.With_Narrow] | over-approximation of intersection |
narrow [Float_interval_sig.S] | |
narrow [Bottom.Top] | |
narrow [Bottom] | |
narrow_reinterpret [Offsetmap_sig.Make_Narrow] | Variant of the function above that bitwise-reinterprets values before performing the intersection (in order to get normal forms). |
nativeint [Datatype] | |
nb_errors [Messages] | |
nb_messages [Messages] | Number of stored warning messages, error messages, or all messages. |
nb_stmts [Dataflows.FUNCTION_ENV] | |
nb_warnings [Messages] | |
nearest_common_ancestor [Dominators] | Finds the statement lowest in the function that dominates all the statements in the list passed as argument. |
nearest_elt_ge [FCSet.S] |
|
nearest_elt_le [FCSet.S] |
|
need_cast [Cil] |
|
neg [Utf8_logic] | |
neg [Integer] | |
neg [Int_Base] | |
neg [Float_sig.S] | |
neg [Float_interval_sig.S] | |
neg_int [Ival] | Negation of an integer ival. |
neg_min_denormal [Floating_point] | |
neg_min_single_precision_denormal [Floating_point] | |
negative_integers [Ival] | The lattice element that contains exactly the negative or null integers |
neq [Utf8_logic] | |
never_any_project [Datatype] | Must be used for |
never_write [Journal] |
|
newAlphaName [Alpha] | Create a new name based on a given name. |
new_acsl_extension [Logic_const] | creates a new acsl_extension with a fresh id. |
new_channel [Log] | |
new_code_annotation [Logic_const] | creates a code annotation with a fresh id. |
new_exp [Cil] | creates an expression with a fresh id |
new_file_type [File] |
|
new_identified_term [Logic_const] | creates a new identified term with a fresh id |
new_machdep [File] |
|
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_float [Fval.F] | First double strictly above the argument. |
next_float [Float_sig.S] | First value above the argument in the given precision. |
nextafter [Floating_point] | |
nextafterf [Floating_point] | |
nextident [Cabshelper] | |
no_category [Parameter_customize] | Prevent a collection parameter to use categories and the extension '+', and '-' mechanism. |
no_element_of_string [Parameter_sig.Builder] | |
no_op_coerce [Cil] |
|
no_results [Db.Value] | Returns |
node_key [Db.Pdg] | |
non_bottom [Bottom] | |
none [Parameter_sig.Collection_category] | The category '@none' |
nop [Task] | The task that immediately returns unit |
nop [Extlib] | Do nothing. |
nop [Cmdline] | |
normalisation [Kernel] | |
normalization_parameters [Kernel] | All the normalization options that influence the AST (in particular, changing one will reset the AST entirely.contents |
normalize [Filepath] | Returns an absolute path leading to the given file. |
not_yet_implemented [Logic_interp.To_zone] | |
not_yet_implemented [Log.Messages] | raises |
notify [Log] | Send an event over the associated listeners. |
nth [Qstack.Make] | |
nth [FCBuffer] | get the n-th character of the buffer. |
nth_opt [Transitioning.List] | 4.05 |
null [Unmarshal] | recursive values cannot be completely formed at the time they are passed to their transformation function. |
null [Pretty_utils] | Prints nothing. |
null [Log] | Prints nothing. |
null [Base] | |
null_set [Base] | Set containing only the base |
nullprintf [Pretty_utils] | Discards the message and returns unit. |
nullprintf [Log] | Discards the message and returns unit. |
number_to_color [Extlib] | |
numeric_coerce [Logic_utils] |
|
O | |
o_loc_of_stmt [Property] | create a Loc_contract or Loc_stmt depending on the kinstr. |
ocaml_wflags [Config] | Warning flags used when compiling Frama-C. |
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] | |
of_float [Fval.F] | fails on NaNs, but allows infinities. |
of_float [Float_sig.S] | Converts a caml float into a floating-point number of the given precision. |
of_int [Json] | |
of_int [Ival] | |
of_int [Integer] | |
of_int32 [Integer] | |
of_int64 [Ival] | |
of_int64 [Integer] | |
of_lexing_loc [Cil_datatype.Location] | |
of_lexing_pos [Cil_datatype.Position] | |
of_list [State_selection] | The selection containing only the given list of states. |
of_list [Offsetmap_sig] |
|
of_list [Leftistheap.Make] | |
of_list [Json] | |
of_list [FCSet.S_Basic_Compare] |
|
of_pack [Structural_descr] | |
of_singleton_string [Parameter_sig.String_datatype_with_collections] | If a single string can be mapped to several elements. |
of_string [Parameter_sig.Multiple_value_datatype] | |
of_string [Parameter_sig.Value_datatype] |
|
of_string [Parameter_sig.String_datatype_with_collections] | |
of_string [Parameter_sig.String_datatype] | |
of_string [Json] | |
of_string [Integer] | |
of_string [Datatype.Filepath] | |
of_string [Filepath.Normalized] |
|
of_string_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 |
off [Dynamic.Parameter.Bool] | Set the parameter to |
offset_to_term_offset [Logic_utils] | |
old_gtk_compat [Gtk_helper] | Catch exception |
old_label [Logic_const] | |
on [Wutil] | |
on [Project] |
|
on [Parameter_sig.Bool] | Set the boolean to |
on [Dynamic.Parameter.Bool] | Set the parameter to |
on_bool [Gtk_helper] | Pack a check button |
on_combo [Gtk_helper] | Pack a string-selector |
on_current_history [History] |
|
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_string [Gtk_helper] | Pack a string chooser |
on_string_completion [Gtk_helper] | |
on_string_set [Gtk_helper] | Pack a string-set chooser |
once [Wutil_once] | |
once [Wutil] | |
once [Bitvector] | return |
one [Ival] | The lattice element that contains only the integer 1. |
one [Integer] | |
one [Int_Base] | |
one [Cil] | 1 |
oneret [Oneret] | Make sure that there is only one Return statement in the whole body. |
onethousand [Integer] | |
only_codependencies [State_selection.S] | The selection containing all the co-dependencies of the given state (but not this state itself). |
only_dependencies [State_selection.S] | The selection containing all the dependencies of the given state (but not this state itself). |
open_in_external_viewer [Gtk_helper] | Opens |
optMapNoCopy [Cil] | same as mapNoCopy for options |
opt_bind [Extlib] |
|
opt_compare [Extlib] | |
opt_conv [Extlib] |
|
opt_equal [Extlib] | |
opt_filter [Extlib] | |
opt_fold [Extlib] | |
opt_hash [Extlib] | |
opt_if [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] |
|
osizeof [Bit_utils] |
|
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_graph [Service_graph.S] | |
output_to_dot [Interpreted_automata.UnrollUnnatural] | |
output_to_dot [Interpreted_automata.Compute] | |
output_to_dot [Interpreted_automata] | |
overlaps [Locations] | Is there a possibly non-empty intersection between two given locations?
If |
overlaps [Ival] | |
P | |
p_abstract [Structural_descr] | Equivalent to |
p_bool [Structural_descr] | |
p_float [Structural_descr] | |
p_int [Structural_descr] | |
p_int32 [Structural_descr] | |
p_int64 [Structural_descr] | |
p_nativeint [Structural_descr] | |
p_string [Structural_descr] | |
p_unit [Structural_descr] | |
pack [Structural_descr] | Pack a structural descriptor in order to embed it inside another one. |
pack [Descr] | |
packed_descr [Fval.F] | |
packed_descr [Float_sig.S] | |
packed_descr [Float_interval_sig.S] | |
packed_descr [Datatype.S_no_copy] | Packed version of the descriptor. |
pair [Datatype] | |
pallocable [Logic_const] | \allocable |
pand [Logic_const] | && |
pands [Logic_const] | Folds && over a list of predicates. |
panel [Wbox] | Helper to create a full featured window:
|
papp [Logic_const] | application of predicate |
par [Type] |
|
par_ty_name [Type] |
|
param_visible [Filter.RemoveInfo] | tells if the n-th formal parameter is visible. |
parameter [Parameter_sig.S] | |
parameters [Parameter_sig.Builder] | |
parse [Frontc] | the main command to parse a file. |
parse [Floating_point] |
|
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] | |
parsing [Kernel] | |
partition [Wto.Make] | Implements Bourdoncle "Efficient chaotic iteration strategies with widenings" algorithm to compute a WTO. |
partition [Rangemap.S] |
|
partition [FCSet.S_Basic_Compare] |
|
partition [FCMap.S] |
|
partition [Bag] | |
partitionAttributes [Cil] | Partition the attributes into classes:name attributes, function type, and type attributes |
paste_offsetmap [Lmap_sig] |
|
paste_slice [Offsetmap_sig] | |
pat [Logic_const] | \at |
pdangling [Logic_const] | \dangling |
peepHole1 [Cil] | Similar to |
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] |
|
pi [Utf8_logic] | |
pi [Fval] | Real representation of \pi. |
pif [Logic_const] | ? : |
piff [Logic_const] | <==> |
pimplies [Logic_const] | ==> |
pinitialized [Logic_const] | \initialized |
place_paned [Gtk_helper] | Sets the position of the paned widget to the given ratio |
plain_or_set [Logic_const] |
|
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_subpath [Plugin] | Use the given string as the sub-directory in which the plugin files will be installed (ie. |
plus_zero [Fval.F] | |
plus_zero [Fval] | |
pnot [Logic_const] | |
pointed_type [Ast_info] | |
pointer_comparable [Logic_utils] | \pointer_comparable |
pold [Logic_const] | \old |
pool [Task] | |
pop_attr_test [Cabshelper] | |
pop_context [Lexerhack] | |
pop_context [Clexer] | Remove all names added in this context |
pop_state [Logic_lexer] | |
popcount [Integer] | |
por [Logic_const] | || |
pors [Logic_const] | Folds || over a list of predicates. |
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 |
post_state [Dataflows.Simple_backward] | |
post_state_env [Logic_typing] | enter a given post-state and put |
pow [Float_sig.S] | |
pow [Float_interval_sig.S] | |
power_int_positive_int [Integer] | Exponentiation |
powf [Floating_point] | |
pp [Json] | |
pp_abs [Datatype.Filepath] | |
pp_abs [Filepath.Normalized] | Pretty-prints the normalized (absolute) path. |
pp_acsl_extension [Cil_types_debug] | |
pp_acsl_extension_kind [Cil_types_debug] | |
pp_all_warn_categories_status [Log.Messages] | |
pp_allocation [Printer_api.S_pp] | |
pp_allocation [Cil_types_debug] | |
pp_array [Pretty_utils] | pretty prints an array. |
pp_assigns [Printer_api.S_pp] | |
pp_assigns [Cil_types_debug] | |
pp_attr [Cabs_debug] | |
pp_attribute [Printer_api.S_pp] | |
pp_attribute [Cil_types_debug] | |
pp_attributes [Printer_api.S_pp] | |
pp_attributes [Cil_types_debug] | |
pp_attrparam [Printer_api.S_pp] | |
pp_attrparam [Cil_types_debug] | |
pp_attrs [Cabs_debug] | |
pp_behavior [Printer_api.S_pp] | |
pp_behavior [Cil_types_debug] | |
pp_bhv [Description] | prints nothing for default behavior, and " for 'b'" otherwise |
pp_bin [Integer] | Print binary format. |
pp_bin_op [Cabs_debug] | |
pp_binop [Printer_api.S_pp] | |
pp_binop [Cil_types_debug] | |
pp_bits [Bitvector] | 0b... |
pp_bitsSizeofTyp [Cil_types_debug] | |
pp_bitsSizeofTypCache [Cil_types_debug] | |
pp_block [Printer_api.S_pp] | |
pp_block [Cil_types_debug] | |
pp_block [Cabs_debug] | |
pp_blocklist [Pretty_utils] | |
pp_bool [Cil_types_debug] | |
pp_builtin_logic_info [Printer_api.S_pp] | |
pp_builtin_logic_info [Cil_types_debug] | |
pp_cabsloc [Cabs_debug] | |
pp_catch_binder [Cil_types_debug] | |
pp_category [Log.Messages] | pretty-prints a category. |
pp_char [Cil_types_debug] | |
pp_cil_function [Cil_types_debug] | |
pp_close_block [Pretty_utils] | |
pp_close_stag [Transitioning.Format] | |
pp_code_annotation [Printer_api.S_pp] | |
pp_code_annotation [Cil_types_debug] | |
pp_code_annotation_node [Cil_types_debug] | |
pp_compare [Description] | Computes a partial order compatible with pretty printing |
pp_compinfo [Printer_api.S_pp] | |
pp_compinfo [Cil_types_debug] | |
pp_cond [Pretty_utils] |
|
pp_const [Cabs_debug] | |
pp_constant [Printer_api.S_pp] | |
pp_constant [Cil_types_debug] | |
pp_context_from_file [Errorloc] | prints the line identified by the position, together with |
pp_custom_tree [Cil_types_debug] | |
pp_cvspec [Cabs_debug] | |
pp_decl_type [Cabs_debug] | |
pp_decreases [Printer_api.S_pp] | |
pp_def [Cabs_debug] | |
pp_deps [Cil_types_debug] | |
pp_dump [Json] | without formatting |
pp_enum_item [Cabs_debug] | |
pp_enuminfo [Cil_types_debug] | |
pp_enumitem [Cil_types_debug] | |
pp_exp [Printer_api.S_pp] | |
pp_exp [Cil_types_debug] | |
pp_exp [Cil_descriptive_printer] | |
pp_exp [Cabs_debug] | |
pp_exp_info [Cil_types_debug] | |
pp_exp_node [Cil_types_debug] | |
pp_exp_node [Cabs_debug] | |
pp_extended [Printer_api.S_pp] | |
pp_extended_asm [Cil_types_debug] | |
pp_fail [Datatype] | Must be used for |
pp_field [Printer_api.S_pp] | |
pp_field_group [Cabs_debug] | |
pp_field_groups [Cabs_debug] | |
pp_fieldinfo [Cil_types_debug] | |
pp_file [Printer_api.S_pp] | |
pp_file [Cil_types_debug] | |
pp_file [Cabs_debug] | |
pp_filepath_position [Cil_types_debug] | |
pp_fkind [Printer_api.S_pp] | |
pp_fkind [Cil_types_debug] | |
pp_float [Cil_types_debug] | |
pp_flowlist [Pretty_utils] | |
pp_for [Description] | prints nothing or " for 'b1,...,bn'" |
pp_for_clause [Cabs_debug] | |
pp_from [Printer_api.S_pp] | |
pp_from [Cil_types_debug] | |
pp_from_file [Command] |
|
pp_full_assigns [Printer_api.S_pp] | first parameter is the introducing keyword (e.g. |
pp_fun_spec [Cabs_debug] | |
pp_funbehavior [Cil_types_debug] | |
pp_fundec [Printer_api.S_pp] | |
pp_fundec [Cil_types_debug] | |
pp_funspec [Printer_api.S_pp] | |
pp_funspec [Cil_types_debug] | |
pp_get_formatter_stag_functions [Transitioning.Format] | |
pp_global [Printer_api.S_pp] | |
pp_global [Cil_types_debug] | |
pp_global_annotation [Printer_api.S_pp] | |
pp_global_annotation [Cil_types_debug] | |
pp_hex [Integer] | Print hexadecimal format. |
pp_identified_predicate [Printer_api.S_pp] | |
pp_identified_predicate [Cil_types_debug] | |
pp_identified_term [Printer_api.S_pp] | |
pp_identified_term [Cil_types_debug] | |
pp_idpred [Description] | prints the "'<labels>'" or the "(<location>)" of the predicate |
pp_ikind [Printer_api.S_pp] | |
pp_ikind [Cil_types_debug] | |
pp_impact_pragma [Cil_types_debug] | |
pp_init [Printer_api.S_pp] | |
pp_init [Cil_types_debug] | |
pp_init_exp [Cabs_debug] | |
pp_init_name [Cabs_debug] | |
pp_init_name_group [Cabs_debug] | |
pp_initinfo [Printer_api.S_pp] | |
pp_initinfo [Cil_types_debug] | |
pp_initwhat [Cabs_debug] | |
pp_instr [Printer_api.S_pp] | |
pp_instr [Cil_types_debug] | |
pp_int [Cil_types_debug] | |
pp_int64 [Cil_types_debug] | |
pp_integer [Cil_types_debug] | |
pp_items [Pretty_utils] | Prints a collection of elements, with the possibility of aligning titles with each others. |
pp_iter [Pretty_utils] | pretty prints any structure using an iterator on it. |
pp_iter2 [Pretty_utils] | pretty prints any map-like structure using an iterator on it. |
pp_kernel_function [Cil_types_debug] | |
pp_kinstr [Description] | prints nothing for global, or " at <stmt>" |
pp_kinstr [Cil_types_debug] | |
pp_label [Printer_api.S_pp] | |
pp_label [Cil_types_debug] | |
pp_labels [Cabs_debug] | |
pp_lexing_position [Cil_types_debug] | |
pp_lhost [Cil_types_debug] | |
pp_list [Pretty_utils] | pretty prints a list. |
pp_list [Cil_types_debug] | |
pp_local [Description] | completely local printer |
pp_localisation [Cil_types_debug] | |
pp_localized [Description] | prints more-or-less localized property |
pp_location [Printer_api.S_pp] | |
pp_location [Cil_types_debug] | |
pp_logic_body [Cil_types_debug] | |
pp_logic_builtin_label [Printer_api.S_pp] | |
pp_logic_builtin_label [Cil_types_debug] | |
pp_logic_constant [Printer_api.S_pp] | |
pp_logic_constant [Cil_types_debug] | |
pp_logic_ctor_info [Printer_api.S_pp] | |
pp_logic_ctor_info [Cil_types_debug] | |
pp_logic_info [Printer_api.S_pp] | |
pp_logic_info [Cil_types_debug] | |
pp_logic_label [Printer_api.S_pp] | |
pp_logic_label [Cil_types_debug] | |
pp_logic_real [Cil_types_debug] | |
pp_logic_type [Printer_api.S_pp] | |
pp_logic_type [Cil_types_debug] | |
pp_logic_type_def [Cil_types_debug] | |
pp_logic_type_info [Printer_api.S_pp] | |
pp_logic_type_info [Cil_types_debug] | |
pp_logic_var [Printer_api.S_pp] | |
pp_logic_var [Cil_types_debug] | |
pp_logic_var_kind [Cil_types_debug] | |
pp_loop_allocation [Printer_api.S_pp] | |
pp_loop_assigns [Printer_api.S_pp] | |
pp_loop_from [Printer_api.S_pp] | |
pp_loop_pragma [Cil_types_debug] | |
pp_lval [Printer_api.S_pp] | |
pp_lval [Cil_types_debug] | |
pp_lval [Cil_descriptive_printer] | |
pp_mach [Cil_types_debug] | |
pp_margin [Pretty_utils] | Prints a text with margins wrt to marger. |
pp_ml_name [Type] | |
pp_model_field [Printer_api.S_pp] | |
pp_model_info [Printer_api.S_pp] | |
pp_model_info [Cil_types_debug] | |
pp_name [Cabs_debug] | |
pp_name_group [Cabs_debug] | |
pp_named [Description] | prints the name of a named logic structure (if any), separated by ','. |
pp_offset [Printer_api.S_pp] | |
pp_offset [Cil_types_debug] | |
pp_open_block [Pretty_utils] | |
pp_open_stag [Transitioning.Format] | |
pp_opt [Pretty_utils] | pretty-prints an optional value. |
pp_option [Cil_types_debug] | |
pp_pair [Pretty_utils] |
|
pp_pair [Cil_types_debug] | |
pp_pos [Filepath] | Pretty-prints a position, in the format file:line. |
pp_post_cond [Printer_api.S_pp] | |
pp_pragma [Cil_types_debug] | |
pp_predicate [Printer_api.S_pp] | |
pp_predicate [Cil_types_debug] | |
pp_predicate_node [Printer_api.S_pp] | |
pp_predicate_node [Cil_types_debug] | |
pp_print_string_fill [Pretty_utils] | transforms every space in a string in breakable spaces. |
pp_property [Description] | prints an identified property |
pp_quantifiers [Cil_types_debug] | |
pp_raw_stmt [Cabs_debug] | |
pp_ref [Cil_types_debug] | |
pp_region [Description] | prints message "nothing" or the "'<names>'" or the "(<location>)" of the relation |
pp_relation [Printer_api.S_pp] | |
pp_relation [Cil_types_debug] | |
pp_set_formatter_stag_functions [Transitioning.Format] | |
pp_single_name [Cabs_debug] | |
pp_slice_pragma [Cil_types_debug] | |
pp_spec [Cil_types_debug] | |
pp_spec [Cabs_debug] | |
pp_spec_elem [Cabs_debug] | |
pp_stmt [Printer_api.S_pp] | |
pp_stmt [Description] | prints "<instruction>" or "<instruction> (<file,line>)" |
pp_stmt [Cil_types_debug] | |
pp_stmt [Cabs_debug] | |
pp_stmtkind [Cil_types_debug] | |
pp_storage [Printer_api.S_pp] | |
pp_storage [Cil_types_debug] | |
pp_storage [Cabs_debug] | |
pp_string [Cil_types_debug] | |
pp_term [Printer_api.S_pp] | |
pp_term [Cil_types_debug] | |
pp_term_lhost [Printer_api.S_pp] | |
pp_term_lhost [Cil_types_debug] | |
pp_term_lval [Printer_api.S_pp] | |
pp_term_lval [Cil_types_debug] | |
pp_term_node [Cil_types_debug] | |
pp_term_offset [Printer_api.S_pp] | |
pp_term_offset [Cil_types_debug] | |
pp_termination_kind [Cil_types_debug] | |
pp_thisloc [Cil] | Pretty-print |
pp_to_file [Command] |
|
pp_trail [Pretty_utils] | pretty-prints its contents inside an '(** ... |
pp_tuple3 [Cil_types_debug] | |
pp_tuple4 [Cil_types_debug] | |
pp_tuple5 [Cil_types_debug] | |
pp_typ [Printer_api.S_pp] | |
pp_typ [Gui_printers] | Same as |
pp_typ [Cil_types_debug] | |
pp_typ_unfolded [Gui_printers] | Pretty-prints a type, unfolding it once if it is a typedef, enum, struct or union. |
pp_typeSpecifier [Cabs_debug] | |
pp_typeinfo [Cil_types_debug] | |
pp_un_op [Cabs_debug] | |
pp_unop [Printer_api.S_pp] | |
pp_unop [Cil_types_debug] | |
pp_variant [Printer_api.S_pp] | |
pp_variant [Cil_types_debug] | |
pp_varinfo [Printer_api.S_pp] | |
pp_varinfo [Cil_types_debug] | |
pp_varname [Printer_api.S_pp] | |
pp_warn_category [Log.Messages] | |
pp_with_col [Cil_datatype.Position] | |
ppc_32 [Machdeps] | |
ppcm [Integer] |
|
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 |
precondition [Ast_info] | Builds the precondition from |
precondition_at_call [Statuses_by_call] |
|
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 |
prel [Logic_const] | Binary relation. |
prepareCFG [Cfg] | This function converts all |
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] |
|
preprocessor_supported_arch_options [Config] | architecture-related options (e.g. |
pretty [Tr_offset] | |
pretty [Task] | |
pretty [State_selection.S] | Display a selection. |
pretty [Rich_text] | Pretty-print the message onto the given formatter, with the tags. |
pretty [Property_status.Feedback] | |
pretty [Offsetmap_bitwise_sig] | |
pretty [Locations] | |
pretty [Lmap_sig] | |
pretty [Journal.Reverse_binding] | |
pretty [Interpreted_automata.UnrollUnnatural.G] | |
pretty [Integer] | |
pretty [Fval.F] | |
pretty [Floating_point] | |
pretty [Float_sig.S] | |
pretty [Float_interval_sig.S] | |
pretty [Db.INOUTKF] | |
pretty [Db.Pdg] | For debugging... |
pretty [Db.From] | |
pretty [Db.Value] | |
pretty [Datatype.Make_input] | |
pretty [Datatype.S_no_copy] | Pretty print each value in an user-friendly way. |
pretty [Datatype.Undefined] | |
pretty [Datatype] | |
pretty [Dataflows.JOIN_SEMILATTICE] | Display the contents of an element of the lattice. |
pretty [Dataflow2.BackwardsTransfer] | Pretty-print the state |
pretty [Dataflow2.ForwardsTransfer] | Pretty-print the state. |
pretty [Filepath.Normalized] | Pretty-print a path according to these rules: relative filenames are kept, except for leading './',
which are stripped;, absolute filenames are relativized if their prefix is included in the
current working directory; also, symbolic names are resolved,
i.e. the result may be prefixed by known aliases (e.g. FRAMAC_SHARE).
See |
pretty [Filepath] | DEPRECATED: use |
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_as_reason [Origin] | Pretty-print |
pretty_ast [File] | Print the project CIL file on the given Formatter. |
pretty_bits [Bit_utils] | Pretty prints a range of bits in a type for the user. |
pretty_code [Datatype.S_no_copy] | Pretty print each value in an ML-like style: the result must be a valid OCaml expression. |
pretty_code [Datatype] | |
pretty_comp [Abstract_interp.Comp] | |
pretty_component [Wto.Make] | |
pretty_debug [Property] | Internal use only. |
pretty_debug [Offsetmap_bitwise_sig] | |
pretty_debug [Map_lattice.MapSet_Lattice] | |
pretty_debug [Locations.Zone] | |
pretty_debug [Lmap_sig] | |
pretty_debug [Lmap_bitwise.Location_map_bitwise] | |
pretty_debug [Ival] | |
pretty_debug [Hptmap.V] | |
pretty_debug [Hptset.S] | |
pretty_diff [Lmap_sig] | |
pretty_edge [Interpreted_automata] | |
pretty_english [Locations] | |
pretty_filter [Lmap_sig] |
|
pretty_generic [Offsetmap_sig] | |
pretty_generic [Offsetmap_bitwise_sig] | |
pretty_generic_printer [Lmap_bitwise.Location_map_bitwise] | |
pretty_key [Db.Pdg] | Pretty print information on a node key |
pretty_kind [Fval] | |
pretty_line [Cil_datatype.Location] | Prints only the line of the location |
pretty_long [Cil_datatype.Location] | Pretty the location under the form |
pretty_machdep [File] | Prints the associated |
pretty_node [Db.Pdg] | Pretty print information on a node : with |
pretty_normal [Fval.F] | |
pretty_normal [Floating_point] | |
pretty_parameter [Emitter.Usable_emitter] | Pretty print the parameter (given by its name) with its value. |
pretty_partition [Wto.Make] | |
pretty_predicate_kind [Property] | |
pretty_sid [Cil_datatype.Stmt] | Pretty print the sid of the statement |
pretty_state [Db.Value] | |
pretty_transition [Interpreted_automata] | |
pretty_typ [Offsetmap_lattice_with_isotropy] | |
pretty_typ [Int_Intervals_sig] | Pretty-printer that supposes the intervals are subranges of a C type, and use the type to print nice offsets |
pretty_validity [Base] | |
pretty_witness [State_selection.S] | Display a selection in a more concise form. |
prev_float [Fval.F] | First double strictly below the argument. |
prev_float [Float_sig.S] | First value below the argument in the given precision. |
prevent [Journal] |
|
printComments [Cprint] | |
printCounters [Cprint] | |
printFile [Cprint] | |
printLn [Cprint] | |
printLnComment [Cprint] | |
print_assigns [Logic_print] | |
print_attribute [Cprint] | |
print_attributes [Cprint] | |
print_block [Cprint] | |
print_code_annot [Logic_print] | |
print_constant [Logic_print] | |
print_decl [Logic_print] | |
print_decl [Cprint] | |
print_def [Cprint] | |
print_defs [Cprint] | |
print_delayed [Log] | Direct printing on output. |
print_dot [Db.PostdominatorsTypes.Sig] | Print a representation of the postdominators in a dot file
whose name is |
print_enum_items [Cprint] | |
print_expression [Cprint] | |
print_expression_level [Cprint] | |
print_field [Cprint] | |
print_field_group [Cprint] | |
print_fields [Cprint] | |
print_file [Command] | Properly flush and close the channel and re-raise exceptions |
print_global [Cil_printer] | Is the given global displayed by the pretty-printer. |
print_help [Parameter_sig.S_no_parameter] | Print the help of the parameter in the given formatter as it would be printed on the command line by -<plugin>-help. |
print_init_expression [Cprint] | |
print_init_name [Cprint] | |
print_init_name_group [Cprint] | |
print_lexpr [Logic_print] | |
print_logic_type [Logic_print] | First arguments prints the name of identifier declared with the corresponding type (None for pure type. |
print_name [Cprint] | |
print_name_group [Cprint] | |
print_on_output [Log] | Direct printing on output. |
print_onlytype [Cprint] | |
print_params [Cprint] | |
print_quantifiers [Logic_print] | |
print_single_name [Cprint] | |
print_spec [Logic_print] | |
print_specifiers [Cprint] | |
print_statement [Cprint] | |
print_struct_name_attr [Cprint] | |
print_type_annot [Logic_print] | |
print_type_spec [Cprint] | |
print_typedef [Logic_print] | |
print_variant [Logic_print] | |
printf [Log.Messages] | Outputs the formatted message on |
private_ops [State] | |
product [Extlib] |
|
product_fold [Extlib] |
|
progress [Task] | Make the thread progress and return |
progress [Db] | This function should be called from time to time by all analysers taking time. |
project [Lattice_type.Lattice_Base] | |
project [Kernel] | |
project [Int_Base] | |
project [Lattice_type.Lattice_Set] | |
project_float [Ival] | Should be used only when we know it is a float |
project_float [Fval] | |
project_int [Ival] | |
project_set [Int_Intervals_sig] | May raise |
project_singleton [Int_Intervals_sig] | |
property_kind_and_node [Description] | Returns separately the kind and the node of a property. |
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 [Rich_text] | Sub-string with range. |
range_covers_whole_type [Int_Intervals_sig] | Does the interval cover the entire range of bits that are valid for the given type. |
range_loc [Cil] | Returns a location that ranges over the two locations in arguments. |
range_selector [Gtk_helper] | |
rank [Cil] | Returns a unique number representing the integer conversion rank. |
reachable_stmts [Stmts_graph] |
|
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 term. |
refresh_local_name [Cil] | if needed, rename the given varinfo so that its |
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 [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 [Gtk_helper.Icon] |
|
register [Gtk_form] | |
register [Globals.Functions] | |
register [Dynamic] |
|
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 [Project] |
|
register_after_set_current_hook [Project] |
|
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_remove_hook [Project] |
|
register_behavior_extension [Logic_typing] |
|
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_category [Log.Messages] | register a new debugging/verbose category. |
register_code_annot_extension [Logic_typing] | register an extension for code annotation to be evaluated at _current_ program point. |
register_code_annot_extension [Cil_printer] | Register a pretty-printer used for behavior extension. |
register_code_annot_next_both_extension [Logic_typing] | register an extension both for code and loop annotations. |
register_code_annot_next_loop_extension [Logic_typing] | register an extension for loop annotation. |
register_code_annot_next_stmt_extension [Logic_typing] | register an extension for code annotation to be evaluated for the _next_ statement. |
register_code_transformation_category [File] | Adds a new category of code transformation |
register_compute [Db] | |
register_conditional_side_effect_hook [Cabs2cil] | new hook called when an expression with side-effect is evaluated conditionally (RHS of && or ||, 2nd and 3rd term of ?:). |
register_create_hook [Project] |
|
register_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_env] | register a given name as a clause name for extended category. |
register_extension [Design] | Register an extension to the main GUI. |
register_for_loop_all_hook [Cabs2cil] | new hook that will be called when processing a for loop. |
register_for_loop_body_hook [Cabs2cil] | new hook that will called when processing a for loop. |
register_for_loop_incr_hook [Cabs2cil] | new hook that will be called when processing a for loop. |
register_for_loop_init_hook [Cabs2cil] | new hook that will be called when processing a for loop. |
register_for_loop_test_hook [Cabs2cil] | new hook that will be called when processing a for loop. |
register_global_extension [Logic_typing] | register an extension for global annotation. |
register_global_extension [Cil_printer] | Register a pretty-printer used for behavior extension. |
register_guarded_compute [Db] | |
register_ignore_pure_exp_hook [Cabs2cil] | |
register_ignore_side_effect_hook [Cabs2cil] | new hook called when side-effects are dropped. |
register_implicit_prototype_hook [Cabs2cil] | new hook called when an implicit prototype is generated. |
register_incompatible_decl_hook [Cabs2cil] | new hook called when two conflicting declarations are found. |
register_key [Hook.S_ordered] | |
register_local_func_hook [Cabs2cil] | new hook called when encountering a definition of a local function. |
register_locking_machinery [Gtk_helper] | Add hooks to the locking mechanism of the GUI. |
register_loop_annot_extension [Cil_printer] | Register a pretty-printer used for behavior extension. |
register_memory_var [Base] | Memory variables are variables not present in the source of the program. |
register_new_global_hook [Cabs2cil] | Hook called when a new global is created. |
register_property_add_hook [Property_status] | add an hook that will be called for any newly registered property |
register_property_remove_hook [Property_status] | Add and hook that will be called each time a property is removed. |
register_reset_extension [Design] | Register a function to be called whenever the main GUI reset method is called. |
register_shallow_attribute [Cil_printer] | Register an attribute that will never be pretty printed. |
register_stmt [Kernel_function] | Register a new statement in a kernel function, with the list of blocks that contain the statement (innermost first). |
register_tag_handlers [Log.Messages] | |
register_todo_after_clear [Project] | Register an action performed just after clearing a project. |
register_todo_before_clear [Project] | Register an action performed just before clearing a project. |
register_warn_category [Log.Messages] | |
registered_builtins [Db.Value] | Returns a list of the pairs (name, builtin_sig) registered via
|
rehash [Datatype.Make_input] | How to rehashconsed values. |
rehash [Datatype.Undefined] | |
reinterpret_as_float [Ival] | Bitwise reinterpretation of the given value as a float of the given kind. |
reinterpret_as_int [Ival] | Bitwise reinterpretation of the given value, of size |
relativize [Filepath] |
|
remove [State_builder.Weak_hashtbl] |
|
remove [Rangemap.S] |
|
remove [Qstack.Make] | Remove an element from the stack. |
remove [Property_status] | Remove the property deeply. |
remove [Project] | Default project is |
remove [Indexer.Make] | Log complexity. |
remove [Hptmap_sig.S] |
|
remove [Globals.Functions] | Removes the given varinfo, which must have already been removed from the AST. |
remove [Globals.Vars] | Removes the given varinfo, which must have already been removed from the AST. |
remove [FCSet.S_Basic_Compare] |
|
remove [FCMap.S] |
|
remove [Emitter.Make_table] | |
remove [Dynamic.Parameter.StringList] | |
remove [Dynamic.Parameter.StringSet] | |
remove [State_builder.Set_ref] | |
remove [State_builder.Hashtbl] | |
remove [Alarms] | Remove the alarms and the associated annotations emitted by the given emitter. |
removeAttribute [Cil] | Remove an attribute previously registered. |
removeFormalsDecl [Cil] | remove a binding from the table. |
removeOffset [Cil] | Remove ONE offset from the end of an offset sequence. |
removeOffsetLval [Cil] | Remove ONE offset from the end of an lvalue. |
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 |
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 |
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_exn [Exn_flow] | transforms functions that may throw into functions returning a union type composed of the normal return or one of the exceptions. |
remove_extended [Annotations] | |
remove_global [Annotations] | Remove a global annotation. |
remove_global_annotations [Globals.FileIndex] | |
remove_logic_coerce [Logic_utils] | Removes TLogic_coerce at head of term. |
remove_logic_ctor [Logic_env] | removes the given logic constructor. |
remove_logic_function [Logic_env] | removes all overloaded bindings to a given symbol. |
remove_logic_info_gen [Logic_env] |
|
remove_logic_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_terminates [Annotations] | Remove the terminates clause attached to a function. |
remove_typename [Logic_env] | removes latest typename status associated to a given identifier |
remove_unused_labels [Rmtmps] | removes unused labels for which |
remove_variables [Lmap_sig] | |
remove_whole [Rangemap.Make] | |
reorder_ast [File] | reorder globals so that all uses of an identifier are preceded by its declaration. |
reorder_custom_ast [File] | |
replace [Hptmap_sig.S] |
|
replace [Extlib] |
|
replace [Dataflow2.StmtStartData] | |
replace [State_builder.Hashtbl] | Add a new binding. |
replace_by_declaration [Globals.Functions] | Note: if the varinfo is already registered and bound to a definition,
the definition will be erased only if |
replace_by_definition [Globals.Functions] | TODO: do not take a funspec as argument |
replace_call_precondition [Statuses_by_call] |
|
reprs [Type.Polymorphic4_input] | |
reprs [Type.Polymorphic3_input] | |
reprs [Type.Polymorphic2_input] | |
reprs [Type.Polymorphic_input] | How to make the representant of each monomorphic instance of the polymorphic type value from an underlying representant. |
reprs [Type] | Not usable in the "no-obj" mode |
reprs [Datatype.Make_input] | Must be non-empty. |
reprs [Datatype.S_no_copy] | List of representants of the descriptor. |
res_call_visible [Filter.RemoveInfo] | tells if the lvalue of the call has to be visible |
reset [FCBuffer] | Empty the buffer and deallocate the internal byte sequence holding the
buffer contents, replacing it with the initial internal byte sequence
of length |
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 |
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 |
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 |
return [Task] | The task that immediately returns a result |
return [Descr] | Similar to |
return [Command] | |
returns_void [Kernel_function] | |
rmUnusedInlines [Rmtmps] | |
rmUnusedStatic [Rmtmps] | |
rm_asserts [Db.Value] | |
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_to_precision [Float_sig.S] | Rounds a number to a given precision. |
round_to_single_precision_float [Fval] | |
round_to_single_precision_float [Floating_point] | |
round_up_to_r [Integer] |
|
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. |
S | |
safe_at_exit [Extlib] | Register function to call with |
safe_remove [Extlib] | Tries to delete a file and never fails. |
safe_remove_dir [Extlib] | |
save [Project] | Save a given project in a file. |
save [Journal] | Save the current state of the journal for future restoration. |
save [Gtk_helper.Configuration] | |
saveConfiguration [Cilconfig] | Save the configuration in a file. |
save_all [Project] | Save all the projects in a file. |
save_buffer [Json] | |
save_channel [Json] | |
save_file [Json] | |
save_formatter [Json] | |
save_paned_ratio [Gtk_helper] | Saves the current ratio of the panel associated to the given key. |
save_string [Json] | |
saveload [Kernel] | |
scalar_term_to_predicate [Logic_utils] | Compare the given term with the constant 0 (of the appropriate type)
to return the result of the comparison |
scale [Ival] |
|
scale_div [Ival] |
|
scale_div_under [Ival] |
|
scale_int_base [Ival] | |
scale_rem [Ival] |
|
scharPtrType [Cil] | |
scharType [Cil] | |
scheduled [Task] | Number of scheduled process |
scroll [Wbox] | default policy is AUTOMATIC |
select_file [Source_manager] | Selection by page filename |
select_file [Gtk_helper] | Launches a standard gtk file chooser window and returns the name of the selected file. |
select_name [Source_manager] | Selection by page title |
selected_localizable [History] |
|
selection_locked [Source_manager] | Prevents the filetree callback from resetting the selected line when it was selected via a click in the original source viewer. |
self [State_builder.Hashcons] | |
self [State_builder.Counter] | |
self [State_builder.Queue] | |
self [State_builder.S] | The kind of the registered state. |
self [Property_status] | The state which stores the computed status. |
self [Property.Names] | |
self [Property.LegacyNames] | |
self [Messages] | Internal state of stored messages |
self [Logic_env.Logic_builtin_used] | |
self [Kernel_function] | |
self [Hptset.Make] | |
self [Hptmap_sig.S] | |
self [Globals.Syntactic_search] | |
self [Globals.FileIndex] | The state kind corresponding to the table of global C symbols. |
self [Globals.Functions] | |
self [Globals.Vars] | |
self [Emitter.Make_table] | |
self [Emitter] | |
self [Db.Pdg] | |
self [Db.Security] | |
self [Db.RteGen] | |
self [Db.From] | |
self [Db.Value] | Internal state of the value analysis from projects viewpoint. |
self [Cil_datatype.Varinfo.Hptset] | |
self [Cil_datatype.Stmt.Hptset] | |
self [Cabshelper.Comments] | |
self [Ast.UntypedFiles] | |
self [Ast] | The state kind associated to the cil AST. |
self [Alarms] | |
selfFormalsDecl [Cil] | state of the table associating formals to each prototype. |
selfMachine [Cil] | |
selfMachine_is_computed [Cil] | whether current project has set its machine description. |
self_external [Db.INOUTKF] | |
self_internal [Db.INOUTKF] | |
self_with_formals [Db.Inputs] | |
sentinel [Binary_cache.Result] | |
sentinel [Binary_cache.Cacheable] | |
separateStorageModifiers [Cil] | Separate out the storage-modifier name attributes |
separate_if_succs [Cil] | Provided |
separate_switch_succs [Cil] | Provided |
seq [Kernel] | |
sequence [Task] |
|
server [Task] | Creates a server of commands. |
set [Vector] | Raise |
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] | |
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 |
setFormals [Cil] | Update the formals of a |
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 |
setReturnType [Cil] | |
setReturnTypeVI [Cil] | Change the return type of the function passed as 1st argument to be the type passed as 2nd argument. |
setTypeAttrs [Cil] | Sets the attributes of the type to the given list. |
set_bold_font [Wutil] | |
set_bold_font [Gtk_compat.Pango] | makes the font bold. |
set_bool [Gtk_helper.Configuration] | Sets a ConfigBool |
set_cmdline_stage [Parameter_customize] | Set the stage where the option corresponding to the parameter is recognized. |
set_compinfo [Cil] | |
set_conversion [Logic_const] |
|
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_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_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_module_load_path [Dynamic] | Sets the load path for modules in FRAMAC_PLUGIN, prepending it with |
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_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_pane_ratio [Wutil] | |
set_possible_values [Parameter_sig.String] | Set what are the acceptable values for this parameter. |
set_printer [Printer_api.S] | Set the current pretty-printer, typically to a printer previously
obtained through |
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_small_font [Gtk_compat.Pango] | makes the font smaller. |
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] | |
set_warn_status [Log.Messages] | |
setup_all_preconditions_proxies [Statuses_by_call] |
|
setup_precondition_proxy [Statuses_by_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 |
shape [Hptset.S] | Export the shape of the set. |
share [Wutil] | |
share [Task] | New instance of shared task. |
shared [Task] | Build a shareable task. |
shared_icon [Widget] | |
shift [Locations.Location_Bytes] | |
shift_bits [Offsetmap_lattice_with_isotropy] | Left-shift the given value, of size |
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. |
shrink [Rich_text] | Resize the buffer to roughly fit its actual content. |
sidebar [Wbox] | The first list is packed to the top of the sidebar. |
signof_typeof_lval [Bit_utils] | |
sin [Float_sig.S] | |
sin [Float_interval_sig.S] | |
sinf [Floating_point] | |
single_interval_value [Offsetmap_sig] |
|
single_interval_value [Offsetmap_bitwise_sig] |
|
singleton [State_selection] | The selection containing only the given state. |
singleton [Rangemap.S] |
|
singleton [Qstack.Make] | Create a new qstack with a single element. |
singleton [Hptmap_sig.S] |
|
singleton [Float_interval_sig.S] |
|
singleton [FCSet.S_Basic_Compare] |
|
singleton [FCMap.S] |
|
singleton [Bag] | |
singleton_one [Locations.Location_Bytes] | the set containing only the value |
singleton_zero [Locations.Location_Bytes] | the set containing only the value for to the C expression |
sixteen [Integer] | |
size [Vector] | Same as |
size [Task] | Auto-flush. |
size [State_builder.Info_with_size] | Initial size for the hash table. |
size [Rich_text] | |
size [Indexer.Make] | Number of elements in the collection. |
sizeOf [Cil] | The size of a type, in bytes. |
size_from_validity [Offsetmap_sig] |
|
size_from_validity [Offsetmap_bitwise_sig] |
|
sizeof [Bit_utils] |
|
sizeof_lval [Bit_utils] | |
sizeof_pointed [Bit_utils] | |
sizeof_pointed_lval [Bit_utils] | |
sizeof_vid [Bit_utils] | |
sizeofchar [Bit_utils] |
|
sizeofpointer [Bit_utils] |
|
snd [Lattice_type.Lattice_Product] | |
sort [Bag] | The returned list preserves duplicates and order of equals elements. |
sort_unique [Extlib] | Same as List.sort , but also remove duplicates. |
source [Property] | returns the location of the property, if not unknown. |
source [Log] | |
source_files_chooser [Gtk_helper] | Open a dialog box for choosing C source files and performing an action on them. |
spawn [Task] | Schedules a task on the server. |
spawn_command [Gtk_helper] | Launches the given command and calls the given function when the process terminates. |
spec [Logic_parser] | |
spec [Logic_lexer] | |
spinner [Gtk_form] | |
split [Wbox] | |
split [Map_lattice.MapSet_Lattice] |
|
split [Locations.Location_Bytes] | |
split [FCSet.S] |
|
split [FCMap.S] |
|
splitArrayAttributes [Cil] | given some attributes on an array type, split them into those that belong to the type of the elements of the array (currently, qualifiers such as const and volatile), and those that must remain on the array, in that order |
splitFunctionType [Cil] | Given a function type split it into return type, arguments, is_vararg and attributes. |
splitFunctionTypeVI [Cil] | |
split_category [Log] | Split a category specification into its constituants. |
split_on_char [Transitioning.String] | 4.04 |
sqrt [Float_sig.S] | |
sqrt [Float_interval_sig.S] | |
sqrtf [Floating_point] | |
stag_of_string [Transitioning.Format] | |
startParsing [Errorloc] | Call this function to start parsing. |
startsWith [Cil] | sm: return true if the first is a prefix of the second string |
state [Cil_printer] | |
state_stack [Logic_lexer] | |
statement [Db.INOUT] | |
status [Task] | The task that immediately finishes with provided status |
status_feedback [Description] | User-friendly description of property statuses. |
stmtFallsThrough [Cabs2cil] | returns |
stmt_can_reach [Stmts_graph] |
|
stmt_can_reach_filtered [Stmts_graph] | Just like |
stmt_in_loop [Kernel_function] |
|
stmt_is_in_cycle [Stmts_graph] |
|
stmt_is_in_cycle_filtered [Stmts_graph] | Just like |
stmt_of_instr_list [Cil] | if the list has 2 elements or more, it will return a block with
|
stmt_postdominators [Db.PostdominatorsTypes.Sig] | |
stmt_start [Pretty_source] | Offset at which the current statement starts in the buffer
corresponding to |
str [Descr] | |
string [Rich_text] | |
string [Json] | Convert |
string [Datatype] | |
string_del_prefix [Extlib] |
|
string_del_suffix [Extlib] |
|
string_of_c_rounding_mode [Floating_point] | |
string_of_stag [Transitioning.Format] | |
string_prefix [Extlib] |
|
string_selector [Gtk_helper] | |
string_split [Extlib] |
|
string_suffix [Extlib] |
|
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 |
stripInfo [Cil] | Removes info wrappers and return underlying expression |
stripTermCasts [Cil] | Equivalent to |
strip_underscore [Extlib] | remove underscores at the beginning and end of a string. |
structural_descr [Type.Polymorphic4_input] | |
structural_descr [Type.Polymorphic3_input] | |
structural_descr [Type.Polymorphic2_input] | |
structural_descr [Type.Polymorphic_input] | How to build the structural descriptor for each monomorphic instance. |
structural_descr [Type] | |
structural_descr [Datatype.Hashtbl_with_descr] | |
structural_descr [Datatype.Make_input] | |
structural_descr [Datatype.Undefined] | |
sub [Rich_text] | Similar to |
sub [Integer] | |
sub [Float_sig.S] | |
sub [Float_interval_sig.S] | |
sub [FCBuffer] |
|
sub [Abstract_interp.Rel] | |
sub_abs [Abstract_interp.Rel] | |
sub_bytes [FCBuffer] | Same as |
sub_int [Ival] | |
sub_int_under [Ival] | |
sub_pointer [Locations.Location_Bytes] | Subtracts the offsets of two locations. |
sub_pointwise [Locations.Location_Bytes] | Subtracts the offsets of two locations |
subdiv_float_interval [Fval] | Raise |
subdivide [Ival] | Subdivisions into two intervals |
subdivide [Float_interval_sig.S] | Subdivides an interval of a given precision into two intervals. |
subset [FCSet.S_Basic_Compare] |
|
subsets [Extlib] |
|
substring [Rich_text] | |
succ [Transitioning.Stdlib] | |
succ [Integer] | |
swap [Extlib] | Swap arguments. |
sym [Abstract_interp.Comp] | Opposite relation: |
symmetric_binary_predicate [Hptmap_sig.S] | Same as |
sync [Task] | Schedules a task such that only one can run simultaneously for a given mutex. |
sys_single_precision_of_string [Floating_point] | |
T | |
t_abstract [Structural_descr] | |
t_array [Unmarshal] | |
t_array [Structural_descr] | |
t_bool [Unmarshal] | |
t_bool [Structural_descr] | |
t_bool [Descr] | |
t_float [Unmarshal] | |
t_float [Structural_descr] | |
t_float [Descr] | |
t_hashtbl_changedhashs [Unmarshal] | |
t_hashtbl_unchanged_hashs [Structural_descr] | |
t_hashtbl_unchangedhashs [Unmarshal] | |
t_int [Unmarshal] | |
t_int [Structural_descr] | |
t_int [Descr] | |
t_int32 [Unmarshal] | |
t_int32 [Structural_descr] | |
t_int32 [Descr] | |
t_int64 [Unmarshal] | |
t_int64 [Structural_descr] | |
t_int64 [Descr] | |
t_list [Unmarshal] | |
t_list [Structural_descr] | |
t_list [Descr] | Type descriptor for lists. |
t_map_unchanged_compares [Structural_descr] | |
t_map_unchangedcompares [Unmarshal] | |
t_nativeint [Unmarshal] | |
t_nativeint [Structural_descr] | |
t_nativeint [Descr] | |
t_option [Unmarshal] | |
t_option [Structural_descr] | |
t_option [Descr] | Type descriptor for options. |
t_pair [Descr] | Type descriptor for pairs (2-tuples). |
t_queue [Unmarshal] | |
t_queue [Structural_descr] | |
t_queue [Descr] | Type descriptor for queues. |
t_record [Unmarshal] | |
t_record [Structural_descr] | |
t_record [Descr] | Type descriptor for records (the length of the array must be equal to the number of fields in the record). |
t_ref [Unmarshal] | |
t_ref [Structural_descr] | |
t_ref [Descr] | Type descriptor for references. |
t_ref [Datatype] | |
t_set_unchanged_compares [Structural_descr] | |
t_set_unchangedcompares [Unmarshal] | |
t_string [Unmarshal] | |
t_string [Structural_descr] | |
t_string [Descr] | |
t_sum [Structural_descr] | |
t_tuple [Unmarshal] | |
t_tuple [Structural_descr] | |
t_tuple [Descr] | Type descriptor for tuples of any range (the length of the array range is the range of the tuple). |
t_unit [Unmarshal] | |
t_unit [Structural_descr] | |
t_unit [Descr] | |
t_unknown [Structural_descr] | |
taddrof [Logic_const] | & |
tags_at [Rich_text] | Returns the list of tags at the given position. |
tat [Logic_const] | \at |
temp_dir_cleanup_at_exit [Extlib] | |
temp_file_cleanup_at_exit [Extlib] | Similar to |
term [Logic_typing.Make] | type-checks a term. |
term [Logic_const] | returns a anonymous term of the given type. |
term [Db.Properties.Interp] | |
term_lval [Db.Properties.Interp] | |
term_lval_to_lval [Db.Properties.Interp] | |
term_lvals_of_term [Ast_info] | |
term_of_exp_info [Cil] | Constructs a term from a term node and an expression information |
term_offset_to_offset [Db.Properties.Interp] | |
term_to_exp [Db.Properties.Interp] | |
term_to_lval [Db.Properties.Interp] | |
terminated [Task] | Number of terminated process |
terminates [Annotations] | If any, get the terminates clause of the contract associated to the given function. |
the [Extlib] | |
theMachine [Cil] | Current machine description |
thirtytwo [Integer] | |
thread [Task] | |
time [Command] | Compute the elapsed time with |
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 |
to_array [Vector] | Makes a copy. |
to_bytes [FCBuffer] | Return a copy of the current contents of the buffer. |
to_float [Transitioning.Q] | |
to_float [Integer] | |
to_float [Fval.F] | |
to_float [Float_sig.S] | Converts a floating-point number of single or double precision into a caml float. |
to_int [Integer] | |
to_int32 [Integer] | |
to_int64 [Integer] | |
to_lexing_loc [Cil_datatype.Location] | |
to_lexing_pos [Cil_datatype.Position] | |
to_list [State_selection.S] | Convert a selection into a list of states. |
to_list [Bottom] | Conversion functions. |
to_ordered [Ordered_stmt] | Conversion functions between stmt and ordered_stmt. |
to_ordered [Dataflows.FUNCTION_ENV] | |
to_pretty_string [Filepath.Normalized] |
|
to_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] |
|
to_string [Parameter_sig.String_datatype_with_collections] | |
to_string [Parameter_sig.String_datatype] | |
to_string [Integer] | |
to_utf8 [Wutil] | |
to_varinfo [Base] | |
todo [Task] | Specialized version of |
token [Logic_lexer] | |
told [Logic_const] | \old |
toolbar [Wbox] | The first list is packed to the left side of the toolbar. |
toolbar [Menu_manager] | |
toolmenubar [Menu_manager] | |
top [Utf8_logic] | |
top [Qstack.Make] | Return the top element of the stack. |
top [Origin] | |
top [Map_lattice.MapSet_Lattice] | |
top [Map_lattice.Value] | |
top [Lmap_sig] | |
top [Lattice_type.With_Top] | largest element |
top [Int_Base] | |
top [Fval] | |
top [Float_interval_sig.S] | Top interval for a given precision, including infinite and NaN values. |
top_finite [Float_interval_sig.S] | The interval of all finite values in the given precision. |
top_float [Locations.Location_Bytes] | |
top_float [Ival] | |
top_int [Locations.Location_Bytes] | |
top_opt [Lattice_type.With_Top_Opt] | optional largest element |
top_single_precision_float [Locations.Location_Bytes] | |
top_single_precision_float [Ival] | |
top_string [Unicode] | |
top_with_origin [Locations.Location_Bytes] | Completely imprecise value. |
topify_arith_origin [Locations.Location_Bytes] | Topifying of values, in case of imprecise accesses |
topify_leaf_origin [Locations.Location_Bytes] | |
topify_merge_origin [Locations.Location_Bytes] | |
topify_misaligned_read_origin [Locations.Location_Bytes] | |
topify_with_origin [Offsetmap_lattice_with_isotropy] | Force a value to be isotropic, when a loss of imprecision occurs. |
topify_with_origin [Locations.Location_Bytes] | |
topify_with_origin_kind [Locations.Location_Bytes] | |
toplevel_attr [Cil_datatype.Typ] | returns the attributes associated to the toplevel type, without adding attributes from compinfo, enuminfo or typeinfo. |
trace_event [Gtk_helper] | Trace all events on stderr for the given object. |
track_garbled_mix [Locations.Location_Bytes] | |
trange [Logic_const] |
|
transfer_if_from_guard [Dataflows] |
|
transfer_stmt [Dataflows.FORWARD_MONOTONE_PARAMETER] |
|
transfer_stmt [Dataflows.BACKWARD_MONOTONE_PARAMETER] |
|
transfer_switch_from_guard [Dataflows] | Same as |
transform [Lattice_type.Lattice_Base] | |
transform [Descr] | Similar to |
transform_category [Exn_flow] | category of the code transformation above. |
transform_category [Destructors] | category of the transformation. |
transform_element [Logic_const] |
|
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] |
|
tresult [Logic_const] | \result |
trim [Rich_text] | Range of non-blank leading and trailing characters. |
trim_by_validity [Tr_offset] |
|
triple [Datatype] | |
trunc [Fval] | |
trunc [Floating_point] | Rounds to integer, toward zero (like trunc() in C). |
trunc [Float_sig.S] | |
trunc [Float_interval_sig.S] | |
truncate [FCBuffer] |
|
truncateInteger64 [Cil] | Represents an integer as for a given kind. |
truncate_to_integer [Floating_point] | Raises |
try_finally [Extlib] | |
tstring [Logic_const] | string constant |
tuning_parameters [Emitter.Usable_emitter] | |
tuning_parameters [Emitter] | |
tvar [Logic_const] | variable |
two [Integer] | |
two_power [Integer] | Computes |
two_power_32 [Integer] | |
two_power_64 [Integer] | |
two_power_of_int [Integer] | Computes |
ty [Type.Abstract] | |
ty [State_selection] | Type value representing |
ty [Datatype.Ty] | |
typ_of_link [Gui_printers] | Convert a string of the form |
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 [Cabs2cil] | A hook into the code that creates temporary local vars. |
typeHasAttribute [Cil] | Does the type have the given attribute. |
typeHasAttributeDeep [Cil] | |
typeHasAttributeMemoryBlock [Cil] |
|
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 |
typeOf_array_elem [Cil] | Returns the type of the array elements of the given type. |
typeOf_pointed [Cil] | Returns the type pointed by the given type. |
typeOffset [Cil] | Compute the type of an offset from a base type |
typeRemoveAllAttributes [Cil] | same as above, but remove any existing attribute from the type. |
typeRemoveAttributes [Cil] | Remove all attributes with the given names from a type. |
typeRemoveAttributesDeep [Cil] | Same as |
typeTermOffset [Cil] | Equivalent to |
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] | 4.03 |
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 [Utf8_logic] | |
union [State_selection.S] | Union of two selections. |
union [FCSet.S_Basic_Compare] | Set union. |
union_string [Unicode] | |
uniqueVarNames [Cil] | Assign unique names to local variables. |
unique_name_from_name [State] | |
unit [Datatype] | |
unknown [Cil_datatype.Location] | |
unknown [Cil_datatype.Position] | |
unknown [Filepath.Normalized] | Unknown filepath, used as 'dummy' for |
unmarshable [Descr] | Descriptor for unmarshallable types. |
unrollType [Cil] | Unroll a type until it exposes a non
|
unrollTypeDeep [Cil] | Unroll all the TNamed in a type (even under type constructors such as
|
unroll_ltdef [Logic_const] | expands logic type definitions only. |
unroll_transform [Unroll_loops] | |
unroll_type [Logic_utils] | expands logic type definitions. |
unroll_unnatural_loop [Interpreted_automata.UnrollUnnatural] | |
unsafeSetFormalsDecl [Cil] | replace formals of a function declaration with the given list of varinfo. |
unsafe_pack [Structural_descr] | |
unsafe_set [Kernel.LibEntry] | Not for casual users. |
unsafe_set [Kernel.MainFunction] | |
unset_compinfo [Cil] | |
unset_enuminfo [Cil] | |
unset_enumitem [Cil] | |
unset_fieldinfo [Cil] | |
unset_fundec [Cil] | |
unset_kernel_function [Cil] | |
unset_logic_info [Cil] | |
unset_logic_type_info [Cil] | |
unset_logic_var [Cil] | |
unset_model_info [Cil] | |
unset_orig_compinfo [Cil] | |
unset_orig_enuminfo [Cil] | |
unset_orig_enumitem [Cil] | |
unset_orig_fieldinfo [Cil] | |
unset_orig_fundec [Cil] | |
unset_orig_kernel_function [Cil] | |
unset_orig_logic_info [Cil] | |
unset_orig_logic_type_info [Cil] | |
unset_orig_logic_var [Cil] | |
unset_orig_model_info [Cil] | |
unset_orig_stmt [Cil] | |
unset_orig_typeinfo [Cil] | |
unset_orig_varinfo [Cil] | remove the entry associated with the given new varinfo in the current state of the visitor. |
unset_stmt [Cil] | |
unset_typeinfo [Cil] | |
unset_varinfo [Cil] | remove the entry associated to the given varinfo in the current state of the visitor. |
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 [Indexer.Make] |
|
update_file_loc [Logic_lexer] | |
update_imprecise_everywhere [Offsetmap_sig] |
|
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 |
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] | 4.03 |
uppercase_ascii [Transitioning.String] | 4.03 |
use [Parameter_category] |
|
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 |
use_float [Gtk_helper.Configuration] | Same as |
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 |
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 |
V | |
v [Wbox] |
|
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 |
valid_offset [Base] | Computes all offsets that may be valid for an |
valid_part [Locations] | Overapproximation of the valid part of the given location. |
valid_range [Base] |
|
validity [Base] | |
validity_from_size [Base] |
|
validity_from_type [Base] | |
valueOfDigit [Cabshelper] | |
value_of_integral_const [Ast_info] | |
value_of_integral_expr [Ast_info] | |
value_of_integral_logic_const [Ast_info] | |
var [Cil] | Makes an lvalue out of a given variable |
var_is_in_scope [Kernel_function] |
|
variable_term [Ast_info] | |
varinfo_of_link [Gui_printers] | Convert a string of the form |
varinfo_of_localizable [Printer_tag] | |
varinfo_of_localizable [Pretty_source] | |
varname [Datatype.Make_input] | |
varname [Datatype.S_no_copy] | A good prefix name to use for an OCaml variable of this type. |
varname [Datatype.Undefined] | |
varname [Datatype] | |
vbox [Wbox] | Pack a list of boxes vertically. |
verbose_atleast [Log.Messages] | |
verify [Log.Messages] | If the first argument is |
verify_assigns_froms [Db.Value] | For internal use only. |
version [Cprint] | |
version [Config] | Frama-C Version identifier. |
version_and_codename [Config] | Frama-C version and codename. |
vertex [Service_graph.S] | |
vertex_attributes [State_dependency_graph.Attributes] | |
vertex_name [State_dependency_graph.Attributes] | |
vgroup [Wbox] | Pack a list of widgets vertically, with all widgets stuck to the same width |
vi [Cil_datatype.Kf] | |
visit [Rich_text] | Visit the message, with depth-first recursion on tags. |
visitCabsAttributes [Cabsvisit] | |
visitCabsBlock [Cabsvisit] | |
visitCabsDeclType [Cabsvisit] | Visits a decl_type. |
visitCabsDefinition [Cabsvisit] | |
visitCabsExpression [Cabsvisit] | |
visitCabsFile [Cabsvisit] | |
visitCabsName [Cabsvisit] | |
visitCabsSpecifier [Cabsvisit] | |
visitCabsStatement [Cabsvisit] | |
visitCabsTypeSpecifier [Cabsvisit] | |
visitCilAllocates [Cil] | |
visitCilAllocation [Cil] | |
visitCilAnnotation [Cil] | |
visitCilAssigns [Cil] | |
visitCilAttributes [Cil] | Visit a list of attributes |
visitCilBehavior [Cil] | |
visitCilBehaviors [Cil] | |
visitCilBlock [Cil] | Visit a block |
visitCilCodeAnnotation [Cil] | |
visitCilDeps [Cil] | |
visitCilEnumInfo [Cil] | |
visitCilExpr [Cil] | |
visitCilExtended [Cil] | visit an extended clause of a behavior. |
visitCilFile [Cil] | Same thing, but the result is ignored. |
visitCilFileCopy [Cil] | Visit a file. |
visitCilFileSameGlobals [Cil] | A visitor for the whole file that does not *physically* change the globals (but maybe changes things inside the globals through side-effects). |
visitCilFrees [Cil] | |
visitCilFrom [Cil] | |
visitCilFunction [Cil] | Visit a function definition |
visitCilFunspec [Cil] | |
visitCilGlobal [Cil] | Visit a global |
visitCilIdPredicate [Cil] | |
visitCilIdTerm [Cil] | visit identified_term. |
visitCilInit [Cil] | Visit an initializer, pass also the global to which this belongs and the offset. |
visitCilInitOffset [Cil] | Visit an initializer offset |
visitCilInstr [Cil] | Visit an instruction |
visitCilLocal_init [Cil] | Visit a local initializer (with the local being initialized). |
visitCilLogicInfo [Cil] | |
visitCilLogicType [Cil] | |
visitCilLogicVarDecl [Cil] | |
visitCilLogicVarUse [Cil] | |
visitCilLval [Cil] | Visit an lvalue |
visitCilModelInfo [Cil] | |
visitCilOffset [Cil] | Visit an lvalue or recursive offset |
visitCilPredicate [Cil] | |
visitCilPredicateNode [Cil] | |
visitCilPredicates [Cil] | |
visitCilStmt [Cil] | Visit a statement |
visitCilTerm [Cil] | |
visitCilTermLhost [Cil] | |
visitCilTermLval [Cil] | visit term_lval. |
visitCilTermOffset [Cil] | |
visitCilType [Cil] | Visit a type |
visitCilVarDecl [Cil] | Visit a variable declaration |
visitFramacAllocation [Visitor] | |
visitFramacAnnotation [Visitor] | |
visitFramacAssigns [Visitor] | |
visitFramacAttributes [Visitor] | Visit a list of attributes |
visitFramacBehavior [Visitor] | |
visitFramacBehaviors [Visitor] | |
visitFramacBlock [Visitor] | Visit a block |
visitFramacCodeAnnotation [Visitor] | |
visitFramacDeps [Visitor] | |
visitFramacExpr [Visitor] | Visit an expression |
visitFramacExtended [Visitor] | |
visitFramacFile [Visitor] | Same thing, but the result is ignored. |
visitFramacFileCopy [Visitor] | Visit a file. |
visitFramacFileSameGlobals [Visitor] | A visitor for the whole file that does not change the globals (but maybe changes things inside the globals). |
visitFramacFrom [Visitor] | |
visitFramacFunction [Visitor] | Visit a function definition. |
visitFramacFunspec [Visitor] | |
visitFramacGlobal [Visitor] | Visit a global. |
visitFramacIdPredicate [Visitor] | |
visitFramacIdTerm [Visitor] | visit identified_term. |
visitFramacInit [Visitor] | Visit an initializer, pass also the global to which this belongs and the offset. |
visitFramacInitOffset [Visitor] | Visit an initializer offset |
visitFramacInstr [Visitor] | Visit an instruction |
visitFramacKf [Visitor] | Visit a kernel_function. |
visitFramacLogicInfo [Visitor] | |
visitFramacLogicType [Visitor] | |
visitFramacLogicVarDecl [Visitor] | Visit a logic variable declaration |
visitFramacLval [Visitor] | Visit an lvalue |
visitFramacModelInfo [Visitor] | |
visitFramacOffset [Visitor] | Visit an lvalue or recursive offset |
visitFramacPredicate [Visitor] | |
visitFramacPredicateNode [Visitor] | |
visitFramacPredicates [Visitor] | |
visitFramacStmt [Visitor] | Visit a statement |
visitFramacTerm [Visitor] | |
visitFramacTermLhost [Visitor] | |
visitFramacTermLval [Visitor] | |
visitFramacTermOffset [Visitor] | |
visitFramacType [Visitor] | Visit a type |
visitFramacVarDecl [Visitor] | Visit a variable declaration |
voidConstPtrType [Cil] | void const * |
voidPtrType [Cil] | void * |
voidType [Cil_const] | |
voidType [Cil] | void |
vscroll [Wbox] | Same as |
W | |
w [Wbox] | Helper to |
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 [Lmap_sig] | |
widen [Lattice_type.With_Widening] |
|
widen [Float_interval_sig.S] | |
widen_down [Float_sig.S] | |
widen_up [Float_sig.S] |
|
window [Gtk_compat] | |
with_codependencies [State_selection.S] | The selection containing the given state and all its co-dependencies. |
with_dependencies [State_selection.S] | The selection containing the given state and all its dependencies. |
with_error [Log.Messages] |
|
with_failure [Log.Messages] |
|
with_null [Pretty_utils] | Discards the message and call the continuation. |
with_null [Log] | Discards the message and call the continuation. |
with_result [Log.Messages] |
|
with_unfold_precond [Printer_tag.S_pp] | |
with_warning [Log.Messages] |
|
without_annot [Printer_api.S_pp] |
|
without_unicode [Kernel.Unicode] | Execute the given function as if the option |
wkey_acsl_extension [Kernel] | |
wkey_acsl_float_compare [Kernel] | |
wkey_annot_error [Kernel] | error in annotation. |
wkey_cert_exp_10 [Kernel] | |
wkey_cert_exp_46 [Kernel] | |
wkey_cert_msc_38 [Kernel] | |
wkey_check_volatile [Kernel] | |
wkey_cmdline [Kernel] | Command-line related warning, e.g. |
wkey_decimal_float [Kernel] | |
wkey_drop_unused [Kernel] | |
wkey_implicit_conv_void_ptr [Kernel] | |
wkey_implicit_function_declaration [Kernel] | |
wkey_incompatible_pointer_types [Kernel] | |
wkey_incompatible_types_call [Kernel] | |
wkey_int_conversion [Kernel] | |
wkey_jcdb [Kernel] | |
wkey_missing_spec [Kernel] | |
wkey_name [Log.Messages] | returns the warning category name as a string. |
wkey_no_proto [Kernel] | |
write [Journal] |
|
write_file [Command] | Properly close the channel and re-raise exceptions |
wto_index_diff [Wto_statement] | |
wto_index_diff [Interpreted_automata.Compute] | |
wto_index_diff [Interpreted_automata] | |
wto_index_diff_of_stmt [Wto_statement] | |
wto_index_of_stmt [Wto_statement] | |
wto_of_kf [Wto_statement] | |
X | |
x86_16 [Machdeps] | |
x86_32 [Machdeps] | |
x86_64 [Machdeps] | |
x_or [Utf8_logic] | |
xor [Extlib] | exclusive-or. |
Z | |
zero [Ival] | The lattice element that contains only the integer 0. |
zero [Integer] | |
zero [Int_Base] | |
zero [Cil] | 0 |
zero [Abstract_interp.Rel] | |
zero_or_one [Locations.Location_Bytes] | |
zero_or_one [Ival] | The lattice element that contains only the integers 0 and 1. |
zeros [Fval] | Both positive and negative zero |
zone_of_varinfo [Locations] |