diff options
author | Luca Dariz <l.dariz@imamoter.cnr.t> | 2014-09-23 14:52:00 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2015-02-13 18:49:49 +0000 |
commit | dbe13e13a215aa7212b5737dd8903699301a4940 (patch) | |
tree | 95981808ecab4298b54544bc5c28a1b9a1373b1b /utils | |
parent | 64a404f89da5aa6a99e688c007c56f1f422541bc (diff) | |
download | klee-dbe13e13a215aa7212b5737dd8903699301a4940.tar.gz |
Fix overflow detection in unsigned multiplication
Previously the check was done as unsigned int a, b, c; c = a * b; if (c < a) // error but it is wrong, since it catches only a subset of all the possible overflows. This patch improves the check as unsigned int a, b, c; if ((a > 1) && (b > 1){ if ((UINT_MAX/a) < b) // error } An additional case has been added to the tests, with two 32-bit values that cause overflow and are not detected by the old check. It is also necessary to break the lowering procedure in case the current BasicBlock is splitted; in this case it was necessary in order not to trigger the division by 0 error.
Diffstat (limited to 'utils')
0 files changed, 0 insertions, 0 deletions