Skip to content

Commit d821c53

Browse files
NlightNFotisNlightNFotis
committed
Update the tests to match for the correct type on windows.
On windows, the type reported for the pointer is `long long`, so this change updates the tests to make them match the correct type on both Unix and Windows, and therefore pass CI successfully.
1 parent 4353e2d commit d821c53

File tree

6 files changed

+32
-32
lines changed

6 files changed

+32
-32
lines changed

‎regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ invalid_index_range.c
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
line 9 dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: FAILURE
7+
line 9 dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE
88
--
99
--
1010
Check that memory checks fail for pointer dereferences inside an existential

‎regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ smt_missing_range_check.c
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
\[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: SUCCESS
8-
\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: FAILURE
8+
\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE
99
--
1010
--
1111
Check that memory checks fail for pointer dereferences inside an existential

‎regression/cbmc-primitives/forall_6231_1/test.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@ test.c
44
^EXIT=0$
55
^SIGNAL=0$
66
\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
7-
\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed long int\)i\]: SUCCESS
8-
\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed long int\)i\]: SUCCESS
9-
\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed long int\)i\]: SUCCESS
10-
\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed long int\)i\]: SUCCESS
11-
\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: SUCCESS
12-
\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
7+
\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
8+
\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
9+
\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
10+
\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
11+
\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
12+
\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
1313
^VERIFICATION SUCCESSFUL$
1414
--
1515
--

‎regression/cbmc-primitives/forall_6231_2/test.desc

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -4,19 +4,19 @@ test.c
44
^EXIT=0$
55
^SIGNAL=0$
66
\[main\.assertion\.1\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
7-
\[main\.pointer_dereference\.1\] line \d dereference failure: pointer NULL in a\[\(signed long int\)i\]: SUCCESS
8-
\[main\.pointer_dereference\.2\] line \d dereference failure: pointer invalid in a\[\(signed long int\)i\]: SUCCESS
9-
\[main\.pointer_dereference\.3\] line \d dereference failure: deallocated dynamic object in a\[\(signed long int\)i\]: SUCCESS
10-
\[main\.pointer_dereference\.4\] line \d dereference failure: dead object in a\[\(signed long int\)i\]: SUCCESS
11-
\[main\.pointer_dereference\.5\] line \d dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: SUCCESS
12-
\[main\.pointer_dereference\.6\] line \d dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
7+
\[main\.pointer_dereference\.1\] line \d dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
8+
\[main\.pointer_dereference\.2\] line \d dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
9+
\[main\.pointer_dereference\.3\] line \d dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
10+
\[main\.pointer_dereference\.4\] line \d dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
11+
\[main\.pointer_dereference\.5\] line \d dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
12+
\[main\.pointer_dereference\.6\] line \d dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
1313
\[main\.assertion.2] line \d+ assertion __CPROVER_forall \{ int j; \!\(0 <= j && j < 1\) || \(j == 0 && \*\(a\+j\) == \*\(a+j\)\) \}: SUCCESS
14-
\[main\.pointer_dereference\.7] line \d+ dereference failure: pointer NULL in a\[\(signed long int\)j\]: SUCCESS
15-
\[main\.pointer_dereference\.8] line \d+ dereference failure: pointer invalid in a\[\(signed long int\)j\]: SUCCESS
16-
\[main\.pointer_dereference\.9] line \d+ dereference failure: deallocated dynamic object in a\[\(signed long int\)j\]: SUCCESS
17-
\[main\.pointer_dereference\.10] line \d+ dereference failure: dead object in a\[\(signed long int\)j\]: SUCCESS
18-
\[main\.pointer_dereference\.11] line \d+ dereference failure: pointer outside object bounds in a\[\(signed long int\)j\]: SUCCESS
19-
\[main\.pointer_dereference\.12] line \d+ dereference failure: invalid integer address in a\[\(signed long int\)j\]: SUCCESS
14+
\[main\.pointer_dereference\.7] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)j\]: SUCCESS
15+
\[main\.pointer_dereference\.8] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)j\]: SUCCESS
16+
\[main\.pointer_dereference\.9] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)j\]: SUCCESS
17+
\[main\.pointer_dereference\.10] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)j\]: SUCCESS
18+
\[main\.pointer_dereference\.11] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)j\]: SUCCESS
19+
\[main\.pointer_dereference\.12] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)j\]: SUCCESS
2020
^VERIFICATION SUCCESSFUL$
2121
--
2222
--

‎regression/cbmc-primitives/forall_6231_3/test.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@ test.c
44
^EXIT=0$
55
^SIGNAL=0$
66
\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
7-
\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed long int\)i\]: SUCCESS
8-
\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed long int\)i\]: SUCCESS
9-
\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed long int\)i\]: SUCCESS
10-
\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed long int\)i\]: SUCCESS
11-
\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: SUCCESS
12-
\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
7+
\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
8+
\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
9+
\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
10+
\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
11+
\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
12+
\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
1313
^VERIFICATION SUCCESSFUL$
1414
--
1515
--

‎regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,12 @@ test_malloc_less_than_bound.c
44
^EXIT=10$
55
^SIGNAL=0$
66
\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
7-
\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed long int\)i\]: SUCCESS
8-
\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed long int\)i\]: SUCCESS
9-
\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed long int\)i\]: SUCCESS
10-
\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed long int\)i\]: SUCCESS
11-
\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: FAILURE
12-
\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
7+
\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
8+
\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
9+
\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
10+
\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
11+
\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE
12+
\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
1313
^VERIFICATION FAILED$
1414
--
1515
--

0 commit comments

Comments
 (0)