Check extensions of generated files in tests

Yuzhou-Fang · Sep 14, 2022 · f3f4736 · f3f4736
1 parent d244508
commit f3f4736
Show file tree

Hide file tree

Showing 32 changed files with 83 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1,13 +1,17 @@
 // 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"
 
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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"