Single_value_abstraction.IvalSourceOur main bitvector abstraction: interval and congruence abstraction, for both the signed and unsigned interpretation of bitvectors.
module Integer_Forward :
Operator.INTEGER_FORWARD
with module Arity := Operator.Forward_Arity
and type boolean := boolean
and type integer := integermodule Integer_Backward :
Operator.INTEGER_BACKWARD
with module Arity := Operator.Backward_Arity
and type boolean := boolean
and type integer := integermodule Boolean_Forward :
Operator.BOOLEAN_FORWARD
with module Arity := Operator.Forward_Arity
and type boolean := booleanmodule Boolean_Backward :
Operator.BOOLEAN_BACKWARD
with module Arity := Operator.Backward_Arity
and type boolean := booleanmodule Bitvector_Forward :
Operator.BITVECTOR_FORWARD_WITH_BIMUL_ADD
with module Arity := Operator.Forward_Arity
and type boolean := boolean
and type bitvector := bitvector