diff options
author | Frank Busse <bb0xfb@gmail.com> | 2023-03-24 14:27:17 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-03-26 16:06:47 +0100 |
commit | 67ec44723e9ce232f067964e7e9fb26090be305d (patch) | |
tree | 1fa06d0fa085891fbabf3d2fa502751e2324fac0 | |
parent | 7c9ce86abd16624a6d6ee509b3dce86d191568ca (diff) | |
download | klee-67ec44723e9ce232f067964e7e9fb26090be305d.tar.gz |
tests: add some missing headers
-rw-r--r-- | test/Coverage/ReplayOutDir.c | 2 | ||||
-rw-r--r-- | test/Feature/AddressOfLabelsSymbolic.c | 2 | ||||
-rw-r--r-- | test/Feature/ExprLogging.c | 2 | ||||
-rw-r--r-- | test/Feature/WithLibc.c | 5 | ||||
-rw-r--r-- | test/Feature/arithmetic-right-overshift-sym-conc.c | 3 | ||||
-rw-r--r-- | test/Runtime/klee-libc/bcmp.c | 2 | ||||
-rw-r--r-- | test/regression/2016-06-28-div-zero-bug.c | 2 |
7 files changed, 18 insertions, 0 deletions
diff --git a/test/Coverage/ReplayOutDir.c b/test/Coverage/ReplayOutDir.c index 6476f32f..d2e34b6e 100644 --- a/test/Coverage/ReplayOutDir.c +++ b/test/Coverage/ReplayOutDir.c @@ -3,6 +3,8 @@ // RUN: %klee --output-dir=%t1.out %t1.bc // RUN: %klee --output-dir=%t1.replay --replay-ktest-dir=%t1.out %t1.bc +#include "klee/klee.h" + int main() { int i; klee_make_symbolic(&i, sizeof i, "i"); diff --git a/test/Feature/AddressOfLabelsSymbolic.c b/test/Feature/AddressOfLabelsSymbolic.c index 0b24a42d..1097a189 100644 --- a/test/Feature/AddressOfLabelsSymbolic.c +++ b/test/Feature/AddressOfLabelsSymbolic.c @@ -4,6 +4,8 @@ // RUN: FileCheck %s -check-prefix=CHECK-MSG --input-file=%t.log // RUN: FileCheck %s -check-prefix=CHECK-ERR --input-file=%t.stderr.log +#include "klee/klee.h" + #include <stdio.h> int main(void) { diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c index 70aaa49b..d892272a 100644 --- a/test/Feature/ExprLogging.c +++ b/test/Feature/ExprLogging.c @@ -11,6 +11,8 @@ // RUN: grep "^; Query" %t.klee-out/all-queries.smt2 | wc -l | grep -q 17 // RUN: grep "^; Query" %t.klee-out/solver-queries.smt2 | wc -l | grep -q 17 +#include "klee/klee.h" + #include <assert.h> int constantArr[16 ] = { diff --git a/test/Feature/WithLibc.c b/test/Feature/WithLibc.c index bb1c66c0..2babbe62 100644 --- a/test/Feature/WithLibc.c +++ b/test/Feature/WithLibc.c @@ -4,6 +4,11 @@ // RUN: echo "good" > %t3.good // RUN: diff %t3.log %t3.good +#include "klee/klee.h" + +#include <stdio.h> +#include <string.h> + int main() { char buf[4]; char *s = "foo"; diff --git a/test/Feature/arithmetic-right-overshift-sym-conc.c b/test/Feature/arithmetic-right-overshift-sym-conc.c index c58f13a1..efe946f2 100644 --- a/test/Feature/arithmetic-right-overshift-sym-conc.c +++ b/test/Feature/arithmetic-right-overshift-sym-conc.c @@ -3,6 +3,9 @@ // RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc // RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt // RUN: grep "KLEE: done: explored paths = 1" %t.klee-out/info + +#include "klee/klee.h" + #include <stdio.h> #include <assert.h> diff --git a/test/Runtime/klee-libc/bcmp.c b/test/Runtime/klee-libc/bcmp.c index d0f5d7e5..1cc72aa1 100644 --- a/test/Runtime/klee-libc/bcmp.c +++ b/test/Runtime/klee-libc/bcmp.c @@ -4,6 +4,8 @@ // test bcmp for sizes including zero +#include "klee/klee.h" + #include <assert.h> #include <stdlib.h> #include <strings.h> diff --git a/test/regression/2016-06-28-div-zero-bug.c b/test/regression/2016-06-28-div-zero-bug.c index 6e2e8c5e..dfab14d3 100644 --- a/test/regression/2016-06-28-div-zero-bug.c +++ b/test/regression/2016-06-28-div-zero-bug.c @@ -6,6 +6,8 @@ // See https://github.com/klee/klee/issues/308 // and https://github.com/stp/stp/issues/206 +#include "klee/klee.h" + int b, a, g; int *c = &b, *d = &b, *f = &a; |