In GNU C there are functions to check for overflows of arithmetic operations (__builtin_*_overflow). These functions perform an arithmetic operation on the first two arguments (without producing any overflows), write the result to the third argument and return whether an overflow would occur using the normal arithmetic operation.
Currently, we simply overapproximate the return value of these functions. This is in general unsound as we do not consider that the third argument changes at all. Also this is quite imprecise, which led to 55 unknown results in SV-COMP 24.
Therefore this PR handles these functions properly. This is done in the following way:
First we calculate the result of the arithmetic operation (without any overflows). For the integer translation this is the "usual" operations, while for the bitvector translation we choose a large enough bitvector to store the result (e.g. 64bit for the multiplication of two 32bit integers).
Then we have to shrink this result to fit in the result type again, s.t. we can write it to the third argument (Note: This also uses the optimization to avoid "unnecessary" heap variables, if the third argument is of the form &x. Therefore this depends on #685).
Then we return 1 iff the original result did fit in the result type.
For each of the three cases I added a new method to ExpressionTranslation accordingly, as these cases differ between the integer translation and the bitvector translation.
In GNU C there are functions to check for overflows of arithmetic operations (
__builtin_*_overflow). These functions perform an arithmetic operation on the first two arguments (without producing any overflows), write the result to the third argument and return whether an overflow would occur using the normal arithmetic operation. Currently, we simply overapproximate the return value of these functions. This is in general unsound as we do not consider that the third argument changes at all. Also this is quite imprecise, which led to 55unknownresults in SV-COMP 24.Therefore this PR handles these functions properly. This is done in the following way:
&x. Therefore this depends on #685).For each of the three cases I added a new method to
ExpressionTranslationaccordingly, as these cases differ between the integer translation and the bitvector translation.