Signed overflow in DIV_MACRO

[chandradeepdey]

Post macro-expansion, the code in

8086tiny/8086tiny.c

Line 391 in c79ca2a

i_w ? DIV_MACRO(unsigned short, unsigned, regs16) : DIV_MACRO(unsigned char, unsigned short, regs8)

becomes

(scratch_int = *(unsigned short *)&mem[rm_addr]) &&
        !(scratch2_uint = (unsigned)(scratch_uint = (regs16[i_w + 1] << 16) + regs16[0]) / scratch_int,
          scratch2_uint - (unsigned short)scratch2_uint)
    ? regs16[i_w + 1] = scratch_uint - scratch_int * (*regs16 = scratch2_uint)

The type of scratch_int * (*regs16 = scratch2_uint) is int due to the LHS being an int and the RHS being an unsigned short. It is promoted to unsigned int before the subtraction. A counterexample generated by CBMC was -
scratch_int = 33793, scratch_uint = 2181038080, scratch2_uint (division result) = 64541. scratch_int * scratch2_uint = 2181034013 does not fit inside a 4-byte int.

Detected using Frama-C (eva) and CBMC while doing a project for the Software Verification and Analysis course under Prof @mksrivas at CMI