File 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch of Package klee
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Mon, 30 Oct 2023 11:59:29 +0000
Subject: Assume C compiler's default standard is `-std=gnu17`
Patch-mainline: no
References: llvm16
Newer compilers use `-std=gnu17` as the default when compiling C code.
Fix all the test cases that violate this behaviour or explicitly request
older standards `-std=c89` where necessary.
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
---
test/ArrayOpt/test_feasible.c | 3 ++-
test/DeterministicAllocation/OneOutOfBounds.c | 2 +-
test/Expr/ReadExprConsistency.c | 10 +++++-----
test/Feature/BFSSearcherAndDFSSearcherInterleaved.c | 2 +-
test/Feature/ByteSwap.c | 2 +-
test/Feature/CheckMemoryAccess.c | 4 ++--
test/Feature/CompressedExprLogging.c | 2 +-
test/Feature/CopyOnWrite.c | 2 +-
test/Feature/DanglingConcreteReadExpr.c | 2 +-
test/Feature/DefineFixedObject.c | 2 +-
test/Feature/Envp.c | 3 ++-
test/Feature/GetValue.c | 4 ++--
test/Feature/InAndOutOfBounds.c | 2 ++
test/Feature/IndirectCallToExternal.c | 2 +-
test/Feature/InlineAsm.c | 2 +-
test/Feature/IsSymbolic.c | 2 +-
test/Feature/KleeReportError.c | 1 +
test/Feature/LowerSwitch.c | 2 +-
test/Feature/MakeSymbolicAPI.c | 3 +--
test/Feature/MakeSymbolicName.c | 2 +-
test/Feature/Memalign.c | 4 ++--
test/Feature/MultiMkSym.c | 2 +-
test/Feature/MultipleReadResolution.c | 3 ++-
test/Feature/MultipleReallocResolution.c | 4 ++--
test/Feature/MultipleWriteResolution.c | 4 ++--
test/Feature/NamedSeedMatching.c | 4 ++--
test/Feature/NoExternalCallsAllowed.c | 2 +-
test/Feature/OneOutOfBounds.c | 1 +
test/Feature/Optimize.c | 1 +
test/Feature/OverlappedError.c | 2 +-
test/Feature/PreferCex.c | 5 +----
test/Feature/RaiseAsm.c | 2 +-
test/Feature/ReplayPath.c | 4 ++--
test/Feature/Searchers.c | 2 +-
test/Feature/SetForking.c | 2 +-
test/Feature/SilentKleeAssume.c | 4 ++--
test/Feature/SolverTimeout.c | 2 +-
test/Feature/WriteCov.c | 2 +-
test/Feature/consecutive_divide_by_zero.c | 2 ++
test/Feature/const_array_opt1.c | 1 +
test/Feature/left-overshift-sym-conc.c | 3 ++-
test/Feature/logical-right-overshift-sym-conc.c | 3 ++-
test/Feature/srem.c | 3 +--
test/Merging/merge_fail.c | 1 +
.../libkleeruntest/replay_cex_after_assumed_malloc.c | 1 +
test/Runtime/POSIX/FDNumbers.c | 4 ++--
test/Runtime/POSIX/Fcntl.c | 2 +-
test/Runtime/POSIX/FreeArgv.c | 3 ++-
test/Runtime/POSIX/Getenv.c | 5 +++--
test/Runtime/POSIX/Openat.c | 3 ++-
test/Runtime/POSIX/Replay.c | 1 +
test/Runtime/POSIX/Stdin.c | 7 ++++---
test/Runtime/POSIX/Write1.c | 4 +++-
test/Runtime/POSIX/Write2.c | 4 ++--
.../Uclibc/2008-03-04-libc-atexit-uses-dso-handle.c | 1 +
test/VectorInstructions/insert_element.c | 3 ++-
...07-07-25-invalid-stp-array-binding-to-objectstate.c | 1 +
test/regression/2007-07-30-unflushed-byte.c | 2 +-
.../2007-08-01-cache-unclear-on-overwrite-flushed.c | 1 +
test/regression/2007-08-06-64bit-shift.c | 1 +
test/regression/2007-08-06-access-after-free.c | 2 ++
test/regression/2007-08-16-invalid-constant-value.c | 4 +---
.../2007-08-16-valid-write-to-freed-object.c | 2 ++
test/regression/2007-10-11-free-of-alloca.c | 2 +-
.../2007-10-12-failed-make-symbolic-after-copy.c | 2 +-
test/regression/2008-03-04-free-of-global.c | 3 ++-
test/regression/2008-03-11-free-of-malloc-zero.c | 2 +-
test/regression/2008-04-10-bad-alloca-free.c | 1 +
test/regression/2014-07-04-unflushed-error-report.c | 1 +
test/regression/2015-08-05-invalid-fork.c | 1 +
test/regression/2015-08-30-empty-constraints.c | 1 +
test/regression/2015-08-30-sdiv-1.c | 1 +
test/regression/2017-02-21-pathOS-id.c | 3 +++
test/regression/2017-11-01-test-with-empty-varname.c | 2 +-
test/regression/2020-04-27-stp-array-names.c | 2 +-
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;
--
2.43.0
