Refactoring in boolbvt::convert_byte_extract

Author: romainbrenguier

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -22,15 +22,14 @@ Author: Daniel Kroening, [email protected]
 
 bvt map_bv(const bv_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];
   }
 
@@ -39,15 +38,14 @@ bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
 
 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()))
   {
     try
     {
-      exprt tmp = flatten_byte_extract(expr, ns);
+      const exprt tmp = flatten_byte_extract(expr, ns);
       return convert_bv(tmp);
     }
     catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception)
@@ -57,7 +55,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
     }
   }
 
-  std::size_t width=boolbv_width(expr.type());
+  const std::size_t width = boolbv_width(expr.type());
 
   // special treatment for bit-fields and big-endian:
   // we need byte granularity
@@ -80,22 +78,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
-
-  bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width);
+  const bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width);
   const bvt op_bv=map_bv(op_map, convert_bv(op));
 
   // do result