cprover
boolbv_struct.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/base_type.h>
13 
15 {
16  const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
17 
18  std::size_t width=boolbv_width(struct_type);
19 
20  const struct_typet::componentst &components=struct_type.components();
21 
22  if(expr.operands().size()!=components.size())
23  {
25  error() << "struct: wrong number of arguments" << eom;
26  throw 0;
27  }
28 
29  bvt bv;
30  bv.resize(width);
31 
32  std::size_t offset=0;
33 
34  exprt::operandst::const_iterator op_it=expr.operands().begin();
35  for(const auto &comp : components)
36  {
37  const typet &subtype=comp.type();
38  const exprt &op=*op_it;
39 
40  if(!base_type_eq(subtype, op.type(), ns))
41  {
43  error() << "struct: component type does not match: "
44  << subtype.pretty() << " vs. "
45  << op.type().pretty() << eom;
46  throw 0;
47  }
48 
49  std::size_t subtype_width=boolbv_width(subtype);
50 
51  if(subtype_width!=0)
52  {
53  const bvt &op_bv=convert_bv(op);
54 
55  assert(offset<width);
56  assert(op_bv.size()==subtype_width);
57  assert(offset+op_bv.size()<=width);
58 
59  for(std::size_t j=0; j<op_bv.size(); j++)
60  bv[offset+j]=op_bv[j];
61 
62  offset+=op_bv.size();
63  }
64 
65  ++op_it;
66  }
67 
68  assert(offset==width);
69 
70  return bv;
71 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
boolbv_widtht boolbv_width
Definition: boolbv.h:90
std::vector< componentt > componentst
Definition: std_types.h:240
virtual bvt convert_struct(const struct_exprt &expr)
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
Structure type.
Definition: std_types.h:296
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
const namespacet & ns
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Base class for all expressions.
Definition: expr.h:46
mstreamt & error()
Definition: message.h:223
Base Type Computation.
operandst & operands()
Definition: expr.h:70
struct constructor from list of elements
Definition: std_expr.h:1464
std::vector< literalt > bvt
Definition: literal.h:197