cprover
boolbv_concatenation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #include "boolbv.h"
11 
13 {
14  std::size_t width=boolbv_width(expr.type());
15 
16  if(width==0)
17  return conversion_failed(expr);
18 
19  const exprt::operandst &operands=expr.operands();
20 
21  if(operands.empty())
22  throw "concatenation takes at least one operand";
23 
24  std::size_t offset=width;
25  bvt bv;
26  bv.resize(width);
27 
28  forall_expr(it, operands)
29  {
30  const bvt &op=convert_bv(*it);
31 
32  if(op.size()>offset)
33  throw "concatenation operand width too big";
34 
35  offset-=op.size();
36 
37  for(std::size_t i=0; i<op.size(); i++)
38  bv[offset+i]=op[i];
39  }
40 
41  if(offset!=0)
42  throw "concatenation operand width too small";
43 
44  return bv;
45 }
virtual bvt convert_concatenation(const exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:90
#define forall_expr(it, expr)
Definition: expr.h:28
typet & type()
Definition: expr.h:60
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
std::vector< exprt > operandst
Definition: expr.h:49
Base class for all expressions.
Definition: expr.h:46
operandst & operands()
Definition: expr.h:70
std::vector< literalt > bvt
Definition: literal.h:197