[feat] uint128

UnitTestBot · Oct 5, 2023 · 90e8cbf · 90e8cbf
1 parent 37f0da6
commit 90e8cbf
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 0 deletions.
diff --git a/include/klee-test-comp.c b/include/klee-test-comp.c
@@ -33,6 +33,12 @@ unsigned int __VERIFIER_nondet_uint(void) {
   return x;
 }
 
+unsigned __int128 __VERIFIER_nondet_uint128(void) {
+  unsigned __int128 x;
+  klee_make_symbolic(&x, sizeof(x), "unsigned __int128");
+  return x;
+}
+
 unsigned __VERIFIER_nondet_unsigned(void) {
   unsigned x;
   klee_make_symbolic(&x, sizeof(x), "unsigned");

diff --git a/test/Feature/uint128.c b/test/Feature/uint128.c
@@ -0,0 +1,11 @@
+// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
+// CHECK-NOT: failed external call
+#include "klee-test-comp.c"
+extern unsigned __int128 __VERIFIER_nondet_uint128();
+
+int main() {
+  __int128 x = __VERIFIER_nondet_uint128();
+  return x > 0;
+}