package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Deprecated module: use the Eva.mli API instead.

  • alert db_deprecated Db.Value is deprecated and will be removed in a future version of Frama-C. Please use the Eva.mli public API instead.
type state = Cvalue.Model.t

Internal state of the value analysis.

type t = Cvalue.V.t

Internal representation of a value.

val emitter : Emitter.t ref

Emitter used by Value to emit statuses

val self : State.t

Internal state of the value analysis from projects viewpoint.

val mark_as_computed : unit -> unit

Indicate that the value analysis has been done already.

val compute : (unit -> unit) ref

Compute the value analysis using the entry point of the current project. You may set it with Globals.set_entry_point.

val is_computed : unit -> bool

Return true iff the value analysis has been done.

Table containing the results of the value analysis, ie. the state before the evaluation of each reachable statement.

Table containing the state of the value analysis after the evaluation of each reachable and evaluable statement. Filled only if Value_parameters.ResultsAfter is set.

val ignored_recursive_call : Cil_types.kernel_function -> bool

This functions returns true if the value analysis found and ignored a recursive call to this function during the analysis.

val condition_truth_value : Cil_types.stmt -> bool * bool

Provided stmt is an 'if' construct, fst (condition_truth_value stmt) (resp. snd) is true if and only if the condition of the 'if' has been evaluated to true (resp. false) at least once during the analysis.

Parameterization

val use_spec_instead_of_definition : (Cil_types.kernel_function -> bool) ref

To be called by derived analyses to determine if they must use the body of the function (if available), or only its spec. Used for value builtins, and option -val-use-spec.

Arguments of the main function

The functions below are related to the arguments that are passed to the function that is analysed by the value analysis. Specific arguments are set by fun_set_args. Arguments reset to default values when fun_use_default_args is called, when the ast is changed, or if the options -libentry or -main are changed.

val fun_set_args : t list -> unit

Specify the arguments to use.

val fun_use_default_args : unit -> unit
val fun_get_args : unit -> t list option

For this function, the result None means that default values are used for the arguments.

exception Incorrect_number_of_arguments

Raised by Db.Compute when the arguments set by fun_set_args are not coherent with the prototype of the function (if there are too few or too many of them)

Initial state of the analysis

The functions below are related to the value of the global variables when the value analysis is started. If globals_set_initial_state has not been called, the given state is used. A default state (which depends on the option -libentry) is used when globals_use_default_initial_state is called, or when the ast changes.

val globals_set_initial_state : state -> unit

Specify the initial state to use.

val globals_use_default_initial_state : unit -> unit
val globals_state : unit -> state

Initial state used by the analysis

val globals_use_supplied_state : unit -> bool
  • returns

    true if the initial state for globals used by the value analysis has been supplied by the user (through globals_set_initial_state), or false if it is automatically computed by the value analysis

Getters

State of the analysis at various points

val get_initial_state : Cil_types.kernel_function -> state
val get_initial_state_callstack : Cil_types.kernel_function -> state Value_types.Callstack.Hashtbl.t option
val get_state : ?after:bool -> Cil_types.kinstr -> state

after is false by default.

val get_stmt_state_callstack : after:bool -> Cil_types.stmt -> state Value_types.Callstack.Hashtbl.t option
val get_stmt_state : ?after:bool -> Cil_types.stmt -> state

after is false by default.

val fold_stmt_state_callstack : (state -> 'a -> 'a) -> 'a -> after:bool -> Cil_types.stmt -> 'a
val fold_state_callstack : (state -> 'a -> 'a) -> 'a -> after:bool -> Cil_types.kinstr -> 'a
val find : state -> Locations.location -> t

Evaluations

val eval_lval : (?with_alarms:CilE.warn_mode -> Locations.Zone.t option -> state -> Cil_types.lval -> Locations.Zone.t option * t) ref
val eval_expr : (?with_alarms:CilE.warn_mode -> state -> Cil_types.exp -> t) ref
val eval_expr_with_state : (?with_alarms:CilE.warn_mode -> state -> Cil_types.exp -> state * t) ref
val reduce_by_cond : (state -> Cil_types.exp -> bool -> state) ref
val find_lv_plus : (Cvalue.Model.t -> Cil_types.exp -> (Cil_types.lval * Ival.t) list) ref

returns the list of all decompositions of expr into the sum an lvalue and an interval.

Values and kernel functions

val expr_to_kernel_function : (Cil_types.kinstr -> ?with_alarms:CilE.warn_mode -> deps:Locations.Zone.t option -> Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t) ref
val expr_to_kernel_function_state : (state -> deps:Locations.Zone.t option -> Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t) ref
exception Not_a_call
val call_to_kernel_function : Cil_types.stmt -> Kernel_function.Hptset.t

Return the functions that can be called from this call.

