cprover
boolbv_union.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/arith_tools.h>
12 #include <util/config.h>
13 
14 #include "bv_endianness_map.h"
15 
17 {
18  std::size_t width=boolbv_width(expr.type());
19 
20  if(width==0)
21  return conversion_failed(expr);
22 
23  const bvt &op_bv=convert_bv(expr.op());
24 
25  if(width<op_bv.size())
26  throw "union: unexpected operand op width";
27 
28  bvt bv;
29  bv.resize(width);
30 
32  {
33  for(std::size_t i=0; i<op_bv.size(); i++)
34  bv[i]=op_bv[i];
35 
36  // pad with nondets
37  for(std::size_t i=op_bv.size(); i<bv.size(); i++)
38  bv[i]=prop.new_variable();
39  }
40  else
41  {
42  assert(
44 
45  bv_endianness_mapt map_u(expr.type(), false, ns, boolbv_width);
46  bv_endianness_mapt map_op(expr.op0().type(), false, ns, boolbv_width);
47 
48  for(std::size_t i=0; i<op_bv.size(); i++)
49  bv[map_u.map_bit(i)]=op_bv[map_op.map_bit(i)];
50 
51  // pad with nondets
52  for(std::size_t i=op_bv.size(); i<bv.size(); i++)
53  bv[map_u.map_bit(i)]=prop.new_variable();
54  }
55 
56  return bv;
57 }
struct configt::ansi_ct ansi_c
exprt & op0()
Definition: expr.h:72
const exprt & op() const
Definition: std_expr.h:340
boolbv_widtht boolbv_width
Definition: boolbv.h:90
endiannesst endianness
Definition: config.h:76
typet & type()
Definition: expr.h:56
configt config
Definition: config.cpp:23
virtual literalt new_variable()=0
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
union constructor from single element
Definition: std_expr.h:1730
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const namespacet & ns
virtual bvt convert_union(const union_exprt &expr)
Map bytes according to the configured endianness.
std::vector< literalt > bvt
Definition: literal.h:200