diff options
Diffstat (limited to 'test/Feature')
40 files changed, 54 insertions, 47 deletions
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) |