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 #include <util/endianness_map.h>
14 
16 {
17  std::size_t width=boolbv_width(expr.type());
18 
19  if(width==0)
20  return conversion_failed(expr);
21 
22  const bvt &op_bv=convert_bv(expr.op());
23 
24  if(width<op_bv.size())
25  throw "union: unexpected operand op width";
26 
27  bvt bv;
28  bv.resize(width);
29 
31  {
32  for(std::size_t i=0; i<op_bv.size(); i++)
33  bv[i]=op_bv[i];
34 
35  // pad with nondets
36  for(std::size_t i=op_bv.size(); i<bv.size(); i++)
37  bv[i]=prop.new_variable();
38  }
39  else
40  {
41  assert(
43 
44  endianness_mapt map_u(expr.type(), false, ns);
45  endianness_mapt map_op(expr.op0().type(), false, ns);
46 
47  for(std::size_t i=0; i<op_bv.size(); i++)
48  bv[map_u.map_bit(i)]=op_bv[map_op.map_bit(i)];
49 
50  // pad with nondets
51  for(std::size_t i=op_bv.size(); i<bv.size(); i++)
52  bv[map_u.map_bit(i)]=prop.new_variable();
53  }
54 
55  return bv;
56 }
struct configt::ansi_ct ansi_c
Maps a big-endian offset to a little-endian offset.
exprt & op0()
Definition: expr.h:84
const exprt & op() const
Definition: std_expr.h:258
boolbv_widtht boolbv_width
Definition: boolbv.h:90
endiannesst endianness
Definition: config.h:75
typet & type()
Definition: expr.h:60
configt config
Definition: config.cpp:21
virtual literalt new_variable()=0
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
union constructor from single element
Definition: std_expr.h:1389
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const namespacet & ns
virtual bvt convert_union(const union_exprt &expr)
std::vector< literalt > bvt
Definition: literal.h:197