Module Frama_c_kernel.Lattice_messages

Message and logging facility for abstract lattices.

type t =
  1. | Approximation of string
    (*

    Abstract transfer function that intentionally approximates its result

    *)
  2. | Imprecision of string
    (*

    Abstract transfer function not fully implemented

    *)
  3. | Costly of string
    (*

    Abstract operation will be costly

    *)
  4. | Unsoundness of string
    (*

    Unsound abstract operation

    *)
type emitter
val register : string -> emitter

Register a new emitter for a message.

val emit : emitter -> t -> unit

Emit a message.

val emit_imprecision : emitter -> string -> unit
val emit_approximation : emitter -> ('a, Format.formatter, unit) format -> 'a
val emit_costly : emitter -> ('a, Format.formatter, unit) format -> 'a