package frama-c

  1. Overview
  2. Docs
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

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. A
    Anne Pacalet
  36. V
    Valentin Perrelle
  37. G
    Guillaume Petiot
  38. D
    Dario Pinto
  39. V
    Virgile Prevosto
  40. A
    Armand Puccetti
  41. F
    Félix Ridoux
  42. V
    Virgile Robles
  43. M
    Muriel Roger
  44. J
    Julien Signoles
  45. N
    Nicolas Stouls
  46. K
    Kostyantyn Vorobyov
  47. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-27.0-beta-Cobalt.tar.gz
sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

doc/frama-c-eva.core/Eva/Results/index.html

Module Eva.Results

Eva's result API is a new interface to access the results of an analysis, once it is completed. It may slightly change in the future. It aims at replacing most uses of Db.Value, and has some advantages over Db's :

  • evaluations uses every available domains and not only Cvalue;
  • the caller may distinguish failure cases when a request is unsucessful;
  • working with callstacks is easy;
  • some common shortcuts are provided (e.g. for extracting ival directly);
  • overall, individual functions are simpler.

The idea behind this API is that requests must be decomposed in several steps. For instance, to evaluate an expression :

1. first, you have to state where you want to evaluate it, 2. optionally, you may specify in which callstack, 3. you choose the expression to evaluate, 4. you require a destination type to evaluate into.

Usage sketch :

Eva.Results.( before stmt |> in_callstack cs |> eval_var vi |> as_int |> default 0)

or equivalently, if you prefer

Eva.Results.( default O (as_int (eval_var vi (in_callstack cs (before stmt))))

val are_available : Frama_c_kernel.Cil_types.kernel_function -> bool

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

  • the function has not been reached by the analysis: all requests in the function will lead to a Bottom error.
  • a specification or a builtin has been used instead of analyzing the function body: all requests in the function will lead to a Bottom error.
  • results have not been saved, due to the -eva-no-results parameter: all requests in the function will lead to a Top error.
type request
type value
type address
type 'a evaluation
type error =
  1. | Bottom
  2. | Top
  3. | DisabledDomain
type 'a result = ('a, error) Result.t

Results handling

val string_of_error : error -> string

Translates an error to a human readable string.

val pretty_error : Format.formatter -> error -> unit

Pretty printer for errors.

val pretty_result : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a result -> unit

Pretty printer for API's results.

val default : 'a -> 'a result -> 'a

default d r extracts the value of r if r is Ok, or use the default value d otherwise. Equivalent to Result.value ~default:d r

Control point selection

val at_start : request

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

val at_end : unit -> request

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

At the start of the given function.

At the end of the given function.

  • raises Kernel_function.No_statement

    if the function has no body.

Just before a statement is executed.

Just after a statement is executed.

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

val in_cvalue_state : Frama_c_kernel.Cvalue.Model.t -> request

Evaluation in a given cvalue state. Callstacks selection are silently ignored on such requests. For internal use, could be modified or removed in a future version.

Callstack selection

val in_callstack : callstack -> request -> request

Only consider the given callstack. Replaces previous calls to in_callstack or in_callstacks.

val in_callstacks : callstack list -> request -> request

Only consider the callstacks from the given list. Replaces previous calls to in_callstack or in_callstacks.

val filter_callstack : (callstack -> bool) -> request -> request

Only consider callstacks satisfying the given predicate. Several filters can be added. If callstacks are also selected with in_callstack or in_callstacks, only the selected callstacks will be filtered.

Working with callstacks

val callstacks : request -> callstack list

Returns the list of reachable callstacks from the given request. An empty list is returned if the request control point has not been reached by the analysis, or if no information has been saved at this point (for instance with the -eva-no-results option). Use is_empty request to distinguish these two cases.

val by_callstack : request -> (callstack * request) list

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

State requests

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

val get_cvalue_model : request -> Frama_c_kernel.Cvalue.Model.t

Returns the Cvalue state. Error cases are converted into the bottom or top cvalue state accordingly.

val get_cvalue_model_result : request -> Frama_c_kernel.Cvalue.Model.t result

Returns the Cvalue model.

