Remove unnecessary use of dynamic_object

dynamic_object() was used as left-hand side of an implication despite the
right-hand side being independent of that condition. This avoids generating
duplicate assertions, as witnessed by the changes to regression tests.

Author: tautschnig

regression/cbmc-primitives/r_w_ok_bug/test.desc

@@ -1,9 +1,8 @@
 CORE
 main.c
 --pointer-check --no-simplify --no-propagation
-^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside dynamic object bounds in \*p1: FAILURE$
 ^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$
-^\*\* 2 of \d+ failed
+^\*\* 1 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Malloc23/test.desc

@@ -3,10 +3,10 @@ main.c
 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-pointer outside dynamic object bounds in \*p: FAILURE
-pointer outside dynamic object bounds in \*p: FAILURE
-pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
-pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
+pointer outside object bounds in \*p: FAILURE
+pointer outside object bounds in \*p: FAILURE
+pointer outside object bounds in p2\[.*1\]: FAILURE
+pointer outside object bounds in p2\[.*0\]: FAILURE
 \*\* 4 of [0-9]+ failed
 --
 ^warning: ignoring

regression/cbmc/Malloc4/test.desc

@@ -4,6 +4,6 @@ main.c
 ^SIGNAL=0$
 ^EXIT=10$
 ^VERIFICATION FAILED$
-^\[analyze_this.pointer_dereference.5\] line 19 dereference failure: pointer outside dynamic object bounds in p->i: FAILURE$
+^\[analyze_this.pointer_dereference.5\] line 19 dereference failure: pointer outside object bounds in p->i: FAILURE$
 --
 ^warning: ignoring

regression/cbmc/Malloc5/test.desc

@@ -4,6 +4,6 @@ main.c
 ^SIGNAL=0$
 ^EXIT=10$
 ^VERIFICATION FAILED$
-^\[analyze_this.pointer_dereference.5\] line 16 dereference failure: pointer outside dynamic object bounds in \*p_int: FAILURE$
+^\[analyze_this.pointer_dereference.5\] line 16 dereference failure: pointer outside object bounds in \*p_int: FAILURE$
 --
 ^warning: ignoring

regression/cbmc/alloca1/test.desc

@@ -5,6 +5,6 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 free called for stack-allocated object: FAILURE$
-^\*\* 1 of 13 failed
+^\*\* 1 of 12 failed
 --
 ^warning: ignoring

regression/cbmc/array_constraints1/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 2 of 16
+^\*\* 2 of 14
 --
 ^warning: ignoring

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

@@ -12,9 +12,8 @@ main.c
 ^\[main.pointer_dereference.7\] .* dereference failure: pointer invalid in \*s: FAILURE$
 ^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$
 ^\[main.pointer_dereference.9\] .* dereference failure: dead object in \*s: FAILURE$
-^\[main.pointer_dereference.10\] .* dereference failure: pointer outside dynamic object bounds in \*s: FAILURE$
-^\[main.pointer_dereference.11\] .* dereference failure: pointer outside object bounds in \*s: FAILURE$
-^\[main.pointer_dereference.12\] .* dereference failure: invalid integer address in \*s: FAILURE$
+^\[main.pointer_dereference.10\] .* dereference failure: pointer outside object bounds in \*s: FAILURE$
+^\[main.pointer_dereference.11\] .* dereference failure: invalid integer address in \*s: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc/pointer-overflow1/test.desc

@@ -3,14 +3,14 @@ main.c
 --pointer-overflow-check --unsigned-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.pointer_arithmetic\.\d+\] line 8 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
-^\[main\.pointer_arithmetic\.\d+\] line 9 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 8 pointer arithmetic: pointer outside object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 9 pointer arithmetic: pointer outside object bounds in .*: FAILURE
 ^\[main\.overflow\.\d+\] line 10 (pointer )?arithmetic overflow on .*: FAILURE
