Module Frama_c_kernel.Lattice_messages

Message and logging facility for abstract lattices.

type t =
| Approximation of string(*

Abstract transfer function that intentionally approximates its result

*)
| Imprecision of string(*

Abstract transfer function not fully implemented

*)
| Costly of string(*

Abstract operation will be costly

*)
| 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, Stdlib.Format.formatter, unit ) Stdlib.format -> 'a
val emit_costly : emitter -> ( 'a, Stdlib.Format.formatter, unit ) Stdlib.format -> 'a