package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameterization
1. Arguments of the main function
2. Initial state of the analysis
Getters
Evaluations
Values and kernel functions
Reachability
About kernel functions
State before a kinstr
Locations of left values
Callbacks
Pretty printing

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.kernel/Frama_c_kernel/Db/Value/index.html

Module `Db.Value`

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 proxy : State_builder.Proxy.t

val self : State.t

Internal state of the value analysis from projects viewpoint.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

raises Globals.No_such_entry_point
if the entry point is incorrect

raises Db.Value.Incorrect_number_of_arguments
if some arguments are specified for the entry point using Db.Value.fun_set_args, and an incorrect number of them is given.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val is_computed : unit -> bool

Return true iff the value analysis has been done.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

module Table_By_Callstack : 
  State_builder.Hashtbl
    with type key = Cil_types.stmt
     and type data = state Value_types.Callstack.Hashtbl.t

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

module AfterTable_By_Callstack : 
  State_builder.Hashtbl
    with type key = Cil_types.stmt
     and type data = state Value_types.Callstack.Hashtbl.t

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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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.

raises Not_a_call
if the statement is not a 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

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

val is_reachable_stmt : Cil_types.stmt -> bool

About kernel functions

exception Void_Function

val find_return_loc : Cil_types.kernel_function -> Locations.location

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

raises Void_Function
if the function does not return any value.

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

val callers : 
  (Cil_types.kernel_function ->
    (Cil_types.kernel_function * Cil_types.stmt list) list)
    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

module Record_Value_Callbacks : 
  Hook.Iter_hook
    with type param = callstack * state Cil_datatype.Stmt.Hashtbl.t Lazy.t

module Record_Value_Superposition_Callbacks : 
  Hook.Iter_hook
    with type param = callstack * state list Cil_datatype.Stmt.Hashtbl.t Lazy.t

module Record_Value_After_Callbacks : 
  Hook.Iter_hook
    with type param = callstack * state Cil_datatype.Stmt.Hashtbl.t Lazy.t

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

module Call_Value_Callbacks : 
  Hook.Iter_hook with type param = state * callstack

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