Frama-C:
Plug-ins:
Libraries:

Frama-C API - Abstract_location

Abstract memory locations of the analysis.

type 'v truth = 'v Abstract_value.truth
module type S = sig ... end

Signature of abstract memory locations.

type 'loc key = 'loc Structure.Key_Location.key
module type Leaf = sig ... end

Signature for a leaf module of abstract locations.

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

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