Inspectof the (first) analysis.
abs_xis a signed integer so can only hold values between
xcontains the shift value
INT_MIN = -2147483648, calculating the opposite of
xcauses a signed overflow.
tis_interval, an integer range between
INT_MAXinstead of a single integer value:
--, that the shift value has been initialized to the interval
abs_shiftof the input shift can take any value between
2147483647and the input string is made of
80. Adding the two together triggers a signed overflow.
tis_make_unknown, an abstract input string representing all possible char arrays of a given size:
INT_MAXand any input string of length
39, you have formally proved it is free of undefined behaviors!