about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/ArrayOpt/test_feasible.c3
-rw-r--r--test/DeterministicAllocation/OneOutOfBounds.c2
-rw-r--r--test/Expr/ReadExprConsistency.c10
-rw-r--r--test/Feature/BFSSearcherAndDFSSearcherInterleaved.c2
-rw-r--r--test/Feature/ByteSwap.c2
-rw-r--r--test/Feature/CheckMemoryAccess.c4
-rw-r--r--test/Feature/CompressedExprLogging.c2
-rw-r--r--test/Feature/CopyOnWrite.c2
-rw-r--r--test/Feature/DanglingConcreteReadExpr.c2
-rw-r--r--test/Feature/DefineFixedObject.c2
-rw-r--r--test/Feature/Envp.c3
-rw-r--r--test/Feature/GetValue.c4
-rw-r--r--test/Feature/InAndOutOfBounds.c2
-rw-r--r--test/Feature/IndirectCallToExternal.c2
-rw-r--r--test/Feature/InlineAsm.c2
-rw-r--r--test/Feature/IsSymbolic.c2
-rw-r--r--test/Feature/KleeReportError.c1
-rw-r--r--test/Feature/LowerSwitch.c2
-rw-r--r--test/Feature/MakeSymbolicAPI.c3
-rw-r--r--test/Feature/MakeSymbolicName.c2
-rw-r--r--test/Feature/Memalign.c4
-rw-r--r--test/Feature/MultiMkSym.c2
-rw-r--r--test/Feature/MultipleReadResolution.c3
-rw-r--r--test/Feature/MultipleReallocResolution.c4
-rw-r--r--test/Feature/MultipleWriteResolution.c4
-rw-r--r--test/Feature/NamedSeedMatching.c4
-rw-r--r--test/Feature/NoExternalCallsAllowed.c2
-rw-r--r--test/Feature/OneOutOfBounds.c1
-rw-r--r--test/Feature/Optimize.c1
-rw-r--r--test/Feature/OverlappedError.c2
-rw-r--r--test/Feature/PreferCex.c5
-rw-r--r--test/Feature/RaiseAsm.c2
-rw-r--r--test/Feature/ReplayPath.c4
-rw-r--r--test/Feature/Searchers.c2
-rw-r--r--test/Feature/SetForking.c2
-rw-r--r--test/Feature/SilentKleeAssume.c4
-rw-r--r--test/Feature/SolverTimeout.c2
-rw-r--r--test/Feature/WriteCov.c2
-rw-r--r--test/Feature/consecutive_divide_by_zero.c2
-rw-r--r--test/Feature/const_array_opt1.c1
-rw-r--r--test/Feature/left-overshift-sym-conc.c3
-rw-r--r--test/Feature/logical-right-overshift-sym-conc.c3
-rw-r--r--test/Feature/srem.c3
-rw-r--r--test/Merging/merge_fail.c1
-rw-r--r--test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c1
-rw-r--r--test/Runtime/POSIX/FDNumbers.c4
-rw-r--r--test/Runtime/POSIX/Fcntl.c2
-rw-r--r--test/Runtime/POSIX/FreeArgv.c3
-rw-r--r--test/Runtime/POSIX/Getenv.c5
-rw-r--r--test/Runtime/POSIX/Openat.c3
-rw-r--r--test/Runtime/POSIX/Replay.c1
-rw-r--r--test/Runtime/POSIX/Stdin.c7
-rw-r--r--test/Runtime/POSIX/Write1.c4
-rw-r--r--test/Runtime/POSIX/Write2.c4
-rw-r--r--test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c1
-rw-r--r--test/VectorInstructions/insert_element.c3
-rw-r--r--test/regression/2007-07-25-invalid-stp-array-binding-to-objectstate.c1
-rw-r--r--test/regression/2007-07-30-unflushed-byte.c2
-rw-r--r--test/regression/2007-08-01-cache-unclear-on-overwrite-flushed.c1
-rw-r--r--test/regression/2007-08-06-64bit-shift.c1
-rw-r--r--test/regression/2007-08-06-access-after-free.c2
-rw-r--r--test/regression/2007-08-16-invalid-constant-value.c4
-rw-r--r--test/regression/2007-08-16-valid-write-to-freed-object.c2
-rw-r--r--test/regression/2007-10-11-free-of-alloca.c2
-rw-r--r--test/regression/2007-10-12-failed-make-symbolic-after-copy.c2
-rw-r--r--test/regression/2008-03-04-free-of-global.c3
-rw-r--r--test/regression/2008-03-11-free-of-malloc-zero.c2
-rw-r--r--test/regression/2008-04-10-bad-alloca-free.c1
-rw-r--r--test/regression/2014-07-04-unflushed-error-report.c1
-rw-r--r--test/regression/2015-08-05-invalid-fork.c1
-rw-r--r--test/regression/2015-08-30-empty-constraints.c1
-rw-r--r--test/regression/2015-08-30-sdiv-1.c1
-rw-r--r--test/regression/2017-02-21-pathOS-id.c3
-rw-r--r--test/regression/2017-11-01-test-with-empty-varname.c2
-rw-r--r--test/regression/2020-04-27-stp-array-names.c2
75 files changed, 111 insertions, 78 deletions
diff --git a/test/ArrayOpt/test_feasible.c b/test/ArrayOpt/test_feasible.c
index 8e7009b4..8dc3c4e3 100644
--- a/test/ArrayOpt/test_feasible.c
+++ b/test/ArrayOpt/test_feasible.c
@@ -22,8 +22,9 @@
 // CHECK-OPT_V: KLEE: WARNING: OPT_V: successful
 // CHECK-CONST_ARR: const_arr
 
