Merge pull request #2410 from tautschnig/vs-deref-type

Remove unused parameter dereference_type

Author: kroening

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)),

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(

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)
 {

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);