-^\[main\.pointer_arithmetic\.\d+\] line 10 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
-^\[main\.pointer_arithmetic\.\d+\] line 11 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
-^\[main\.pointer_arithmetic\.\d+\] line 12 pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 10 pointer arithmetic: pointer outside object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 11 pointer arithmetic: pointer outside object bounds in .*: FAILURE
+^\[main\.pointer_arithmetic\.\d+\] line 12 pointer arithmetic: pointer outside object bounds in .*: FAILURE
 ^VERIFICATION FAILED$
 --
 ^\[main\.overflow\.\d+\] line 1[45] (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
-^\[main\.overflow\.\d+\] line 1[45] pointer arithmetic: pointer outside dynamic object bounds in .*: FAILURE
+^\[main\.overflow\.\d+\] line 1[45] pointer arithmetic: pointer outside object bounds in .*: FAILURE
 ^warning: ignoring

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

@@ -1,8 +1,8 @@
 CORE broken-smt-backend
 main.c
 --pointer-overflow-check --no-simplify
-^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
-^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE
 ^\*\* 4 of \d+ failed

regression/cbmc/pointer-overflow3/test.desc

@@ -1,8 +1,8 @@
 CORE
 main.c
 --pointer-overflow-check
-^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
-^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE
 ^\*\* 4 of \d+ failed

regression/cbmc/pointer-primitive-check-01/test.desc

@@ -6,38 +6,31 @@ main.c
 \[main.pointer_primitives.1\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
 \[main.pointer_primitives.2\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
 \[main.pointer_primitives.3\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
-\[main.pointer_primitives.4\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
-\[main.pointer_primitives.5\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
-\[main.pointer_primitives.6\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
-\[main.pointer_primitives.7\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
-\[main.pointer_primitives.8\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
-\[main.pointer_primitives.9\] line \d+ pointer outside dynamic object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
-\[main.pointer_primitives.10\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
-\[main.pointer_primitives.11\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
-\[main.pointer_primitives.12\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
-\[main.pointer_primitives.13\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
-\[main.pointer_primitives.14\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
-\[main.pointer_primitives.15\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
-\[main.pointer_primitives.16\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
-\[main.pointer_primitives.17\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
-\[main.pointer_primitives.18\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
-\[main.pointer_primitives.19\] line \d+ pointer outside dynamic object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
-\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
-\[main.pointer_primitives.21\] line \d+ pointer invalid in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.23\] line \d+ dead object in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.24\] line \d+ pointer outside dynamic object bounds in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.25\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.26\] line \d+ pointer invalid in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.27\] line \d+ deallocated dynamic object in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.28\] line \d+ dead object in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.29\] line \d+ pointer outside dynamic object bounds in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.30\] line \d+ pointer outside object bounds in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.31\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
-\[main.pointer_primitives.32\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
-\[main.pointer_primitives.33\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
-\[main.pointer_primitives.34\] line \d+ pointer outside dynamic object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
-\[main.pointer_primitives.35\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
+\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
+\[main.pointer_primitives.5\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
+\[main.pointer_primitives.6\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
+\[main.pointer_primitives.7\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
+\[main.pointer_primitives.8\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
+\[main.pointer_primitives.9\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
+\[main.pointer_primitives.10\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
+\[main.pointer_primitives.11\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
+\[main.pointer_primitives.12\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
+\[main.pointer_primitives.13\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
+\[main.pointer_primitives.14\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
+\[main.pointer_primitives.15\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
+\[main.pointer_primitives.16\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
+\[main.pointer_primitives.17\] line \d+ pointer invalid in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
+\[main.pointer_primitives.18\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): SUCCESS
+\[main.pointer_primitives.19\] line \d+ dead object in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): SUCCESS
+\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
+\[main.pointer_primitives.21\] line \d+ pointer invalid in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
+\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): SUCCESS
+\[main.pointer_primitives.23\] line \d+ dead object in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): SUCCESS
+\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
+\[main.pointer_primitives.25\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
+\[main.pointer_primitives.26\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
+\[main.pointer_primitives.27\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
+\[main.pointer_primitives.28\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
 --
 ^warning: ignoring
 --

regression/cbmc/pointer-primitive-check-04/test.desc

@@ -6,8 +6,7 @@ main.c
 \[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
 \[main.pointer_primitives.2\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): SUCCESS
 \[main.pointer_primitives.3\] line \d+ dead object in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): SUCCESS
-\[main.pointer_primitives.4\] line \d+ pointer outside dynamic object bounds in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
-\[main.pointer_primitives.5\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
+\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
 --
 ^warning: ignoring
 --

regression/cbmc/union12/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.assertion\.2\] line 20 should fail: FAILURE$
-^\*\* 1 of 17 failed
+^\*\* 1 of 15 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/goto-analyzer/value-set-function-pointers-structs/test.desc

@@ -5,7 +5,7 @@ main.c
 ^file main.c line 46 function main: replacing function pointer by 2 possible targets$
 ^file main.c line 54 function main: replacing function pointer by 2 possible targets$
 ^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
-^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end @ \[30, 32\]} @ \[30, 32\]
+^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end @ \[29, 31\]} @ \[29, 31\]
 ^main::1::fun2 \(\) -> value-set-begin: ptr ->\(g\) :value-set-end
 ^EXIT=0$
 ^SIGNAL=0$

regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc

@@ -3,6 +3,6 @@ test.c
 --harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5
 ^EXIT=10$
 ^SIGNAL=0$
-\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE
+\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE
 VERIFICATION FAILED
 --

regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc

@@ -7,6 +7,5 @@ test.c
 \[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
 \[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
 \[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
-\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
-\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
+\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
 --

regression/goto-harness/pointer-to-array-function-parameters/test.desc

@@ -1,8 +1,8 @@
 CORE
 test.c
 --harness-type call-function --function test --treat-pointer-as-array arr
-\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
-\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
+\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --

src/analyses/goto_check.cpp

@@ -2258,7 +2258,7 @@ goto_checkt::get_pointer_points_to_valid_memory_conditions(
       "dead object"));
   }
 
-  if(unknown || flags.is_dynamic_heap())
+  if(flags.is_dynamic_heap())
   {
     const or_exprt object_bounds_violation(
       object_lower_bound(address, nil_exprt()),
@@ -2267,8 +2267,7 @@ goto_checkt::get_pointer_points_to_valid_memory_conditions(
     conditions.push_back(conditiont(
       or_exprt(
         in_bounds_of_some_explicit_allocation,
-        implies_exprt(
-          dynamic_object(address), not_exprt(object_bounds_violation))),
+        not_exprt(object_bounds_violation)),
       "pointer outside dynamic object bounds"));
   }
 
@@ -2281,9 +2280,7 @@ goto_checkt::get_pointer_points_to_valid_memory_conditions(
     conditions.push_back(conditiont(
       or_exprt(
         in_bounds_of_some_explicit_allocation,
-        implies_exprt(
-          not_exprt(dynamic_object(address)),
-          not_exprt(object_bounds_violation))),
+        not_exprt(object_bounds_violation)),
       "pointer outside object bounds"));
   }