Module Operator.AutologSource

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.

Sourcemodule type BOOLEAN_CONVERSION = sig ... end
Sourcemodule type INTEGER_CONVERSION = sig ... end
Sourcemodule type ENUM_CONVERSION = sig ... end
Sourcemodule type BITVECTOR_CONVERSION = sig ... end
Sourcemodule type MEMORY_CONVERSION = sig ... end
Sourcemodule Log_Boolean_Backward (C : BOOLEAN_CONVERSION) (F : sig ... end) : sig ... end
Sourcemodule Log_Integer_Backward (C : INTEGER_CONVERSION) (F : sig ... end) : sig ... end
Sourcemodule Log_Bitvector_Forward (C : BITVECTOR_CONVERSION) (F : sig ... end) : sig ... end
Sourcemodule Log_Bitvector_Forward_With_Bimul_add (C : BITVECTOR_CONVERSION) (F : sig ... end) : sig ... end
Sourcemodule Log_Binary_Forward (C : BITVECTOR_CONVERSION) (F : sig ... end) : sig ... end
Sourcemodule Log_Enum_Forward (C : ENUM_CONVERSION) (F : sig ... end) : sig ... end
Sourcemodule Log_Memory_Forward (C : MEMORY_CONVERSION) (F : sig ... end) : sig ... end