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.

Returns true if base is a global, or a formal or local of either kf or one of its callers.

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

Adds a state into an index.

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

add loc typ v state binds loc to v in state.

Add a new binding.

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

Add the given bindings to the map, in order.

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

Under-approximating variant of Cvalue.V.add_untyped.

Computes (an overapproximation of) the memory zones that must be read to evaluate the given lvalue, excluding the lvalue zone itself.

Computes (an overapproximation of) the memory zones that must be read to evaluate the given lvalue, excluding the lvalue zone itself.

Just after a statement is executed.

Just after a statement is executed.

Emit an alarm, either as warning or as a result, according to status associated to Self.wkey_alarm

Returns the set of alarms emitted during the evaluation.

Returns the set of alarms emitted during the evaluation.

all alarms: all potential assertions have a Unknown status.

Default mode: all permissions are granted.

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

Returns the current analysis status of a given function.

annot_predicate_deps ~pre ~here p computes the logic dependencies needed to evaluate the predicate p in a code annotation in cvalue state here, in a function whose pre-state is pre.

annot_predicate_deps ~pre ~here p computes the logic dependencies needed to evaluate the predicate p in a code annotation in cvalue state here, in a function whose pre-state is pre.

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

Are results available for a given function? True if the function body has been has been analyzed and the results have been saved.

Are results available for a given function? True if the function body has been has been analyzed and the results have been saved.

Converts the value into a Cvalue abstraction.

Converts the value into a Cvalue abstraction.

Converts the value into a Cvalue abstraction with 'undefined' and 'escaping addresses' flags.

Converts the value into a Cvalue abstraction with 'undefined' and 'escaping addresses' flags.

Converts the value into a Cvalue abstraction.

Converts the value into a Cvalue abstraction.

Converts the value into a floating point number.

Converts the value into a floating point number.

Converts the value into a floating point abstraction.

Converts the value into a floating point abstraction.

Converts the value into a singleton ocaml int.

Converts the value into a singleton ocaml int.

Converts the value into a singleton unbounded integer.

Converts the value into a singleton unbounded integer.

Converts the value into a C number abstraction.

Converts the value into a C number abstraction.

Converts into a C location abstraction.

Converts into a C location abstraction.

Converts into a Zone.

Converts into a Zone.

Converts into a Zone result.

Converts into a Zone result.

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.

Assumes that two locations do not overlap.

Assumes that the abstract value only represents well-formed pointer values: pointers either to an element of an array object or one past the last element of an array object.

Assumes that the given location is valid for a read or write operation, according to the for_writing boolean.

At the end of the analysis, after the main function has returned.

At the end of the analysis, after the main function has returned.

At the end of the given function.

At the end of the given function.

At the start of the analysis, but after the initialization of globals.

At the start of the analysis, but after the initialization of globals.

At the start of the given function.

At the start of the given function.

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

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 of a cast, given the result of the cast.

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

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.

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

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

Just before a statement is executed.

Just before a statement is executed.

Just before a statement or at the start of the analysis.

Just before a statement or at the start of the analysis.

Return the list of all bindings of the given map.

A list of builtins for the domain: each builtin is associated with the name of the C function it interprets.

Returns a list of subrequests for each reachable callstack from the given request.

Returns a list of subrequests for each reachable callstack from the given request.

After the analysis of a function call, recombines callee partitioning keys with the caller key.

Returns the kernel functions called in the given statement.

Returns the kernel functions called in the given statement.

Returns the list of inferred callers of the given function.

Returns the list of inferred callers of the given function.

Returns the list of inferred callers of the given function.

Returns the list of inferred callers, and for each of them, the list of callsites (the call statements) inside.

Returns the list of inferred callers, and for each of them, the list of callsites (the call statements) inside.

Returns the list of inferred callers, and for each of them, the list of callsites (the call statements) inside.

Returns the list of reachable callstacks from the given request.

Returns the list of reachable callstacks from the given request.

Return the number of bindings of a map.

Return the number of elements of the equality.

