Skip to content

Commit 019a921

Browse files
authored
Merge pull request #6083 from tautschnig/no-dynamic_object
Remove unnecessary use of dynamic_object
2 parents 07380f6 + dfe2d55 commit 019a921

File tree

18 files changed

+56
-70
lines changed

18 files changed

+56
-70
lines changed

regression/cbmc-primitives/r_w_ok_bug/test.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
11
CORE
22
main.c
33
--pointer-check --no-simplify --no-propagation
4-
^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside dynamic object bounds in \*p1: FAILURE$
54
^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$
6-
^\*\* 2 of \d+ failed
5+
^\*\* 1 of \d+ failed
76
^VERIFICATION FAILED$
87
^EXIT=10$
98
^SIGNAL=0$

regression/cbmc/Malloc23/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ main.c
33
--pointer-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
pointer outside dynamic object bounds in \*p: FAILURE
7-
pointer outside dynamic object bounds in \*p: FAILURE
8-
pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
9-
pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
6+
pointer outside object bounds in \*p: FAILURE
7+
pointer outside object bounds in \*p: FAILURE
8+
pointer outside object bounds in p2\[.*1\]: FAILURE
9+
pointer outside object bounds in p2\[.*0\]: FAILURE
1010
\*\* 4 of [0-9]+ failed
1111
--
1212
^warning: ignoring

regression/cbmc/Malloc4/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^SIGNAL=0$
55
^EXIT=10$
66
^VERIFICATION FAILED$
7-
^\[analyze_this.pointer_dereference.5\] line 19 dereference failure: pointer outside dynamic object bounds in p->i: FAILURE$
7+
^\[analyze_this.pointer_dereference.5\] line 19 dereference failure: pointer outside object bounds in p->i: FAILURE$
88
--
99
^warning: ignoring

regression/cbmc/Malloc5/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^SIGNAL=0$
55
^EXIT=10$
66
^VERIFICATION FAILED$
7-
^\[analyze_this.pointer_dereference.5\] line 16 dereference failure: pointer outside dynamic object bounds in \*p_int: FAILURE$
7+
^\[analyze_this.pointer_dereference.5\] line 16 dereference failure: pointer outside object bounds in \*p_int: FAILURE$
88
--
99
^warning: ignoring

regression/cbmc/alloca1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ main.c
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
free called for stack-allocated object: FAILURE$
8-
^\*\* 1 of 13 failed
8+
^\*\* 1 of 12 failed
99
--
1010
^warning: ignoring

regression/cbmc/array_constraints1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
^\*\* 2 of 16
7+
^\*\* 2 of 14
88
--
99
^warning: ignoring

regression/cbmc/pointer-extra-checks/test.desc

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,8 @@ main.c
1212
^\[main.pointer_dereference.7\] .* dereference failure: pointer invalid in \*s: FAILURE$
1313
^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$
1414
^\[main.pointer_dereference.9\] .* dereference failure: dead object in \*s: FAILURE$
15-
^\[main.pointer_dereference.10\] .* dereference failure: pointer outside dynamic object bounds in \*s: FAILURE$
16-
^\[main.pointer_dereference.11\] .* dereference failure: pointer outside object bounds in \*s: FAILURE$
17-
^\[main.pointer_dereference.12\] .* dereference failure: invalid integer address in \*s: FAILURE$
15+
^\[main.pointer_dereference.10\] .* dereference failure: pointer outside object bounds in \*s: FAILURE$
16+
^\[main.pointer_dereference.11\] .* dereference failure: invalid integer address in \*s: FAILURE$
1817
^VERIFICATION FAILED$
1918
--
2019
^warning: ignoring

regression/cbmc/pointer-overflow1/test.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,14 @@ main.c
33
--pointer-overflow-check --unsigned-overflow-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main\.pointer_arithmetic\.\d+\] line 8 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
7-
^\[main\.pointer_arithmetic\.\d+\] line 9 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
6+
^\[main\.pointer_arithmetic\.\d+\] line 8 pointer arithmetic: pointer outside object bounds in .*: FAILURE
7+
^\[main\.pointer_arithmetic\.\d+\] line 9 pointer arithmetic: pointer outside object bounds in .*: FAILURE
88
^\[main\.overflow\.\d+\] line 10 (pointer )?arithmetic overflow on .*: FAILURE
9-
^\[main\.pointer_arithmetic\.\d+\] line 10 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
10-
^\[main\.pointer_arithmetic\.\d+\] line 11 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
11-
^\[main\.pointer_arithmetic\.\d+\] line 12 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
9+
^\[main\.pointer_arithmetic\.\d+\] line 10 pointer arithmetic: pointer outside object bounds in .*: FAILURE
10+
^\[main\.pointer_arithmetic\.\d+\] line 11 pointer arithmetic: pointer outside object bounds in .*: FAILURE
11+
^\[main\.pointer_arithmetic\.\d+\] line 12 pointer arithmetic: pointer outside object bounds in .*: FAILURE
1212
^VERIFICATION FAILED$
1313
--
1414
^\[main\.overflow\.\d+\] line 1[45] (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
15-
^\[main\.overflow\.\d+\] line 1[45] pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
15+
^\[main\.overflow\.\d+\] line 1[45] pointer arithmetic: pointer outside object bounds in .*: FAILURE
1616
^warning: ignoring

regression/cbmc/pointer-overflow3/no-simplify.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE broken-smt-backend
22
main.c
33
--pointer-overflow-check --no-simplify
4-
^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
5-
^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
4+
^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
5+
^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
66
^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
77
^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE
88
^\*\* 4 of \d+ failed

regression/cbmc/pointer-overflow3/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main.c
33
--pointer-overflow-check
4-
^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
5-
^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
4+
^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
5+
^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
66
^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
77
^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE
88
^\*\* 4 of \d+ failed

0 commit comments

Comments
 (0)