Support null-pointer without operand in interpreter

Matthias Güdemann · Matthias Güdemann · commit 8b3bfaac75df · 2018-09-07T17:27:09.000+02:00
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
@@ -339,11 +339,19 @@ void interpretert::evaluate(
         evaluate(expr.op0(), dest);
         return;
       }
-      if(expr.has_operands() && !to_integer(expr.op0(), i))
+      else if(
+        expr.has_operands() && !to_integer(to_constant_expr(expr.op0()), i))
       {
         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 == 0)
+      {
+        dest.push_back(i);
+      }
     }
     else if(expr.type().id()==ID_floatbv)
     {

Original file line number	Diff line number	Diff line change
`@@ -339,11 +339,19 @@ void interpretert::evaluate(`
`339`	`339`	`evaluate(expr.op0(), dest);`
`340`	`340`	`return;`
`341`	`341`	`}`
`342`		`- if(expr.has_operands() && !to_integer(expr.op0(), i))`
	`342`	`+ else if(`
	`343`	`+ expr.has_operands() && !to_integer(to_constant_expr(expr.op0()), i))`
`343`	`344`	`{`
`344`	`345`	`dest.push_back(i);`
`345`	`346`	`return;`
`346`	`347`	`}`
	`348`	`+ // check if expression is constant null pointer without operands`
	`349`	`+ else if(`
	`350`	`+ !expr.has_operands() && !to_integer(to_constant_expr(expr), i) &&`
	`351`	`+ i == 0)`
	`352`	`+ {`
	`353`	`+ dest.push_back(i);`
	`354`	`+ }`
`347`	`355`	`}`
`348`	`356`	`else if(expr.type().id()==ID_floatbv)`
`349`	`357`	`{`