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 /lib/Solver/STPBuilder.cpp | |
| 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 'lib/Solver/STPBuilder.cpp')
0 files changed, 0 insertions, 0 deletions
