Merge pull request #3255 from romainbrenguier/bugfix/typecast-in-interpreter

Fix typecast in interpreter

Author: romainbrenguier

src/goto-programs/interpreter_evaluate.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/string_container.h>
 
 #include <langapi/language_util.h>
+#include <util/expr_util.h>
 
 /// Reads a memory address and loads it into the `dest` variable.
 /// Marks cell as `READ_BEFORE_WRITTEN` if cell has never been written.
@@ -345,24 +346,29 @@ void interpretert::evaluate(
     }
     else if(expr.type().id() == ID_pointer)
     {
-      mp_integer i=0;
-      if(expr.has_operands() && expr.op0().id()==ID_address_of)
+      if(expr.has_operands())
       {
-        evaluate(expr.op0(), dest);
-        return;
-      }
-      else if(expr.has_operands() && !to_integer(expr.op0(), i))
-      {
-        dest.push_back(i);
-        return;
+        const exprt &object = skip_typecast(expr.op0());
+        if(object.id() == ID_address_of)
+        {
+          evaluate(object, dest);
+          return;
+        }
+        else if(const auto i = numeric_cast<mp_integer>(object))
+        {
+          dest.push_back(*i);
+          return;
+        }
       }
       // check if expression is constant null pointer without operands
-      else if(
-        !expr.has_operands() && !to_integer(to_constant_expr(expr), i) &&
-        i.is_zero())
+      else
       {
-        dest.push_back(i);
-        return;
+        const auto i = numeric_cast<mp_integer>(expr);
+        if(i && i->is_zero())
+        {
+          dest.push_back(*i);
+          return;
+        }
       }
     }
     else if(expr.type().id()==ID_floatbv)