diff options
Diffstat (limited to 'test/Feature')
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" |