Index of values

add x y m returns a map containing the same bindings as m, plus a binding of x to y.

Add a new binding.

Adding elements

add_binding state loc v simulates the effect of writing v at location loc in state.

Temporary.

Temporary.

Same as above, but the hook is applied after clean up.

add_code_transformation_before_cleanup name hook adds an hook in the corresponding category that will be called during the normalization of a linked file, before clean up and removal of temps and unused declarations.

Add numeric hints for one or all variables (None), for a a certain stmt or for all statements (None).

Update the trace of all the states in the stateset.

Add a set of bases to widen in priority for a given statement.

apply_all_locs f loc state folds f on all the atomic locations in loc, provided there are less than plevel.

Bind all locals of the the block to their default value (namely UNINITIALIZED)

Return the list of all bindings of the given map.

Return a function that topifies all references to the variables local to the given blocks.

For statements: results are available only if the statement is reachable.

Return the number of bindings of a map.

Should not be used, Precise_locs.valid_cardinal_zero_or_one is almost always more useful

cast ~size ~signed v applies to the abstract value v the conversion to the integer type described by size and signed.

if needed, cast the given abstract value to the given size.

Check the precondition of kf.

Check that kf is not already present in the call stack

Return one binding of the given map, or raise Not_found if the map is empty.

State in which the predicate, found in the given function, should be evaluated

Clean all previously stored results

Clear the table.

Reset the reference to its default value.

Functions dealing with call stacks.

Total ordering between maps.

Deep copy: no possible sharing between x and copy x.

Tempory.

Create and register a new variable inside Frama-C.

Return a new project with a new cil file representation by visiting the file of the current project.

Like File.create_project_from_visitor, but the new generated cil file is generated into a temp .i or .c file according to preprocess, then re-built by Frama-C in the returned project.

The current function is the one on top of the call stack.

A default set of hints

Does the evaluation of stmt modifies the eventual value of X.lv?

Display a complete summary of performance informations.

Builtins with multiple names; the lookup is done using a distinctive prefix

Assumes the current project is old_prj

The empty map.

An empty set of hints

Creation

Creation

Used by auxiliary plugins, that do not supply the other states

equal cmp m1 m2 tests whether the maps m1 and m2 are equal, that is, contain equal keys and associate them with equal data.

Can only be called on the 6 comparison operators

Same functionality as Eval_exprs.eval_expr_with_deps_state.

The arguments are the approximate float value computed during parsing, the size of the floating-point type, and the string representing the initial constant if available.

Return a pair of (under-approximating, over-approximating) zones.

exists p m checks if at least one binding of the map satisfy the predicate p.

Is there some element satisfying the given predicate?

filter p m returns the map with all the bindings in m that satisfy predicate p.

find x m returns the current binding of x in m, or raises Not_found if no such binding exists.

find ?conflate_bottom state loc returns the same value as find_indeterminate, but removes the indeterminate flags from the result.

Tempory.

Return the current binding of the given key.

Search a given key in the map.

Return the list of all data associated with the given key.

Find a previously registered builtin.

find_unspecified ~conflate_bottom state loc returns the value and flags associated to loc in state.

Classify a Cil_types.fkind as either a 32 or 64 floating-point type.

fold f m a computes (f kN dN ... (f k1 d1 a)...), where k1 ... kN are the keys of all bindings in m (in increasing order), and d1 ... dN are the associated data.

Iterators

Iterators

for_all p m checks if all the bindings of the map satisfy the predicate p.

Build a file from its name.

Get the referenced value.

Return the list of toplevel files.

returns the given argument only if it is a valid function name (see Parameter_customize.get_c_ified_functions for more information), and abort otherwise.

File name.

always return the argument, even if the argument is not a function name.

What are the acceptable values for this parameter.

Return the preprocessor command to use.

What is the possible range of values for this parameter.

Logic labels valid at the given location.

Default value.

Widen hints for a given statement, suitable for function Cvalue.Model.widen.