cardinal_estimate v ~size returns an estimation of the cardinal of v, knowing that v fits in size bits.

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

cast_int_to_int ~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.

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

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

Return the representative of the equality.

Return one binding of the given map, or None 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.

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.

Recombinaison of keys after a call

Combines two alarm maps carrying different sets of alarms.

Total ordering between maps.

Computes the Eva analysis, if not already computed, using the entry point of the current project.

Computes the Eva analysis, if not already computed, using the entry point of the current project.

Compute a call to the main function.

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

Compute analysis statistics.

Provided stmt is an 'if' construct, fst (condition_truth_value stmt) (resp.

Provided stmt is an 'if' construct, fst (condition_truth_value stmt) (resp.

Creates the configuration according to the analysis parameters.

Embeds C constants into value abstractions: returns an abstract value for the given constant.

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.

Creates the panel, attaches it to the lower notebook, and returns the display_by_callstack function allowing to display data on it.

Create and register a new variable inside Frama-C.

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

Get the current computation state of the analysis, updated by force_compute and states updates.

Get the current computation state of the analysis, updated by force_compute and states updates.

Get the current computation state of the analysis, updated by force_compute and states updates.

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

Return the initial state of the cvalue domain only.

A default set of hints

default d r extracts the value of r if r is Ok, or use the default value d otherwise.

The default configuration of Eva.

default d r extracts the value of r if r is Ok, or use the default value d otherwise.

Define the analysis target of a function according to Eva parameters.

Display a complete summary of performance informations.

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

Remove all states from the tank, leaving it empty as if it was just created by empty_tank

print information on the garbled mix created during evaluation

Register a dynamic abstraction: the abstraction is built by applying the last argument when starting an analysis, if the -eva-domains option has been set to name.

Returns the list of all elements of the given set.

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

The empty map.

An empty set of hints

The initial state with which the analysis start.

Creates an empty index.

Initial key: no partitioning.

Returns the list (name, descr) of currently enabled abstract domains.

Returns the list (name, descr) of currently enabled abstract domains.

Introduces a list of variables in the state.

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.

Are two maps equal?

Returns the list of expressions which have been inferred to be equal to the given expression by the Equality domain.

Returns the list of expressions which have been inferred to be equal to the given expression by the Equality domain.

Returns (an overapproximation of) the possible addresses of the lvalue.

Returns (an overapproximation of) the possible addresses of the lvalue.

Returns the kernel functions into which the given expression may evaluate.

Returns the kernel functions into which the given expression may evaluate.

Returns (an overapproximation of) the possible values of the expression.

Returns (an overapproximation of) the possible values of the expression.

Evaluation of the function argument of a Call constructor

Returns (an overapproximation of) the possible values of the lvalue.

Returns (an overapproximation of) the possible values of the lvalue.

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

Returns (an overapproximation of) the possible values of the variable.

Returns (an overapproximation of) the possible values of the variable.

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. Optional arguments are: valuation is a cache of already computed expressions; empty by default., reduction allows the deactivation of the backward reduction performed after the forward evaluation; true by default., subdivnb is the maximum number of subdivisions performed on non-linear sub-expressions of expr. If a lvalue occurs several times in expr, its value can be split up to subdivnb times to gain more precision. Set to the value of the option -eva-subdivide-non-linear by default.

Evaluates a predicate to a logical status in the current state.

exists f m checks if at least one binding of the map satisfies the predicate f.

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

Is there some element satisfying the given predicate?

Computes (an overapproximation of) the memory zones that must be read to evaluate the given expression, including all adresses computations.

Computes (an overapproximation of) the memory zones that must be read to evaluate the given expression, including all adresses computations.

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

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

Fill the states of the flow into the tank, modifying into inplace.

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

filter kf kind bases states reduces the state state to only keep properties about bases — it is a projection on the set of bases.

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

Only consider callstacks satisfying the given predicate.

Only consider callstacks satisfying the given predicate.

filter_map f m applies the function f to every binding of m, and builds a map from the results.

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 value of x in m, or raises Not_found if no binding for x 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.

find loc typ state returns the join of the abstract values stored in the locations abstracted to by loc in state, assuming the result has type typ.

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.

Returns the cvalue builtin for a function, if any.

returns the empty set when the key is not bound

find_first f m, where f is a monotonically increasing function, returns the binding of m with the lowest key k such that f k, or raises Not_found if no such key exists.

find_first_opt f m, where f is a monotonically increasing function, returns an option containing the binding of m with the lowest key k such that f k, or None if no such key exists.

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

find_last f m, where f is a monotonically decreasing function, returns the binding of m with the highest key k such that f k, or raises Not_found if no such key exists.

find_last_opt f m, where f is a monotonically decreasing function, returns an option containing the binding of m with the highest key k such that f k, or None if no such key exists.

find_opt x m returns Some v if the current value of x in m is v, or None if no binding for x exists.

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

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

fold f m init computes (f kN dN ... (f k1 d1 init)...), 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.

Fold on base value pairs.

fold_dynamic_bases f init folds f to each dynamically allocated base, with initial accumulator init.

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

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 typ binop v1 v2 evaluates the value v1 binop v2, resulting from the application of the binary operator binop to the values v1 and v2.

Abstract evaluation of casts operators from src_type to dst_type.

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 typ unop v evaluates the value unop v, resulting from the application of the unary operator unop to the value v.

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

Performs the equivalent of free for each location that was allocated via alloca() in the current function (as per Eva_utils.call_stack ()).

Evaluates the ACSL predicate \freeable(value): holds if and only if the value points to an allocated memory block that can be safely released using the C function free.

Get the current analysis statistics for a function

For a key of type k key: if the values of type t contain a subpart of type k from a module identified by the key, then get key returns an accessor for it., 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.

Special accessors for the main cvalue domain.

Returns the Cvalue state.

Returns the Cvalue state.

Returns the Cvalue model.

Returns the Cvalue model.

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.

Allows accessing the states inferred by an Eva analysis after it has been computed with the domain enabled.

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.

Computes the height of an expression, that is the maximum number of nested operations in this expression.

Computes the height of an lvalue.

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

Range for an integer type with some attributes.

Only consider the given callstack.

Only consider the given callstack.

Only consider the callstacks from the given list.

Only consider the callstacks from the given list.

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.

Build the initial tank for the entry point of a function.

Initializes a local variable in the current state.

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

initialize_variable lval loc ~initialized init_value state initializes the value of the location loc of lvalue lval in state with: – bits 0 if init_value = Zero; – any bits if init_value = Top.

Initializes a variable according to its type.

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.

Interprets an ACSL extension.

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

Returns true if the value may not be a pointer.

Bitfields

Returns true if an evaluation leads to bottom, i.e.

Returns true if an evaluation leads to bottom, i.e.

Has a builtin been registered with the given name?

Has a builtin been registered with the given name?

Is a given function replaced by a builtin?

Returns true if the function has been analyzed.

Returns true if the function has been analyzed.

Returns true if the function has been analyzed.

Return true iff the Eva analysis has been done.

Return true iff the value analysis has been done.

Return true iff the Eva analysis has been done.

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.

Returns true if there are no reachable states for the given request.

Is there an assertion with a non True status ?

Whether the Filepath is empty.

Returns true if there are no reachable states for the given request.

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.

Returns whether the evaluated value is initialized or not.

Returns whether the evaluated value is initialized or not.

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

Returns true if the statement has been reached by the analysis.

Returns true if the statement has been reached by the analysis.

Returns true if the statement has been reached by the analysis, or if the main function has been analyzed for Kglobal.

Returns true if the statement has been reached by the analysis, or if the main function has been analyzed for Kglobal.

Does the evaluated abstraction represents only one possible C value or memory location?

Does the evaluated abstraction represents only one possible C value or memory location?

Return true iff the argument has been created by Eva_utils.normalize_as_cond

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

Iterate on every function statistics

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

Iterates over all functions in the callgraph in reverse order, i.e.

Semi-lattice structure.

Join all incoming propagations into the given store.

The key identifies the module and the type t of abstract locations.

The key identifies the domain and the type t of its states.

The key identifies the module and the type t of abstract values.

Removes a list of local and formal variables from the state.

The configuration corresponding to the old "Value" analysis, with only the cvalue domain enabled.

Length of the table.

Slevel to use in this function

Category for the messages about the domain.

logic_assign None loc state removes from state all inferred properties that depend on the memory location loc.

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

Computes (an overapproximation of) the memory zones that must be read to evaluate the given lvalue, including the lvalue zone itself.

Computes (an overapproximation of) the memory zones that must be read to evaluate the given lvalue, including the lvalue zone itself.

This function is memoized to avoid creating too many expressions

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

Builds the abstractions according to a configuration.

Creates the information about a recursive call.

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.

Add a tab to the main GUI (for red alarms), and return its widget.

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.

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

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

Marks all RTE as generated.

Same as Map.S.min_binding, but returns the binding with the largest key in the given map.

Same as Map.S.min_binding_opt, but returns the binding with the largest key in the given map.

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

Returns true if the given flag is in the configuration.

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

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

Tests whether a key belongs to the module.

Does the given element belong to the set?

Memoization.

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

Slevel merge strategy for this function

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

Return the binding with the smallest key in the given map (with respect to the Ord.compare ordering), or None if the map is empty.

Over-approximation of the intersection of two abstract states (called meet in the literature).

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

Creates a new monitor that allows to split up to split_limit states.

Creates a new rationing, that can be used successively on several flows.

no alarms: all potential assertions have a True status.

normalize_as_cond e positive returns the expression corresponding to e != 0 when positive is true, and e == 0 otherwise.

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

Build a map from the given bindings

Set the boolean to false.

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.

Computes the offsetmap for an assignment: in case of a copy, extracts the offsetmap from the state;, otherwise, translates the value assigned into an offsetmap.

Returns the offsetmap at a precise_location from a state.

offsetmap_of_lval state lval loc extracts from state state the offsetmap at location loc, corresponding to the lvalue lval.

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

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.

True if some results are not stored due to options -eva-no-results or -eva-no-results-function.

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

This function is called after the analysis.

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

Prints the current callstack.

Parses all widening hints defined via the widen_hint syntax extension.

predicate_deps env p computes the logic dependencies needed to evaluate p in the given evaluation environment env.

Prepares the builtins to be used for an analysis.

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

Can be equal to pretty

Pretty printer for errors.

Pretty printer for errors.

Print a hash of the callstack when '-kernel-msg-key callstack' is enabled (prints nothing otherwise).

Pretty printer for API's results.

Pretty printer for API's results.

Print a call stack without displaying call sites.

Pretty the abstract value assuming it has the type given as argument.

Prints a summary of the analysis.

Raises Not_based_on_null if the value may be a pointer.

Raises Not_based_on_null if the value may be a pointer.

protect f ~cleanup runs f.

Checks inclusion of two integer ranges.

Trigger the recomputation of function stats

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.

reduce_by_predicate env state pred b reduces the current state by assuming that the predicate pred evaluates to b.

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

Registers an abstract domain.

register_builtin name ?replace ?typ cacheable f registers the function f as a builtin to be used instead of the C function of name name.

Registers available cvalue builtins for the -eva-builtin option.

register_builtin name ?replace ?typ cacheable f registers the function f as a builtin to be used instead of the C function of name name.

Registers a hook that will be called each time the analysis starts or finishes.

Registers a hook that will be called each time the analysis starts or finishes.

Registers a hook that will be called each time the analysis starts or finishes.

Registers available domain names for the -eva-domains option.

Called once at the analysis beginning for the entry state of the main function.

Registers a hook that will be called each time the current analyzer is changed.

Register a hook modifying the three abstractions after their building by the engine, before the start of each analysis.

Set a hook on function statistics computation

Register a reduction function for a value reduced product.

relate kf bases state returns the set of bases bases in relation with bases in state — i.e.

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 lval set remove any expression e such that lval belongs to syntactic_lval e from the set of equalities set.

remove x s returns the equality between all elements of s, except x.

remove loc state drops all information on the locations pointed to by loc from state.

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

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

remove_variables list state drops all information about the variables in list from state.

replace shape set replaces the elements of set according to shape.

Replaces all occurrences of the lvalue late by the expression heir.

Add a new binding.

replace_base substitution location replaces the variables represented by the location according to substitution.

For pointer values, replace_base substitution value replaces the bases pointed to by value according to substitution.

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

Resets (or just delays) the widening counter.

resolve_functions v returns the list of functions that may be pointed to by the abstract value v (representing a function pointer).

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

reuse kf bases current_input previous_output merges the initial state current_input with a final state previous_output from a previous analysis of kf started with an equivalent initial state.

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.

Changes the information about a recursive call to be used at the end of the call.

rewrap_integer irange t wraps around the abstract value t to fit the integer range irange, assuming 2's complement.

Removes redundant assertions.

Runs some programmatic tests on Eva.

Runs some programmatic tests on Eva.

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.

Returns true if the user has requested that no results should be recorded for the given function.

True if the results should be saved for the given function.

Returns true if the user has requested that no results should be recorded for the given function.

Internal state of Eva analysis from projects viewpoint.

Internal state of Eva analysis from projects viewpoint.

For a key of type k key: if the values of type t contain a subpart of type k from a module identified by the key, then set key v t returns the value t in which this subpart has been replaced by v., 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.

Set the current computation state.

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.

Called on the Frama_C_domain_show_each directive.

Mark the analysis as aborted.

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

singleton ?status alarm creates the map set alarm status none: alarm has a by default an unkown status (which can be overridden through 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.

Should we skip the specifications of this function, according to -eva-skip-stdlib-specs

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.

start_call stmt call recursion valuation state returns an initial state for the analysis of a called function.

Returns the analysis status of a given function.

Returns the analysis status of a given function.

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.

Translates an error to a human readable string.

Translates an error to a human readable string.

See Locations.sub_pointwise.

substitute substitution clob state applies substitution to all pointer values in the offsetmaps bound to variables in clob in state.

syntactic_lvalues e returns the set of lvalues that appear in the expression e.

Evaluation functions store the results of an evaluation into Valuation.t maps.

Iterate on the whole map, in descending order of keys

Iterate on the whole map, in ascending order of keys

to_seq_from k m iterates on a subset of the bindings of m, in ascending order of keys, from key k or above.

Greatest element.

The top abstraction, which maps all variables to V.top.

This function must return true if the given variable should be tracked by the domain.

Apply a transfer function to all the states of a propagation.

Returns the canonical representant of a definitely uninitialized value.

union f m1 m2 computes a map whose keys are a subset of the keys of m1 and of m2.

Union.

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

unite (a, a_set) (b, b_set) map unites a and b in map.

update key f m returns a map containing the same bindings as m, except for the binding of key.

update valuation t updates the state t with the values of expressions and the locations of lvalues available in the valuation record.

use_builtin kf name instructs the analysis to use the builtin name to interpret calls to function kf.

use_builtin kf name instructs the analysis to use the builtin name to interpret calls to function kf.

use_global_value_partitioning vi instructs the analysis to use value partitioning on the global variable vi.

use_global_value_partitioning vi instructs the analysis to use value partitioning on the global variable vi.

Does the analysis ignores the body of a given function, and uses instead its specification or a builtin to interpret it? Please use Eva.Results.are_available instead to known whether results are available for a given function.

Returns true if the Eva analysis use the specification of the given function instead of its body to interpret its calls.

Does the analysis ignores the body of a given function, and uses instead its specification or a builtin to interpret it? Please use Eva.Results.are_available instead to known whether results are available for a given function.

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 (without any access, or for a read or write access).

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

Do not emit any message.

warn_right_imprecision lval loc offsm is used for the assignment of the lvalue lval pointing to the location loc; it warns if the offsetmap offsm contains a garbled mix.

Warns on functions from the frama-c libc with unsupported specification.

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

Widen a flow.

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

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