diff options
Diffstat (limited to 'test/regression')
19 files changed, 24 insertions, 10 deletions
diff --git a/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c b/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c index 1897266a..ac32063c 100644 --- a/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c +++ b/test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c @@ -2,6 +2,7 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc +#include "klee/klee.h" #include <assert.h> int main(void) { diff --git a/test/regression/2007-07-30-unflushed-byte.c b/test/regression/2007-07-30-unflushed-byte.c index bb480b9a..2d2f1e8c 100644 --- a/test/regression/2007-07-30-unflushed-byte.c +++ b/test/regression/2007-07-30-unflushed-byte.c @@ -1,7 +1,7 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc - +#include "klee/klee.h" #include <assert.h> int main() { diff --git a/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c b/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c index 96115557..73ceec91 100644 --- a/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c +++ b/test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c @@ -2,6 +2,7 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc +#include "klee/klee.h" #include <assert.h> #include <stdio.h> diff --git a/test/regression/2007-08-06-64bit-shift.c b/test/regression/2007-08-06-64bit-shift.c index f072e453..675211fd 100644 --- a/test/regression/2007-08-06-64bit-shift.c +++ b/test/regression/2007-08-06-64bit-shift.c @@ -2,6 +2,7 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc +#include "klee/klee.h" #include <assert.h> int main() { diff --git a/test/regression/2007-08-06-access-after-free.c b/test/regression/2007-08-06-access-after-free.c index 7d1f81db..ef47c868 100644 --- a/test/regression/2007-08-06-access-after-free.c +++ b/test/regression/2007-08-06-access-after-free.c @@ -2,7 +2,9 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc +#include "klee/klee.h" #include <assert.h> +#include <stdlib.h> int main() { int a; diff --git a/test/regression/2007-08-16-invalid-constant-value.c b/test/regression/2007-08-16-invalid-constant-value.c index c49357f8..f5474f7a 100644 --- a/test/regression/2007-08-16-invalid-constant-value.c +++ b/test/regression/2007-08-16-invalid-constant-value.c @@ -1,5 +1,5 @@ // RUN: rm -f %t4.out %t4.err %t4.log -// RUN: %clang %s -emit-llvm -O2 -c -o %t1.bc +// RUN: %clang %s -std=c89 -emit-llvm -O2 -c -o %t1.bc // RUN: %llvmas -f %p/../Feature/_utils._ll -o %t2.bc // RUN: %llvmlink %t1.bc %t2.bc -o %t3.bc // RUN: rm -rf %t.klee-out @@ -7,8 +7,6 @@ #include <assert.h> -#include "../Feature/utils.h" - int main() { unsigned char a; diff --git a/test/regression/2007-08-16-valid-write-to-freed-object.c b/test/regression/2007-08-16-valid-write-to-freed-object.c index 6b6efecb..2a43a240 100644 --- a/test/regression/2007-08-16-valid-write-to-freed-object.c +++ b/test/regression/2007-08-16-valid-write-to-freed-object.c @@ -2,6 +2,8 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc +#include "klee/klee.h" +#include <stdio.h> unsigned sym() { unsigned x; klee_make_symbolic(&x, sizeof x, "x"); diff --git a/test/regression/2007-10-11-free-of-alloca.c b/test/regression/2007-10-11-free-of-alloca.c index 6aa6cdb3..cecdeef2 100644 --- a/test/regression/2007-10-11-free-of-alloca.c +++ b/test/regression/2007-10-11-free-of-alloca.c @@ -2,7 +2,7 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s // RUN: test -f %t.klee-out/test000001.free.err - +#include <stdlib.h> int main() { int buf[4]; // CHECK: 2007-10-11-free-of-alloca.c:9: free of alloca diff --git a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c index 64cae9f4..77f9b9f6 100644 --- a/test/regression/2007-10-12-failed-make-symbolic-after-copy.c +++ b/test/regression/2007-10-12-failed-make-symbolic-after-copy.c @@ -2,7 +2,7 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc // RUN: test -f %t.klee-out/test000001.ktest - +#include "klee/klee.h" int main() { unsigned x, y[4]; diff --git a/test/regression/2008-03-04-free-of-global.c b/test/regression/2008-03-04-free-of-global.c index 995e7173..fb4a2df8 100644 --- a/test/regression/2008-03-04-free-of-global.c +++ b/test/regression/2008-03-04-free-of-global.c @@ -3,10 +3,11 @@ // RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s // RUN: test -f %t.klee-out/test000001.free.err +#include <stdlib.h> int buf[4]; int main() { - // CHECK: 2008-03-04-free-of-global.c:10: free of global + // CHECK: 2008-03-04-free-of-global.c:[[@LINE+1]]: free of global free(buf); // this should give runtime error, not crash return 0; } diff --git a/test/regression/2008-03-11-free-of-malloc-zero.c b/test/regression/2008-03-11-free-of-malloc-zero.c index e90baa2c..cdd2ef35 100644 --- a/test/regression/2008-03-11-free-of-malloc-zero.c +++ b/test/regression/2008-03-11-free-of-malloc-zero.c @@ -1,7 +1,7 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc - +#include "klee/klee.h" #include <stdlib.h> int main() { diff --git a/test/regression/2008-04-10-bad-alloca-free.c b/test/regression/2008-04-10-bad-alloca-free.c index 5049f47c..d20d07d2 100644 --- a/test/regression/2008-04-10-bad-alloca-free.c +++ b/test/regression/2008-04-10-bad-alloca-free.c @@ -2,6 +2,7 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc +#include "klee/klee.h" void f(int *addr) { klee_make_symbolic(addr, sizeof *addr, "moo"); } diff --git a/test/regression/2014-07-04-unflushed-error-report.c b/test/regression/2014-07-04-unflushed-error-report.c index c929328d..058aef7e 100644 --- a/test/regression/2014-07-04-unflushed-error-report.c +++ b/test/regression/2014-07-04-unflushed-error-report.c @@ -6,6 +6,7 @@ /* This test checks that the error file isn't empty and contains the * right content. */ +#include "klee/klee.h" int main() { unsigned int x = 15; unsigned int y; diff --git a/test/regression/2015-08-05-invalid-fork.c b/test/regression/2015-08-05-invalid-fork.c index a165cab2..5c09cbfc 100644 --- a/test/regression/2015-08-05-invalid-fork.c +++ b/test/regression/2015-08-05-invalid-fork.c @@ -3,6 +3,7 @@ is printed a single time. */ #include "klee/klee.h" +#include <stdio.h> // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out diff --git a/test/regression/2015-08-30-empty-constraints.c b/test/regression/2015-08-30-empty-constraints.c index f92b6978..8598b6ae 100644 --- a/test/regression/2015-08-30-empty-constraints.c +++ b/test/regression/2015-08-30-empty-constraints.c @@ -10,6 +10,7 @@ * are generated. * Make sure we are able to generate an input. */ +#include "klee/klee.h" int main() { int d; diff --git a/test/regression/2015-08-30-sdiv-1.c b/test/regression/2015-08-30-sdiv-1.c index 7356e74c..2b819aea 100644 --- a/test/regression/2015-08-30-sdiv-1.c +++ b/test/regression/2015-08-30-sdiv-1.c @@ -7,6 +7,7 @@ /* Division by constant can be optimized.using mul/shift * For signed division, div by 1 or -1 cannot be optimized like that. */ +#include "klee/klee.h" #include <stdint.h> int main() { int32_t dividend; diff --git a/test/regression/2017-02-21-pathOS-id.c b/test/regression/2017-02-21-pathOS-id.c index b6ee269a..112875de 100644 --- a/test/regression/2017-02-21-pathOS-id.c +++ b/test/regression/2017-02-21-pathOS-id.c @@ -5,6 +5,9 @@ // RUN: cat %t.klee-out/test000002.path | wc -l | grep -q 1 // RUN: cat %t.klee-out/test000003.path | wc -l | grep -q 1 // RUN: cat %t.klee-out/test000004.path | wc -l | grep -q 1 + +#include "klee/klee.h" +#include "stdlib.h" int main(){ int a, b; klee_make_symbolic (&a, sizeof(int), "a"); diff --git a/test/regression/2017-11-01-test-with-empty-varname.c b/test/regression/2017-11-01-test-with-empty-varname.c index 89108d9d..578043ad 100644 --- a/test/regression/2017-11-01-test-with-empty-varname.c +++ b/test/regression/2017-11-01-test-with-empty-varname.c @@ -2,7 +2,7 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc // RUN: FileCheck %s --input-file=%t.klee-out/warnings.txt - +#include "klee/klee.h" int main() { unsigned a; diff --git a/test/regression/2020-04-27-stp-array-names.c b/test/regression/2020-04-27-stp-array-names.c index f06e1b1a..a256441c 100644 --- a/test/regression/2020-04-27-stp-array-names.c +++ b/test/regression/2020-04-27-stp-array-names.c @@ -1,4 +1,4 @@ -// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc +// RUN: %clang -std=c89 %s -emit-llvm %O0opt -g -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee -output-dir=%t.klee-out --search=bfs --max-instructions=1000 %t.bc b; |