Sign Up
Log In
Log In
or
Sign Up
Places
All Projects
Status Monitor
Collapse sidebar
home:aaronpuchert:Backports:SLE-15
klee
0008-Assume-C-compiler-s-default-standard-is-st...
Overview
Repositories
Revisions
Requests
Users
Attributes
Meta
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
Locations
Projects
Search
Status Monitor
Help
OpenBuildService.org
Documentation
API Documentation
Code of Conduct
Contact
Support
@OBShq
Terms
openSUSE Build Service is sponsored by
The Open Build Service is an
openSUSE project
.
Sign Up
Log In
Places
Places
All Projects
Status Monitor
