Module `Operator.Autolog`

These functors allows automatic logging of transfer functions. You define how to handle functions of different arities, and how to print values of different types, and then you can automatically log transfer functions of a given signature (the functor names correspond to this signature).

See Domains.Domain_log and Single_value_abstraction.Log for examples of instantiations.

module type BOOLEAN_CONVERSION = sig ... end

module type INTEGER_CONVERSION = sig ... end

module type ENUM_CONVERSION = sig ... end

module type BITVECTOR_CONVERSION = sig ... end

module type MEMORY_CONVERSION = sig ... end

module Log_Boolean_Backward
  (C : BOOLEAN_CONVERSION)
  (F : sig ... end) : 
  sig ... end

module Log_Integer_Backward
  (C : INTEGER_CONVERSION)
  (F : sig ... end) : 
  sig ... end

module Log_Bitvector_Forward
  (C : BITVECTOR_CONVERSION)
  (F : sig ... end) : 
  sig ... end

module Log_Bitvector_Forward_With_Bimul_add
  (C : BITVECTOR_CONVERSION)
  (F : sig ... end) : 
  sig ... end

module Log_Binary_Forward
  (C : BITVECTOR_CONVERSION)
  (F : sig ... end) : 
  sig ... end

module Log_Enum_Forward (C : ENUM_CONVERSION) (F : sig ... end) : sig ... end

module Log_Memory_Forward
  (C : MEMORY_CONVERSION)
  (F : sig ... end) : 
  sig ... end

Module Operator.Autolog

Module `Operator.Autolog`