Rename variables in boolbv_extractbits for easier readability

Author: hannes-steffenhagen-diffblue

src/solvers/flattening/boolbv_extractbits.cpp

@@ -12,9 +12,9 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
+  const std::size_t bv_width = boolbv_width(expr.type());
 
-  if(width==0)
+  if(bv_width == 0)
     return conversion_failed(expr);
 
   if(expr.operands().size()!=3)
@@ -24,50 +24,52 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
     throw 0;
   }
 
-  mp_integer o1, o2;
-  const bvt &bv0=convert_bv(expr.op0());
+  mp_integer upper_as_int, lower_as_int;
+  auto const &src_bv = convert_bv(expr.src());
 
   // We only do constants for now.
   // Should implement a shift here.
-  if(to_integer(expr.op1(), o1) ||
-     to_integer(expr.op2(), o2))
+  if(
+    to_integer(expr.op1(), upper_as_int) ||
+    to_integer(expr.op2(), lower_as_int))
     return conversion_failed(expr);
 
-  if(o1<0 || o1>=bv0.size())
+  if(upper_as_int < 0 || upper_as_int >= src_bv.size())
   {
     error().source_location=expr.find_source_location();
     error() << "extractbits: second operand out of range: "
             << expr.pretty() << eom;
   }
 
-  if(o2<0 || o2>=bv0.size())
+  if(lower_as_int < 0 || lower_as_int >= src_bv.size())
   {
     error().source_location=expr.find_source_location();
     error() << "extractbits: third operand out of range: "
             << expr.pretty() << eom;
     throw 0;
   }
 
-  if(o2>o1)
-    std::swap(o1, o2);
+  if(lower_as_int > upper_as_int)
+    std::swap(upper_as_int, lower_as_int);
 
   // now lower_as_int <= upper_as_int
 
-  if((o1-o2+1)!=width)
+  if((upper_as_int - lower_as_int + 1) != bv_width)
   {
     error().source_location=expr.find_source_location();
-    error() << "extractbits: wrong width (expected " << (o1-o2+1)
-            << " but got " << width << "): " << expr.pretty() << eom;
+    error() << "extractbits: wrong width (expected "
+            << (upper_as_int - lower_as_int + 1) << " but got " << bv_width
+            << "): " << expr.pretty() << eom;
     throw 0;
   }
 
-  std::size_t offset=integer2unsigned(o2);
+  const std::size_t offset = integer2unsigned(lower_as_int);
 
-  bvt bv;
-  bv.resize(width);
+  bvt result_bv;
+  result_bv.resize(bv_width);
 
-  for(std::size_t i=0; i<width; i++)
-    bv[i]=bv0[offset+i];
+  for(std::size_t i = 0; i < bv_width; i++)
+    result_bv[i] = src_bv[offset + i];
 
-  return bv;
+  return result_bv;
 }