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