val valid_behaviors : (Cil_types.kernel_function -> state -> Cil_types.funbehavior list) ref
val add_formals_to_state : (state -> Cil_types.kernel_function -> Cil_types.exp list -> state) ref

add_formals_to_state state kf exps evaluates exps in state and binds them to the formal arguments of kf in the resulting state

Reachability

val is_accessible : Cil_types.kinstr -> bool
val is_reachable : state -> bool
val is_reachable_stmt : Cil_types.stmt -> bool

About kernel functions

exception Void_Function

Return the location of the returned lvalue of the given function.

val is_called : (Cil_types.kernel_function -> bool) ref
  • returns

    the list of callers with their call sites. Each function is present only once in the list.

State before a kinstr

val access : (Cil_types.kinstr -> Cil_types.lval -> t) ref
val access_expr : (Cil_types.kinstr -> Cil_types.exp -> t) ref
val access_location : (Cil_types.kinstr -> Locations.location -> t) ref

Locations of left values

val lval_to_loc : (Cil_types.kinstr -> ?with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.location) ref
val lval_to_loc_with_deps : (Cil_types.kinstr -> ?with_alarms:CilE.warn_mode -> deps:Locations.Zone.t -> Cil_types.lval -> Locations.Zone.t * Locations.location) ref
val lval_to_loc_with_deps_state : (state -> deps:Locations.Zone.t -> Cil_types.lval -> Locations.Zone.t * Locations.location) ref
val lval_to_loc_state : (state -> Cil_types.lval -> Locations.location) ref
val lval_to_offsetmap : (Cil_types.kinstr -> ?with_alarms:CilE.warn_mode -> Cil_types.lval -> Cvalue.V_Offsetmap.t option) ref
val lval_to_offsetmap_state : (state -> Cil_types.lval -> Cvalue.V_Offsetmap.t option) ref
  • since Carbon-20110201
val lval_to_zone : (Cil_types.kinstr -> ?with_alarms:CilE.warn_mode -> Cil_types.lval -> Locations.Zone.t) ref
val lval_to_zone_state : (state -> Cil_types.lval -> Locations.Zone.t) ref

Does not emit alarms.

val lval_to_zone_with_deps_state : (state -> for_writing:bool -> deps:Locations.Zone.t option -> Cil_types.lval -> Locations.Zone.t * Locations.Zone.t * bool) ref

lval_to_zone_with_deps_state state ~for_writing ~deps lv computes res_deps, zone_lv, exact, where res_deps are the memory zones needed to evaluate lv in state joined with deps. zone_lv contains the valid memory zones that correspond to the location that lv evaluates to in state. If for_writing is true, zone_lv is restricted to memory zones that are writable. exact indicates that lv evaluates to a valid location of cardinal at most one.

val lval_to_precise_loc_state : (?with_alarms:CilE.warn_mode -> state -> Cil_types.lval -> state * Precise_locs.precise_location * Cil_types.typ) ref
val lval_to_precise_loc_with_deps_state : (state -> deps:Locations.Zone.t option -> Cil_types.lval -> Locations.Zone.t * Precise_locs.precise_location) ref
val assigns_inputs_to_zone : (state -> Cil_types.assigns -> Locations.Zone.t) ref

Evaluation of the \from clause of an assigns clause.

val assigns_outputs_to_zone : (state -> result:Cil_types.varinfo option -> Cil_types.assigns -> Locations.Zone.t) ref

Evaluation of the left part of assigns clause (without \from).

val assigns_outputs_to_locations : (state -> result:Cil_types.varinfo option -> Cil_types.assigns -> Locations.location list) ref

Evaluation of the left part of assigns clause (without \from). Each assigns term results in one location.

val verify_assigns_froms : (Kernel_function.t -> pre:state -> Function_Froms.t -> unit) ref

For internal use only. Evaluate the assigns clause of the given function in the given prestate, compare it with the computed froms, return warning and set statuses.

module Logic : sig ... end

Callbacks

type callstack = Value_types.callstack

Actions to perform at end of each function analysis. Not compatible with option -memexec-all

val no_results : (Cil_types.fundec -> bool) ref

Returns true if the user has requested that no results should be recorded for this function. If possible, hooks registered on Record_Value_Callbacks and Record_Value_Callbacks_New should not force their lazy argument

Actions to perform at each treatment of a "call" statement. state is the state before the call.

module Call_Type_Value_Callbacks : Hook.Iter_hook with type param = [ `Builtin of Value_types.call_froms | `Spec of Cil_types.funspec | `Def | `Memexec ] * state * callstack

Actions to perform at each treatment of a "call" statement. state is the state before the call.

Actions to perform whenever a statement is handled.

val rm_asserts : (unit -> unit) ref

Pretty printing

val pretty : Format.formatter -> t -> unit
val pretty_state : Format.formatter -> state -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct