diff --git a/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c b/regression/goto-analyzer/constant_propagation_01/main.c similarity index 84% rename from regression/goto-analyzer/constant_propagation_01/constant_propagation1.c rename to regression/goto-analyzer/constant_propagation_01/main.c index 801a21535a9..6689d8d4562 100644 --- a/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c +++ b/regression/goto-analyzer/constant_propagation_01/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index 1eb849c3c7a..a4a79f28ab1 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -1,9 +1,9 @@ -FUTURE -constant_propagation1.c ---constants --simplify out.goto +CORE +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$ -^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c b/regression/goto-analyzer/constant_propagation_02/main.c similarity index 81% rename from regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c rename to regression/goto-analyzer/constant_propagation_02/main.c index ff139437bd8..db0c8dc3f3e 100644 --- a/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c +++ b/regression/goto-analyzer/constant_propagation_02/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_02/original b/regression/goto-analyzer/constant_propagation_02/original deleted file mode 100644 index 13a9e245c81..00000000000 --- a/regression/goto-analyzer/constant_propagation_02/original +++ /dev/null @@ -1,3 +0,0 @@ -Task defaults to --show -Domain defaults to --constants -GOTO-ANALYSER version 5.5 64-bit x86_64 linux diff --git a/regression/goto-analyzer/constant_propagation_02/simplified b/regression/goto-analyzer/constant_propagation_02/simplified deleted file mode 100644 index 6c722a607de..00000000000 --- a/regression/goto-analyzer/constant_propagation_02/simplified +++ /dev/null @@ -1,81 +0,0 @@ -Reading GOTO program from `out.goto' -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -main /* main */ - // 0 file constant_propagation_02.c line 5 function main - signed int i; - // 1 file constant_propagation_02.c line 5 function main - i = 0; - // 2 file constant_propagation_02.c line 5 function main - signed int j; - // 3 file constant_propagation_02.c line 5 function main - j = 2; - // 4 file constant_propagation_02.c line 7 function main - IF FALSE THEN GOTO 1 - // 5 file constant_propagation_02.c line 9 function main - 0 = 1; - // 6 file constant_propagation_02.c line 10 function main - 2 = 3; - // 7 no location - 1: SKIP - // 8 file constant_propagation_02.c line 12 function main - ASSERT FALSE // assertion j!=3 - // 9 file constant_propagation_02.c line 12 function main - GOTO 2 - // 10 file constant_propagation_02.c line 12 function main - (void)0; - // 11 no location - 2: SKIP - // 12 file constant_propagation_02.c line 13 function main - dead j; - // 13 file constant_propagation_02.c line 13 function main - dead i; - // 14 file constant_propagation_02.c line 13 function main - main#return_value = NONDET(signed int); - // 15 file constant_propagation_02.c line 13 function main - END_FUNCTION -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -_start /* _start */ - // 16 no location - __CPROVER_initialize(); - // 17 file constant_propagation_02.c line 3 - main(); - // 18 file constant_propagation_02.c line 3 - return' = main#return_value; - // 19 file constant_propagation_02.c line 3 - dead main#return_value; - // 20 file constant_propagation_02.c line 3 - OUTPUT("return", return'); - // 21 no location - END_FUNCTION -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -__CPROVER_initialize /* __CPROVER_initialize */ - // 22 no location - // Labels: __CPROVER_HIDE - SKIP - // 23 file line 39 - __CPROVER_dead_object = NULL; - // 24 file line 38 - __CPROVER_deallocated = NULL; - // 25 file line 42 - __CPROVER_malloc_is_new_array = FALSE; - // 26 file line 40 - __CPROVER_malloc_object = NULL; - // 27 file line 41 - __CPROVER_malloc_size = 0ul; - // 28 file line 43 - __CPROVER_memory_leak = NULL; - // 29 file line 31 - __CPROVER_next_thread_id = 0ul; - // 30 file line 85 - __CPROVER_pipe_count = 0u; - // 31 file line 65 - __CPROVER_rounding_mode = 0; - // 32 file line 29 - __CPROVER_thread_id = 0ul; - // 33 file line 30 - __CPROVER_threads_exited = ARRAY_OF(FALSE); - // 34 no location - END_FUNCTION diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index 20cc5fcf86e..6a28820a4b0 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -1,9 +1,9 @@ -FUTURE -constant_propagation_02.c ---constants --simplify out.goto +CORE +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ -^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c b/regression/goto-analyzer/constant_propagation_03/main.c similarity index 81% rename from regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c rename to regression/goto-analyzer/constant_propagation_03/main.c index f08f6020d82..09a5434dead 100644 --- a/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c +++ b/regression/goto-analyzer/constant_propagation_03/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index 2225c1a666e..ffe6d41d638 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_03.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ -^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c b/regression/goto-analyzer/constant_propagation_04/main.c similarity index 81% rename from regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c rename to regression/goto-analyzer/constant_propagation_04/main.c index ca003ccd2b8..2c6c3f39db1 100644 --- a/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c +++ b/regression/goto-analyzer/constant_propagation_04/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index 2510b3f8a5e..ffe6d41d638 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_04.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ -^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c b/regression/goto-analyzer/constant_propagation_05/main.c similarity index 81% rename from regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c rename to regression/goto-analyzer/constant_propagation_05/main.c index 037fbbe0632..b740fc135c0 100644 --- a/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c +++ b/regression/goto-analyzer/constant_propagation_05/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc index ddb22cc3616..e84fdb08b4f 100644 --- a/regression/goto-analyzer/constant_propagation_05/test.desc +++ b/regression/goto-analyzer/constant_propagation_05/test.desc @@ -1,8 +1,8 @@ FUTURE -constant_propagation_05.c +main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE (if reachable)$ +^\[main.assertion.1\] file main.c line 12 function main, assertion j!=3: Failure (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_06/main.c b/regression/goto-analyzer/constant_propagation_06/main.c new file mode 100644 index 00000000000..6290aa89e6b --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_06/main.c @@ -0,0 +1,13 @@ + +int main() +{ + int i=0, j=2; + + while (i<50) + { + i++; + j++; + } + assert(i<51); +} + diff --git a/regression/goto-analyzer/constant_propagation_06/test.desc b/regression/goto-analyzer/constant_propagation_06/test.desc index 2c2596fe092..77a7349569f 100644 --- a/regression/goto-analyzer/constant_propagation_06/test.desc +++ b/regression/goto-analyzer/constant_propagation_06/test.desc @@ -1,15 +1,8 @@ -FUTURE -constant_propagation_06.c ---intervals --verify +CORE +main.c +--constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=10: SUCCESS$ -^\[main.assertion.2\] file constant_propagation_06.c line 11 function main, assertion i!=30: SUCCESS$ -^\[main.assertion.3\] file constant_propagation_06.c line 14 function main, assertion i!=15: UNKNOWN$ -^\[main.assertion.4\] file constant_propagation_06.c line 17 function main, assertion 0: SUCCESS$ -^\[main.assertion.5\] file constant_propagation_06.c line 20 function main, assertion j>=10: SUCCESS$ -^\[main.assertion.6\] file constant_propagation_06.c line 23 function main, assertion i>=j: UNKNOWN$ -^\[main.assertion.7\] file constant_propagation_06.c line 26 function main, assertion i>=11: SUCCESS$ -^\[main.assertion.8\] file constant_propagation_06.c line 29 function main, assertion j<100: SUCCESS$ +^\[main.assertion.1\] file main.c line 11 function main, assertion i\s*<\s*51: Unknown$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c b/regression/goto-analyzer/constant_propagation_07/main.c similarity index 93% rename from regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c rename to regression/goto-analyzer/constant_propagation_07/main.c index f0dea39a424..1fb6fee8e15 100644 --- a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c +++ b/regression/goto-analyzer/constant_propagation_07/main.c @@ -1,4 +1,4 @@ -#include + int main() { signed int i; diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 615893d4f78..c4b03cd8738 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -1,8 +1,9 @@ FUTURE -constant_propagation_07.c ---constants --verify +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$ +^Simplified: assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c b/regression/goto-analyzer/constant_propagation_08/main.c similarity index 87% rename from regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c rename to regression/goto-analyzer/constant_propagation_08/main.c index 3022a4f0f19..295e23c636d 100644 --- a/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c +++ b/regression/goto-analyzer/constant_propagation_08/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]; diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc index 994c2c532df..07a97596c15 100644 --- a/regression/goto-analyzer/constant_propagation_08/test.desc +++ b/regression/goto-analyzer/constant_propagation_08/test.desc @@ -1,10 +1,9 @@ FUTURE -constant_propagation_08.c ---intervals --verify +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$ -^\[main.assertion.2\] file constant_propagation_08.c line 13 function main, assertion i<51: UNKNOWN$ -^\[main.assertion.3\] file constant_propagation_08.c line 14 function main, assertion i<52: SUCCESS$ +^Simplified: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c b/regression/goto-analyzer/constant_propagation_09/main.c similarity index 82% rename from regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c rename to regression/goto-analyzer/constant_propagation_09/main.c index 55ea9ac7fc2..9bd38159f67 100644 --- a/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c +++ b/regression/goto-analyzer/constant_propagation_09/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc index 6a1b75f0c1b..eebfe27dd49 100644 --- a/regression/goto-analyzer/constant_propagation_09/test.desc +++ b/regression/goto-analyzer/constant_propagation_09/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_09.c ---intervals --verify +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -******** Function main -^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c b/regression/goto-analyzer/constant_propagation_10/main.c similarity index 84% rename from regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c rename to regression/goto-analyzer/constant_propagation_10/main.c index ac5933e9177..217faa4c9a7 100644 --- a/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c +++ b/regression/goto-analyzer/constant_propagation_10/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc index 52d98cb611b..527325b84bb 100644 --- a/regression/goto-analyzer/constant_propagation_10/test.desc +++ b/regression/goto-analyzer/constant_propagation_10/test.desc @@ -1,9 +1,8 @@ FUTURE -constant_propagation_10.c ---constants --simplify out.goto +main.c +--constants --verify ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$ -^UNMODIFIED: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ +^\[main.assertion.1\] file main.c line 10 function main, assertion a\[0\]==2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c b/regression/goto-analyzer/constant_propagation_11/main.c similarity index 84% rename from regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c rename to regression/goto-analyzer/constant_propagation_11/main.c index 124d1e30a20..cefa0c479ab 100644 --- a/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c +++ b/regression/goto-analyzer/constant_propagation_11/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index 7c849326cf6..4e9c8715429 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_11.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$ -^UNMODIFIED: assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c b/regression/goto-analyzer/constant_propagation_12/main.c similarity index 80% rename from regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c rename to regression/goto-analyzer/constant_propagation_12/main.c index 9a7e7692d62..a8379b64712 100644 --- a/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c +++ b/regression/goto-analyzer/constant_propagation_12/main.c @@ -1,4 +1,4 @@ -#include + int main() { int i=0, y; diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index ca5803363ad..208b235ccd5 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_12.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$ -^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c b/regression/goto-analyzer/constant_propagation_13/main.c similarity index 80% rename from regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c rename to regression/goto-analyzer/constant_propagation_13/main.c index 102cfd7f812..a4307c4d431 100644 --- a/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c +++ b/regression/goto-analyzer/constant_propagation_13/main.c @@ -1,4 +1,4 @@ -#include + int main() { int i=0, y; diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc index 22f10d125e3..2d2e078a424 100644 --- a/regression/goto-analyzer/constant_propagation_13/test.desc +++ b/regression/goto-analyzer/constant_propagation_13/test.desc @@ -1,8 +1,8 @@ FUTURE -constant_propagation_13.c +main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_13.c line 10 function main, assertion a\[0\]==2: FAILURE$ +^\[main.assertion.1\] file main.c line 9 function main, assertion y==0: Failure (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c b/regression/goto-analyzer/constant_propagation_14/main.c similarity index 88% rename from regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c rename to regression/goto-analyzer/constant_propagation_14/main.c index 8b426fe84b5..7a659b87c60 100644 --- a/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c +++ b/regression/goto-analyzer/constant_propagation_14/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc index a39a1f66cda..fc3be910670 100644 --- a/regression/goto-analyzer/constant_propagation_14/test.desc +++ b/regression/goto-analyzer/constant_propagation_14/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_14.c ---constants --simplify out.goto +main.c +--constants --verify ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 0$ -^UNKNOWN: assert: 0, assume: 0, goto: 0$ +^\[main.assertion.1\] file main.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: Success$ +^\[main.assertion.2\] file main.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c b/regression/goto-analyzer/constant_propagation_15/main.c similarity index 82% rename from regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c rename to regression/goto-analyzer/constant_propagation_15/main.c index 6639f9b5c81..e3dd672831d 100644 --- a/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c +++ b/regression/goto-analyzer/constant_propagation_15/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc index 20d36183eb0..aba11ba0c06 100644 --- a/regression/goto-analyzer/constant_propagation_15/test.desc +++ b/regression/goto-analyzer/constant_propagation_15/test.desc @@ -1,9 +1,8 @@ FUTURE -constant_propagation_15.c ---constants --simplify out.goto +main.c +--constants --verify ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$ -^UNMODIFIED: assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$ +^\[main.assertion.1\] file main.c line 9 function main, assertion a\[0\]==2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_16/main.c b/regression/goto-analyzer/constant_propagation_16/main.c new file mode 100644 index 00000000000..22fbac6a427 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_16/main.c @@ -0,0 +1,13 @@ + +void func() +{ + while(1) {} +} + +int main() +{ + func(); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_16/test.desc b/regression/goto-analyzer/constant_propagation_16/test.desc index b56c871deb4..ef4ab9321a2 100644 --- a/regression/goto-analyzer/constant_propagation_16/test.desc +++ b/regression/goto-analyzer/constant_propagation_16/test.desc @@ -1,8 +1,7 @@ -FUTURE -constant_propagation_16.c ---constants --verify +CORE +main.c +--show --constants ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_16.c line 9 function main, assertion y==0: FAILURE (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c b/regression/goto-analyzer/constant_propagation_17/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c rename to regression/goto-analyzer/constant_propagation_17/main.c diff --git a/regression/goto-analyzer/constant_propagation_17/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc index acecb91eb0a..76dc0fca897 100644 --- a/regression/goto-analyzer/constant_propagation_17/test.desc +++ b/regression/goto-analyzer/constant_propagation_17/test.desc @@ -1,9 +1,8 @@ -FUTURE -constant_propagation_17.c +CORE +main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_17.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: SUCCESS$ -^\[main.assertion.2\] file constant_propagation_17.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: FAILURE$ +^\[main.assertion.1\] file main.c line 12 function main, assertion i\s*<\s*51: (Unknown|Failure \(if reachable\))$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_18/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc deleted file mode 100644 index 7ea74c4d264..00000000000 --- a/regression/goto-analyzer/constant_propagation_18/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -constant_propagation_18.c ---constants --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_18.c line 9 function main, assertion a\[0\]==2: FAILURE$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals1/test.desc b/regression/goto-analyzer/intervals1/test.desc deleted file mode 100644 index 5a9802eeb20..00000000000 --- a/regression/goto-analyzer/intervals1/test.desc +++ /dev/null @@ -1,15 +0,0 @@ -KNOWNBUG -intervals1.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals1.c line 8 function main, assertion i>=10: SUCCESS$ -^\[main.assertion.2\] file intervals1.c line 11 function main, assertion i!=30: SUCCESS$ -^\[main.assertion.3\] file intervals1.c line 14 function main, assertion i!=15: UNKNOWN$ -^\[main.assertion.4\] file intervals1.c line 17 function main, assertion 0: SUCCESS$ -^\[main.assertion.5\] file intervals1.c line 20 function main, assertion j>=10: SUCCESS$ -^\[main.assertion.6\] file intervals1.c line 23 function main, assertion i>=j: UNKNOWN$ -^\[main.assertion.7\] file intervals1.c line 26 function main, assertion i>=11: SUCCESS$ -^\[main.assertion.8\] file intervals1.c line 29 function main, assertion j<100: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals10/test.desc b/regression/goto-analyzer/intervals10/test.desc deleted file mode 100644 index 794198505f1..00000000000 --- a/regression/goto-analyzer/intervals10/test.desc +++ /dev/null @@ -1,12 +0,0 @@ -FUTURE -intervals10.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals10.c line 8 function main, assertion j<=100: SUCCESS$ -^\[main.assertion.2\] file intervals10.c line 11 function main, assertion j<101: SUCCESS$ -^\[main.assertion.3\] file intervals10.c line 14 function main, assertion j>100: FAILURE (if reachable)$ -^\[main.assertion.4\] file intervals10.c line 17 function main, assertion j<99: UNKNOWN$ -^\[main.assertion.5\] file intervals10.c line 20 function main, assertion j==100: FAILURE (if reachable)$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals11/test.desc b/regression/goto-analyzer/intervals11/test.desc deleted file mode 100644 index 039cbffbeb0..00000000000 --- a/regression/goto-analyzer/intervals11/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -FUTURE -intervals11.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals11.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$ -^\[main.assertion.2\] file intervals11.c line 35 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals12/test.desc b/regression/goto-analyzer/intervals12/test.desc deleted file mode 100644 index 59a724c28b5..00000000000 --- a/regression/goto-analyzer/intervals12/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -FUTURE -intervals12.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^[main.assertion.1] file intervals12.c line 8 function main, assertion j < 0: SUCCESS$ -^[main.assertion.2] file intervals12.c line 11 function main, assertion j < 0: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals2/test.desc b/regression/goto-analyzer/intervals2/test.desc deleted file mode 100644 index 65aae030db1..00000000000 --- a/regression/goto-analyzer/intervals2/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals2.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals2.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals3/test.desc b/regression/goto-analyzer/intervals3/test.desc deleted file mode 100644 index 69ded2182ee..00000000000 --- a/regression/goto-analyzer/intervals3/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals3.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals3.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals4/test.desc b/regression/goto-analyzer/intervals4/test.desc deleted file mode 100644 index 2b725180e3f..00000000000 --- a/regression/goto-analyzer/intervals4/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals4.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals4.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals5/test.desc b/regression/goto-analyzer/intervals5/test.desc deleted file mode 100644 index eb64fbc13d1..00000000000 --- a/regression/goto-analyzer/intervals5/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals5.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals5.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals6/test.desc b/regression/goto-analyzer/intervals6/test.desc deleted file mode 100644 index 6e36b7948d2..00000000000 --- a/regression/goto-analyzer/intervals6/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -intervals6.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: FAILURE (if reachable)$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals7/test.desc b/regression/goto-analyzer/intervals7/test.desc deleted file mode 100644 index 6a42b4a30ec..00000000000 --- a/regression/goto-analyzer/intervals7/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -intervals7.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: FAILURE (if reachable)$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals8/test.desc b/regression/goto-analyzer/intervals8/test.desc deleted file mode 100644 index 7500059a717..00000000000 --- a/regression/goto-analyzer/intervals8/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -intervals8.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals8.c line 6 function main, assertion x < -10 && x < 100: FAILURE (if reachable)$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals9/test.desc b/regression/goto-analyzer/intervals9/test.desc deleted file mode 100644 index 37c33b97288..00000000000 --- a/regression/goto-analyzer/intervals9/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals9.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals9.c line 9 function main, assertion i>=1 && i<=2: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals1/intervals1.c b/regression/goto-analyzer/intervals_01/main.c similarity index 93% rename from regression/goto-analyzer/intervals1/intervals1.c rename to regression/goto-analyzer/intervals_01/main.c index cdec490fe6d..aeb37b99e07 100644 --- a/regression/goto-analyzer/intervals1/intervals1.c +++ b/regression/goto-analyzer/intervals_01/main.c @@ -1,9 +1,8 @@ -#include int main() { int i, j=20; - + if(i>=20) assert(i>=10); diff --git a/regression/goto-analyzer/intervals_01/test.desc b/regression/goto-analyzer/intervals_01/test.desc new file mode 100644 index 00000000000..af3180985b5 --- /dev/null +++ b/regression/goto-analyzer/intervals_01/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: Success$ +^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: Success$ +^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: Unknown$ +^\[main.assertion.4\] file main.c line 16 function main, assertion 0: Success$ +^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: Success$ +^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: Unknown$ +^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: Success$ +^\[main.assertion.8]\ file main.c line 28 function main, assertion j\s*<\s*100: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals2/intervals2.c b/regression/goto-analyzer/intervals_02/main.c similarity index 67% rename from regression/goto-analyzer/intervals2/intervals2.c rename to regression/goto-analyzer/intervals_02/main.c index d542854bb6a..00659353325 100644 --- a/regression/goto-analyzer/intervals2/intervals2.c +++ b/regression/goto-analyzer/intervals_02/main.c @@ -1,11 +1,8 @@ -#include int main(){ int x; if (x > 0 && x < 20) { - //if (x < 20) { assert(x > -10 && x < 100); - //} } return 0; } diff --git a/regression/goto-analyzer/intervals_02/test.desc b/regression/goto-analyzer/intervals_02/test.desc new file mode 100644 index 00000000000..fa4f926287f --- /dev/null +++ b/regression/goto-analyzer/intervals_02/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 && x < 100: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals3/intervals3.c b/regression/goto-analyzer/intervals_03/main.c similarity index 84% rename from regression/goto-analyzer/intervals3/intervals3.c rename to regression/goto-analyzer/intervals_03/main.c index bbaa3ce4e1e..de8c1eead32 100644 --- a/regression/goto-analyzer/intervals3/intervals3.c +++ b/regression/goto-analyzer/intervals_03/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_03/test.desc b/regression/goto-analyzer/intervals_03/test.desc new file mode 100644 index 00000000000..79042c334de --- /dev/null +++ b/regression/goto-analyzer/intervals_03/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 || x < 100: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals4/intervals4.c b/regression/goto-analyzer/intervals_04/main.c similarity index 80% rename from regression/goto-analyzer/intervals4/intervals4.c rename to regression/goto-analyzer/intervals_04/main.c index 790a5f1379f..1ca11e32143 100644 --- a/regression/goto-analyzer/intervals4/intervals4.c +++ b/regression/goto-analyzer/intervals_04/main.c @@ -1,4 +1,3 @@ -//#include int main() { diff --git a/regression/goto-analyzer/intervals_04/test.desc b/regression/goto-analyzer/intervals_04/test.desc new file mode 100644 index 00000000000..5bb03255f37 --- /dev/null +++ b/regression/goto-analyzer/intervals_04/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 && i <= 2: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals5/intervals5.c b/regression/goto-analyzer/intervals_05/main.c similarity index 80% rename from regression/goto-analyzer/intervals5/intervals5.c rename to regression/goto-analyzer/intervals_05/main.c index ed19ba71590..2cd79130dc9 100644 --- a/regression/goto-analyzer/intervals5/intervals5.c +++ b/regression/goto-analyzer/intervals_05/main.c @@ -1,4 +1,3 @@ -//#include int main() { diff --git a/regression/goto-analyzer/intervals_05/test.desc b/regression/goto-analyzer/intervals_05/test.desc new file mode 100644 index 00000000000..5c9af29a2b1 --- /dev/null +++ b/regression/goto-analyzer/intervals_05/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 || i <= 2: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals6/intervals6.c b/regression/goto-analyzer/intervals_06/main.c similarity index 84% rename from regression/goto-analyzer/intervals6/intervals6.c rename to regression/goto-analyzer/intervals_06/main.c index e93240e7573..0e8a1f37c13 100644 --- a/regression/goto-analyzer/intervals6/intervals6.c +++ b/regression/goto-analyzer/intervals_06/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_06/test.desc b/regression/goto-analyzer/intervals_06/test.desc new file mode 100644 index 00000000000..2dc8d29a3b6 --- /dev/null +++ b/regression/goto-analyzer/intervals_06/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 || x > 100: Failure (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals7/intervals7.c b/regression/goto-analyzer/intervals_07/main.c similarity index 84% rename from regression/goto-analyzer/intervals7/intervals7.c rename to regression/goto-analyzer/intervals_07/main.c index c893c413ad5..75da9413b97 100644 --- a/regression/goto-analyzer/intervals7/intervals7.c +++ b/regression/goto-analyzer/intervals_07/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_07/test.desc b/regression/goto-analyzer/intervals_07/test.desc new file mode 100644 index 00000000000..aa3962f39de --- /dev/null +++ b/regression/goto-analyzer/intervals_07/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 && x > 100: Failure (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals8/intervals8.c b/regression/goto-analyzer/intervals_08/main.c similarity index 83% rename from regression/goto-analyzer/intervals8/intervals8.c rename to regression/goto-analyzer/intervals_08/main.c index 4128ac07ce5..3bcb7fe69c7 100644 --- a/regression/goto-analyzer/intervals8/intervals8.c +++ b/regression/goto-analyzer/intervals_08/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_08/test.desc b/regression/goto-analyzer/intervals_08/test.desc new file mode 100644 index 00000000000..7b83ecd0f21 --- /dev/null +++ b/regression/goto-analyzer/intervals_08/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 6 function main, assertion x < -10 && x < 100: Failure (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals9/intervals9.c b/regression/goto-analyzer/intervals_09/main.c similarity index 82% rename from regression/goto-analyzer/intervals9/intervals9.c rename to regression/goto-analyzer/intervals_09/main.c index 27739c7aa28..73b8e73dc85 100644 --- a/regression/goto-analyzer/intervals9/intervals9.c +++ b/regression/goto-analyzer/intervals_09/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_09/test.desc b/regression/goto-analyzer/intervals_09/test.desc new file mode 100644 index 00000000000..83776b8ae34 --- /dev/null +++ b/regression/goto-analyzer/intervals_09/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i>=1 && i<=2: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals10/intervals10.c b/regression/goto-analyzer/intervals_10/main.c similarity index 92% rename from regression/goto-analyzer/intervals10/intervals10.c rename to regression/goto-analyzer/intervals_10/main.c index b27cc6f2001..b245b3f5b7c 100644 --- a/regression/goto-analyzer/intervals10/intervals10.c +++ b/regression/goto-analyzer/intervals_10/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_10/test.desc b/regression/goto-analyzer/intervals_10/test.desc new file mode 100644 index 00000000000..468ce13a550 --- /dev/null +++ b/regression/goto-analyzer/intervals_10/test.desc @@ -0,0 +1,12 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 8 function main, assertion j<=100: Success$ +^\[main.assertion.2\] file main.c line 11 function main, assertion j<101: Success$ +^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: Failure (if reachable)$ +^\[main.assertion.4\] file main.c line 17 function main, assertion j<99: Unknown$ +^\[main.assertion.5\] file main.c line 20 function main, assertion j==100: Failure (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals11/intervals11.c b/regression/goto-analyzer/intervals_11/main.c similarity index 97% rename from regression/goto-analyzer/intervals11/intervals11.c rename to regression/goto-analyzer/intervals_11/main.c index 2f061cd554d..a6496ef764d 100644 --- a/regression/goto-analyzer/intervals11/intervals11.c +++ b/regression/goto-analyzer/intervals_11/main.c @@ -1,4 +1,4 @@ -#include + const int xLen = 10; const int Alen = 2; const int Blen = 1; diff --git a/regression/goto-analyzer/intervals_11/test.desc b/regression/goto-analyzer/intervals_11/test.desc new file mode 100644 index 00000000000..799ad36f64f --- /dev/null +++ b/regression/goto-analyzer/intervals_11/test.desc @@ -0,0 +1,9 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: Unknown$ +^\[main.assertion.2\] file main.c line 35 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals12/intervals12.c b/regression/goto-analyzer/intervals_12/main.c similarity index 87% rename from regression/goto-analyzer/intervals12/intervals12.c rename to regression/goto-analyzer/intervals_12/main.c index 15d865adf80..506e118f898 100644 --- a/regression/goto-analyzer/intervals12/intervals12.c +++ b/regression/goto-analyzer/intervals_12/main.c @@ -1,4 +1,3 @@ -#include int main (void) { int i; diff --git a/regression/goto-analyzer/intervals_12/test.desc b/regression/goto-analyzer/intervals_12/test.desc new file mode 100644 index 00000000000..ffdf46857de --- /dev/null +++ b/regression/goto-analyzer/intervals_12/test.desc @@ -0,0 +1,9 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^[main.assertion.1] file main.c line 8 function main, assertion j < 0: Success$ +^[main.assertion.2] file main.c line 11 function main, assertion j < 0: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c b/regression/goto-analyzer/intervals_13/main.c similarity index 95% rename from regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c rename to regression/goto-analyzer/intervals_13/main.c index d1d29427250..b631969e8f6 100644 --- a/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c +++ b/regression/goto-analyzer/intervals_13/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_13/test.desc b/regression/goto-analyzer/intervals_13/test.desc new file mode 100644 index 00000000000..8d9720faf63 --- /dev/null +++ b/regression/goto-analyzer/intervals_13/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: Success$ +^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: Success$ +^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: Unknown$ +^\[main.assertion.4\] file main.c line 16 function main, assertion 0: Success$ +^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: Success$ +^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: Unknown$ +^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: Success$ +^\[main.assertion.8\] file main.c line 28 function main, assertion j\s*<\s*100: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c b/regression/goto-analyzer/intervals_14/main.c similarity index 86% rename from regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c rename to regression/goto-analyzer/intervals_14/main.c index 3909e3889e4..7e4d53d5e06 100644 --- a/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c +++ b/regression/goto-analyzer/intervals_14/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_14/test.desc b/regression/goto-analyzer/intervals_14/test.desc new file mode 100644 index 00000000000..20a01bf3e12 --- /dev/null +++ b/regression/goto-analyzer/intervals_14/test.desc @@ -0,0 +1,10 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 12 function main, assertion i<50: Unknown$ +^\[main.assertion.2\] file main.c line 13 function main, assertion i<51: Unknown$ +^\[main.assertion.3\] file main.c line 14 function main, assertion i<52: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c b/regression/goto-analyzer/intervals_15/main.c similarity index 82% rename from regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c rename to regression/goto-analyzer/intervals_15/main.c index 002e9063228..52ef248b772 100644 --- a/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c +++ b/regression/goto-analyzer/intervals_15/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_15/test.desc b/regression/goto-analyzer/intervals_15/test.desc new file mode 100644 index 00000000000..e61667afcd4 --- /dev/null +++ b/regression/goto-analyzer/intervals_15/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals_16/main.c b/regression/goto-analyzer/intervals_16/main.c new file mode 100644 index 00000000000..52ef248b772 --- /dev/null +++ b/regression/goto-analyzer/intervals_16/main.c @@ -0,0 +1,13 @@ + +int main() +{ + int i=0, j=2; + + while (i<=50) + { + i++; + j++; + } + assert(j<52); +} + diff --git a/regression/goto-analyzer/intervals_16/test.desc b/regression/goto-analyzer/intervals_16/test.desc new file mode 100644 index 00000000000..c23e2bcf4f5 --- /dev/null +++ b/regression/goto-analyzer/intervals_16/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: (Unknown|Failure \(if reachable\))$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/reachable-functions-basic-json/test.desc b/regression/goto-analyzer/reachable-functions-basic-json/test.desc new file mode 100644 index 00000000000..56938b7514e --- /dev/null +++ b/regression/goto-analyzer/reachable-functions-basic-json/test.desc @@ -0,0 +1,9 @@ +CORE +../unreachable-instructions-basic-text/unreachable.c +--reachable-functions --json - +"function": "main",$ +"function": "dead_inside",$ +"function": "obviously_dead",$ +"function": "not_obviously_dead",$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/reachable-functions-basic-text/test.desc b/regression/goto-analyzer/reachable-functions-basic-text/test.desc new file mode 100644 index 00000000000..86a1a62015c --- /dev/null +++ b/regression/goto-analyzer/reachable-functions-basic-text/test.desc @@ -0,0 +1,9 @@ +CORE +../unreachable-instructions-basic-text/unreachable.c +--reachable-functions +unreachable.c main 35 42$ +unreachable.c dead_inside 8 14$ +unreachable.c obviously_dead 16 23$ +unreachable.c not_obviously_dead 25 31$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/reachable-functions-domain-text/test.desc b/regression/goto-analyzer/reachable-functions-domain-text/test.desc new file mode 100644 index 00000000000..cefc3ad4120 --- /dev/null +++ b/regression/goto-analyzer/reachable-functions-domain-text/test.desc @@ -0,0 +1,11 @@ +CORE +../unreachable-instructions-basic-text/unreachable.c +--reachable-functions --constants +^EXIT=0$ +^SIGNAL=0$ +unreachable.c main 35 42$ +unreachable.c dead_inside 8 14$ +unreachable.c obviously_dead 16 23$ +unreachable.c not_obviously_dead 25 31$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/regenerate-entry-function/test.desc b/regression/goto-analyzer/regenerate-entry-function/test.desc index 289b7cbd276..ecc9f85a199 100644 --- a/regression/goto-analyzer/regenerate-entry-function/test.desc +++ b/regression/goto-analyzer/regenerate-entry-function/test.desc @@ -2,7 +2,7 @@ CORE main.c --function fun --show-goto-functions ^\s*fun\(x\);$ -^EXIT=6$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/unreachable-functions-basic-json/test.desc b/regression/goto-analyzer/unreachable-functions-basic-json/test.desc new file mode 100644 index 00000000000..1a343aab6f1 --- /dev/null +++ b/regression/goto-analyzer/unreachable-functions-basic-json/test.desc @@ -0,0 +1,9 @@ +CORE +../unreachable-instructions-basic-text/unreachable.c +--unreachable-functions --json - +"file name": ".*unreachable.c", +"first line": 3, +"function": "not_called", +"last line": 6 +-- +^warning: ignoring diff --git a/regression/goto-analyzer/unreachable-functions-basic-text/test.desc b/regression/goto-analyzer/unreachable-functions-basic-text/test.desc new file mode 100644 index 00000000000..a6918166e71 --- /dev/null +++ b/regression/goto-analyzer/unreachable-functions-basic-text/test.desc @@ -0,0 +1,6 @@ +CORE +../unreachable-instructions-basic-text/unreachable.c +--unreachable-functions +unreachable.c not_called 3 6$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/unreachable-functions-domain-text/test.desc b/regression/goto-analyzer/unreachable-functions-domain-text/test.desc new file mode 100644 index 00000000000..06c5ab7ec9d --- /dev/null +++ b/regression/goto-analyzer/unreachable-functions-domain-text/test.desc @@ -0,0 +1,8 @@ +CORE +../unreachable-instructions-basic-text/unreachable.c +--unreachable-functions --constants +^EXIT=0$ +^SIGNAL=0$ +unreachable.c not_called 3 6$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc b/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc new file mode 100644 index 00000000000..e5e0a7d1a91 --- /dev/null +++ b/regression/goto-analyzer/unreachable-instructions-basic-json/test.desc @@ -0,0 +1,21 @@ +CORE +../unreachable-instructions-basic-text/unreachable.c +--unreachable-instructions --json - +"function": "not_called", +"unreachableInstructions": +"sourceLocation": +"function": "not_called", +"line": "5", +"statement": "not_called#return_value = x \+ x;" +"sourceLocation": +"function": "not_called", +"line": "5", +"statement": "GOTO 1" +"function": "dead_inside", +"unreachableInstructions": +"sourceLocation": +"function": "dead_inside", +"line": "12", +"statement": "y = y \+ 1;" +-- +^warning: ignoring diff --git a/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc b/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc new file mode 100644 index 00000000000..c71ba15f5c9 --- /dev/null +++ b/regression/goto-analyzer/unreachable-instructions-basic-text/test.desc @@ -0,0 +1,15 @@ +CORE +unreachable.c +--unreachable-instructions +^EXIT=0$ +^SIGNAL=0$ +not_called +// 28 file unreachable.c line 5 function not_called$ +not_called#return_value = x \+ x;$ +// 29 file unreachable.c line 5 function not_called$ +GOTO 1$ +dead_inside +// 34 file unreachable.c line 12 function dead_inside$ +y = y \+ 1;$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/unreachable-instructions-basic-text/unreachable.c b/regression/goto-analyzer/unreachable-instructions-basic-text/unreachable.c new file mode 100644 index 00000000000..2527951dd5a --- /dev/null +++ b/regression/goto-analyzer/unreachable-instructions-basic-text/unreachable.c @@ -0,0 +1,42 @@ +#include + +int not_called(int x) +{ + return x + x; +} + +int dead_inside(int x) +{ + int y = x + x; + goto end; + ++y; + end : return y; +} + +int obviously_dead(int x) +{ + if (0) + { + x++; + } + return x; +} + +int not_obviously_dead(int x) +{ + if (dead_inside(x) != x + x) { + x++; + } + return obviously_dead(x); +} + +int nondet_int(void); + +int main(int argc, char **argv) +{ + int x = 23; + + assert(x == not_obviously_dead(x)); + + return; +} diff --git a/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc b/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc new file mode 100644 index 00000000000..fd3ce8b0c91 --- /dev/null +++ b/regression/goto-analyzer/unreachable-instructions-domain-text/test.desc @@ -0,0 +1,18 @@ +CORE +../unreachable-instructions-basic-text/unreachable.c +--unreachable-instructions --constants +^EXIT=0$ +^SIGNAL=0$ +not_called +// 28 file unreachable.c line 5 function not_called$ +not_called#return_value = x \+ x;$ +// 29 file unreachable.c line 5 function not_called$ +GOTO 1$ +dead_inside +// 34 file unreachable.c line 12 function dead_inside$ +y = y \+ 1;$ +obviously_dead +// 40 file unreachable-instructions-basic-text/unreachable.c line 20 function obviously_dead +x = x \+ 1; +-- +^warning: ignoring diff --git a/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc b/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc index 6e48067136c..40cb3664871 100644 --- a/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc +++ b/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc @@ -2,7 +2,7 @@ CORE main.c '--function fun --show-goto-functions' ^\s*fun\(x\);$ -^EXIT=6$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index da9e1c50d7d..1be5be97dc7 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -1,9 +1,11 @@ SRC = goto_analyzer_main.cpp \ goto_analyzer_parse_options.cpp \ - static_analyzer.cpp \ taint_analysis.cpp \ taint_parser.cpp \ unreachable_instructions.cpp \ + static_show_domain.cpp \ + static_simplifier.cpp \ + static_verifier.cpp \ # Empty last line OBJ += ../ansi-c/ansi-c$(LIBEXT) \ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 1bd52d34560..f8d1fc1d331 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Goto-Analyser Command Line Option Processing +Module: Goto-Analyzer Command Line Option Processing Author: Daniel Kroening, kroening@kroening.com @@ -38,7 +38,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include +#include +#include +#include #include @@ -47,12 +52,15 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include "taint_analysis.h" #include "unreachable_instructions.h" -#include "static_analyzer.h" +#include "static_show_domain.h" +#include "static_simplifier.h" +#include "static_verifier.h" goto_analyzer_parse_optionst::goto_analyzer_parse_optionst( int argc, @@ -91,7 +99,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(config.set(cmdline)) { usage_error(); - exit(1); + exit(CPROVER_EXIT_USAGE_ERROR); } #if 0 @@ -131,6 +139,232 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("error-label")) options.set_option("error-label", cmdline.get_values("error-label")); #endif + + // Select a specific analysis + if(cmdline.isset("taint")) + { + options.set_option("taint", true); + options.set_option("specific-analysis", true); + } + // For backwards compatibility, + // these are first recognised as specific analyses + bool reachability_task = false; + if(cmdline.isset("unreachable-instructions")) + { + options.set_option("unreachable-instructions", true); + options.set_option("specific-analysis", true); + reachability_task = true; + } + if(cmdline.isset("unreachable-functions")) + { + options.set_option("unreachable-functions", true); + options.set_option("specific-analysis", true); + reachability_task = true; + } + if(cmdline.isset("reachable-functions")) + { + options.set_option("reachable-functions", true); + options.set_option("specific-analysis", true); + reachability_task = true; + } + if(cmdline.isset("show-local-may-alias")) + { + options.set_option("show-local-may-alias", true); + options.set_option("specific-analysis", true); + } + + // Output format choice + if(cmdline.isset("text")) + { + options.set_option("text", true); + options.set_option("outfile", cmdline.get_value("text")); + } + else if(cmdline.isset("json")) + { + options.set_option("json", true); + options.set_option("outfile", cmdline.get_value("json")); + } + else if(cmdline.isset("xml")) + { + options.set_option("xml", true); + options.set_option("outfile", cmdline.get_value("xml")); + } + else if(cmdline.isset("dot")) + { + options.set_option("dot", true); + options.set_option("outfile", cmdline.get_value("dot")); + } + else + { + options.set_option("text", true); + options.set_option("outfile", "-"); + } + + // The use should either select: + // 1. a specific analysis, or + // 2. a triple of task / analyzer / domain, or + // 3. one of the general display options + + // Task options + if(cmdline.isset("show")) + { + options.set_option("show", true); + options.set_option("general-analysis", true); + } + else if(cmdline.isset("verify")) + { + options.set_option("verify", true); + options.set_option("general-analysis", true); + } + else if(cmdline.isset("simplify")) + { + options.set_option("simplify", true); + options.set_option("outfile", cmdline.get_value("simplify")); + options.set_option("general-analysis", true); + + // For development allow slicing to be disabled in the simplify task + options.set_option( + "simplify-slicing", + !(cmdline.isset("no-simplify-slicing"))); + } + else if(cmdline.isset("show-intervals")) + { + // For backwards compatibility + options.set_option("show", true); + options.set_option("general-analysis", true); + options.set_option("intervals", true); + options.set_option("domain set", true); + } + else if(cmdline.isset("(show-non-null)")) + { + // For backwards compatibility + options.set_option("show", true); + options.set_option("general-analysis", true); + options.set_option("non-null", true); + options.set_option("domain set", true); + } + else if(cmdline.isset("intervals") || cmdline.isset("non-null")) + { + // For backwards compatibility either of these on their own means show + options.set_option("show", true); + options.set_option("general-analysis", true); + } + + if(options.get_bool_option("general-analysis") || reachability_task) + { + // Abstract interpreter choice + if(cmdline.isset("location-sensitive")) + options.set_option("location-sensitive", true); + else if(cmdline.isset("concurrent")) + options.set_option("concurrent", true); + else + { + // Silently default to location-sensitive as it's the "default" + // view of abstract interpretation. + options.set_option("location-sensitive", true); + } + + // Domain choice + if(cmdline.isset("constants")) + { + options.set_option("constants", true); + options.set_option("domain set", true); + } + else if(cmdline.isset("dependence-graph")) + { + options.set_option("dependence-graph", true); + options.set_option("domain set", true); + } + else if(cmdline.isset("intervals")) + { + options.set_option("intervals", true); + options.set_option("domain set", true); + } + else if(cmdline.isset("non-null")) + { + options.set_option("non-null", true); + options.set_option("domain set", true); + } + + // Reachability questions, when given with a domain swap from specific + // to general tasks so that they can use the domain & parameterisations. + if(reachability_task) + { + if(options.get_bool_option("domain set")) + { + options.set_option("specific-analysis", false); + options.set_option("general-analysis", true); + } + } + else + { + if(!options.get_bool_option("domain set")) + { + // Default to constants as it is light-weight but useful + status() << "Domain not specified, defaulting to --constants" << eom; + options.set_option("constants", true); + } + } + } +} + +/// For the task, build the appropriate kind of analyzer +/// Ideally this should be a pure function of options. +/// However at the moment some domains require the goto_model +ai_baset *goto_analyzer_parse_optionst::build_analyzer(const optionst &options) +{ + ai_baset *domain = nullptr; + + if(options.get_bool_option("location-sensitive")) + { + if(options.get_bool_option("constants")) + { + // constant_propagator_ait derives from ait + domain=new constant_propagator_ait(goto_model.goto_functions); + } + else if(options.get_bool_option("dependence-graph")) + { + domain=new dependence_grapht(namespacet(goto_model.symbol_table)); + } + else if(options.get_bool_option("intervals")) + { + domain=new ait(); + } +#if 0 + // Not actually implemented, despite the option... + else if(options.get_bool_option("non-null")) + { + domain=new ait(); + } +#endif + } + else if(options.get_bool_option("concurrent")) + { +#if 0 + // Disabled until merge_shared is implemented for these + if(options.get_bool_option("constants")) + { + domain=new concurrency_aware_ait(); + } + else if(options.get_bool_option("dependence-graph")) + { + domain=new dependence_grapht(namespacet(goto_model.symbol_table)); + } + else if(options.get_bool_option("intervals")) + { + domain=new concurrency_aware_ait(); + } +#if 0 + // Not actually implemented, despite the option... + else if(options.get_bool_option("non-null")) + { + domain=new concurrency_aware_ait(); + } +#endif +#endif + } + + return domain; } /// invoke main modules @@ -139,7 +373,7 @@ int goto_analyzer_parse_optionst::doit() if(cmdline.isset("version")) { std::cout << CBMC_VERSION << '\n'; - return 0; + return CPROVER_EXIT_SUCCESS; } // @@ -168,45 +402,80 @@ int goto_analyzer_parse_optionst::doit() catch(const char *e) { error() << e << eom; - return true; + return CPROVER_EXIT_EXCEPTION; } catch(const std::string &e) { error() << e << eom; - return true; + return CPROVER_EXIT_EXCEPTION; } - catch(int) + catch(int e) { - return true; + error() << "Numeric exception: " << e << eom; + return CPROVER_EXIT_EXCEPTION; } if(process_goto_program(options)) - return 6; + return CPROVER_EXIT_INTERNAL_ERROR; // show it? if(cmdline.isset("show-symbol-table")) { ::show_symbol_table(goto_model.symbol_table, get_ui()); - return 6; + return CPROVER_EXIT_SUCCESS; } // show it? if(cmdline.isset("show-goto-functions")) { show_goto_functions(goto_model, get_ui()); - return 6; + return CPROVER_EXIT_SUCCESS; } - if(cmdline.isset("taint")) + try + { + return perform_analysis(options); + } + + catch(const char *e) + { + error() << e << eom; + return CPROVER_EXIT_EXCEPTION; + } + + catch(const std::string &e) + { + error() << e << eom; + return CPROVER_EXIT_EXCEPTION; + } + + catch(int e) + { + error() << "Numeric exception: " << e << eom; + return CPROVER_EXIT_EXCEPTION; + } + + catch(const std::bad_alloc &) + { + error() << "Out of memory" << eom; + return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY; + } +} + + +/// Depending on the command line mode, run one of the analysis tasks +int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) +{ + if(options.get_bool_option("taint")) { std::string taint_file=cmdline.get_value("taint"); if(cmdline.isset("show-taint")) { taint_analysis(goto_model, taint_file, get_message_handler(), true, ""); - return 0; + return CPROVER_EXIT_SUCCESS; } else { @@ -214,11 +483,13 @@ int goto_analyzer_parse_optionst::doit() bool result= taint_analysis( goto_model, taint_file, get_message_handler(), false, json_file); - return result?10:0; + return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS; } } - if(cmdline.isset("unreachable-instructions")) + // If no domain is given, this lightweight version of the analysis is used. + if(options.get_bool_option("unreachable-instructions") && + options.get_bool_option("specific-analysis")) { const std::string json_file=cmdline.get_value("json"); @@ -233,16 +504,17 @@ int goto_analyzer_parse_optionst::doit() { error() << "Failed to open json output `" << json_file << "'" << eom; - return 6; + return CPROVER_EXIT_INTERNAL_ERROR; } unreachable_instructions(goto_model, true, ofs); } - return 0; + return CPROVER_EXIT_SUCCESS; } - if(cmdline.isset("unreachable-functions")) + if(options.get_bool_option("unreachable-functions") && + options.get_bool_option("specific-analysis")) { const std::string json_file=cmdline.get_value("json"); @@ -257,16 +529,17 @@ int goto_analyzer_parse_optionst::doit() { error() << "Failed to open json output `" << json_file << "'" << eom; - return 6; + return CPROVER_EXIT_INTERNAL_ERROR; } unreachable_functions(goto_model, true, ofs); } - return 0; + return CPROVER_EXIT_SUCCESS; } - if(cmdline.isset("reachable-functions")) + if(options.get_bool_option("reachable-functions") && + options.get_bool_option("specific-analysis")) { const std::string json_file=cmdline.get_value("json"); @@ -281,16 +554,16 @@ int goto_analyzer_parse_optionst::doit() { error() << "Failed to open json output `" << json_file << "'" << eom; - return 6; + return CPROVER_EXIT_INTERNAL_ERROR; } reachable_functions(goto_model, true, ofs); } - return 0; + return CPROVER_EXIT_SUCCESS; } - if(cmdline.isset("show-local-may-alias")) + if(options.get_bool_option("show-local-may-alias")) { namespacet ns(goto_model.symbol_table); @@ -304,7 +577,7 @@ int goto_analyzer_parse_optionst::doit() std::cout << '\n'; } - return 0; + return CPROVER_EXIT_SUCCESS; } label_properties(goto_model); @@ -312,32 +585,112 @@ int goto_analyzer_parse_optionst::doit() if(cmdline.isset("show-properties")) { show_properties(goto_model, get_ui()); - return 0; + return CPROVER_EXIT_SUCCESS; } if(set_properties()) - return 7; + return CPROVER_EXIT_SET_PROPERTIES_FAILED; - if(cmdline.isset("show-intervals")) + if(options.get_bool_option("general-analysis")) { - show_intervals(goto_model, std::cout); - return 0; - } - if(cmdline.isset("non-null") || - cmdline.isset("intervals")) - { - optionst options; - options.set_option("json", cmdline.get_value("json")); - options.set_option("xml", cmdline.get_value("xml")); - bool result= - static_analyzer(goto_model, options, get_message_handler()); - return result?10:0; + // Output file factory + const std::string outfile=options.get_option("outfile"); + std::ofstream output_stream; + if(!(outfile=="-")) + output_stream.open(outfile); + + std::ostream &out((outfile=="-") ? std::cout : output_stream); + + if(!out) + { + error() << "Failed to open output file `" + << outfile << "'" << eom; + return CPROVER_EXIT_INTERNAL_ERROR; + } + + // Build analyzer + status() << "Selecting abstract domain" << eom; + std::unique_ptr analyzer(build_analyzer(options)); + + if(analyzer == nullptr) + { + status() << "Task / Interpreter / Domain combination not supported" + << messaget::eom; + return CPROVER_EXIT_INTERNAL_ERROR; + } + + + // Run + status() << "Computing abstract states" << eom; + (*analyzer)(goto_model); + + // Perform the task + status() << "Performing task" << eom; + bool result = true; + if(options.get_bool_option("show")) + { + result = static_show_domain(goto_model, + *analyzer, + options, + get_message_handler(), + out); + } + else if(options.get_bool_option("verify")) + { + result = static_verifier(goto_model, + *analyzer, + options, + get_message_handler(), + out); + } + else if(options.get_bool_option("simplify")) + { + result = static_simplifier(goto_model, + *analyzer, + options, + get_message_handler(), + out); + } + else if(options.get_bool_option("unreachable-instructions")) + { + result = static_unreachable_instructions(goto_model, + *analyzer, + options, + get_message_handler(), + out); + } + else if(options.get_bool_option("unreachable-functions")) + { + result = static_unreachable_functions(goto_model, + *analyzer, + options, + get_message_handler(), + out); + } + else if(options.get_bool_option("reachable-functions")) + { + result = static_reachable_functions(goto_model, + *analyzer, + options, + get_message_handler(), + out); + } + else + { + error() << "Unhandled task" << eom; + return CPROVER_EXIT_INTERNAL_ERROR; + } + + return result ? + CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_VERIFICATION_SAFE; } + + // Final defensive error case error() << "no analysis option given -- consider reading --help" << eom; - return 6; + return CPROVER_EXIT_USAGE_ERROR; } bool goto_analyzer_parse_optionst::set_properties() @@ -447,7 +800,7 @@ void goto_analyzer_parse_optionst::help() { std::cout << "\n" - "* * GOTO-ANALYSER " CBMC_VERSION " - Copyright (C) 2016 "; + "* * GOTO-ANALYZER " CBMC_VERSION " - Copyright (C) 2017 "; std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; @@ -462,22 +815,39 @@ void goto_analyzer_parse_optionst::help() " goto-analyzer [-h] [--help] show help\n" " goto-analyzer file.c ... source file names\n" "\n" - "Analyses:\n" - "\n" + "Task options:\n" + " --show display the abstract domains\n" // NOLINTNEXTLINE(whitespace/line_length) - " --taint file_name perform taint analysis using rules in given file\n" + " --verify use the abstract domains to check assertions\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --simplify file_name use the abstract domains to simplify the program\n" " --unreachable-instructions list dead code\n" // NOLINTNEXTLINE(whitespace/line_length) " --unreachable-functions list functions unreachable from the entry point\n" // NOLINTNEXTLINE(whitespace/line_length) " --reachable-functions list functions reachable from the entry point\n" - " --intervals interval analysis\n" - " --non-null non-null analysis\n" "\n" - "Analysis options:\n" + "Abstract interpreter options:\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --location-sensitive use location-sensitive abstract interpreter\n" + " --concurrent use concurrency-aware abstract interpreter\n" + "\n" + "Domain options:\n" + " --constants constant domain\n" + " --intervals interval domain\n" + " --non-null non-null domain\n" + " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*) + "\n" + "Output options:\n" + " --text file_name output results in plain text to given file\n" // NOLINTNEXTLINE(whitespace/line_length) " --json file_name output results in JSON format to given file\n" " --xml file_name output results in XML format to given file\n" + " --dot file_name output results in DOT format to given file\n" + "\n" + "Specific analyses:\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --taint file_name perform taint analysis using rules in given file\n" "\n" "C/C++ frontend options:\n" " -I path set include path (C/C++)\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 4b8f494d402..a5d5d0f4c9c 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -8,6 +8,95 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Goto-Analyser Command Line Option Processing +/// +/// Goto-analyze is the tool front-end for CPROVER's classic style abstract +/// interpretation analyses. By "classic style" I mean, domains are C++ +/// objects, transformers are computed using C++ functions and the +/// fix-points are computed by iteration. This is in contrast to 2LS's +/// approach where everything is computed using quantifier-elimination. +/// +/// The analyses are mostly in analyses/ and although they are used in other +/// places in the code, the goal is that goto-analyze should eventually +/// provide an executable front-end for all of them. +/// +/// There are a lot of different analyses and a lot of ways they can be +/// used. Goto-analyze has five, largely independent, sets of options: +/// +/// 1. Task : What you do once you've computed the domains. +/// 2. Abstract interpreter : What kind of abstract interpretation you do. +/// 3. Domain : What domain you use. +/// 4. Sensitivity : How that domain handles things like arrays, pointers, etc. +/// (see variable_sensitivity_domain.h) +/// 5. Output : What you do with the results. +/// +/// Formally speaking, 2, 3 and 4 are an artificial distinction as they are +/// all really parts of the "what domain" question. However they correspond +/// to parts of our code architecture, so ... they should stay. +/// +/// Ideally, the cross product of options should be supported but ... in +/// practice there will always be ones that are not meaningful. Those +/// should give errors. In addition there are some analyses which are +/// currently stand alone as they don't fit directly in to this model. For +/// example the unwind bounds analysis, which is both the task, the abstract +/// interpreter and the output. Where possible these should be integrated / +/// support the other options. In the case of the unwind analysis this +/// means the domain and it's sensitivity should be configurable. +/// +/// +/// Task +/// ---- +/// +/// Tasks are implemented by the relevant file in goto-analyze/static_*. At +/// the moment they are each responsible for building the domain / using the +/// other options. As much as possible of this code should be shared. Some +/// of these inherit from messaget. They all probably should. +/// +/// Show : Prints out the domains for inspection or further use. +/// +/// Verify : Uses the domain to check all assertions in the code, marking +/// each one "SUCCESS" (the assertion always holds), "FAILURE if +/// reachable" (the assertion never holds), "UNKNOWN" (the assertion may or +/// may not hold). This is implemented using domain_simplify(). +/// +/// Simplify : Generates a new goto program with branch conditions, +/// assertions, assumptions and assignments simplified using the information +/// in the domain (again using domain_simplify()). This task is intended to +/// be used as a preprocessing step for other analysis. +/// +/// Instrument : (Not implemented yet) Use the domains to add assume() +/// statements to the code giving invariants generated from the domain. +/// These assumes don't reduce the space of possible executions; they make +/// existing invariants explicit. Again, intended as a preprocessing step. +/// +/// +/// Abstract Interpreter +/// -------------------- +/// +/// This option is effectively about how we compute the fix-point(s) / +/// which child class of ai_baset we use. I.E. ait or +/// concurrency_aware_ait, etc. For migrating / refactor / +/// unifying with the pointer analysis code we might want a +/// location_insensitive_ait or something but this is not urgent. +/// We will need a context_aware_ait. +/// +/// +/// Domain +/// ------ +/// +/// Which child of ai_domain_baset we use to represent the abstract state at +/// each location / implement the transformers. I expect most of these will +/// be non-relational (i.e. an abstract object for each variable) due to the +/// cost of implementing effective non-relational domains in this style vs. +/// using 2LS. The exception might be equalities, which we could implement +/// here. +/// +/// +/// Output +/// ------ +/// +/// Text, XML, JSON plus some others for specific domains such as dependence +/// graphs in DOT format. + #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H @@ -19,6 +108,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -43,10 +133,16 @@ class optionst; "(taint):(show-taint)" \ "(show-local-may-alias)" \ "(json):(xml):" \ + "(text):(dot):" \ "(unreachable-instructions)(unreachable-functions)" \ "(reachable-functions)" \ "(intervals)(show-intervals)" \ "(non-null)(show-non-null)" \ + "(constants)" \ + "(dependence-graph)" \ + "(show)(verify)(simplify):" \ + "(location-sensitive)(concurrent)" \ + "(no-simplify-slicing)" \ JAVA_BYTECODE_LANGUAGE_OPTIONS class goto_analyzer_parse_optionst: @@ -70,6 +166,10 @@ class goto_analyzer_parse_optionst: virtual bool process_goto_program(const optionst &options); bool set_properties(); + virtual int perform_analysis(const optionst &options); + + ai_baset *build_analyzer(const optionst &options); + void eval_verbosity(); ui_message_handlert::uit get_ui() diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp index e92a8da8d68..df85702500d 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -6,7 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#define USE_DEPRECATED_STATIC_ANALYZER_H #include "static_analyzer.h" +#undef USE_DEPRECATED_STATIC_ANALYZER_H #include diff --git a/src/goto-analyzer/static_analyzer.h b/src/goto-analyzer/static_analyzer.h index fdab261d8c1..6021daadb8f 100644 --- a/src/goto-analyzer/static_analyzer.h +++ b/src/goto-analyzer/static_analyzer.h @@ -10,6 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_ANALYZER_STATIC_ANALYZER_H #define CPROVER_GOTO_ANALYZER_STATIC_ANALYZER_H +#ifndef USE_DEPRECATED_STATIC_ANALYZER_H +#error Deprecated, use static_show_domain.h instead +#endif + #include #include diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp new file mode 100644 index 00000000000..99c8d63cefd --- /dev/null +++ b/src/goto-analyzer/static_show_domain.cpp @@ -0,0 +1,53 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#include "static_show_domain.h" + +#include + +/// Runs the analyzer and then prints out the domain +/// \param goto_model: the program analyzed +/// \param ai: the abstract interpreter after it has been run to fix point +/// \param options: the parsed user options +/// \param message_handler: the system message handler +/// \param out: output stream for the printing +/// \return: false on success with the domain printed to out +bool static_show_domain( + const goto_modelt &goto_model, + const ai_baset &ai, + const optionst &options, + message_handlert &message_handler, + std::ostream &out) +{ + if(options.get_bool_option("json")) + { + out << ai.output_json(goto_model); + } + else if(options.get_bool_option("xml")) + { + out << ai.output_xml(goto_model); + } + else if(options.get_bool_option("dot") && + options.get_bool_option("dependence-graph")) + { + const dependence_grapht *d=dynamic_cast(&ai); + INVARIANT(d!=nullptr, + "--dependence-graph sets ai to be a dependence_graph"); + + out << "digraph g {\n"; + d->output_dot(out); + out << "}\n"; + } + else + { + INVARIANT(options.get_bool_option("text"), "Other output formats handled"); + ai.output(goto_model, out); + } + + return false; +} diff --git a/src/goto-analyzer/static_show_domain.h b/src/goto-analyzer/static_show_domain.h new file mode 100644 index 00000000000..5284cc6a9ec --- /dev/null +++ b/src/goto-analyzer/static_show_domain.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H +#define CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H + +#include + +#include +#include + +#include + +#include + +bool static_show_domain( + const goto_modelt &, + const ai_baset &, + const optionst &, + message_handlert &, + std::ostream &); + +#endif // CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp new file mode 100644 index 00000000000..9e6ffa57822 --- /dev/null +++ b/src/goto-analyzer/static_simplifier.cpp @@ -0,0 +1,176 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#include +#include +#include + +#include +#include +#include +#include + +#include "static_simplifier.h" + + +/// Simplifies the program using the information in the abstract domain. +/// \param goto_model: the program analyzed +/// \param ai: the abstract interpreter after it has been run to fix point +/// \param options: the parsed user options +/// \param message_handler: the system message handler +/// \param out: output stream for the simplified program +/// \return: false on success with the domain printed to out +bool static_simplifier( + goto_modelt &goto_model, + const ai_baset &ai, + const optionst &options, + message_handlert &message_handler, + std::ostream &out) +{ + struct counterst + { + counterst() : + asserts(0), + assumes(0), + gotos(0), + assigns(0), + function_calls(0) {} + + std::size_t asserts; + std::size_t assumes; + std::size_t gotos; + std::size_t assigns; + std::size_t function_calls; + }; + + counterst simplified; + counterst unmodified; + + namespacet ns(goto_model.symbol_table); + + messaget m(message_handler); + m.status() << "Simplifying program" << messaget::eom; + + Forall_goto_functions(f_it, goto_model.goto_functions) + { + Forall_goto_program_instructions(i_it, f_it->second.body) + { + m.progress() << "Simplifying " << f_it->first << messaget::eom; + + if(i_it->is_assert()) + { + bool unchanged= + ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns); + + if(unchanged) + unmodified.asserts++; + else + simplified.asserts++; + } + else if(i_it->is_assume()) + { + bool unchanged= + ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns); + + if(unchanged) + unmodified.assumes++; + else + simplified.assumes++; + } + else if(i_it->is_goto()) + { + bool unchanged= + ai.abstract_state_before(i_it).ai_simplify(i_it->guard, ns); + + if(unchanged) + unmodified.gotos++; + else + simplified.gotos++; + } + else if(i_it->is_assign()) + { + code_assignt &assign=to_code_assign(i_it->code); + + // Simplification needs to be aware of which side of the + // expression it is handling as: + // i=j + // should simplify to i=1, not to 0=1. + + bool unchanged_lhs= + ai.abstract_state_before(i_it).ai_simplify_lhs(assign.lhs(), ns); + + bool unchanged_rhs= + ai.abstract_state_before(i_it).ai_simplify(assign.rhs(), ns); + + if(unchanged_lhs && unchanged_rhs) + unmodified.assigns++; + else + simplified.assigns++; + } + else if(i_it->is_function_call()) + { + code_function_callt &fcall=to_code_function_call(i_it->code); + + bool unchanged= + ai.abstract_state_before(i_it).ai_simplify(fcall.function(), ns); + + exprt::operandst &args=fcall.arguments(); + + for(auto &o : args) + unchanged&=ai.abstract_state_before(i_it).ai_simplify(o, ns); + + if(unchanged) + unmodified.function_calls++; + else + simplified.function_calls++; + } + } + } + + // Make sure the references are correct. + goto_model.goto_functions.update(); + + m.status() << "Simplified: " + << " assert: " << simplified.asserts + << ", assume: " << simplified.assumes + << ", goto: " << simplified.gotos + << ", assigns: " << simplified.assigns + << ", function calls: " << simplified.function_calls + << "\n" + << "Unmodified: " + << " assert: " << unmodified.asserts + << ", assume: " << unmodified.assumes + << ", goto: " << unmodified.gotos + << ", assigns: " << unmodified.assigns + << ", function calls: " << unmodified.function_calls + << messaget::eom; + + + // Remove obviously unreachable things and (now) unconditional branches + if(options.get_bool_option("simplify-slicing")) + { + m.status() << "Removing unreachable instructions" << messaget::eom; + + // Removes goto false + remove_skip(goto_model.goto_functions); + goto_model.goto_functions.update(); + + // Convert unreachable to skips + remove_unreachable(goto_model.goto_functions); + goto_model.goto_functions.update(); + + // Remove all of the new skips + remove_skip(goto_model.goto_functions); + goto_model.goto_functions.update(); + } + + m.status() << "Writing goto binary" << messaget::eom; + return write_goto_binary(out, + ns.get_symbol_table(), + goto_model.goto_functions); +} diff --git a/src/goto-analyzer/static_simplifier.h b/src/goto-analyzer/static_simplifier.h new file mode 100644 index 00000000000..ee810bf8793 --- /dev/null +++ b/src/goto-analyzer/static_simplifier.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_H +#define CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_H + +#include + +#include +#include + +#include + +#include + +bool static_simplifier( + goto_modelt &, + const ai_baset &, + const optionst &, + message_handlert &, + std::ostream &); + +#endif // CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_H diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp new file mode 100644 index 00000000000..660d20bd37e --- /dev/null +++ b/src/goto-analyzer/static_verifier.cpp @@ -0,0 +1,207 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#include "static_verifier.h" + +#include +#include +#include +#include + + +/// Runs the analyzer and then prints out the domain +/// \param goto_model: the program analyzed +/// \param ai: the abstract interpreter after it has been run to fix point +/// \param options: the parsed user options +/// \param message_handler: the system message handler +/// \param out: output stream for the printing +/// \return: false on success with the domain printed to out +bool static_verifier( + const goto_modelt &goto_model, + const ai_baset &ai, + const optionst &options, + message_handlert &message_handler, + std::ostream &out) +{ + std::size_t pass=0, fail=0, unknown=0; + + namespacet ns(goto_model.symbol_table); + + messaget m(message_handler); + m.status() << "Checking assertions" << messaget::eom; + + if(options.get_bool_option("json")) + { + json_arrayt json_result; + + forall_goto_functions(f_it, goto_model.goto_functions) + { + m.progress() << "Checking " << f_it->first << messaget::eom; + + if(!f_it->second.body.has_assertion()) + continue; + + forall_goto_program_instructions(i_it, f_it->second.body) + { + if(!i_it->is_assert()) + continue; + + exprt e(i_it->guard); + const ai_domain_baset &domain(ai.abstract_state_before(i_it)); + domain.ai_simplify(e, ns); + + json_objectt &j=json_result.push_back().make_object(); + + if(e.is_true()) + { + j["status"]=json_stringt("SUCCESS"); + ++pass; + } + else if(e.is_false()) + { + j["status"]=json_stringt("FAILURE (if reachable)"); + ++fail; + } + else if(domain.is_bottom()) + { + j["status"]=json_stringt("SUCCESS (unreachable)"); + ++pass; + } + else + { + j["status"]=json_stringt("UNKNOWN"); + ++unknown; + } + + j["sourceLocation"]=json(i_it->source_location); + } + } + m.status() << "Writing JSON report" << messaget::eom; + out << json_result; + } + else if(options.get_bool_option("xml")) + { + xmlt xml_result; + + forall_goto_functions(f_it, goto_model.goto_functions) + { + m.progress() << "Checking " << f_it->first << messaget::eom; + + if(!f_it->second.body.has_assertion()) + continue; + + forall_goto_program_instructions(i_it, f_it->second.body) + { + if(!i_it->is_assert()) + continue; + + exprt e(i_it->guard); + const ai_domain_baset &domain(ai.abstract_state_before(i_it)); + domain.ai_simplify(e, ns); + + xmlt &x=xml_result.new_element("result"); + + if(e.is_true()) + { + x.set_attribute("status", "SUCCESS"); + ++pass; + } + else if(e.is_false()) + { + x.set_attribute("status", "FAILURE (if reachable)"); + ++fail; + } + else if(domain.is_bottom()) + { + x.set_attribute("status", "SUCCESS (unreachable)"); + ++pass; + } + else + { + x.set_attribute("status", "UNKNOWN"); + ++unknown; + } + + x.set_attribute("file", id2string(i_it->source_location.get_file())); + x.set_attribute("line", id2string(i_it->source_location.get_line())); + x.set_attribute( + "description", + id2string(i_it->source_location.get_comment())); + } + } + + m.status() << "Writing XML report" << messaget::eom; + out << xml_result; + } + else + { + INVARIANT(options.get_bool_option("text"), "Other output formats handled"); + + forall_goto_functions(f_it, goto_model.goto_functions) + { + m.progress() << "Checking " << f_it->first << messaget::eom; + + if(!f_it->second.body.has_assertion()) + continue; + + out << "******** Function " << f_it->first << '\n'; + + forall_goto_program_instructions(i_it, f_it->second.body) + { + if(!i_it->is_assert()) + continue; + + exprt e(i_it->guard); + const ai_domain_baset &domain(ai.abstract_state_before(i_it)); + domain.ai_simplify(e, ns); + + out << '[' << i_it->source_location.get_property_id() + << ']' << ' '; + + out << i_it->source_location; + + if(!i_it->source_location.get_comment().empty()) + out << ", " << i_it->source_location.get_comment(); + + out << ": "; + + if(e.is_true()) + { + out << "Success"; + pass++; + } + else if(e.is_false()) + { + out << "Failure (if reachable)"; + fail++; + } + else if(domain.is_bottom()) + { + out << "Success (unreachable)"; + pass++; + } + else + { + out << "Unknown"; + unknown++; + } + + out << '\n'; + } + + out << '\n'; + } + } + + m.status() << "Summary: " + << pass << " pass, " + << fail << " fail if reachable, " + << unknown << " unknown\n"; + + return false; +} diff --git a/src/goto-analyzer/static_verifier.h b/src/goto-analyzer/static_verifier.h new file mode 100644 index 00000000000..77eeacbe527 --- /dev/null +++ b/src/goto-analyzer/static_verifier.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: goto-analyzer + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H +#define CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H + +#include + +#include +#include + +#include + +#include + +bool static_verifier( + const goto_modelt &, + const ai_baset &, + const optionst &, + message_handlert &, + std::ostream &); + +#endif // CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index 183b149eff2..81fe0c608ec 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -18,6 +18,7 @@ Date: April 2016 #include #include #include +#include #include @@ -54,6 +55,16 @@ static void all_unreachable( dest.insert(std::make_pair(it->location_number, it)); } +static void build_dead_map_from_ai( + const goto_programt &goto_program, + const ai_baset &ai, + dead_mapt &dest) +{ + forall_goto_program_instructions(it, goto_program) + if(ai.abstract_state_before(it).is_bottom()) + dest.insert(std::make_pair(it->location_number, it)); +} + static void output_dead_plain( const namespacet &ns, const goto_programt &goto_program, @@ -74,6 +85,35 @@ static void output_dead_plain( goto_program.output_instruction(ns, "", os, *it->second); } +static void add_to_xml( + const namespacet &ns, + const goto_programt &goto_program, + const dead_mapt &dead_map, + xmlt &dest) +{ + PRECONDITION(!goto_program.instructions.empty()); + goto_programt::const_targett end_function= + goto_program.instructions.end(); + --end_function; + DATA_INVARIANT(end_function->is_end_function(), + "The last instruction in a goto-program must be END_FUNCTION"); + + xmlt &x = dest.new_element("function"); + x.set_attribute("name", id2string(end_function->function)); + + for(dead_mapt::const_iterator it=dead_map.begin(); + it!=dead_map.end(); + ++it) + { + xmlt &inst = x.new_element("instruction"); + inst.set_attribute("location_number", + std::to_string(it->second->location_number)); + inst.set_attribute("source_location", + it->second->source_location.as_string()); + } + return; +} + static void add_to_json( const namespacet &ns, const goto_programt &goto_program, @@ -82,11 +122,12 @@ static void add_to_json( { json_objectt &entry=dest.push_back().make_object(); - assert(!goto_program.instructions.empty()); + PRECONDITION(!goto_program.instructions.empty()); goto_programt::const_targett end_function= goto_program.instructions.end(); --end_function; - assert(end_function->is_end_function()); + DATA_INVARIANT(end_function->is_end_function(), + "The last instruction in a goto-program must be END_FUNCTION"); entry["function"]=json_stringt(id2string(end_function->function)); entry["fileName"]= @@ -164,6 +205,56 @@ void unreachable_instructions( os << json_result << '\n'; } +bool static_unreachable_instructions( + const goto_modelt &goto_model, + const ai_baset &ai, + const optionst &options, + message_handlert &message_handler, + std::ostream &out) +{ + json_arrayt json_result; + xmlt xml_result("unreachable-instructions"); + + const namespacet ns(goto_model.symbol_table); + + forall_goto_functions(f_it, goto_model.goto_functions) + { + if(!f_it->second.body_available()) + continue; + + const goto_programt &goto_program=f_it->second.body; + dead_mapt dead_map; + build_dead_map_from_ai(goto_program, ai, dead_map); + + if(!dead_map.empty()) + { + if(options.get_bool_option("json")) + { + add_to_json(ns, f_it->second.body, dead_map, json_result); + } + else if(options.get_bool_option("xml")) + { + add_to_xml(ns, f_it->second.body, dead_map, xml_result); + } + else + { + INVARIANT(options.get_bool_option("text"), + "Other output formats handled"); + output_dead_plain(ns, f_it->second.body, dead_map, out); + } + } + } + + if(options.get_bool_option("json") && !json_result.array.empty()) + out << json_result << '\n'; + else if(options.get_bool_option("xml")) + out << xml_result << '\n'; + + return false; +} + + + static void json_output_function( const irep_idt &function, const source_locationt &first_location, @@ -183,16 +274,34 @@ static void json_output_function( json_numbert(id2string(last_location.get_line())); } +static void xml_output_function( + const irep_idt &function, + const source_locationt &first_location, + const source_locationt &last_location, + xmlt &dest) +{ + xmlt &x=dest.new_element("function"); + + x.set_attribute("name", id2string(function)); + x.set_attribute("file name", + concat_dir_file( + id2string(first_location.get_working_directory()), + id2string(first_location.get_file()))); + x.set_attribute("first line", id2string(first_location.get_line())); + x.set_attribute("last line", id2string(last_location.get_line())); +} + static void list_functions( const goto_modelt &goto_model, - const bool json, + const std::set called, + const optionst &options, std::ostream &os, bool unreachable) { json_arrayt json_result; - - std::set called= - compute_called_functions(goto_model); + xmlt xml_result(unreachable ? + "unreachable-functions" : + "reachable-functions"); const namespacet ns(goto_model.symbol_table); @@ -226,7 +335,7 @@ static void list_functions( // this to macros/asm renaming continue; - if(!json) + if(options.get_bool_option("text")) { os << concat_dir_file( id2string(first_location.get_working_directory()), @@ -235,6 +344,14 @@ static void list_functions( << first_location.get_line() << " " << last_location.get_line() << "\n"; } + else if(options.get_bool_option("xml")) + { + xml_output_function( + decl.base_name, + first_location, + last_location, + xml_result); + } else json_output_function( decl.base_name, @@ -243,8 +360,10 @@ static void list_functions( json_result); } - if(json && !json_result.array.empty()) + if(options.get_bool_option("json") && !json_result.array.empty()) os << json_result << '\n'; + else if(options.get_bool_option("xml")) + os << xml_result << '\n'; } void unreachable_functions( @@ -252,7 +371,15 @@ void unreachable_functions( const bool json, std::ostream &os) { - list_functions(goto_model, json, os, true); + optionst options; + if(json) + options.set_option("json", true); + else + options.set_option("text", true); + + std::set called = compute_called_functions(goto_model); + + list_functions(goto_model, called, options, os, true); } void reachable_functions( @@ -260,5 +387,62 @@ void reachable_functions( const bool json, std::ostream &os) { - list_functions(goto_model, json, os, false); + optionst options; + if(json) + options.set_option("json", true); + else + options.set_option("text", true); + + std::set called = compute_called_functions(goto_model); + + list_functions(goto_model, called, options, os, false); +} + + +std::set compute_called_functions_from_ai( + const goto_modelt &goto_model, + const ai_baset &ai) +{ + std::set called; + + forall_goto_functions(f_it, goto_model.goto_functions) + { + if(!f_it->second.body_available()) + continue; + + const goto_programt &p = f_it->second.body; + + if(!ai.abstract_state_before(p.instructions.begin()).is_bottom()) + called.insert(f_it->first); + } + + return called; +} + +bool static_unreachable_functions( + const goto_modelt &goto_model, + const ai_baset &ai, + const optionst &options, + message_handlert &message_handler, + std::ostream &out) +{ + std::set called = compute_called_functions_from_ai(goto_model, ai); + + list_functions(goto_model, called, options, out, true); + + return false; +} + +bool static_reachable_functions( + const goto_modelt &goto_model, + const ai_baset &ai, + const optionst &options, + message_handlert &message_handler, + std::ostream &out) +{ + std::set called = compute_called_functions_from_ai(goto_model, ai); + + list_functions(goto_model, called, options, out, false); + + return false; } diff --git a/src/goto-analyzer/unreachable_instructions.h b/src/goto-analyzer/unreachable_instructions.h index 9b71e4f66f5..edffd0f7b1c 100644 --- a/src/goto-analyzer/unreachable_instructions.h +++ b/src/goto-analyzer/unreachable_instructions.h @@ -16,6 +16,11 @@ Date: April 2016 #include +#include + +#include +#include + class goto_modelt; void unreachable_instructions( @@ -33,4 +38,25 @@ void reachable_functions( const bool json, std::ostream &os); +bool static_unreachable_instructions( + const goto_modelt &, + const ai_baset &, + const optionst &, + message_handlert &, + std::ostream &); + +bool static_unreachable_functions( + const goto_modelt &, + const ai_baset &, + const optionst &, + message_handlert &, + std::ostream &); + +bool static_reachable_functions( + const goto_modelt &, + const ai_baset &, + const optionst &, + message_handlert &, + std::ostream &); + #endif // CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H