diff --git a/regression/cbmc-primitives/r_w_ok_bug/test.desc b/regression/cbmc-primitives/r_w_ok_bug/test.desc index f1c4086cba7..e47b34c18b2 100644 --- a/regression/cbmc-primitives/r_w_ok_bug/test.desc +++ b/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$ diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc index a190cab817e..39d94af76fd 100644 --- a/regression/cbmc/Malloc23/test.desc +++ b/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 diff --git a/regression/cbmc/Malloc4/test.desc b/regression/cbmc/Malloc4/test.desc index a165ca3f6ea..ac6b317a781 100644 --- a/regression/cbmc/Malloc4/test.desc +++ b/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 diff --git a/regression/cbmc/Malloc5/test.desc b/regression/cbmc/Malloc5/test.desc index bb4ebdb3876..72b27267062 100644 --- a/regression/cbmc/Malloc5/test.desc +++ b/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 diff --git a/regression/cbmc/alloca1/test.desc b/regression/cbmc/alloca1/test.desc index 79c333b2257..66fa40a9537 100644 --- a/regression/cbmc/alloca1/test.desc +++ b/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 diff --git a/regression/cbmc/array_constraints1/test.desc b/regression/cbmc/array_constraints1/test.desc index 9d4f5476bc3..8040e5651bf 100644 --- a/regression/cbmc/array_constraints1/test.desc +++ b/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 diff --git a/regression/cbmc/pointer-extra-checks/test.desc b/regression/cbmc/pointer-extra-checks/test.desc index 5d6a062f3c1..b793e876bf8 100644 --- a/regression/cbmc/pointer-extra-checks/test.desc +++ b/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 diff --git a/regression/cbmc/pointer-overflow1/test.desc b/regression/cbmc/pointer-overflow1/test.desc index f075fb98df5..af678d78121 100644 --- a/regression/cbmc/pointer-overflow1/test.desc +++ b/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 diff --git a/regression/cbmc/pointer-overflow3/no-simplify.desc b/regression/cbmc/pointer-overflow3/no-simplify.desc index 7a98821d501..6a6134eb02b 100644 --- a/regression/cbmc/pointer-overflow3/no-simplify.desc +++ b/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 diff --git a/regression/cbmc/pointer-overflow3/test.desc b/regression/cbmc/pointer-overflow3/test.desc index 429f07b4f66..a82964bcaa3 100644 --- a/regression/cbmc/pointer-overflow3/test.desc +++ b/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 diff --git a/regression/cbmc/pointer-primitive-check-01/test.desc b/regression/cbmc/pointer-primitive-check-01/test.desc index ff46717e585..b188c0a0282 100644 --- a/regression/cbmc/pointer-primitive-check-01/test.desc +++ b/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 -- diff --git a/regression/cbmc/pointer-primitive-check-04/test.desc b/regression/cbmc/pointer-primitive-check-04/test.desc index 8b15168fcdb..b9dbbbb6893 100644 --- a/regression/cbmc/pointer-primitive-check-04/test.desc +++ b/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 -- diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc index d568171b1a6..6b04b86af6e 100644 --- a/regression/cbmc/union12/test.desc +++ b/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 diff --git a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc index c7418935086..20d6e0f8275 100644 --- a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc +++ b/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$ diff --git a/regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc b/regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc index 40c9b20f5aa..d37096e99bc 100644 --- a/regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc +++ b/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 -- diff --git a/regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc b/regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc index 0ed4b256468..2d09e75635c 100644 --- a/regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc +++ b/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 -- diff --git a/regression/goto-harness/pointer-to-array-function-parameters/test.desc b/regression/goto-harness/pointer-to-array-function-parameters/test.desc index e0092198354..f010f238e1b 100644 --- a/regression/goto-harness/pointer-to-array-function-parameters/test.desc +++ b/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$ -- diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 42d302cf5ab..59607ae6893 100644 --- a/src/analyses/goto_check.cpp +++ b/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")); }