Index of values

This monad propagates the `Bottom value if needed, and join the alarms of each evaluation.

Use this monad of the following function returns no alarms.

Use this monad if the following function returns a simple value.

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

add x s returns the equality between all elements of s and x.

! Different semantics according to the kind of the alarm map.

Add a new binding.

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

add_untyped ~factor e1 e2 computes e1+factor*e2 using C semantic for +, i.e.

Under-approximating variant of Cvalue.V.add_untyped.

Emit an alarm, either as warning or as a result, according to option AlarmsWarnings.

all alarms: all potential assertions have a Unknown status.

all_values ~size v returns true iff v contains all integer values representable in size bits.

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

assign kinstr lv expr v valuation state is the transfer function for the assignment lv = expr for state.

Transfer function for an assumption.

assume ~valuation state expr value assumes in the valuation that the expression expr has the value value in the state state, and backward propagates this information to the subterm of expr.

Backward evaluation of the binary operation left binop right = result; tries to reduce the argument left and right according to result.

This function tries to reduce the argument values of a binary operation, given its result.

Backward evaluation of the cast of the value src_val of type src_typ into the value dst_val of type dst_typ.

This function tries to reduce the argument of a cast, given the result of the cast.

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

backward_location state lval typ loc v reduces the location loc of the lvalue lval of type typ, so that only the locations that may have value v are kept.

Backward evaluation of the unary operation unop arg = res; tries to reduce the argument arg according to res.

This function tries to reduce the argument value of an unary operation, given its result.

Return the list of all bindings of the given map.

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

can_copy is_ret state kf lv e checks whether assigning e to lv inside function kf and in the context of state can be a simple copy of an lval or must be an assignment (see Eval.assigned for more information).

Return the number of bindings of a map.

Return the number of elements of the equality.

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.

Change the callstacks for the results for which this is meaningful.

Needed for unspecified sequences.

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

Return the representative of the equality.

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.

Clear all the caches used internally by the functions of this module.

Functions dealing with call stacks.

Removes from the valuation all the subexpressions of expr that contain subexpr, except subexpr itself.

clobbered_set_from_ret state ret can be used for functions that return a pointer to where they have written some data.

Total ordering between maps.

Test that two functions types are compatible; used to verify that a call through a function pointer is ok.

Perform a full analysis, starting from the given kernel_function and with the abstractions specified by the configuration.

Compute a call to the main function.

Compute a call to the main function from the given initial state.

Evaluate kf in state with_formals, first by reducing by the preconditions, then by evaluating the assigns, then by reducing by the post-conditions.

Build a configuration according to the analysis parameters.

Returns the abstract value of a literal constant, and potentially some alarms in case of floating point constants overflow.

contains elt set = true iff elt belongs to an equality of set.

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

Computes the value of a lvalue, with possible indeterminateness: the returned value may be uninitialized, or contain escaping addresses.

Create and register a new variable inside Frama-C.

The abstractions used in the latest analysis, and its results.

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

Return the initial state of the cvalue domain only.

Key for cvalues.

A default set of hints

Default configuration of EVA.

Display a complete summary of performance informations.

Debug category used when emitting an alarm in "non-warning" mode

Debug category used to print garbled mix

Debug categories responsible for printing initial and final states of Value.

Debug category used to print information about invalid pointer comparisons

print information on the garbled mix created during evaluation

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

Emits the alarms according to the given warn mode, at the given instruction.

Emit an ACSL assert (using \warning predicate) to signal that the builtin encountered an alarm described by the string.

The empty map.

An empty set of hints

Initialization

Generate an empty spec assigns \nothing or assigns \result \from \nothing, to be used to "approximate" the results of a recursive call.

Scoping: abstract transformers for entering and exiting blocks.

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.

The equality predicate used to compare keys.

Are two maps equal?

Evaluation of the function argument of a Call constructor

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

evaluate ~valuation state expr evaluates the expression expr in the state state, and returns the pair result, alarms, where: alarms are the set of alarms ensuring the soundness of the evaluation;, result is either `Bottom if the evaluation leads to an error, or `Value (valuation, value), where value is the numeric value computed for the expression expr, and valuation contains all the intermediate results of the evaluation. The valuation argument is a cache of already computed expressions. It is empty by default. The reduction argument allows deactivating the backward reduction performed after the forward evaluation.

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

exists p s checks if at least one element of the equality satisfies the predicate p.

Is there some element satisfying the given predicate?

Query function for compound expressions: eval oracle t exp returns the known value of exp by the state t.

Query function for lvalues: find oracle t lval typ loc returns the known value stored at the location loc of the left value lval of type typ.

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

filter p s returns the equality between all elements in s that satisfy predicate p.

Mem exec.

finalize_call stmt call ~pre ~post computes the state after a function call, given the state pre before the call, and the state post at the end of the called function.

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.

find elt set return the (single) equality involving elt that belongs to set, or raise Not_found if no such equality exists.

may raise Not_found

may raise Not_found

Returns the status of a given alarm.

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.

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

returns the empty set when the key is not bound

returns the empty set when the key is not bound

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

Same as find, but return None in the last case.

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.

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s, in increasing order.

Iteration on special assertions built by the builtins

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

for_all p s checks if all elements of the equality satisfy the predicate p.

Perform a full analysis, starting from the main function.

forward_binop context typ binop v1 v2 evaluates the value v1 binop v2, and the alarms resulting from the operations.

Computes the field offset of a fieldinfo, with the given remaining offset.

forward_index typ value offset computes the array index offset of (Index (ind, off)), where the index expression ind evaluates to value and the remaining offset off evaluates to offset.

Mem case in the AST: the host is a pointer.

forward_unop context typ unop v evaluates the value unop v, and the alarms resulting from the operations.

Var case in the AST: the host is a variable.

Build a set from another elt-indexed map or set.

For a key of type k key: if the states of this domain (of type t) contain a part (of type k) from the domain identified by the key, then get key returns an accessor for this part of a state., otherwise, get key returns None.

Get the referenced value.

getWidenHints kf s retrieves the set of widening hints related to function kf and statement s.

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.

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

What are the acceptable values for this parameter.

What is the possible range of values for this parameter.

Fake varinfo used by Value to store the result of functions.

get_stmt_widen_hint_terms s returns the list of widen hints associated to s.

Logic labels valid at the given location.

Default value.

A hashing function on keys.

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

Identity of a key.

Range for an integer type with some attributes.

Increment the integer.

Given a function computing the location of lvalues, computes the memory zone on which the offset and the pointer expression (if any) of an lvalue depend.

Compute the initial state for an analysis.

Compute the initial state for an analysis (as in Initialization.S.initial_state), but also bind the formal parameters of the function given as argument.

add to the current state a varinfo with its initialization.

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.

Abstract address for the given varinfo.

Intersection.

Pointwise intersection of property status: the most precise status is kept.

intersect s s' = true iff the two equalities both involve the same element.

intersects s1 s2 returns true if and only if s1 and s2 have an element in common

Key for intervals.

Returns true if the value may not be a pointer.

Bitfields

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

is_dynamic wh returns true iff widening hint wh has a "dynamic" prefix.

Test whether a map is empty or not.

Is there an assertion with a non True status ?

is_global wh returns true iff widening hint wh has a "global" prefix.

Inclusion test.

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).

Given the current state of the call stack, detect whether the given given function would start a recursive cycle.

Return true iff the argument has been created by Value_util.zero

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

iter f s applies f in turn to all elements of s.

Semi-lattice structure.

Do both operations simultaneously

returns true if the function assigns only \result or variables that have volatile qualifier (that are usually not tracked by domains anyway).

Legacy configuration of EVA, with only the cvalue domain enabled.

Length of the table.

Loads the saved initial global state, and merges it with the given state (locals plus new globals which were not present in the original AST).

Slevel to use in this function

Those two expressions indicate that one l-value contained inside the arguments (or the l-value itself for lval_contains_volatile) has volatile qualifier.

lvaluate ~valuation ~for_writing state lval evaluates the left value lval in the state state.

Builds the abstractions according to a configuration.

make_escaping ~exact ~escaping ~on_escaping ~within state changes all references to the variables in escaping to "escaping address".

make_escaping_fundec fdec clob l state changes all references to the local or formal variables in l to "escaping".

'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.

All bases that have been dynamically created in the current execution.

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.

initialized/escaping information is the join of the information on each argument.

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.

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

mem x s tests whether x belongs to the equality s.

Tests whether a key belongs to the domain.

mem equality set = true iff ∃ eq ∈ set, equality ⊆ eq

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

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

See the corresponding functions in Offsetmap_sig.

return true if the two types are statically distinct, and a cast from one to the other may have an effect on an abstract value.

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

no alarms: all potential assertions have a True status.

Calls the functions registered in the warn_mode according to the set of alarms.

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

Set the boolean to false.

Needed for Evaluation.get_influential_vars

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.

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

Are apron domains available?

Set the boolean to true.

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

The equality between two elements.

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.

Key for precise locs.

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

Prints the current callstack.

Parses all widening hints defined via the widen_hint syntax extension.

Pretty-prints a set of hints (for debug purposes only).

Print a call stack without displaying call sites.

Raises Not_based_on_null if the value may be a pointer.

Check inclusion of two integer ranges.

Inter-reduction of values.

reduce ~valuation state expr positive evaluates the expression expr in the state state, and then reduces the valuation such that the expression expr evaluates to a zero or a non-zero value, according to positive.

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.

Given a reduction expr = value, provides more reductions that may be performed.

Same behavior as reduce_previous_binding, but takes a value with 'undefined' and 'escaping addresses' flags.

reduce_index_by_array_size ~size_expr ~index_expr size index reduces the value index to fit into the interval 0..(size-1).

reduce_loc_by_validity for_writing bitfield lval loc reduce the location loc by its valid part for a read or write operation, according to the for_writing boolean.

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.

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

Returns a list of the pairs (name, builtin_sig) registered via register_builtin.

Read the given value with the given type.

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

Add the given set of bases to an existing clobbered set

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 x s returns the equality between all elements of s, except x.

remove elt set remove any occurrence of elt in set.

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

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

Add a new binding.

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

resolve_functions ~typ_pointer v finds within v all the functions with a type compatible with typ_pointer.

given (funs, warn) = resolve_functions typ v, funs is the set of functions pointed to by v that have a type compatible with typ.

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

reuse_previous_call kf init_state args searches amongst the previous analyzes of kf one that matches the initial state init_state and the values of arguments args.

safe_argument e returns true if e (which is supposed to be an actual parameter) is guaranteed to evaluate in the same way before and after the call.

Saves the final state of globals variables after the return statement of the function defined via Value_parameters.SaveFunctionState.

For a key of type k key: if the states of this domain (of type t) contain a part (of type k) from the domain identified by the key, then set key d state returns the state state in which this part has been replaced by d., otherwise, set key _ is the identity function.

set alarm status t binds the alarm to the status in the map t.

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.

Export the shape of the set.

Mark the analysis as aborted.

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

singleton alarm creates the map add alarm none: alarm has a Unknown status, and all others have a True status.

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.

Decision on a function call: start_call stmt call valuation state decides on the analysis of a call site.

Call start_doing when finishing analyzing a function.

store_computed_call kf init_state args call_results memoizes the fact that calling kf with initial state init_state and arguments args resulted in the results call_results.

A structure matching the type of the domain.

See Locations.sub_pointwise.

Greatest element.

Returns the canonical representant of a definitely uninitialized value.

Union.

Pointwise union of property status: the least precise status is kept.

unite a b map unites a and b in map.

update valuation t updates the state t by the values of expressions and the locations of lvalues stored in valuation.

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

Overapproximation of the valid part of the given location for a read or write operation, according to the for_writing boolean.

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

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

Emits warnings for each function definition that will be overridden by an EVA built-in.

division.

Do not emit any message.

warn on invalid pointer comparison.

Abort the analysis, signaling that Top has been found.

widen h t1 t2 is an over-approximation of join t1 t2.

Specialization of the function above for standard types

written_formals kf is an over-approximation of the formals of kf which may be internally overwritten by kf during its call.

Return a zero constant compatible with the type of the argument

Given a function computing the location of lvalues, computes the memory zone on which the value of an expression depends.