val print_states : ?filter:Frama_c_kernel.Base.Hptset.t -> request -> (string * string) list

Returns a textual representation of the internal domain states for the given request. If filter is provided, states are filtered on the given bases (for domains that support this feature). Returns a list of pair (name, state) for all available domains.

Dependencies

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 lvalue, including 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.

type deps = Frama_c_kernel.Function_Froms.Deps.deps = {
  1. data : Frama_c_kernel.Locations.Zone.t;
    (*

    Memory zone directly required to evaluate the given expression.

    *)
  2. indirect : Frama_c_kernel.Locations.Zone.t;
    (*

    Memory zone read to compute data addresses.

    *)
}

Memory dependencies of an expression.

type taint =
  1. | Direct
    (*

    Direct data dependency from values provided by the attacker to the given memory zone, meaning that the attacker may be able to alter its value.

    *)
  2. | Indirect
    (*

    Indirect dependency from values provided by the attacker to the given memory zone. The attacker cannot directly alter this memory, but he may be able to impact on the path by which its value is computed.

    *)
  3. | Untainted
    (*

    No taint: the given memory zone cannot be modified by the attacker.

    *)

Taint of a memory zone, according to the taint domain.

Evaluates the taint of a given memory zone, according to the taint domain. Returns an error if the taint domain was not enabled.

val expr_dependencies : Frama_c_kernel.Cil_types.exp -> request -> deps

Computes (an overapproximation of) the memory dependencies of an expression.

Evaluation

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

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

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

val eval_address : ?for_writing:bool -> Frama_c_kernel.Cil_types.lval -> request -> address evaluation

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

Returns the kernel functions into which the given expression may evaluate. If the callee expression doesn't always evaluate to a function, those spurious values are ignored. If it always evaluate to a non-function value then the returned list is empty. Raises Stdlib.Invalid_argument if the callee expression is not an lvalue without offset. Also see callee for a function which applies directly on Call statements.

Evaluated values conversion

In all functions below, if the abstract value inferred by Eva does not fit in the required type, Error Top is returned, as Top is the only possible over-approximation of the request.

val as_int : value evaluation -> int result

Converts the value into a singleton ocaml int.

Converts the value into a singleton unbounded integer.

val as_float : value evaluation -> float result

Converts the value into a floating point number.

Converts the value into a C number abstraction.

Converts the value into a floating point abstraction.

Converts the value into a Cvalue abstraction. Converts error cases into bottom and top values accordingly.

Converts the value into a Cvalue abstraction.

val as_cvalue_or_uninitialized : value evaluation -> Frama_c_kernel.Cvalue.V_Or_Uninitialized.t

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

Converts into a C location abstraction. Error cases are converted into bottom or top locations accordingly.

Converts into a C location abstraction.

Converts into a Zone. Error cases are converted into bottom or top zones accordingly.

Converts into a Zone result.

Converts into a C location abstraction. Error cases are converted into bottom or top locations accordingly.

Converts into a C location abstraction.

Evaluation properties

val is_singleton : 'a evaluation -> bool

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

val is_initialized : value evaluation -> bool

Returns whether the evaluated value is initialized or not. If the value have been evaluated from a Cil expression, it is always initialized.

val alarms : 'a evaluation -> Frama_c_kernel.Alarms.t list

Returns the set of alarms emitted during the evaluation.

Reachability

val is_empty : request -> bool

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

val is_bottom : 'a evaluation -> bool

Returns true if an evaluation leads to bottom, i.e. if the given expression or lvalue cannot be evaluated to a valid result for the given request.

Returns true if the function has been analyzed.

val is_reachable : Frama_c_kernel.Cil_types.stmt -> bool

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

val is_reachable_kinstr : Frama_c_kernel.Cil_types.kinstr -> bool

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

val condition_truth_value : Frama_c_kernel.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.

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 kernel functions called in the given statement. If the callee expression doesn't always evaluate to a function, those spurious values are ignored. If it always evaluate to a non-function value then the returned list is empty. Raises Stdlib.Invalid_argument if the statement is not a Call instruction or a Local_init with ConsInit initializer.