Merge pull request #3009 from diffblue/goto-interpreter-bugfix

tautschnig · web-flow · commit 8d396f3b13ac · 2018-09-24T16:51:28.000+01:00
bugfix: array literals are array_exprt, not constant_exprt
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
@@ -551,7 +551,7 @@ exprt interpretert::get_value(
   }
   else if(real_type.id()==ID_array)
   {
-    constant_exprt result(type);
+    array_exprt result(to_array_type(real_type));
     const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
 
     // Get size of array
@@ -603,12 +603,7 @@ exprt interpretert::get_value(
   else if(real_type.id() == ID_pointer)
   {
     if(rhs[integer2size_t(offset)]==0)
-    {
-      // NULL pointer
-      constant_exprt result(type);
-      result.set_value(ID_NULL);
-      return result;
-    }
+      return null_pointer_exprt(to_pointer_type(real_type)); // NULL pointer
 
     if(rhs[integer2size_t(offset)]<memory.size())
     {

Original file line number	Diff line number	Diff line change
`@@ -551,7 +551,7 @@ exprt interpretert::get_value(`
`551`	`551`	`}`
`552`	`552`	`else if(real_type.id()==ID_array)`
`553`	`553`	`{`
`554`		`- constant_exprt result(type);`
	`554`	`+ array_exprt result(to_array_type(real_type));`
`555`	`555`	`const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));`
`556`	`556`
`557`	`557`	`// Get size of array`
`@@ -603,12 +603,7 @@ exprt interpretert::get_value(`
`603`	`603`	`else if(real_type.id() == ID_pointer)`
`604`	`604`	`{`
`605`	`605`	`if(rhs[integer2size_t(offset)]==0)`
`606`		`- {`
`607`		`- // NULL pointer`
`608`		`- constant_exprt result(type);`
`609`		`- result.set_value(ID_NULL);`
`610`		`- return result;`
`611`		`- }`
	`606`	`+ return null_pointer_exprt(to_pointer_type(real_type)); // NULL pointer`
`612`	`607`
`613`	`608`	`if(rhs[integer2size_t(offset)]<memory.size())`
`614`	`609`	`{`