cprover
boolbv_member.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/base_type.h>
12 #include <util/byte_operators.h>
13 #include <util/arith_tools.h>
14 #include <util/c_types.h>
15 
17 {
18  const exprt &struct_op=expr.struct_op();
19  const typet &struct_op_type=ns.follow(struct_op.type());
20 
21  const bvt &struct_bv=convert_bv(struct_op);
22 
23  if(struct_op_type.id()==ID_union)
24  {
25  return convert_bv(
27  struct_op,
29  expr.type()));
30  }
31  else if(struct_op_type.id()==ID_struct)
32  {
33  const irep_idt &component_name=expr.get_component_name();
34  const struct_typet::componentst &components=
35  to_struct_type(struct_op_type).components();
36 
37  std::size_t offset=0;
38 
39  for(struct_typet::componentst::const_iterator
40  it=components.begin();
41  it!=components.end();
42  it++)
43  {
44  const typet &subtype=it->type();
45  std::size_t sub_width=boolbv_width(subtype);
46 
47  if(it->get_name()==component_name)
48  {
49  if(!base_type_eq(subtype, expr.type(), ns))
50  {
51  #if 0
52  std::cout << "DEBUG " << expr.pretty() << "\n";
53  #endif
54 
56  error() << "member: component type does not match: "
57  << subtype.pretty() << " vs. "
58  << expr.type().pretty() << eom;
59  throw 0;
60  }
61 
62  bvt bv;
63  bv.resize(sub_width);
64  assert(offset+sub_width<=struct_bv.size());
65 
66  for(std::size_t i=0; i<sub_width; i++)
67  bv[i]=struct_bv[offset+i];
68 
69  return bv;
70  }
71 
72  offset+=sub_width;
73  }
74 
76  error() << "component " << component_name
77  << " not found in structure" << eom;
78  throw 0;
79  }
80  else
81  {
83  error() << "member takes struct or union operand" << eom;
84  throw 0;
85  }
86 }
The type of an expression.
Definition: type.h:22
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:326
boolbv_widtht boolbv_width
Definition: boolbv.h:90
std::vector< componentt > componentst
Definition: std_types.h:243
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Extract member of struct or union.
Definition: std_expr.h:3869
const irep_idt & id() const
Definition: irep.h:259
Expression classes for byte-level operators.
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
const source_locationt & find_source_location() const
Definition: expr.cpp:246
source_locationt source_location
Definition: message.h:214
mstreamt & error() const
Definition: message.h:302
irep_idt byte_extract_id()
const namespacet & ns
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3909
irep_idt get_component_name() const
Definition: std_expr.h:3893
virtual bvt convert_member(const member_exprt &expr)
Base Type Computation.
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::vector< literalt > bvt
Definition: literal.h:200