Frama-C:
Plug-ins:
Libraries:

Frama-C API - Abstract_value

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 = 'v Structure.Key_Value.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.