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

1 files changed, 19 insertions, 0 deletions

diff --git a/test/Feature/ubsan_uadd_overflow.c b/test/Feature/ubsan_uadd_overflow.c
new file mode 100644
index 00000000..9dc6832d
--- /dev/null
+++ b/test/Feature/ubsan_uadd_overflow.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -fsanitize=unsigned-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %klee %t.bc 2> %t.log
+// RUN: grep -c "overflow on unsigned addition" %t.log
+// RUN: grep -c "ubsan_uadd_overflow.c:16: overflow" %t.log
+
+#include "klee/klee.h"
+
+int main()
+{
+  unsigned int x;
+  unsigned int y;
+  volatile unsigned int result;
+
+  klee_make_symbolic(&x, sizeof(x), "unsigned add 1");
+  klee_make_symbolic(&y, sizeof(y), "unsigned add 2");
+  result = x + y;
+
+  return 0;
+}