Increment the integer.

Initialize the cil file representation of the current project.

Initialize the cil file representation with the file given on the command line.

Initialize the cil file representation with the given file for the given project from the current one.

init_project_from_visitor prj vis initialize the cil file representation of prj.

initialize_var_using_type varinfo state uses the type of varinfo to create an initial value in state.

initialized v returns the definitely initialized, non-escaping representant of v.

Bitfields

Detect that the type is const, and that option -global-const is set.

Test whether a map is empty or not.

Information

Information

is_indeterminate v = false implies v only has definitely initialized values and non-escaping addresses.

is_initialized v = true implies v is definitely initialized.

is_noesc v = true implies v has no escaping addresses.

Returns true iff there exists executions of the statement that does not always fail/loop (for function calls).

iter f m applies f to all bindings in map m.

Export

Export

Join the given state_set.

Length of the table.

Slevel to use in this function

machdep_macro machine returns the name of a macro __FC_MACHDEP_XXX so that the preprocessor can select std lib definition consistent with the selected machdep.

'Simplify' the location if it represents a contiguous zone: instead of multiple offsets with a small size, change it into a single offset with a size that covers the entire range.

make_volatile ?typ v makes the value v more general (to account for external modifications), whenever typ is None or when it has type qualifier volatile

map f m returns a map with same domain as m, where the associated value a of all bindings of m has been replaced by the result of the application of f to a.

Same as FCMap.S.map, but the function receives as arguments both the key and the associated value for each binding of the map.

Same as FCMap.S.min_binding, but returns the largest binding of the given map.

Print a message about the given location containing a completely indeterminate value.

Emit an alarm about a non-null divisor when the supplied value may contain zero.

Warn for unitialized or escaping bits in the value passed as argument.

mem x m returns true if m contains a binding for x, and false otherwise.

Does the given element belong to the set?

Does the builtin table contain an entry for name?

memo tbl k f returns the binding of k in tbl.

Memoization.

merge f m1 m2 computes a map whose keys is a subset of keys of m1 and of m2.

Slevel merge strategy for this function

Merge the two sets together.

Raise Unchanged if the first set was already included in into

For all formals of kf whose address is taken, merge their values in prev_state and new_state, and update new_state.

Return the smallest binding of the given map (with respect to the Ord.compare ordering), or raise Not_found if the map is empty.

must_recompute_cfg f must be called by code transformation hooks when they modify statements in function f.

Counter that must be used each time a new call is analyzed, in order to refer to it later

new_file_type suffix func funcname registers a new type of files (with corresponding suffix) as recognized by Frama-C through func.

new_machdep name module registers a new machdep name as recognized by Frama-C through The usual uses is Cmdline.run_after_loading_stage (fun () -> File.new_machdep "my_machdep" my_machdep_implem)

Set the boolean to false.

Returns the first eventual imprecise part contained in an offsetmap

offsetmap_matches_type t o returns true if either: o contains a single scalar binding, of the expected scalar type t (float or integer), o contains multiple bindings, pointers, etc., t is not a scalar type.

May raise Int_Base.Error_Top

Transformation a value into an offsetmap of size sizeof(typ) bytes.

offsetmap_top_addresses_of_locals is_local returns a function that topifies all the parts of an offsetmap that contains a pointer verifying is_local.

Set the boolean to true.

To be used by the plugin to output the results of the option in a controlled way.

Should the given function be replaced by a call to a builtin

partition p m returns a pair of maps (m1, m2), where m1 contains all the bindings of s that satisfy the predicate p, and m2 is the map with all the bindings of s that do not satisfy p.

Returns the list of terminating callstacks and the list of non-terminating callstacks.

Temporary.

Does the post-conditions of this specification mention \result?

Prints the current callstack.

Register some file as source file before command-line files

Initialize the AST of the current project according to the current filename list.

Print the project CIL file on the given Formatter.

Print a call stack.

Raises Not_based_on_null if the value may be a pointer.

