Check extensions of generated files in tests

32 files changed, 83 insertions, 5 deletions

diff --git a/test/Feature/ubsan/ubsan_alignment-assumption.c b/test/Feature/ubsan/ubsan_alignment-assumption.c
index b48929ac..d18f2a28 100644
--- a/test/Feature/ubsan/ubsan_alignment-assumption.c
+++ b/test/Feature/ubsan/ubsan_alignment-assumption.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=alignment -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdlib.h>
diff --git a/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c b/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c
index 587c5108..d0b5c03a 100644
--- a/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c
+++ b/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=alignment -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdlib.h>
diff --git a/test/Feature/ubsan/ubsan_alignment-type-mismatch.c b/test/Feature/ubsan/ubsan_alignment-type-mismatch.c
index 37eb0927..4fde8921 100644
--- a/test/Feature/ubsan/ubsan_alignment-type-mismatch.c
+++ b/test/Feature/ubsan/ubsan_alignment-type-mismatch.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=alignment -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdlib.h>
diff --git a/test/Feature/ubsan/ubsan_array_bounds.c b/test/Feature/ubsan/ubsan_array_bounds.c
index 626d016b..ba4e7b5c 100644
--- a/test/Feature/ubsan/ubsan_array_bounds.c
+++ b/test/Feature/ubsan/ubsan_array_bounds.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=array-bounds -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_bool.c b/test/Feature/ubsan/ubsan_bool.c
index 4c2a9dbb..360af183 100644
--- a/test/Feature/ubsan/ubsan_bool.c
+++ b/test/Feature/ubsan/ubsan_bool.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=bool -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep undefined_behavior.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_builtin.c b/test/Feature/ubsan/ubsan_builtin.c
index 85603646..72ff73da 100644
--- a/test/Feature/ubsan/ubsan_builtin.c
+++ b/test/Feature/ubsan/ubsan_builtin.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=builtin -w -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_enum.c b/test/Feature/ubsan/ubsan_enum.c
index d6422fcb..1c79629a 100644
--- a/test/Feature/ubsan/ubsan_enum.c
+++ b/test/Feature/ubsan/ubsan_enum.c
@@ -1,6 +1,8 @@
 // RUN: %clangxx %s -fsanitize=enum -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_float_cast_overflow.c b/test/Feature/ubsan/ubsan_float_cast_overflow.c
