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

[SV-COMP'18 6/19] Abort on byte_update(pointer)
diffblue · Apr 4, 2018 · 69fb74a · 69fb74a
2 parents 988b818 + 8300147
commit 69fb74a
Showing 1 changed file with 6 additions and 0 deletions.
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);
 }