Merge pull request diffblue#1995 from tautschnig/byte-update-soundness

tautschnig · web-flow · commit 69fb74acb32f · 2018-04-04T18:57:42.000+01:00
[SV-COMP'18 6/19] Abort on byte_update(pointer)
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
@@ -441,6 +441,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   {
     return SUB::convert_byte_extract(to_byte_extract_expr(expr));
   }
+  else if(
+    expr.id() == ID_byte_update_little_endian ||
+    expr.id() == ID_byte_update_big_endian)
+  {
+    throw "byte-wise updates of pointers are unsupported";
+  }
 
   return conversion_failed(expr);
 }

Original file line number	Diff line number	Diff line change
`@@ -441,6 +441,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)`
`441`	`441`	`{`
`442`	`442`	`return SUB::convert_byte_extract(to_byte_extract_expr(expr));`
`443`	`443`	`}`
	`444`	`+ else if(`
	`445`	`+ expr.id() == ID_byte_update_little_endian \|\|`
	`446`	`+ expr.id() == ID_byte_update_big_endian)`
	`447`	`+ {`
	`448`	`+ throw "byte-wise updates of pointers are unsupported";`
	`449`	`+ }`
`444`	`450`
`445`	`451`	`return conversion_failed(expr);`
`446`	`452`	`}`