index 749a340e..6f17c6fa 100644
--- a/test/Feature/ubsan/ubsan_float_cast_overflow.c
+++ b/test/Feature/ubsan/ubsan_float_cast_overflow.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=float-cast-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
@@ -8,6 +10,8 @@ int main() {
   float f = 0x7fffff80;
   volatile int result;
 
+  // TODO: uncomment when support for floating points is integrated
+
   //  klee_make_symbolic(&f, sizeof(f), "f");
 
   // CHECK: runtime/Sanitizer/ubsan/ubsan_handlers.cpp:35: float-cast-overflow
diff --git a/test/Feature/ubsan/ubsan_float_divide_by_zero.c b/test/Feature/ubsan/ubsan_float_divide_by_zero.c
index eec44393..84857190 100644
--- a/test/Feature/ubsan/ubsan_float_divide_by_zero.c
+++ b/test/Feature/ubsan/ubsan_float_divide_by_zero.c
@@ -1,12 +1,16 @@
 // RUN: %clang %s -fsanitize=float-divide-by-zero -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .div.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
 int main() {
   float x = 1.0;
 
+  // TODO: uncomment when support for floating points is integrated
+
   //  klee_make_symbolic(&x, sizeof(x), "x");
   //  klee_assume(x != 0.0);
 
diff --git a/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c b/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c
index d8e99e54..9b334664 100644
--- a/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c
+++ b/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=implicit-integer-sign-change -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .implicit_conversion.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c b/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
index 3d6ffcd1..cc511f7f 100644
--- a/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
+++ b/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=implicit-signed-integer-truncation -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .implicit_conversion.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c b/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
index 5421d10f..b90fac70 100644
--- a/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
+++ b/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=implicit-unsigned-integer-truncation -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .implicit_conversion.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_integer_divide_by_zero.c b/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
index ff5458ab..c33bab38 100644
--- a/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
+++ b/test/Feature/ubsan/ubsan_integer_divide_by_zero.c
@@ -1,6 +1,10 @@
 // RUN: %clang %s -fsanitize=integer-divide-by-zero -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime --check-div-zero=false %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 1
+
+#include "klee/klee.h"
 
 #if defined(__SIZEOF_INT128__) && !defined(_WIN32)
 typedef __int128 intmax;
diff --git a/test/Feature/ubsan/ubsan_nonnull_attribute.c b/test/Feature/ubsan/ubsan_nonnull_attribute.c
index 0e1c8411..a98aeadd 100644
--- a/test/Feature/ubsan/ubsan_nonnull_attribute.c
+++ b/test/Feature/ubsan/ubsan_nonnull_attribute.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=nonnull-attribute -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .nullable_attribute.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_null.c b/test/Feature/ubsan/ubsan_null.c
index 5f3a516f..f5ad6fdf 100644
--- a/test/Feature/ubsan/ubsan_null.c
+++ b/test/Feature/ubsan/ubsan_null.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=null -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_nullability_arg.c b/test/Feature/ubsan/ubsan_nullability_arg.c
index 72cb79aa..c7393649 100644
--- a/test/Feature/ubsan/ubsan_nullability_arg.c
+++ b/test/Feature/ubsan/ubsan_nullability_arg.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=nullability-arg -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .nullable_attribute.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_nullability_assign.c b/test/Feature/ubsan/ubsan_nullability_assign.c
index 84421bb7..eaf58a65 100644
--- a/test/Feature/ubsan/ubsan_nullability_assign.c
+++ b/test/Feature/ubsan/ubsan_nullability_assign.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=nullability-assign -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_nullability_return.c b/test/Feature/ubsan/ubsan_nullability_return.c
index 3e1a76d3..25b2b5e0 100644
--- a/test/Feature/ubsan/ubsan_nullability_return.c
+++ b/test/Feature/ubsan/ubsan_nullability_return.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=nullability-return -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .nullable_attribute.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c
index acf551bc..dcbba073 100644
--- a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdio.h>
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c
index 529c0d11..cb126742 100644
--- a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdio.h>
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c
index dc9ff50f..20286bcc 100644
--- a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdio.h>
@@ -12,6 +14,7 @@ int main() {
   volatile char *result;
 
   klee_make_symbolic(&address, sizeof(address), "address");
+  klee_assume(address != 0);
 
   char *ptr = (char *)address;
 
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c b/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c
index 29df3823..301952b9 100644
--- a/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c
@@ -3,6 +3,8 @@
 // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdio.h>
diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c b/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c
index be15628c..123034b5 100644
--- a/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c
+++ b/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
 
 #include "klee/klee.h"
 #include <stdio.h>
diff --git a/test/Feature/ubsan/ubsan_return.c b/test/Feature/ubsan/ubsan_return.c
index 3e9c8ccb..c2327db4 100644
--- a/test/Feature/ubsan/ubsan_return.c
+++ b/test/Feature/ubsan/ubsan_return.c
@@ -1,6 +1,8 @@
 // RUN: %clangxx %s -fsanitize=return -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c b/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c
index d8fd661c..f2a1c6e4 100644
--- a/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c
+++ b/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=returns-nonnull-attribute -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .nullable_attribute.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_shift_base.c b/test/Feature/ubsan/ubsan_shift_base.c
index 31d87f43..2da71582 100644
--- a/test/Feature/ubsan/ubsan_shift_base.c
+++ b/test/Feature/ubsan/ubsan_shift_base.c
@@ -1,6 +1,14 @@
-// RUN: %clang %s -fsanitize=shift -emit-llvm -g %O0opt -c -o %t.bc
+// RUN: %clang %s -fsanitize=shift-base -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime --check-overshift=false %t.bc 2>&1 | FileCheck %s
+//
+// There may be 2 or 3 test cases depending on the search heuristic, so we don't check the number of tests.
+// For example, 2 test cases may be as follows:
+// (1) b <= 31 without overflow, (2) a > 0 and b > 31 with overflow
+// For example, 3 test cases may be as follows:
+// (1) a = 0 and b > 31 without overflow, (2) b < 31 without overflow, (3) a > 0 and b > 31 with overflow
+//
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_shift_exponent.c b/test/Feature/ubsan/ubsan_shift_exponent.c
index 1716ecb9..548ebb66 100644
--- a/test/Feature/ubsan/ubsan_shift_exponent.c
+++ b/test/Feature/ubsan/ubsan_shift_exponent.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=shift-exponent -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime --check-overshift=false %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_signed_integer_overflow.c b/test/Feature/ubsan/ubsan_signed_integer_overflow.c
index 306d0935..df798e79 100644
--- a/test/Feature/ubsan/ubsan_signed_integer_overflow.c
+++ b/test/Feature/ubsan/ubsan_signed_integer_overflow.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=signed-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 5
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 4
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_unreachable.c b/test/Feature/ubsan/ubsan_unreachable.c
index 56de8e61..76e2e909 100644
--- a/test/Feature/ubsan/ubsan_unreachable.c
+++ b/test/Feature/ubsan/ubsan_unreachable.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=unreachable -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .undefined_behavior.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c b/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c
index fb90d97f..a11c8d07 100644
--- a/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c
+++ b/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c
@@ -1,6 +1,8 @@
 // RUN: %clang %s -fsanitize=unsigned-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 5
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 4
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_unsigned_shift_base.c b/test/Feature/ubsan/ubsan_unsigned_shift_base.c
index d08bfe16..92c61353 100644
--- a/test/Feature/ubsan/ubsan_unsigned_shift_base.c
+++ b/test/Feature/ubsan/ubsan_unsigned_shift_base.c
@@ -2,7 +2,9 @@
 
 // RUN: %clang %s -fsanitize=unsigned-shift-base -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime --check-overshift=false %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 2
+// RUN: ls %t.klee-out/ | grep .overflow.err | wc -l | grep 1
 
 #include "klee/klee.h"
 
diff --git a/test/Feature/ubsan/ubsan_vla_bound.c b/test/Feature/ubsan/ubsan_vla_bound.c
index 24a95d17..a057c62c 100644
--- a/test/Feature/ubsan/ubsan_vla_bound.c
+++ b/test/Feature/ubsan/ubsan_vla_bound.c
@@ -1,6 +1,9 @@
 // RUN: %clang %s -fsanitize=vla-bound -emit-llvm -g %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s
+// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 3
+// RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 1
+// RUN: ls %t.klee-out/ | grep .model.err | wc -l | grep 1
 
 #include "klee/klee.h"