Frama-C:
Plug-ins:
Libraries:

Frama-C API - Origin

This module is used to track the origin of very imprecise values (namely "garbled mix", created on imprecise or unsupported operations on addresses) propagated by an Eva analysis.

include Datatype.S
include Datatype.S_no_copy
include Datatype.Ty
type t
val ty : t Type.t
val name : string

Unique name of the datatype.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : Stdlib.Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

val mem_project : (Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

type kind =
  1. | Misalign_read
  2. | Misalign_write
  3. | Leaf
  4. | Merge
  5. | Arith
val current : kind -> t

Creates an origin of the given kind, associated with the current source location extracted from Current_loc.

val well : t

Origin for garbled mix created in the initial state of the analysis (not associated to a source location).

val unknown : t

Unknown origin.

val is_unknown : t -> bool
val pretty_as_reason : Stdlib.Format.formatter -> t -> unit

Pretty-print because of <origin> if the origin is not Unknown, or nothing otherwise.

val descr : t -> string

Short description of an origin.

val join : t -> t -> t
val register : Base.SetLattice.t -> t -> unit

Records the creation of an imprecise value of the given bases.

val register_write : Base.SetLattice.t -> t -> bool

Records the write of an imprecise value of the given bases, with the given origin. Returns true if the given origin has never been written before, and if it is related to the current location — in which case a warning should probably be emitted.

val register_read : Base.SetLattice.t -> t -> unit

Records the read of an imprecise value of the given bases, with the given origin.

val pretty_history : Stdlib.Format.formatter -> unit

Pretty-print a summary of the origins of imprecise values recorded by register_write and register_read above.

val clear : unit -> unit

Clears the history of origins saved by register_write and register_read above.