Support null-pointer without operand in interpreter

Matthias Güdemann · Matthias Güdemann · commit 624d1aa8205c · 2018-09-07T15:26:24.000+02:00
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
@@ -344,6 +344,12 @@ void interpretert::evaluate(
         dest.push_back(i);
         return;
       }
+      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
`@@ -344,6 +344,12 @@ void interpretert::evaluate(`
`344`	`344`	`dest.push_back(i);`
`345`	`345`	`return;`
`346`	`346`	`}`
	`347`	`+ else if(`
	`348`	`+ !expr.has_operands() && !to_integer(to_constant_expr(expr), i) &&`
	`349`	`+ i == 0)`
	`350`	`+ {`
	`351`	`+ dest.push_back(i);`
	`352`	`+ }`
`347`	`353`	`}`
`348`	`354`	`else if(expr.type().id()==ID_floatbv)`
`349`	`355`	`{`