File tree 2 files changed +12
-12
lines changed
regression/cbmc-primitives/exists_memory_checks 2 files changed +12
-12
lines changed Original file line number Diff line number Diff line change @@ -5,12 +5,12 @@ negated_exists.c
5
5
^SIGNAL=0$
6
6
^VERIFICATION SUCCESSFUL$
7
7
\[main\.assertion\.1\] line 9 assertion !__CPROVER_exists \{ int i; \(0 <= i && i < 10\) && a\[i\] == 42 \}: SUCCESS
8
- \[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[\(signed long int\)i\]: SUCCESS
9
- \[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[\(signed long int\)i\]: SUCCESS
10
- \[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[\(signed long int\)i\]: SUCCESS
11
- \[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[\(signed long int\)i\]: SUCCESS
12
- \[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: SUCCESS
13
- \[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
8
+ \[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[\(signed ( long|long long) int\)i\]: SUCCESS
9
+ \[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[\(signed ( long|long long) int\)i\]: SUCCESS
10
+ \[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[\(signed ( long|long long) int\)i\]: SUCCESS
11
+ \[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[\(signed ( long|long long) int\)i\]: SUCCESS
12
+ \[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[\(signed ( long|long long) int\)i\]: SUCCESS
13
+ \[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[\(signed ( long|long long) int\)i\]: SUCCESS
14
14
--
15
15
--
16
16
Check that memory checks pass for valid pointer dereferences inside a negated
Original file line number Diff line number Diff line change @@ -5,12 +5,12 @@ valid_index_range.c
5
5
^SIGNAL=0$
6
6
^VERIFICATION SUCCESSFUL$
7
7
\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 10\) && a\[i\] == i \*i \}: SUCCESS
8
- \[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[\(signed long int\)i\]: SUCCESS
9
- \[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[\(signed long int\)i\]: SUCCESS
10
- \[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[\(signed long int\)i\]: SUCCESS
11
- \[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[\(signed long int\)i\]: SUCCESS
12
- \[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[\(signed long int\)i\]: SUCCESS
13
- \[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[\(signed long int\)i\]: SUCCESS
8
+ \[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[\(signed ( long|long long) int\)i\]: SUCCESS
9
+ \[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[\(signed ( long|long long) int\)i\]: SUCCESS
10
+ \[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[\(signed ( long|long long) int\)i\]: SUCCESS
11
+ \[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[\(signed ( long|long long) int\)i\]: SUCCESS
12
+ \[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[\(signed ( long|long long) int\)i\]: SUCCESS
13
+ \[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[\(signed ( long|long long) int\)i\]: SUCCESS
14
14
--
15
15
--
16
16
Check that memory checks pass for valid pointer dereferences inside an
You can’t perform that action at this time.
0 commit comments