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 
12 {
13  const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
14 
15  std::size_t width=boolbv_width(struct_type);
16 
17  const struct_typet::componentst &components=struct_type.components();
18 
20  expr.operands().size() == components.size(),
21  "number of operands of a struct expression shall equal the number of"
22  "components as indicated by its type",
23  expr.find_source_location());
24 
25  bvt bv;
26  bv.resize(width);
27 
28  std::size_t bit_idx = 0;
29 
30  exprt::operandst::const_iterator op_it=expr.operands().begin();
31  for(const auto &comp : components)
32  {
33  const typet &subtype=comp.type();
34  const exprt &op=*op_it;
35 
37  subtype == op.type(),
38  "type of a struct expression operand shall equal the type of the "
39  "corresponding struct component",
40  expr.find_source_location(),
41  subtype.pretty(),
42  op.type().pretty());
43 
44  std::size_t subtype_width=boolbv_width(subtype);
45 
46  if(subtype_width!=0)
47  {
48  const bvt &op_bv = convert_bv(op, subtype_width);
49 
50  INVARIANT(
51  bit_idx + op_bv.size() <= width, "bit index shall be within bounds");
52 
53  for(const auto &bit : op_bv)
54  {
55  bv[bit_idx] = bit;
56  bit_idx++;
57  }
58  }
59 
60  ++op_it;
61  }
62 
63  INVARIANT(
64  bit_idx == width, "all bits in the bitvector shall have been assigned");
65 
66  return bv;
67 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:147
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
typet
The type of an expression, extends irept.
Definition: type.h:28
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:495
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:140
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1668
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
DATA_INVARIANT_WITH_DIAGNOSTICS
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:97
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:165
arrayst::ns
const namespacet & ns
Definition: arrays.h:54
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:40
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:231
boolbvt::convert_struct
virtual bvt convert_struct(const struct_exprt &expr)
Definition: boolbv_struct.cpp:11
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:92
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423