Post macro-expansion, the code in
|
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
Post macro-expansion, the code in
8086tiny/8086tiny.c
Line 391 in c79ca2a
The type of
scratch_int * (*regs16 = scratch2_uint)isintdue to the LHS being anintand the RHS being anunsigned short. It is promoted tounsigned intbefore 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-byteint.Detected using Frama-C (eva) and CBMC while doing a project for the Software Verification and Analysis course under Prof @mksrivas at CMI