diff options
author | Luca Dariz <l.dariz@imamoter.cnr.t> | 2014-11-20 12:41:12 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2015-02-13 18:49:49 +0000 |
commit | 714dc22ccb12efdc203e8ce92d6e546ca9ffb157 (patch) | |
tree | cc31c6b8bb0d886d5c86eb93f1517cad8bc326de /test/Feature/ubsan_smul_overflow.c | |
parent | dbe13e13a215aa7212b5737dd8903699301a4940 (diff) | |
download | klee-714dc22ccb12efdc203e8ce92d6e546ca9ffb157.tar.gz |
refactor integer overflow detection, add signed int
Instead of checking for every possible casse which result in overflow, it is much simpler to perform the operation using integers with bigger dimension and check if the result overflow
Diffstat (limited to 'test/Feature/ubsan_smul_overflow.c')
-rw-r--r-- | test/Feature/ubsan_smul_overflow.c | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test/Feature/ubsan_smul_overflow.c b/test/Feature/ubsan_smul_overflow.c new file mode 100644 index 00000000..21a796cb --- /dev/null +++ b/test/Feature/ubsan_smul_overflow.c @@ -0,0 +1,19 @@ +// RUN: %llvmgcc %s -fsanitize=signed-integer-overflow -emit-llvm -g -O0 -c -o %t.bc +// RUN: %klee %t.bc 2> %t.log +// RUN: grep -c "overflow on unsigned multiplication" %t.log +// RUN: grep -c "ubsan_smul_overflow.c:16: overflow" %t.log + +#include "klee/klee.h" + +int main() +{ + int x; + int y; + volatile int result; + + klee_make_symbolic(&x, sizeof(x), "signed mul 1"); + klee_make_symbolic(&y, sizeof(y), "signed mul 2"); + result = x * y; + + return 0; +} |