Merge pull request #2429 from tautschnig/vs-endian

Set little_endian in the same way that boolbv_byte_extract already does

Author: tautschnig

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -100,6 +100,9 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
   const exprt &op=expr.op();
   const exprt &offset=expr.offset();
+  PRECONDITION(
+    expr.id() == ID_byte_extract_little_endian ||
+    expr.id() == ID_byte_extract_big_endian);
   const bool little_endian = expr.id() == ID_byte_extract_little_endian;
 
   // first do op0

src/solvers/flattening/boolbv_byte_update.cpp

@@ -25,14 +25,10 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
   const exprt &offset_expr=expr.offset();
   const exprt &value=expr.value();
 
-  bool little_endian;
-
-  if(expr.id()==ID_byte_update_little_endian)
-    little_endian=true;
-  else if(expr.id()==ID_byte_update_big_endian)
-    little_endian=false;
-  else
-    UNREACHABLE;
+  PRECONDITION(
+    expr.id() == ID_byte_update_little_endian ||
+    expr.id() == ID_byte_update_big_endian);
+  const bool little_endian = expr.id() == ID_byte_update_little_endian;
 
   bvt bv=convert_bv(op);
 

src/solvers/flattening/flatten_byte_operators.cpp

@@ -201,14 +201,10 @@ exprt flatten_byte_extract(
 
   assert(src.operands().size()==2);
 
-  bool little_endian;
-
-  if(src.id()==ID_byte_extract_little_endian)
-    little_endian=true;
-  else if(src.id()==ID_byte_extract_big_endian)
-    little_endian=false;
-  else
-    UNREACHABLE;
+  PRECONDITION(
+    src.id() == ID_byte_extract_little_endian ||
+    src.id() == ID_byte_extract_big_endian);
+  const bool little_endian = src.id() == ID_byte_extract_little_endian;
 
   // determine an upper bound of the number of bytes we might need
   exprt upper_bound=size_of_expr(src.type(), ns);