Index of values

Adding elements

Add a new binding.

Update the trace of all the states in the stateset.

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

Check the precondition of kf.

Check that kf is not already present in the call stack

Clean all previously stored results

Reset the reference to its default value.

Clear the table.

Functions dealing with call stacks.

Clobbered list for bases containing addresses of local variables.

List of names of all kernel compilation units.

Evaluate the assigns of kf active according to active_behaviors in the state with_formals.

Compute a call to kf, called from call_kinstr, in the state state.

Compute a call to the main function.

Compute a call to a possible builtin kf in state state.

Compute a call to kf from call_kinstr, assuming kf is not yet present in the callstack.

Compute kf in state with_formals according to the body f of kf.

Compute a call to kf in the state with_formals.

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

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

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

Directory where architecture independent files are.

Compilation date.

Display a complete summary of performance informations.

Precondition: the type of v and the type of loc_lv may be different only through a truncation or an extension.

Dot command name.

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

Creation

Creation

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

Return the current binding of the given key.

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

Find a previously registered builtin.

If possible, decomposes e into lval+offset; where lval is a Cil expression, and offset is an Ival.t, in bytes.

Extraction

Iterators

Iterators

Builtin for free function

Get the referenced value.

Initial state in -lib-entry mode

Initial value for globals and NULL in no-lib-entry mode (everything initialized to 0).

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

Bitfields

Information

Information

Is the Frama-C GUI running?

Export

Export

Join the given state_set.

Length of the table.

Directory where the Frama-C kernel library is.

Change all offsets to top_int.

Does the builtin table contain an entry for name?

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

Memoization.

Memoization.

Merge the two sets together.

Merge the results of the current analysis with the global results.

Raise Unchanged if the first set was already included in into

Increments the counter and returns a fresh value

Name of the bytecode compiler.

Name of the native compiler.

Returns the first eventual imprecise part contained in an offsetmap

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

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

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

Detects if an expression can be considered as a lvalue even though it is hidden by a cast that does not change the lvalue.

Directory where the Frama-C dynamic plug-ins are.

Prints the current callstack.

Name of the default command to call the preprocessor.

true if the default preprocessor selected during compilation is able to keep comments (hence ACSL annotations) in its output.

Print a call stack.

Pretty print the sid of the statement

Reduce the state for comparisons of the form 'v Rel k', 'k Rel v' or 'v = w'

raises Reduce_to_bottom and never returns Cvalue.Model.bottom

Reduce the state for comparisons of the form 'v Rel k', where v evaluates to a location, and k to some value

We are accessing an array of size array_size at indexes index in state state.

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

Auxiliary function that registers a new variable declared by Value within the kernel internal tables

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

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

Add the given set of bases to an existing clobbered set

Same as above with an entire offsetmap

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

Invert the order in which the states are iterated over

Add a new binding.

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

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

Change the referenced value.

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

If reduce is true, reduce in all cases.

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

GUI of plug-ins statically linked within Frama-C.

Plug-ins statically linked within Frama-C.

Call start_doing when finishing analyzing a function.

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

Export

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

Updating

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

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

Frama-C Version identifier.

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

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

Specialization of the function above for standard types