-#include <stdio.h>
 #include "klee/klee.h"
+#include <assert.h>
+#include <stdio.h>
 
 char array[5] = {0,1,0,1,0};
 
diff --git a/test/DeterministicAllocation/OneOutOfBounds.c b/test/DeterministicAllocation/OneOutOfBounds.c
index 499ff06b..c3dbc597 100644
--- a/test/DeterministicAllocation/OneOutOfBounds.c
+++ b/test/DeterministicAllocation/OneOutOfBounds.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --kdalloc %t.bc 2>&1 | FileCheck %s
 // RUN: test -f %t.klee-out/test000001.ptr.err
-
+#include <stdlib.h>
 int main() {
   int *x = malloc(sizeof(int));
   // CHECK: OneOutOfBounds.c:[[@LINE+1]]: memory error: out of bound pointer
diff --git a/test/Expr/ReadExprConsistency.c b/test/Expr/ReadExprConsistency.c
index 9b794ee5..6429dc99 100644
--- a/test/Expr/ReadExprConsistency.c
+++ b/test/Expr/ReadExprConsistency.c
@@ -2,8 +2,9 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t.bc 2>%t.log
 // RUN: cat %t.log | FileCheck %s
-
+#include "klee/klee.h"
 #include <assert.h>
+#include <stdio.h>
 
 /*
 This tests checks ensures that only relevant updates are present when doing
@@ -15,7 +16,6 @@ https://github.com/klee/klee/issues/921
 https://github.com/klee/klee/pull/1061
 */
 
-void klee_print_expr(const char*, char);
 int main() {
 	char  arr[3];
   char symbolic;
@@ -25,12 +25,12 @@ int main() {
   
   
   char a = arr[2];  // (ReadExpr 2 arr)
-  //CHECK: arr[2]:(Read w8 2 arr)
+  // CHECK: arr[2]:(SExt w32 (Read w8 2 arr))
   klee_print_expr("arr[2]", arr[2]);
   arr[1] = 0;
   char b = arr[symbolic];  // (ReadExpr symbolic [1=0]@arr)
-  //CHECK: arr[2]:(Read w8 2 arr)
-  //CHECK-NOT: arr[2]:(Read w8 2 [1=0]@arr)
+  // CHECK: arr[2]:(SExt w32 (Read w8 2 arr))
+  // CHECK-NOT: arr[2]:(SExt w32 (Read w8 2 [1=0]@arr))
   klee_print_expr("arr[2]", arr[2]);
   
   if(a == b) printf("Equal!\n");
diff --git a/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c b/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c
index 88d49548..8e4859a3 100644
--- a/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c
+++ b/test/Feature/BFSSearcherAndDFSSearcherInterleaved.c
@@ -13,7 +13,7 @@
 // RUN: FileCheck -input-file=%t-dfs-bfs.out %s
 
 #include "klee/klee.h"
-
+#include <stdio.h>
 int main() {
   int x, y, z;
   klee_make_symbolic(&x, sizeof(x), "x");
diff --git a/test/Feature/ByteSwap.c b/test/Feature/ByteSwap.c
index 1e4ec190..d862b53d 100644
--- a/test/Feature/ByteSwap.c
+++ b/test/Feature/ByteSwap.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 --libc=klee --exit-on-error %t1.bc
-
+#include "klee/klee.h"
 #include <arpa/inet.h>
 #include <assert.h>
 
diff --git a/test/Feature/CheckMemoryAccess.c b/test/Feature/CheckMemoryAccess.c
index a9e0e6b5..9854f983 100644
--- a/test/Feature/CheckMemoryAccess.c
+++ b/test/Feature/CheckMemoryAccess.c
@@ -3,10 +3,10 @@
 // RUN: %klee --output-dir=%t.klee-out %t.bc > %t.log
 // RUN: grep -q "good" %t.log
 // RUN: not grep -q "bad" %t.log
-
+#include "klee/klee.h"
 #include <assert.h>
-#include <stdlib.h>
 #include <stdio.h>
+#include <stdlib.h>
 
 int main() {
   char buf[4];
diff --git a/test/Feature/CompressedExprLogging.c b/test/Feature/CompressedExprLogging.c
index 42c42402..1344988b 100644
--- a/test/Feature/CompressedExprLogging.c
+++ b/test/Feature/CompressedExprLogging.c
@@ -10,7 +10,7 @@
 // RUN: %klee --output-dir=%t.klee-out2 --use-cex-cache=false --compress-query-log --use-query-log=all:kquery %t1.bc
 // RUN: gunzip -d %t.klee-out2/all-queries.kquery.gz
 // RUN: diff %t.klee-out/all-queries.kquery %t.klee-out/all-queries.kquery
-
+#include "klee/klee.h"
 #include <assert.h>
 
 int constantArr[16] = {1 << 0,  1 << 1,  1 << 2,  1 << 3, 1 << 4,  1 << 5,
diff --git a/test/Feature/CopyOnWrite.c b/test/Feature/CopyOnWrite.c
index 9d443bf6..73342642 100644
--- a/test/Feature/CopyOnWrite.c
+++ b/test/Feature/CopyOnWrite.c
@@ -1,7 +1,7 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --search=random-state --exit-on-error %t1.bc
-
+#include "klee/klee.h"
 #include <assert.h>
 
 #define N 5
diff --git a/test/Feature/DanglingConcreteReadExpr.c b/test/Feature/DanglingConcreteReadExpr.c
index ba7c7bc5..7b0c981d 100644
--- a/test/Feature/DanglingConcreteReadExpr.c
+++ b/test/Feature/DanglingConcreteReadExpr.c
@@ -2,7 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --optimize=false --output-dir=%t.klee-out %t1.bc
 // RUN: grep "total queries = 2" %t.klee-out/info
-
+#include "klee/klee.h"
 #include <assert.h>
 
 int main() {
diff --git a/test/Feature/DefineFixedObject.c b/test/Feature/DefineFixedObject.c
index 6e7efb14..102034d0 100644
--- a/test/Feature/DefineFixedObject.c
+++ b/test/Feature/DefineFixedObject.c
@@ -1,7 +1,7 @@
 // RUN: %clang -emit-llvm -c -o %t1.bc %s
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
-
+#include "klee/klee.h"
 #include <stdio.h>
 
 #define ADDRESS ((int*) 0x0080)
diff --git a/test/Feature/Envp.c b/test/Feature/Envp.c
index 62c91325..2b1b6bdc 100644
--- a/test/Feature/Envp.c
+++ b/test/Feature/Envp.c
@@ -1,8 +1,9 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
-
 #include <assert.h>
+#include <stdio.h>
+#include <string.h>
 
 int main(int argc, char **argv, char **envp) {
   unsigned i;
diff --git a/test/Feature/GetValue.c b/test/Feature/GetValue.c
index d2b046f4..c652658f 100644
--- a/test/Feature/GetValue.c
+++ b/test/Feature/GetValue.c
@@ -1,9 +1,9 @@
 // RUN: %clang -emit-llvm -c -o %t1.bc %s
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
-
-#include <stdio.h>
+#include "klee/klee.h"
 #include <assert.h>
+#include <stdio.h>
 
 int main() {
   int x = klee_int("x");
diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c
index 39ed8322..37c30e8f 100644
--- a/test/Feature/InAndOutOfBounds.c
+++ b/test/Feature/InAndOutOfBounds.c
@@ -4,6 +4,8 @@
 // RUN: test -f %t.klee-out/test000001.ptr.err -o -f %t.klee-out/test000002.ptr.err
 // RUN: not test -f %t.klee-out/test000001.ptr.err -a -f %t.klee-out/test000002.ptr.err
 // RUN: not test -f %t.klee-out/test000003.ktest
+#include "klee/klee.h"
+#include <stdlib.h>
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
diff --git a/test/Feature/IndirectCallToExternal.c b/test/Feature/IndirectCallToExternal.c
index 03447c7d..2d4943dc 100644
--- a/test/Feature/IndirectCallToExternal.c
+++ b/test/Feature/IndirectCallToExternal.c
@@ -8,7 +8,7 @@
 #include <assert.h>
 
 int main() {
-  int (*scmp)(char*,char*) = strcmp;
+  int (*scmp)(const char *, const char *) = strcmp;
 
   assert(scmp("hello","hi") < 0);
 
diff --git a/test/Feature/InlineAsm.c b/test/Feature/InlineAsm.c
index 25e0e72e..e6da7bb9 100644
--- a/test/Feature/InlineAsm.c
+++ b/test/Feature/InlineAsm.c
@@ -1,7 +1,7 @@
 // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --external-calls=all --exit-on-error --output-dir=%t.klee-out %t.bc > %t.output.log 2>&1
-
+#include "klee/klee.h"
 #include <assert.h>
 
 int main() {
diff --git a/test/Feature/IsSymbolic.c b/test/Feature/IsSymbolic.c
index 033d9d6a..266dd23f 100644
--- a/test/Feature/IsSymbolic.c
+++ b/test/Feature/IsSymbolic.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/Feature/KleeReportError.c b/test/Feature/KleeReportError.c
index f406696f..afd447f5 100644
--- a/test/Feature/KleeReportError.c
+++ b/test/Feature/KleeReportError.c
@@ -2,6 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s
 // RUN: ls %t.klee-out/ | grep .my.err | wc -l | grep 2
+#include "klee/klee.h"
 #include <assert.h>
 #include <stdio.h>
 
diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c
index a1bd3f38..76b9e63b 100644
--- a/test/Feature/LowerSwitch.c
+++ b/test/Feature/LowerSwitch.c
@@ -6,7 +6,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --switch-type=simple %t.bc
 // RUN: test -f %t.klee-out/test000010.ktest
-
+#include "klee/klee.h"
 #include <stdio.h>
 
 int main(int argc, char **argv) {
diff --git a/test/Feature/MakeSymbolicAPI.c b/test/Feature/MakeSymbolicAPI.c
index d5305422..ea115936 100644
--- a/test/Feature/MakeSymbolicAPI.c
+++ b/test/Feature/MakeSymbolicAPI.c
@@ -1,9 +1,8 @@
-// RUN: %clang %s -emit-llvm -g -c -o %t1.bc
+// RUN: %clang %s -std=c89 -emit-llvm -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc 2> %t.stderr.log
 // RUN: FileCheck %s -check-prefix=CHECK-WRN --input-file=%t.klee-out/warnings.txt
 // RUN: FileCheck %s -check-prefix=CHECK-ERR --input-file=%t.stderr.log
-
 int main() {
   unsigned a, b, c;
   char *p;
diff --git a/test/Feature/MakeSymbolicName.c b/test/Feature/MakeSymbolicName.c
index a57d9a84..332565d7 100644
--- a/test/Feature/MakeSymbolicName.c
+++ b/test/Feature/MakeSymbolicName.c
@@ -1,7 +1,7 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --search=random-state --exit-on-error %t1.bc
-
+#include "klee/klee.h"
 #include <assert.h>
 
 int main() {
diff --git a/test/Feature/Memalign.c b/test/Feature/Memalign.c
index e5d09f6c..524e257d 100644
--- a/test/Feature/Memalign.c
+++ b/test/Feature/Memalign.c
@@ -1,9 +1,9 @@
+// REQUIRES: not-darwin
 // RUN: %clang -emit-llvm -g -c %s -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t.bc > %t.log
-
+#include <malloc.h>
 #include <stdlib.h>
-
 int main(int argc, char *argv[]) {
   int *a = (int *)memalign(8, sizeof(int) * 5);
   for (int i = 0; i < 5; ++i) {
diff --git a/test/Feature/MultiMkSym.c b/test/Feature/MultiMkSym.c
index 16ac7d1b..e5222a94 100644
--- a/test/Feature/MultiMkSym.c
+++ b/test/Feature/MultiMkSym.c
@@ -6,7 +6,7 @@
 // RUN: grep "a\[100\]" %t1 | wc -l | grep 2
 
 /* Tests that the Array factory correctly distinguishes between arrays created at the same location but with different sizes */
-
+#include "klee/klee.h"
 #include <stdio.h>
 #include <stdlib.h>
 
diff --git a/test/Feature/MultipleReadResolution.c b/test/Feature/MultipleReadResolution.c
index 8701d068..92f3f92b 100644
--- a/test/Feature/MultipleReadResolution.c
+++ b/test/Feature/MultipleReadResolution.c
@@ -7,8 +7,9 @@
 // RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log
 // RUN: diff %t1.res %t1.log
 
+#include "klee/klee.h"
 #include <stdio.h>
-
+#include <stdlib.h>
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
   klee_make_symbolic(&x, sizeof x, "x");
diff --git a/test/Feature/MultipleReallocResolution.c b/test/Feature/MultipleReallocResolution.c
index 84dd15e2..90570537 100644
--- a/test/Feature/MultipleReallocResolution.c
+++ b/test/Feature/MultipleReallocResolution.c
@@ -3,10 +3,10 @@
 // RUN: %klee --output-dir=%t.klee-out %t1.bc
 // RUN: ls %t.klee-out/ | grep .err | wc -l | grep 2
 // RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 2
-
+#include "klee/klee.h"
 #include <assert.h>
-#include <stdlib.h>
 #include <stdio.h>
+#include <stdlib.h>
 
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
diff --git a/test/Feature/MultipleWriteResolution.c b/test/Feature/MultipleWriteResolution.c
index 89296c11..326767f2 100644
--- a/test/Feature/MultipleWriteResolution.c
+++ b/test/Feature/MultipleWriteResolution.c
@@ -6,9 +6,9 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log
 // RUN: diff %t1.res %t1.log
-
+#include "klee/klee.h"
 #include <stdio.h>
-
+#include <stdlib.h>
 unsigned klee_urange(unsigned start, unsigned end) {
   unsigned x;
   klee_make_symbolic(&x, sizeof x, "x");
diff --git a/test/Feature/NamedSeedMatching.c b/test/Feature/NamedSeedMatching.c
index 6f97e4e7..2cc47340 100644
--- a/test/Feature/NamedSeedMatching.c
+++ b/test/Feature/NamedSeedMatching.c
@@ -10,9 +10,9 @@
 // RUN: grep -q "b==4" %t.log
 // RUN: grep -q "c==5" %t.log
 // RUN: grep -q "x==6" %t.log
-
-#include <string.h>
+#include "klee/klee.h"
 #include <stdio.h>
+#include <string.h>
 
 int main(int argc, char **argv) {
   int a, b, c, x;
diff --git a/test/Feature/NoExternalCallsAllowed.c b/test/Feature/NoExternalCallsAllowed.c
index 8a8dc54b..62570434 100644
--- a/test/Feature/NoExternalCallsAllowed.c
+++ b/test/Feature/NoExternalCallsAllowed.c
@@ -2,8 +2,8 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --external-calls=none %t1.bc 2>&1 | FileCheck %s
 // RUN: test %t.klee-out/test000001.user.err
-
 #include <stdio.h>
+#include <stdlib.h>
 
 int main(int argc, char** argv) {
   // CHECK: Disallowed call to external function: abs
diff --git a/test/Feature/OneOutOfBounds.c b/test/Feature/OneOutOfBounds.c
index a3e6db1f..0dfee6d6 100644
--- a/test/Feature/OneOutOfBounds.c
+++ b/test/Feature/OneOutOfBounds.c
@@ -2,6 +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.ptr.err
+#include <stdlib.h>
 
 int main() {
   int *x = malloc(sizeof(int));
diff --git a/test/Feature/Optimize.c b/test/Feature/Optimize.c
index e14be96d..e125eff4 100644
--- a/test/Feature/Optimize.c
+++ b/test/Feature/Optimize.c
@@ -6,6 +6,7 @@
 // RUN: diff %t3.log %t3.good
 
 // should complete by 100 instructions if opt is on
+#include <stdio.h>
 
 int main() {
   int i, res = 0;
diff --git a/test/Feature/OverlappedError.c b/test/Feature/OverlappedError.c
index e6d36b75..e6595cd1 100644
--- a/test/Feature/OverlappedError.c
+++ b/test/Feature/OverlappedError.c
@@ -3,7 +3,7 @@
 // RUN: %klee --output-dir=%t.klee-out %t1.bc
 // RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 4
 // RUN: ls %t.klee-out/ | grep .ptr.err | wc -l | grep 2
-
+#include "klee/klee.h"
 #include <stdlib.h>
 
 int main() {
diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c
index 39337cf5..28a0eb20 100644
--- a/test/Feature/PreferCex.c
+++ b/test/Feature/PreferCex.c
@@ -2,10 +2,7 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
 // RUN: %ktest-tool %t.klee-out/test000001.ktest | FileCheck %s
-
-#include <assert.h>
-#include <stdlib.h>
-#include <stdio.h>
+#include "klee/klee.h"
 
 int main() {
   char buf[4];
diff --git a/test/Feature/RaiseAsm.c b/test/Feature/RaiseAsm.c
index 842d9f3d..865929ae 100644
--- a/test/Feature/RaiseAsm.c
+++ b/test/Feature/RaiseAsm.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 <assert.h>
 
 typedef unsigned short uint16;
diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c
index f77656f8..e2eb95af 100644
--- a/test/Feature/ReplayPath.c
+++ b/test/Feature/ReplayPath.c
@@ -6,9 +6,9 @@
 // RUN: rm -rf %t.klee-out-2
 // RUN: %klee --output-dir=%t.klee-out-2 --replay-path %t.klee-out/test000001.path %t2.bc > %t3.log
 // RUN: diff %t3.log %t3.good
-
-#include <unistd.h>
+#include "klee/klee.h"
 #include <stdio.h>
+#include <unistd.h>
 
 void cond_exit() {
 #ifdef COND_EXIT
diff --git a/test/Feature/Searchers.c b/test/Feature/Searchers.c
index cd806950..c5260f3d 100644
--- a/test/Feature/Searchers.c
+++ b/test/Feature/Searchers.c
@@ -30,7 +30,7 @@
 /* this test is basically just for coverage and doesn't really do any
    correctness check (aside from testing that the various combinations
    don't crash) */
-
+#include "klee/klee.h"
 #include <stdlib.h>
 
 int validate(char *buf, int N) {
diff --git a/test/Feature/SetForking.c b/test/Feature/SetForking.c
index b739910d..a2911743 100644
--- a/test/Feature/SetForking.c
+++ b/test/Feature/SetForking.c
@@ -5,7 +5,7 @@
 // RUN: grep "1 A" %t.uniq.log
 // RUN: grep "1 B" %t.uniq.log
 // RUN: grep "1 C" %t.uniq.log
-
+#include "klee/klee.h"
 #include <stdio.h>
 
 int main() {
diff --git a/test/Feature/SilentKleeAssume.c b/test/Feature/SilentKleeAssume.c
index 06872e9b..24138029 100644
--- a/test/Feature/SilentKleeAssume.c
+++ b/test/Feature/SilentKleeAssume.c
@@ -5,9 +5,9 @@
 // RUN: rm -rf %t.klee-out
 // RUN: not %klee --output-dir=%t.klee-out --exit-on-error %t.bc > %t.default-klee-assume.log 2>&1
 // RUN: FileCheck -input-file=%t.default-klee-assume.log -check-prefix=CHECK-DEFAULT-KLEE-ASSUME %s
-
-#include <stdio.h>
+#include "klee/klee.h"
 #include <assert.h>
+#include <stdio.h>
 
 int main() {
   int x = klee_int("x");
diff --git a/test/Feature/SolverTimeout.c b/test/Feature/SolverTimeout.c
index 98c9ecde..aee7f4da 100644
--- a/test/Feature/SolverTimeout.c
+++ b/test/Feature/SolverTimeout.c
@@ -3,7 +3,7 @@
 // RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t.bc
 //
 // Note: This test occasionally fails when using Z3 4.4.1
-
+#include "klee/klee.h"
 #include <stdio.h>
 
 int main() {
diff --git a/test/Feature/WriteCov.c b/test/Feature/WriteCov.c
index 304198c5..3fd0074c 100644
--- a/test/Feature/WriteCov.c
+++ b/test/Feature/WriteCov.c
@@ -7,7 +7,7 @@
 // RUN: grep %t.klee-out/test000001.cov:1 %t3.txt
 // RUN: grep %t.klee-out/test000002.cov:0 %t3.txt
 // RUN: grep %t.klee-out/test000002.cov:1 %t3.txt
-
+#include "klee/klee.h"
 #include <assert.h>
 #include <stdio.h>
 
diff --git a/test/Feature/consecutive_divide_by_zero.c b/test/Feature/consecutive_divide_by_zero.c
index 0915bbaa..7a0dc1d9 100644
--- a/test/Feature/consecutive_divide_by_zero.c
+++ b/test/Feature/consecutive_divide_by_zero.c
@@ -8,6 +8,8 @@
 *  only one test case is generated EVEN IF THERE ARE MULTIPLE 
 *  DISTINCT ERRORS!
 */
+
+#include "klee/klee.h"
 int main() {
   unsigned int a = 15;
   unsigned int b = 15;
diff --git a/test/Feature/const_array_opt1.c b/test/Feature/const_array_opt1.c
index 1ed3c3ee..f41bdf47 100644
--- a/test/Feature/const_array_opt1.c
+++ b/test/Feature/const_array_opt1.c
@@ -9,6 +9,7 @@
    this takes under 2 seconds w/ the optimization and almost 6 minutes
    w/o.  So we kill it in 10 sec and check if it has finished
    successfully. */
+#include "klee/klee.h"
 
 #include <unistd.h>
 #include <assert.h>
diff --git a/test/Feature/left-overshift-sym-conc.c b/test/Feature/left-overshift-sym-conc.c
index 0320334f..2aaaf6f1 100644
--- a/test/Feature/left-overshift-sym-conc.c
+++ b/test/Feature/left-overshift-sym-conc.c
@@ -3,8 +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 <stdio.h>
+#include "klee/klee.h"
 #include <assert.h>
+#include <stdio.h>
 
 typedef enum
 {
diff --git a/test/Feature/logical-right-overshift-sym-conc.c b/test/Feature/logical-right-overshift-sym-conc.c
index 06bae156..4c4b6f98 100644
--- a/test/Feature/logical-right-overshift-sym-conc.c
+++ b/test/Feature/logical-right-overshift-sym-conc.c
@@ -3,8 +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 <stdio.h>
+#include "klee/klee.h"
 #include <assert.h>
+#include <stdio.h>
 
 typedef enum
 {
diff --git a/test/Feature/srem.c b/test/Feature/srem.c
index 65b324d3..0b542b17 100644
--- a/test/Feature/srem.c
+++ b/test/Feature/srem.c
@@ -3,8 +3,7 @@
 // RUN: %klee --output-dir=%t.klee-out --klee-call-optimisation=false %t.bc 2>&1 | FileCheck %s
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --klee-call-optimisation=false --optimize %t.bc 2>&1 | FileCheck %s
-
-#include <stdio.h>
+#include "klee/klee.h"
 #include <assert.h>
 
 int main(int argc, char** argv)
diff --git a/test/Merging/merge_fail.c b/test/Merging/merge_fail.c
index 00ea21ef..41ced1aa 100644
--- a/test/Merging/merge_fail.c
+++ b/test/Merging/merge_fail.c
@@ -14,6 +14,7 @@
 // This test will not merge because we cannot merge states when they allocated memory.
 
 #include "klee/klee.h"
+#include <stdlib.h>
 
 int main(int argc, char **args) {
 
diff --git a/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c b/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c
index 09d60e79..1ccff177 100644
--- a/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c
+++ b/test/Replay/libkleeruntest/replay_cex_after_assumed_malloc.c
@@ -3,6 +3,7 @@
 // RUN: %klee --output-dir=%t.klee-out %t.ll
 // KLEE just must not fail
 #include "klee/klee.h"
+#include <stdlib.h>
 
 int main() {
   char i;
diff --git a/test/Runtime/POSIX/FDNumbers.c b/test/Runtime/POSIX/FDNumbers.c
index 42f0f5ae..4e0fa79a 100644
--- a/test/Runtime/POSIX/FDNumbers.c
+++ b/test/Runtime/POSIX/FDNumbers.c
@@ -1,10 +1,10 @@
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t2.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
-
 #include <assert.h>
-#include <fcntl.h>
 #include <errno.h>
+#include <fcntl.h>
+#include <unistd.h>
 
 int main(int argc, char **argv) {
   int fd = open("A", O_TRUNC);
diff --git a/test/Runtime/POSIX/Fcntl.c b/test/Runtime/POSIX/Fcntl.c
index 53246a15..737d5da5 100644
--- a/test/Runtime/POSIX/Fcntl.c
+++ b/test/Runtime/POSIX/Fcntl.c
@@ -1,7 +1,7 @@
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t2.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
-
+#include "klee/klee.h"
 #include <assert.h>
 #include <fcntl.h>
 
diff --git a/test/Runtime/POSIX/FreeArgv.c b/test/Runtime/POSIX/FreeArgv.c
index 93ed697e..cdc5487f 100644
--- a/test/Runtime/POSIX/FreeArgv.c
+++ b/test/Runtime/POSIX/FreeArgv.c
@@ -4,7 +4,8 @@
 // RUN: test -f %t.klee-out/test000001.free.err
 // RUN: test -f %t.klee-out/test000002.free.err
 // RUN: test -f %t.klee-out/test000003.free.err
-
+#include "klee/klee.h"
+#include <stdlib.h>
 int main(int argc, char **argv) {
   switch (klee_range(0, 3, "range")) {
   case 0:
diff --git a/test/Runtime/POSIX/Getenv.c b/test/Runtime/POSIX/Getenv.c
index 6dff3c24..d5db7c39 100644
--- a/test/Runtime/POSIX/Getenv.c
+++ b/test/Runtime/POSIX/Getenv.c
@@ -1,9 +1,10 @@
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t2.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --libc=klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
-
 #include <assert.h>
-
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
 int main(int argc, char **argv) {
   char *g = getenv("PWD");
   if (g) {
diff --git a/test/Runtime/POSIX/Openat.c b/test/Runtime/POSIX/Openat.c
index 2341527e..67ff78bd 100644
--- a/test/Runtime/POSIX/Openat.c
+++ b/test/Runtime/POSIX/Openat.c
@@ -2,9 +2,10 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
 // RUN: test -f %t.klee-out/test000001.ktest
-
+#include "klee/klee.h"
 #include <assert.h>
 #include <fcntl.h>
+#include <unistd.h>
 
 int main(int argc, char **argv) {
   int fd = openat(AT_FDCWD, "A", O_RDWR|O_TRUNC);
diff --git a/test/Runtime/POSIX/Replay.c b/test/Runtime/POSIX/Replay.c
index 61862c5f..fb1b400c 100644
--- a/test/Runtime/POSIX/Replay.c
+++ b/test/Runtime/POSIX/Replay.c
@@ -8,6 +8,7 @@
 // REPLAY: Yes
 
 #ifdef KLEE_EXECUTION
+#include "klee/klee.h"
 #define EXIT klee_silent_exit
 #else
 #include <stdlib.h>
diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c
index 6d84baff..84caab3a 100644
--- a/test/Runtime/POSIX/Stdin.c
+++ b/test/Runtime/POSIX/Stdin.c
@@ -9,11 +9,12 @@
 // RUN: grep "mode:lnk" %t.log
 // RUN: grep "read:sym:yes" %t.log
 // RUN: grep "read:sym:no" %t.log
-
-#include <stdio.h>
+#include <assert.h>
 #include <fcntl.h>
+#include <stdio.h>
+#include <string.h>
 #include <sys/stat.h>
-#include <assert.h>
+#include <unistd.h>
 
 int main(int argc, char **argv) {
   struct stat stats;
diff --git a/test/Runtime/POSIX/Write1.c b/test/Runtime/POSIX/Write1.c
index 5fc4ff8f..7f1e6f20 100644
--- a/test/Runtime/POSIX/Write1.c
+++ b/test/Runtime/POSIX/Write1.c
@@ -2,8 +2,10 @@
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --sym-stdout 2>%t.log
 
-#include <stdio.h>
+#include "klee/klee.h"
 #include <assert.h>
+#include <stdio.h>
+#include <string.h>
 
 int main(int argc, char** argv) {
   char buf[32];
diff --git a/test/Runtime/POSIX/Write2.c b/test/Runtime/POSIX/Write2.c
index 04698f21..e9eb6f6b 100644
--- a/test/Runtime/POSIX/Write2.c
+++ b/test/Runtime/POSIX/Write2.c
@@ -1,9 +1,9 @@
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-files 1 10 --sym-stdout 2>%t.log
-
-#include <stdio.h>
+#include "klee/klee.h"
 #include <assert.h>
+#include <stdio.h>
 
 int main(int argc, char** argv) {
   const char* msg = "This will eventually overflow stdout. ";
diff --git a/test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c b/test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c
index 3b66dd21..26bb1dce 100644
--- a/test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c
+++ b/test/Runtime/Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c
@@ -3,6 +3,7 @@
 // RUN: %klee --output-dir=%t.klee-out --exit-on-error --libc=uclibc %t1.bc
 
 // just make sure atexit works ok
+#include <stdlib.h>
 
 void boo() {
 }
diff --git a/test/VectorInstructions/insert_element.c b/test/VectorInstructions/insert_element.c
index df09819d..35054fd9 100644
--- a/test/VectorInstructions/insert_element.c
+++ b/test/VectorInstructions/insert_element.c
@@ -5,9 +5,10 @@
 // RUN: %klee --output-dir=%t.klee-out --optimize=false  %t1.bc > %t.stdout.log 2> %t.stderr.log
 // RUN: FileCheck -check-prefix=CHECK-STDOUT -input-file=%t.stdout.log %s
 // RUN: FileCheck -check-prefix=CHECK-STDERR -input-file=%t.stderr.log %s
+#include "klee/klee.h"
 #include <assert.h>
-#include <stdio.h>
 #include <stdint.h>
+#include <stdio.h>
 
 typedef uint32_t v4ui __attribute__ ((vector_size (16)));
 int main() {
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;