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 #include "boolbv.h"
10 
11 #include <util/invariant.h>
12 
14 {
15  std::size_t width=boolbv_width(expr.type());
16 
17  if(width==0)
18  return conversion_failed(expr);
19 
20  const exprt::operandst &operands=expr.operands();
21 
23  !operands.empty(), "concatentation shall have at least one operand");
24 
25  std::size_t offset=width;
26  bvt bv;
27  bv.resize(width);
28 
29  forall_expr(it, operands)
30  {
31  const bvt &op=convert_bv(*it);
32 
33  INVARIANT(
34  op.size() <= offset,
35  "concatentation operand must fit into the result bitvector");
36 
37  offset-=op.size();
38 
39  for(std::size_t i=0; i<op.size(); i++)
40  bv[offset+i]=op[i];
41  }
42 
43  INVARIANT(
44  offset == 0,
45  "all bits in the result bitvector must have been filled up by the "
46  "concatentation operands");
47 
48  return bv;
49 }
bvt
std::vector< literalt > bvt
Definition: literal.h:201
invariant.h
concatenation_exprt
Concatenation of bit-vector operands.
Definition: std_expr.h:4067
boolbvt::convert_concatenation
virtual bvt convert_concatenation(const concatenation_exprt &expr)
Definition: boolbv_concatenation.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:119
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:95
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:29
validation_modet::INVARIANT
@ INVARIANT