Merge pull request #8455 from tautschnig/protect-value_is_zero_string

Mark constant_exprt::value_is_zero_string protected [depends-on: 8675]

Author: tautschnig

src/goto-programs/json_expr.cpp

@@ -51,9 +51,7 @@ static exprt simplify_json_expr(const exprt &src)
       // simplify expressions of the form &member(object, @class_identifier)
       return simplify_json_expr(object);
     }
-    else if(
-      object.id() == ID_index && to_index_expr(object).index().is_constant() &&
-      to_constant_expr(to_index_expr(object).index()).value_is_zero_string())
+    else if(object.id() == ID_index && to_index_expr(object).index() == 0)
     {
       // simplify expressions of the form  &array[0]
       return simplify_json_expr(to_index_expr(object).array());

src/util/simplify_expr_int.cpp

@@ -782,7 +782,7 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
       }
       else if(
         it->is_constant() && it->type().id() == ID_bv &&
-        to_constant_expr(*it).value_is_zero_string() &&
+        *it == to_bv_type(it->type()).all_zeros_expr() &&
         new_expr.operands().size() > 1)
       {
         it = new_expr.operands().erase(it);

src/util/std_expr.h

@@ -3133,8 +3133,6 @@ class constant_exprt : public nullary_exprt
     set(ID_value, value);
   }
 
-  bool value_is_zero_string() const;
-
   /// Returns true if \p expr has a pointer type and a value NULL; it also
   /// returns true when \p expr has value zero and NULL_is_zero is true; returns
   /// false in all other cases.
@@ -3166,6 +3164,9 @@ class constant_exprt : public nullary_exprt
   {
     check(expr, vm);
   }
+
+protected:
+  bool value_is_zero_string() const;
 };
 
 template <>

unit/goto-symex/goto_symex_state.cpp

@@ -173,8 +173,7 @@ SCENARIO(
           const symbol_exprt object_symbol =
             to_symbol_expr(object_descriptor->object());
           REQUIRE(object_symbol.get_identifier() == "int_value!0");
-          REQUIRE(to_constant_expr(object_descriptor->offset())
-                    .value_is_zero_string());
+          REQUIRE(object_descriptor->offset() == 0);
         }
         THEN("The target equations are unchanged")
         {