From 5732990c805948249bdc3d43a52cfe050ad66a95 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Tue, 30 Jul 2019 12:34:27 +0100 Subject: Use #include "klee/..." (instead of #include ) consistently. --- examples/get_sign/get_sign.c | 2 +- examples/regexp/Regexp.c | 2 +- examples/sort/sort.c | 6 +++--- include/klee/Expr/ExprSMTLIBPrinter.h | 8 ++++---- include/klee/Internal/Module/Cell.h | 2 +- lib/Core/PTree.cpp | 4 ++-- lib/Core/PTree.h | 2 +- runtime/Intrinsic/klee_div_zero_check.c | 2 +- runtime/Intrinsic/klee_overshift_check.c | 2 +- runtime/Intrinsic/klee_range.c | 3 ++- runtime/POSIX/fd.c | 19 ++++++++++--------- runtime/POSIX/fd_64.c | 22 +++++++++++----------- runtime/POSIX/fd_init.c | 8 ++++---- runtime/POSIX/illegal.c | 10 +++++----- runtime/POSIX/misc.c | 7 ++++--- test/Feature/ExitOnErrorType.c | 3 ++- test/Feature/RewriteEqualities.c | 3 ++- test/Merging/batching_break.c | 2 +- test/Merging/easy_merge.c | 3 ++- test/Merging/incomplete_merge.c | 2 +- test/Merging/indirect_value.c | 7 ++++--- test/Merging/loop_merge.c | 2 +- test/Merging/merge_fail.c | 2 +- test/Merging/nested_merge.c | 2 +- test/Merging/split_merge.c | 2 +- test/Merging/state_termination.c | 2 +- test/Merging/unexpected_close.c | 2 +- test/regression/2014-09-13-debug-info.c | 2 +- test/regression/2014-12-08-ashr.c | 3 ++- test/regression/2015-06-22-struct-write.c | 3 ++- test/regression/2016-08-06-klee-get-obj-size.c | 2 +- 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 +#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 +#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 +#include "klee/klee.h" -#include +#include #include +#include #include -#include 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 -#include -#include -#include +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Solver.h" +#include "klee/util/PrintContext.h" #include #include 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 +#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 -#include +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprPPrinter.h" #include 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 +#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 +#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 +#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 -#include 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 +#include "klee/klee.h" + +#include +#include +#include +#include #include #include -#include -#include +#include #include +#include #include -#include -#include -#include #ifndef __FreeBSD__ #include #endif -#include #include #include #include -#include #include -#include #include +#include +#include /* 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 +#include "klee/Config/Version.h" +#include "klee/klee.h" + +#include +#include +#include +#include #include #include -#include -#include +#include #include +#include #include -#include -#include -#include #ifndef __FreeBSD__ #include #endif -#include #include #include #include -#include #include -#include +#include +#include /*** 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 -#include +#include "klee/klee.h" + +#include #include #include -#include +#include #include #include #include - 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 +#include "klee/klee.h" + #include -#include -#include #include +#include +#include #include - -#include +#include 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 -#include -#include #include #include -#include #include +#include +#include #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 -#include 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 -#include 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 +#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 + +#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 +#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 -#include -#include +#include "klee/klee.h" + +#include +#include 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 +#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 +#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 +#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 +#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 +#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 +#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 +#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 -#include 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 -#include 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 #include int main() { -- cgit 1.4.1