Skip to content

Commit da379bd

Browse files
danpoemartin
danpoe
authored and
martin
committed
Update and extend the regression tests for goto-analyse.
This reflects the new task/analyzer/domain approach.
1 parent db75611 commit da379bd

File tree

81 files changed

+262
-306
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

81 files changed

+262
-306
lines changed

‎regression/goto-analyzer/constant_propagation_01/constant_propagation1.c renamed to ‎regression/goto-analyzer/constant_propagation_01/main.c

-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
#include <assert.h>
21

32
int main()
43
{

‎regression/goto-analyzer/constant_propagation_01/test.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
FUTURE
2-
constant_propagation1.c
3-
--constants --simplify out.goto
1+
CORE
2+
main.c
3+
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
7-
^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 5, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c renamed to ‎regression/goto-analyzer/constant_propagation_02/main.c

-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
#include <assert.h>
21

32
int main()
43
{

‎regression/goto-analyzer/constant_propagation_02/original

-3
This file was deleted.

‎regression/goto-analyzer/constant_propagation_02/simplified

-81
This file was deleted.

‎regression/goto-analyzer/constant_propagation_02/test.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
FUTURE
2-
constant_propagation_02.c
3-
--constants --simplify out.goto
1+
CORE
2+
main.c
3+
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
7-
^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c renamed to ‎regression/goto-analyzer/constant_propagation_03/main.c

-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
#include <assert.h>
21

32
int main()
43
{

‎regression/goto-analyzer/constant_propagation_03/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
FUTURE
2-
constant_propagation_03.c
3-
--constants --simplify out.goto
2+
main.c
3+
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
7-
^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c renamed to ‎regression/goto-analyzer/constant_propagation_04/main.c

-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
#include <assert.h>
21

32
int main()
43
{

‎regression/goto-analyzer/constant_propagation_04/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
FUTURE
2-
constant_propagation_04.c
3-
--constants --simplify out.goto
2+
main.c
3+
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
7-
^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c renamed to ‎regression/goto-analyzer/constant_propagation_05/main.c

-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
#include <assert.h>
21

32
int main()
43
{

‎regression/goto-analyzer/constant_propagation_05/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
FUTURE
2-
constant_propagation_05.c
2+
main.c
33
--constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE (if reachable)$
6+
^\[main.assertion.1\] file main.c line 12 function main, assertion j!=3: Failure (if reachable)$
77
--
88
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_06/main.c

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
2+
int main()
3+
{
4+
int i=0, j=2;
5+
6+
while (i<50)
7+
{
8+
i++;
9+
j++;
10+
}
11+
assert(i<51);
12+
}
13+

‎regression/goto-analyzer/constant_propagation_06/test.desc

+4-11
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,8 @@
1-
FUTURE
2-
constant_propagation_06.c
3-
--intervals --verify
1+
CORE
2+
main.c
3+
--constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=10: SUCCESS$
7-
^\[main.assertion.2\] file constant_propagation_06.c line 11 function main, assertion i!=30: SUCCESS$
8-
^\[main.assertion.3\] file constant_propagation_06.c line 14 function main, assertion i!=15: UNKNOWN$
9-
^\[main.assertion.4\] file constant_propagation_06.c line 17 function main, assertion 0: SUCCESS$
10-
^\[main.assertion.5\] file constant_propagation_06.c line 20 function main, assertion j>=10: SUCCESS$
11-
^\[main.assertion.6\] file constant_propagation_06.c line 23 function main, assertion i>=j: UNKNOWN$
12-
^\[main.assertion.7\] file constant_propagation_06.c line 26 function main, assertion i>=11: SUCCESS$
13-
^\[main.assertion.8\] file constant_propagation_06.c line 29 function main, assertion j<100: SUCCESS$
6+
^\[main.assertion.1\] file main.c line 11 function main, assertion i\s*<\s*51: Unknown$
147
--
158
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c renamed to ‎regression/goto-analyzer/constant_propagation_07/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
22
int main()
33
{
44
signed int i;

‎regression/goto-analyzer/constant_propagation_07/test.desc

+4-3
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
FUTURE
2-
constant_propagation_07.c
3-
--constants --verify
2+
main.c
3+
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$
6+
^Simplified: assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
78
--
89
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c renamed to ‎regression/goto-analyzer/constant_propagation_08/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
22
int main()
33
{
44
int a[2];

‎regression/goto-analyzer/constant_propagation_08/test.desc

+4-5
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,9 @@
11
FUTURE
2-
constant_propagation_08.c
3-
--intervals --verify
2+
main.c
3+
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$
7-
^\[main.assertion.2\] file constant_propagation_08.c line 13 function main, assertion i<51: UNKNOWN$
8-
^\[main.assertion.3\] file constant_propagation_08.c line 14 function main, assertion i<52: SUCCESS$
6+
^Simplified: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$
98
--
109
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c renamed to ‎regression/goto-analyzer/constant_propagation_09/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
22
int main()
33
{
44
int a[2]={0,0};

‎regression/goto-analyzer/constant_propagation_09/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
FUTURE
2-
constant_propagation_09.c
3-
--intervals --verify
2+
main.c
3+
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
******** Function main
7-
^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$
6+
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c renamed to ‎regression/goto-analyzer/constant_propagation_10/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
22
int main()
33
{
44
int a[2]={0,0};

‎regression/goto-analyzer/constant_propagation_10/test.desc

+3-4
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
11
FUTURE
2-
constant_propagation_10.c
3-
--constants --simplify out.goto
2+
main.c
3+
--constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^SIMPLIFIED: assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$
7-
^UNMODIFIED: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$
6+
^\[main.assertion.1\] file main.c line 10 function main, assertion a\[0\]==2: Failure$
87
--
98
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c renamed to ‎regression/goto-analyzer/constant_propagation_11/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
22
int main()
33
{
44
int a[2]={0,0};

‎regression/goto-analyzer/constant_propagation_11/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
FUTURE
2-
constant_propagation_11.c
3-
--constants --simplify out.goto
2+
main.c
3+
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$
7-
^UNMODIFIED: assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 0$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c renamed to ‎regression/goto-analyzer/constant_propagation_12/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
22
int main()
33
{
44
int i=0, y;

‎regression/goto-analyzer/constant_propagation_12/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
FUTURE
2-
constant_propagation_12.c
3-
--constants --simplify out.goto
2+
main.c
3+
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^SIMPLIFIED: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
7-
^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$
7+
^Unmodified: assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c renamed to ‎regression/goto-analyzer/constant_propagation_13/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
22
int main()
33
{
44
int i=0, y;

‎regression/goto-analyzer/constant_propagation_13/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
FUTURE
2-
constant_propagation_13.c
2+
main.c
33
--constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.assertion.1\] file constant_propagation_13.c line 10 function main, assertion a\[0\]==2: FAILURE$
6+
^\[main.assertion.1\] file main.c line 9 function main, assertion y==0: Failure (if reachable)$
77
--
88
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c renamed to ‎regression/goto-analyzer/constant_propagation_14/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
22
int main()
33
{
44
int a[2]={0,0};

‎regression/goto-analyzer/constant_propagation_14/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
FUTURE
2-
constant_propagation_14.c
3-
--constants --simplify out.goto
2+
main.c
3+
--constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^SIMPLIFIED: assert: 1, assume: 0, goto: 0$
7-
^UNKNOWN: assert: 0, assume: 0, goto: 0$
6+
^\[main.assertion.1\] file main.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: Success$
7+
^\[main.assertion.2\] file main.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: Failure$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c renamed to ‎regression/goto-analyzer/constant_propagation_15/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#include <assert.h>
1+
22
int main()
33
{
44
int a[2]={0,0};

‎regression/goto-analyzer/constant_propagation_15/test.desc

+3-4
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
11
FUTURE
2-
constant_propagation_15.c
3-
--constants --simplify out.goto
2+
main.c
3+
--constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^SIMPLIFIED: assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$
7-
^UNMODIFIED: assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$
6+
^\[main.assertion.1\] file main.c line 9 function main, assertion a\[0\]==2: Failure$
87
--
98
^warning: ignoring

0 commit comments

Comments
 (0)