From 02d09c585735b08e39c872cfe7318fd7465d53d0 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 1 Nov 2018 12:14:44 +0000
Subject: [PATCH 1/3] Use numeric_cast instead of to_integer

to_integer is deprecated and numeric_cast should be used instead.
---
 src/goto-programs/interpreter_evaluate.cpp | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index ebd3be06e57..554f3f78f3b 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -345,24 +345,28 @@ void interpretert::evaluate(
     }
     else if(expr.type().id() == ID_pointer)
     {
-      mp_integer i=0;
       if(expr.has_operands() && expr.op0().id()==ID_address_of)
       {
         evaluate(expr.op0(), dest);
         return;
       }
-      else if(expr.has_operands() && !to_integer(expr.op0(), i))
+      else if(expr.has_operands())
       {
-        dest.push_back(i);
-        return;
+        if(const auto i = numeric_cast<mp_integer>(expr.op0()))
+        {
+          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 if(!expr.has_operands())
       {
-        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)

From 87e33cef1a45e414d5f3ccd30754a7e30f462cbd Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 1 Nov 2018 12:21:21 +0000
Subject: [PATCH 2/3] Merge the expr.has_operands conditions in one if

This makes the conditions in the `if` a bit simpler.
---
 src/goto-programs/interpreter_evaluate.cpp | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 554f3f78f3b..3d780f79807 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -345,21 +345,21 @@ void interpretert::evaluate(
     }
     else if(expr.type().id() == ID_pointer)
     {
-      if(expr.has_operands() && expr.op0().id()==ID_address_of)
+      if(expr.has_operands())
       {
-        evaluate(expr.op0(), dest);
-        return;
-      }
-      else if(expr.has_operands())
-      {
-        if(const auto i = numeric_cast<mp_integer>(expr.op0()))
+        if(expr.op0().id() == ID_address_of)
+        {
+          evaluate(expr.op0(), dest);
+          return;
+        }
+        else if(const auto i = numeric_cast<mp_integer>(expr.op0()))
         {
           dest.push_back(*i);
           return;
         }
       }
       // check if expression is constant null pointer without operands
-      else if(!expr.has_operands())
+      else
       {
         const auto i = numeric_cast<mp_integer>(expr);
         if(i && i->is_zero())

From be08937b8f31b745c057f171a450cdd45e0b7c5f Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 1 Nov 2018 12:12:13 +0000
Subject: [PATCH 3/3] Make interpreter handle typecast in pointer expr

The interpreter would fail to interpret expressions of type pointer
which contained typecast. This fixes it by skiping the typecasts
that are encountered.
---
 src/goto-programs/interpreter_evaluate.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 3d780f79807..790a457df0a 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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.
@@ -347,12 +348,13 @@ void interpretert::evaluate(
     {
       if(expr.has_operands())
       {
-        if(expr.op0().id() == ID_address_of)
+        const exprt &object = skip_typecast(expr.op0());
+        if(object.id() == ID_address_of)
         {
-          evaluate(expr.op0(), dest);
+          evaluate(object, dest);
           return;
         }
-        else if(const auto i = numeric_cast<mp_integer>(expr.op0()))
+        else if(const auto i = numeric_cast<mp_integer>(object))
         {
           dest.push_back(*i);
           return;