Module `Domains.Overflow_checks`

Adds checks for overflows around bitvector operation. Assumes no overflow occurs and optionaly raise alarms if overflows are possible.

module Make
  (Sub : Sig.BASE_WITH_INTEGER) : 
  Sig.BASE_WITH_INTEGER
    with type boolean = Sub.boolean
     and type binary = Sub.binary
     and type integer = Sub.integer
     and type enum = Sub.enum

This functor adds overflow checks to bitvector operations. I.E. for a biadd with ~size=32 it first performs the addition on 33 bits, then checks if the result fits in 32 bits (Checking signedness according to the various flags). Similarly, it adds guards to bisub, bimul, and bisdiv (dividing min_int by -1 underflows). There are no overflow guards on shifts as of yet.

Module Domains.Overflow_checks

Module `Domains.Overflow_checks`