diff options
31 files changed, 75 insertions, 66 deletions
diff --git a/examples/get_sign/get_sign.c b/examples/get_sign/get_sign.c index fd2ad9f2..a379193d 100644 --- a/examples/get_sign/get_sign.c +++ b/examples/get_sign/get_sign.c @@ -2,7 +2,7 @@ * First KLEE tutorial: testing a small function */ -#include <klee/klee.h> +#include "klee/klee.h" int get_sign(int x) { if (x == 0) diff --git a/examples/regexp/Regexp.c b/examples/regexp/Regexp.c index a48ea928..18198590 100644 --- a/examples/regexp/Regexp.c +++ b/examples/regexp/Regexp.c @@ -7,7 +7,7 @@ * */ -#include <klee/klee.h> +#include "klee/klee.h" static int matchhere(char*,char*); diff --git a/examples/sort/sort.c b/examples/sort/sort.c index a72ccf1e..871feb3e 100644 --- a/examples/sort/sort.c +++ b/examples/sort/sort.c @@ -1,9 +1,9 @@ -#include <klee/klee.h> +#include "klee/klee.h" -#include <stdlib.h> +#include <assert.h> #include <stdio.h> +#include <stdlib.h> #include <string.h> -#include <assert.h> static void insert_ordered(int *array, unsigned nelem, int item) { unsigned i = 0; diff --git a/include/klee/Expr/ExprSMTLIBPrinter.h b/include/klee/Expr/ExprSMTLIBPrinter.h index b042bfeb..a7a604e1 100644 --- a/include/klee/Expr/ExprSMTLIBPrinter.h +++ b/include/klee/Expr/ExprSMTLIBPrinter.h @@ -11,10 +11,10 @@ #ifndef KLEE_EXPRSMTLIBPRINTER_H #define KLEE_EXPRSMTLIBPRINTER_H -#include <klee/Expr/Constraints.h> -#include <klee/Expr/Expr.h> -#include <klee/Solver.h> -#include <klee/util/PrintContext.h> +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Solver.h" +#include "klee/util/PrintContext.h" #include <map> #include <set> diff --git a/include/klee/Internal/Module/Cell.h b/include/klee/Internal/Module/Cell.h index abdce3f6..c7d9ae18 100644 --- a/include/klee/Internal/Module/Cell.h +++ b/include/klee/Internal/Module/Cell.h @@ -10,7 +10,7 @@ #ifndef KLEE_CELL_H #define KLEE_CELL_H -#include <klee/Expr/Expr.h> +#include "klee/Expr/Expr.h" namespace klee { class MemoryObject; diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index 732dc817..67a6e967 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -9,8 +9,8 @@ #include "PTree.h" -#include <klee/Expr/Expr.h> -#include <klee/Expr/ExprPPrinter.h> +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprPPrinter.h" #include <vector> diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index 3185203f..7618e86e 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -10,7 +10,7 @@ #ifndef KLEE_PTREE_H #define KLEE_PTREE_H -#include <klee/Expr/Expr.h> +#include "klee/Expr/Expr.h" namespace klee { class ExecutionState; diff --git a/runtime/Intrinsic/klee_div_zero_check.c b/runtime/Intrinsic/klee_div_zero_check.c index 3fde1af5..36cf8807 100644 --- a/runtime/Intrinsic/klee_div_zero_check.c +++ b/runtime/Intrinsic/klee_div_zero_check.c @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include <klee/klee.h> +#include "klee/klee.h" void klee_div_zero_check(long long z) { if (z == 0) diff --git a/runtime/Intrinsic/klee_overshift_check.c b/runtime/Intrinsic/klee_overshift_check.c index c0cb6102..0a910172 100644 --- a/runtime/Intrinsic/klee_overshift_check.c +++ b/runtime/Intrinsic/klee_overshift_check.c @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include <klee/klee.h> +#include "klee/klee.h" /* This instrumentation call is used to check for overshifting. * If we do try to do x << y or x >> y diff --git a/runtime/Intrinsic/klee_range.c b/runtime/Intrinsic/klee_range.c index 5da6a7a5..7b0b91b3 100644 --- a/runtime/Intrinsic/klee_range.c +++ b/runtime/Intrinsic/klee_range.c @@ -7,8 +7,9 @@ // //===----------------------------------------------------------------------===// +#include "klee/klee.h" + #include <assert.h> -#include <klee/klee.h> int klee_range(int start, int end, const char* name) { int x; diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c index 5a3faa16..a2cbe0ab 100644 --- a/runtime/POSIX/fd.c +++ b/runtime/POSIX/fd.c @@ -10,27 +10,28 @@ #define _LARGEFILE64_SOURCE #include "fd.h" -#include <string.h> +#include "klee/klee.h" + +#include <assert.h> +#include <errno.h> +#include <fcntl.h> +#include <stdarg.h> #include <stdio.h> #include <stdlib.h> -#include <errno.h> -#include <sys/syscall.h> +#include <string.h> #include <sys/stat.h> +#include <sys/syscall.h> #include <sys/types.h> -#include <fcntl.h> -#include <stdarg.h> -#include <assert.h> #ifndef __FreeBSD__ #include <sys/vfs.h> #endif -#include <unistd.h> #include <dirent.h> #include <sys/ioctl.h> #include <sys/mtio.h> -#include <termios.h> #include <sys/select.h> -#include <klee/klee.h> #include <sys/time.h> +#include <termios.h> +#include <unistd.h> /* Returns pointer to the symbolic file structure fs the pathname is symbolic */ static exe_disk_file_t *__get_sym_file(const char *pathname) { diff --git a/runtime/POSIX/fd_64.c b/runtime/POSIX/fd_64.c index 3bf48f5e..61d9dc6f 100644 --- a/runtime/POSIX/fd_64.c +++ b/runtime/POSIX/fd_64.c @@ -15,32 +15,32 @@ #endif #endif - -#include "klee/Config/Version.h" #define _LARGEFILE64_SOURCE #define _FILE_OFFSET_BITS 64 #include "fd.h" -#include <string.h> +#include "klee/Config/Version.h" +#include "klee/klee.h" + +#include <assert.h> +#include <errno.h> +#include <fcntl.h> +#include <stdarg.h> #include <stdio.h> #include <stdlib.h> -#include <errno.h> -#include <sys/syscall.h> +#include <string.h> #include <sys/stat.h> +#include <sys/syscall.h> #include <sys/types.h> -#include <fcntl.h> -#include <stdarg.h> -#include <assert.h> #ifndef __FreeBSD__ #include <sys/vfs.h> #endif -#include <unistd.h> #include <dirent.h> #include <sys/ioctl.h> #include <sys/mtio.h> -#include <termios.h> #include <sys/select.h> -#include <klee/klee.h> +#include <termios.h> +#include <unistd.h> /*** Forward to actual implementations ***/ diff --git a/runtime/POSIX/fd_init.c b/runtime/POSIX/fd_init.c index 327ddb53..8845fc9c 100644 --- a/runtime/POSIX/fd_init.c +++ b/runtime/POSIX/fd_init.c @@ -10,17 +10,17 @@ #define _LARGEFILE64_SOURCE #define _FILE_OFFSET_BITS 64 #include "fd.h" -#include <klee/klee.h> -#include <string.h> +#include "klee/klee.h" + +#include <assert.h> #include <stdio.h> #include <stdlib.h> -#include <assert.h> +#include <string.h> #include <sys/stat.h> #include <sys/syscall.h> #include <unistd.h> - exe_file_system_t __exe_fs; /* NOTE: It is important that these are statically initialized diff --git a/runtime/POSIX/illegal.c b/runtime/POSIX/illegal.c index 8b8c0134..8ded0987 100644 --- a/runtime/POSIX/illegal.c +++ b/runtime/POSIX/illegal.c @@ -7,14 +7,14 @@ // //===----------------------------------------------------------------------===// -#include <stdio.h> +#include "klee/klee.h" + #include <errno.h> -#include <unistd.h> -#include <signal.h> #include <setjmp.h> +#include <signal.h> +#include <stdio.h> #include <sys/types.h> - -#include <klee/klee.h> +#include <unistd.h> void klee_warning(const char*); void klee_warning_once(const char*); diff --git a/runtime/POSIX/misc.c b/runtime/POSIX/misc.c index 7335dee2..94c495f5 100644 --- a/runtime/POSIX/misc.c +++ b/runtime/POSIX/misc.c @@ -7,13 +7,14 @@ // //===----------------------------------------------------------------------===// +#include "klee/klee.h" + #include <assert.h> -#include <unistd.h> -#include <sys/syscall.h> #include <errno.h> #include <stdlib.h> -#include <klee/klee.h> #include <string.h> +#include <sys/syscall.h> +#include <unistd.h> #if 0 #define MAX_SYM_ENV_SIZE 32 diff --git a/test/Feature/ExitOnErrorType.c b/test/Feature/ExitOnErrorType.c index b1a55466..50696da6 100644 --- a/test/Feature/ExitOnErrorType.c +++ b/test/Feature/ExitOnErrorType.c @@ -2,8 +2,9 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out -exit-on-error-type Assert %t1.bc 2>&1 +#include "klee/klee.h" + #include <assert.h> -#include <klee/klee.h> int main() { assert(klee_int("assert")); diff --git a/test/Feature/RewriteEqualities.c b/test/Feature/RewriteEqualities.c index ee77f3e1..ed36ce74 100644 --- a/test/Feature/RewriteEqualities.c +++ b/test/Feature/RewriteEqualities.c @@ -7,8 +7,9 @@ // RUN: %klee --output-dir=%t.klee-out --search=dfs --write-kqueries --rewrite-equalities %t.bc // RUN: FileCheck -input-file=%t.klee-out/test000003.kquery %s +#include "klee/klee.h" + #include <stdio.h> -#include <klee/klee.h> int run(unsigned char * x, unsigned char * y) { y[6] = 15; diff --git a/test/Merging/batching_break.c b/test/Merging/batching_break.c index 4089c2f5..ac537654 100644 --- a/test/Merging/batching_break.c +++ b/test/Merging/batching_break.c @@ -6,7 +6,7 @@ // CHECK: close merge: // CHECK: KLEE: done: generated tests = 3{{$}} -#include <klee/klee.h> +#include "klee/klee.h" int main(int argc, char** args){ diff --git a/test/Merging/easy_merge.c b/test/Merging/easy_merge.c index ceee25a1..be77bcb9 100644 --- a/test/Merging/easy_merge.c +++ b/test/Merging/easy_merge.c @@ -15,7 +15,8 @@ // CHECK: close merge: // CHECK: close merge: // CHECK: generated tests = 2{{$}} -#include <klee/klee.h> + +#include "klee/klee.h" int main(int argc, char** args){ diff --git a/test/Merging/incomplete_merge.c b/test/Merging/incomplete_merge.c index 87ff37e4..783ab993 100644 --- a/test/Merging/incomplete_merge.c +++ b/test/Merging/incomplete_merge.c @@ -21,7 +21,7 @@ // It might occur that the random branch selection completes the heavy branch first, // which results in the branches being merged completely. -#include <klee/klee.h> +#include "klee/klee.h" int main(int argc, char **args) { diff --git a/test/Merging/indirect_value.c b/test/Merging/indirect_value.c index 040a4735..005ddcaf 100644 --- a/test/Merging/indirect_value.c +++ b/test/Merging/indirect_value.c @@ -3,10 +3,11 @@ // RUN: %klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=nurs:covnew --use-batching-search %t.bc 2>&1 | FileCheck %s // CHECK: generated tests = 2{{$}} -#include <stdlib.h> -#include <stdio.h> -#include <klee/klee.h> +#include "klee/klee.h" + +#include <stdio.h> +#include <stdlib.h> int main(int argc, char** argv) { diff --git a/test/Merging/loop_merge.c b/test/Merging/loop_merge.c index 79d9d70b..49dbbfb4 100644 --- a/test/Merging/loop_merge.c +++ b/test/Merging/loop_merge.c @@ -15,7 +15,7 @@ // CHECK: close merge: // CHECK: generated tests = 2{{$}} -#include <klee/klee.h> +#include "klee/klee.h" int main(int argc, char** args){ diff --git a/test/Merging/merge_fail.c b/test/Merging/merge_fail.c index 23ddb0d0..8cfd40f0 100644 --- a/test/Merging/merge_fail.c +++ b/test/Merging/merge_fail.c @@ -11,7 +11,7 @@ // This test will not merge because we cannot merge states when they allocated memory. -#include <klee/klee.h> +#include "klee/klee.h" int main(int argc, char **args) { diff --git a/test/Merging/nested_merge.c b/test/Merging/nested_merge.c index 97fca5d3..f5f571d4 100644 --- a/test/Merging/nested_merge.c +++ b/test/Merging/nested_merge.c @@ -17,7 +17,7 @@ // CHECK: close merge: // CHECK: generated tests = 1{{$}} -#include <klee/klee.h> +#include "klee/klee.h" int main(int argc, char **args) { diff --git a/test/Merging/split_merge.c b/test/Merging/split_merge.c index a138e69a..1f5ebd42 100644 --- a/test/Merging/split_merge.c +++ b/test/Merging/split_merge.c @@ -15,7 +15,7 @@ // CHECK: close merge: // CHECK: generated tests = 2{{$}} -#include <klee/klee.h> +#include "klee/klee.h" int main(int argc, char** args){ diff --git a/test/Merging/state_termination.c b/test/Merging/state_termination.c index 3fe18760..2bf60f91 100644 --- a/test/Merging/state_termination.c +++ b/test/Merging/state_termination.c @@ -2,7 +2,7 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --use-merge --debug-log-merge --search=dfs %t.bc -#include <klee/klee.h> +#include "klee/klee.h" int main(int argc, char** args){ diff --git a/test/Merging/unexpected_close.c b/test/Merging/unexpected_close.c index 59ea72dc..c6cf7398 100644 --- a/test/Merging/unexpected_close.c +++ b/test/Merging/unexpected_close.c @@ -5,7 +5,7 @@ // CHECK: ran into a close at // CHECK: generated tests = 2{{$}} -#include <klee/klee.h> +#include "klee/klee.h" int main(int argc, char **args) { diff --git a/test/regression/2014-09-13-debug-info.c b/test/regression/2014-09-13-debug-info.c index 39b276a3..5cad27f3 100644 --- a/test/regression/2014-09-13-debug-info.c +++ b/test/regression/2014-09-13-debug-info.c @@ -16,7 +16,7 @@ // CHECK: object 0: int : 32 // CHECK: object 0: int : 99 -#include <klee/klee.h> +#include "klee/klee.h" void f0(void) {} void f1(void) {} diff --git a/test/regression/2014-12-08-ashr.c b/test/regression/2014-12-08-ashr.c index ec7050d7..0d17f964 100644 --- a/test/regression/2014-12-08-ashr.c +++ b/test/regression/2014-12-08-ashr.c @@ -2,8 +2,9 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out -exit-on-error %t.bc +#include "klee/klee.h" + #include <assert.h> -#include <klee/klee.h> int f1(int a, int b) { return a + b; diff --git a/test/regression/2015-06-22-struct-write.c b/test/regression/2015-06-22-struct-write.c index 53b04274..67d17032 100644 --- a/test/regression/2015-06-22-struct-write.c +++ b/test/regression/2015-06-22-struct-write.c @@ -2,8 +2,9 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out -exit-on-error %t.bc +#include "klee/klee.h" + #include <assert.h> -#include <klee/klee.h> union U0 { signed f3 :18; diff --git a/test/regression/2016-08-06-klee-get-obj-size.c b/test/regression/2016-08-06-klee-get-obj-size.c index 0e25d1f6..70289e48 100644 --- a/test/regression/2016-08-06-klee-get-obj-size.c +++ b/test/regression/2016-08-06-klee-get-obj-size.c @@ -3,8 +3,8 @@ // RUN: %klee --output-dir=%t.klee-out %t.bc // RUN: test -f %t.klee-out/test000001.assert.err +#include "klee/klee.h" -#include <klee/klee.h> #include <assert.h> int main() { |