Refactoring in boolbvt::convert_byte_extract

Author: romainbrenguier

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -19,34 +19,34 @@ Author: Daniel Kroening, [email protected]
 
 bvt map_bv(const endianness_mapt &map, const bvt &src)
 {
-  assert(map.number_of_bits()==src.size());
-
+  PRECONDITION(map.number_of_bits() == src.size());
   bvt result;
   result.resize(src.size(), const_literal(false));
-
   for(std::size_t i=0; i<src.size(); i++)
   {
-    size_t mapped_index=map.map_bit(i);
-    assert(mapped_index<src.size());
+    const size_t mapped_index = map.map_bit(i);
+    CHECK_RETURN(mapped_index < src.size());
     result[i]=src[mapped_index];
   }
-
   return result;
 }
 
 bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 {
-  if(expr.operands().size()!=2)
-    throw "byte_extract takes two operands";
+  PRECONDITION(expr.operands().size() == 2);
 
   // if we extract from an unbounded array, call the flattening code
   if(is_unbounded_array(expr.op().type()))
   {
-    exprt tmp=flatten_byte_extract(expr, ns);
+    const exprt tmp = flatten_byte_extract(expr, ns);
     return convert_bv(tmp);
   }
 
-  std::size_t width=boolbv_width(expr.type());
+  PRECONDITION(
+    expr.id() == ID_byte_extract_little_endian ||
+    expr.id() == ID_byte_extract_big_endian);
+
+  const std::size_t width = boolbv_width(expr.type());
 
   // special treatment for bit-fields and big-endian:
   // we need byte granularity
@@ -69,22 +69,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
   const exprt &op=expr.op();
   const exprt &offset=expr.offset();
-
-  bool little_endian;
-
-  if(expr.id()==ID_byte_extract_little_endian)
-    little_endian=true;
-  else if(expr.id()==ID_byte_extract_big_endian)
-    little_endian=false;
-  else
-  {
-    little_endian=false;
-    assert(false);
-  }
+  const bool little_endian = expr.id() == ID_byte_extract_little_endian;
 
   // first do op0
-
-  endianness_mapt op_map(op.type(), little_endian, ns);
+  const endianness_mapt op_map(op.type(), little_endian, ns);
   const bvt op_bv=map_bv(op_map, convert_bv(op));
 
   // do result