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 
12 {
13  const exprt &struct_op=expr.struct_op();
14  const typet &struct_op_type=ns.follow(struct_op.type());
15 
16  const bvt &struct_bv=convert_bv(struct_op);
17 
18  const irep_idt &component_name = expr.get_component_name();
19  const struct_union_typet::componentst &components =
20  to_struct_union_type(struct_op_type).components();
21 
22  std::size_t offset = 0;
23 
24  for(const auto &c : components)
25  {
26  const typet &subtype = c.type();
27  const std::size_t sub_width = boolbv_width(subtype);
28 
29  if(c.get_name() == component_name)
30  {
32  subtype == expr.type(),
33  "component type shall match the member expression type",
34  subtype.pretty(),
35  expr.type().pretty());
36  INVARIANT(
37  offset + sub_width <= struct_bv.size(),
38  "bitvector part corresponding to element shall be contained within the "
39  "full aggregate bitvector");
40 
41  return bvt(
42  struct_bv.begin() + offset, struct_bv.begin() + offset + sub_width);
43  }
44 
45  if(struct_op_type.id() != ID_union)
46  offset += sub_width;
47  }
48 
50  false,
51  "struct type shall contain component accessed by member expression",
52  expr.find_source_location(),
53  id2string(component_name));
54 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
boolbvt::convert_member
virtual bvt convert_member(const member_exprt &expr)
Definition: boolbv_member.cpp:11
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
INVARIANT_WITH_DIAGNOSTICS
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:438
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
DATA_INVARIANT_WITH_DIAGNOSTICS
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:512
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:231
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
irept::id
const irep_idt & id() const
Definition: irep.h:418
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
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
boolbv.h
validation_modet::INVARIANT
@ INVARIANT