diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index cb35ef0cef9..b294efafa29 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -934,8 +934,6 @@ void goto_checkt::pointer_validity_check( local_bitvector_analysist::flagst flags= local_bitvector_analysis->get(t, pointer); - const typet &dereference_type=pointer_type.subtype(); - // For Java, we only need to check for null if(mode==ID_java) { @@ -1044,7 +1042,7 @@ void goto_checkt::pointer_validity_check( { const or_exprt dynamic_bounds( dynamic_object_lower_bound(pointer, ns, access_lb), - dynamic_object_upper_bound(pointer, dereference_type, ns, access_ub)); + dynamic_object_upper_bound(pointer, ns, access_ub)); add_guarded_claim( or_exprt( @@ -1065,7 +1063,7 @@ void goto_checkt::pointer_validity_check( { const or_exprt object_bounds( object_lower_bound(pointer, ns, access_lb), - object_upper_bound(pointer, dereference_type, ns, access_ub)); + object_upper_bound(pointer, ns, access_ub)); add_guarded_claim( or_exprt(allocs, dynamic_object(pointer), not_exprt(object_bounds)), diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 739f6dd1b07..17bf64ef4c8 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -394,7 +394,6 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( tmp_guard.add( dynamic_object_upper_bound( pointer_expr, - dereference_type, ns, size_of_expr(dereference_type, ns))); dereference_callback.dereference_failure( diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 966ebdae021..6c2fd0fab57 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -98,7 +98,7 @@ exprt good_pointer_def( not_exprt(dynamic_object_lower_bound(pointer, ns, nil_exprt())), not_exprt( dynamic_object_upper_bound( - pointer, dereference_type, ns, size_of_expr(dereference_type, ns))))); + pointer, ns, size_of_expr(dereference_type, ns))))); const and_exprt good_dynamic_tmp2( not_exprt(deallocated(pointer, ns)), good_dynamic_tmp1); @@ -113,7 +113,7 @@ exprt good_pointer_def( const or_exprt bad_other( object_lower_bound(pointer, ns, nil_exprt()), object_upper_bound( - pointer, dereference_type, ns, size_of_expr(dereference_type, ns))); + pointer, ns, size_of_expr(dereference_type, ns))); const or_exprt good_other(dynamic_object(pointer), not_exprt(bad_other)); @@ -158,7 +158,6 @@ exprt dynamic_object_lower_bound( exprt dynamic_object_upper_bound( const exprt &pointer, - const typet &dereference_type, const namespacet &ns, const exprt &access_size) { @@ -192,7 +191,6 @@ exprt dynamic_object_upper_bound( exprt object_upper_bound( const exprt &pointer, - const typet &dereference_type, const namespacet &ns, const exprt &access_size) { diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h index ca149cfbc83..a017f5d91ae 100644 --- a/src/util/pointer_predicates.h +++ b/src/util/pointer_predicates.h @@ -39,7 +39,6 @@ exprt dynamic_object_lower_bound( const exprt &offset); exprt dynamic_object_upper_bound( const exprt &pointer, - const typet &dereference_type, const namespacet &, const exprt &access_size); exprt object_lower_bound( @@ -48,7 +47,6 @@ exprt object_lower_bound( const exprt &offset); exprt object_upper_bound( const exprt &pointer, - const typet &dereference_type, const namespacet &, const exprt &access_size);