about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2023-03-24 14:27:17 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2023-03-26 16:06:47 +0100
commit67ec44723e9ce232f067964e7e9fb26090be305d (patch)
tree1fa06d0fa085891fbabf3d2fa502751e2324fac0
parent7c9ce86abd16624a6d6ee509b3dce86d191568ca (diff)
downloadklee-67ec44723e9ce232f067964e7e9fb26090be305d.tar.gz
tests: add some missing headers
-rw-r--r--test/Coverage/ReplayOutDir.c2
-rw-r--r--test/Feature/AddressOfLabelsSymbolic.c2
-rw-r--r--test/Feature/ExprLogging.c2
-rw-r--r--test/Feature/WithLibc.c5
-rw-r--r--test/Feature/arithmetic-right-overshift-sym-conc.c3
-rw-r--r--test/Runtime/klee-libc/bcmp.c2
-rw-r--r--test/regression/2016-06-28-div-zero-bug.c2
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;