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.

Absolute value

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

These functions perform arithmetic operations on intervals using the precision <prec>.

The following functions perform floating-point arithmetic operations at the precision <prec> and using the rounding mode <rnd>.

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 NaN into the interval

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.

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

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.

Apply an operation on each fields of the operands

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

Returns a element containing the same value as <dst> but with the sign of <src>

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.

These functions perform backward propagation for arithmetic

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

These functions perform backward propagation on intervals using the precision <prec>

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.

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.

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

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.

Return a new value with the same fields as the input but with an <approx> field with the given precision

Change the precision of the bounds

Change the precision

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.

Comparison functions

Comparison functions

Compute a call to the main function.

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

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.

Check if there is a zero between the bounds of its input (without considering the signs

Check if its input contains at least an infinite bound

Check if its input contains at least a NaN value

Check if there is a negative zero between the bounds of its input

Check if there is a positive zero between the bounds of its input

Check if there is at least a strictly negative value in its input

Check if there is at least a strictly positive value in its input

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 a record from intervals

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.

Returns the abstraction corresponding to the join of the approximation of the inputs.

A default set of hints

The default configuration of Eva.

Returns the integer corresponding to the exponent of the denormalized numbers of the given precision.

Display a complete summary of performance informations.

Debug category used when using Eva callbacks when recording the results of a function analysis.

Debug category used to print the cvalue domain on Frama_C_dump|show_each functions.

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

Debug category used to print information about the iteration

Debug category used to print information about invalid pointer comparisons

Debug category used to print messages about recursive calls.

Debug category used to print the usage of widenings.

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.

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

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

Enlarge the bounds of the interval by taking the previous float of the lower bound and the following float of the upper bound

Introduces a list of variables in the state.

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

Returns the interval -epsilon ; +epsilon for the input precision

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?

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

Returns the exponent of its input

Returns the number of bits of the exponent of the given precision.

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.

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.

Handling of forward interactions

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

Returns the number of bits of the significand of the given precision, counting the implicit one.

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.

Returns the bounds of its inputs

Special accessors for the main cvalue domain.

Returns the exponent of the bounds ot its input

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.

Returns the biggest exponent of its input

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.

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

Check if its input is a zero (positive or negative)

Returns true if the value may not be a pointer.

Bitfields

Has a builtin been registered with the given name?

Is a given function replaced by a builtin?

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 ?

Whether the Filepath is empty.

Check if the bounds of its input are finite

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

Inclusion test.

Lattice functions.

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

Check if its input is an infinite value

is_initialized v = true implies v is definitely initialized.

Check if the interval contains only NaN values

Check if its input is a NaN

Check if its input is negative (is_neg NaN = false)

Check if the bounds of its input are negative infinites

Check if the bounds of its input are negative zeros

Check if its input is a negative zero

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

Check if its input is positive (is_pos NaN = true)

Check if the bounds of its input are positive infinites

Check if the bounds of its input are positive zeros

Check if its input is a positive zero

Check if all the values of its input are negatives

Check if its input is strictly negative (non zero)

Check if all the values of its input are positives

Check if its input is strictly positive (non zero)

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

Check if the bounds of its input are both zero (without considering their signs)

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.

Lattice methods

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.

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.

This function returns a float of precision ?prec containing the machine delta of the mandatory precision parameter also divided by two for the same reason as machine_epsilon.

This function returns a float of precision ?prec containing the machine epsilon divided by two for the mandatory precision parameter.

Creates the information about a recursive call.

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

Replace the infinite bounds of its input into the maximum float of the precision.

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

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.

Maximal negative float in the precision

Maximal positive float in the precision

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.

Returns an interval containing only NaN values at the precision <prec>

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.

These functions perform mathematic unidimensionnal operations of intervals using the precision <prec>

Negation

Returns the interval -oo ; -oo at the precision <prec>

Returns a t element representing a negative infinite value

Returns a t element representing a negative zero 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.

Returns the following floating point number of the same precision

Signal that some analysis results are not stored.

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

Returns the precision associated to the Cil construction fkind, which represents the C floating point type

Works in the same way as of_floats but the bounds are rounded toward nearest

The functions of_<typ> ~rnd ~prec x return a float of precision <prec> containing the value of x (of type <typ>) rounding to <rnd>.

The function of_<typ> ~prec (x, y) returns the interval x' ; y' where x' is a Numerors float containing the value of x (of type <typ>) rounded toward -oo and y' is a Numerors float containing the value of y rounded toward +oo.

Returns the interval corresponding to the given bounds.

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.

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.

Returns the interval +oo ; +oo at the precision <prec>

Returns a t element representing a positive infinite value

Returns the interval +0 ; +0 at the precision <prec>

Returns a t element representing a positive zero value

This function is called after the analysis.

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

Prints the current callstack.

Return the precision of the <approx> field

Returns the precisions of the bounds of its input

Returns the precision of its input

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

Pretty printer

Can be equal to pretty

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

Print a call stack without displaying call sites.

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

Returns the previous floating point number of the same precision

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.

Returns the abstraction corresponding to the join of the approximation of the inputs.

Reduction of an error value according to a floating-point interval.

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.

Registers a hook that will be called each time the current analyzer has been computed.

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.

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.

Runs some programmatic tests on Eva.

Runs the unit tests of 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.

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

Returns the sign of its input.

Mark the analysis as aborted.

Returns the significand of its input.

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.

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.

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.

Returns the interval -oo ; +oo with NaNs at the precision <prec>

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 b adds a builtin override for function `kf` to builtin `b`.

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

use_global_value_partitioning vi enable value partitioning on the global variable `vi`.

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

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.

Warning category used when emitting an alarm in "warning" mode.

Warning category used for "cannot use builtin due to missing spec"

Warning category used for "definition overridden by builtin"

Warning category for experimental domains or features.

Warning category used to print garbled mix

Warning category for 'completely invalid' assigns clause

Warning category used for calls to libc functions whose specification is currently unsupported.

Warning category used for the warning "locals escaping scope".

Warning category used for "Automatic loop unrolling"

Warning category used for "loop not completely unrolled"

Warning category used to identify loops without unroll annotations

Warning category used to identify for loops without unroll annotations

Warning category for signed overflows

Warning category for 'size of type T cannot be computed'.

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

Return a value with all fields to zero.

Returns the interval -0 ; +0 at the precision <prec>

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