reduce_binding state loc v refines the value associated to loc in state according to v, by keeping the values common to the existing value and v.

Never returns Model.bottom.

reduce_by_danglingness dangling v reduces v so that its result r verifies \dangling(r) if dangling is true, and !\dangling(r) otherwise.

reduce_by_initializedness initialized v reduces v so that its result r verifies \initialized(r) if initialized is true, and !\initialized(r) otherwise.

reduce_previous_binding state loc v reduces the value associated to loc in state; use with caution, as the inclusion between the new and the old value is not checked.

Reduction of a Cvalue.V.t by ==, !=, >=, >, <= and <.

Register the given OCaml function as a builtin, that will be used instead of the Cil C function of the same name

Adds a new category of code transformation

Read the given value value as a float int of the given fkind.

Read the given value value as an int of the given ikind.

Add the given set of bases to an existing clobbered set

Same as above with an entire offsetmap

remember_locals_in_value clob loc v adds all bases pointed to by loc to clob if v contains the address of a local or formal

remove x m returns a map containing the same bindings as m, except for x which is unbound in the returned map.

Remove 'unitialized' and 'escaping addresses' flags from the argument

For variables that are coming from the AST, this is equivalent to uninitializing them.

Invert the order in which the states are iterated over

reorder globals so that all uses of an identifier are preceded by its declaration.

Add a new binding.

Reset the internal state of the module; to call at the very beginning of the analysis.

Catch the fact that we are in a function for which -no-results or one of its variants is set.

reuse_previous_call (kf, ki) init_state searches amongst the previous analyzes of kf one that matches the initial state init_state.

Change the referenced value.

This function must be called when callstacks are focused.

Set the dependencies for the output of the option.

Set what are the acceptable values for this parameter.

Set what is the possible range of values for this parameter.

singleton x y returns the one-element map that contains a binding y for x.

Size of the type of a lval, taking into account that the lval might have been a bitfield.

split x m returns a triple (l, data, r), where l is the map with all the bindings of m whose key is strictly less than x; r is the map with all the bindings of m whose key is strictly greater than x; data is None if m contains no binding for x, or Some v if m binds v to x.

If reduce is true, reduce in all cases.

state_top_addresses_of_locals exact warn topoffsm clob generalizes topoffsm into a function that topifies a memory state.

Call start_doing when finishing analyzing a function.

store_computed_call (kf, ki) init_state actuals outputs memoizes the fact that calling kf at statement ki, with initial state init_state and arguments actuals resulted in the states outputs; the expressions in the actuals are not used.

Substracts two pointers (assumed to have type char*) and returns the difference of their offsets.

Return two functions that topifies all references to the locals and formals of the given function.

Helper function to create the best type for a new base.

Returns the canonical representant of a definitely uninitialized value.

Reads the contents of the offsetmap (assuming it contains sizeof(typ) bytes) as a value of type V.t, then convert the result to type typ

Reads the contents of the offsetmap (assuming it contains sizeof(typ) bytes), and return them as an uninterpreted value.

Is the restriction of the given location to its valid part precise enough to perform a strong read, or a strong update.

Emit all messages, including alarms and informative messages regarding the loss of precision.

division.

warning to be emitted when two incompatible accesses to a location are done in unspecified order.

warn_index w ~positive ~range emits a warning signaling an out of bounds access.

This function should be used to treat a call lv = kf(...).

Do not emit any message.

If the supplied offsetmap has an arithmetic type and contains indeterminate bits (uninitialized, or escaping address), raises the corresponding alarm(s) and returns the reduced offsetmap and state.

Warn that the RHS of a shift operator must be positive, and optionnally less than the given size.

Warn that the LHS of the left shift operator must be positive.

Abort the analysis, signaling that Top has been found.

Specialization of the function above for standard types

write_abstract_value ~with_alarms state lv typ_lv loc_lv v writes v at loc_lv in state, casting v to respect the type typ_lv of lv.

Over-approximation of its formals the given function may write into.