diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index ebd3be06e57..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 #include +#include /// 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(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(expr); + if(i && i->is_zero()) + { + dest.push_back(*i); + return; + } } } else if(expr.type().id()==ID_floatbv)