Frama-C:
Plug-ins:
Libraries:

Frama-C API - Abstract_value

Signature of abstract numerical values, representing the set of possible values of an expression or lvalue. Used to exchange information between abstract domains.

Abstract numeric values of the analysis.

type 'v truth = [
  1. | `False
  2. | `Unknown of 'v
  3. | `True
  4. | `TrueReduced of 'v
  5. | `Unreachable
]

Type for the truth value of an assertion in a value abstraction. The two last tags should be used only for a product of value abstractions.

type bound_kind = Frama_c_kernel.Alarms.bound_kind =
  1. | Lower_bound
  2. | Upper_bound
type bound =
  1. | Int of Frama_c_kernel.Z.t
  2. | Float of float * Frama_c_kernel.Cil_types.fkind
type pointer_comparison =
  1. | Equality
  2. | Relation
  3. | Subtraction
type 'a enriched = {
  1. from_domains : 'a;
}

Enriched context. This record could easily be extended to contain more information about the context in which an evaluation takes place, if the need arises.

module type S = sig ... end

Signature of abstract numerical values.

type 'v key
module type Leaf = sig ... end

Signature for a leaf module of abstract values.

type 'v dependencies =
  1. | Leaf : (module Leaf with type t = 'v) -> 'v dependencies
  2. | Node : 'l dependencies * 'r dependencies -> ('l * 'r) dependencies

Eva abstractions are divided between values, locations and domains. Locations and domains depend on values, and use this type to declare such dependencies. In the standard case, a domain depends on a single value module V and uses Leaf (module V) to declare this dependency.