cprover
Loading...
Searching...
No Matches
boolbv_struct.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include <util/namespace.h>
12
14{
15 const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
16
17 std::size_t width=boolbv_width(struct_type);
18
19 const struct_typet::componentst &components=struct_type.components();
20
22 expr.operands().size() == components.size(),
23 "number of operands of a struct expression shall equal the number of"
24 "components as indicated by its type",
26
27 bvt bv;
28 bv.resize(width);
29
30 std::size_t bit_idx = 0;
31
32 exprt::operandst::const_iterator op_it=expr.operands().begin();
33 for(const auto &comp : components)
34 {
35 const typet &subtype=comp.type();
36 const exprt &op=*op_it;
37
39 subtype == op.type(),
40 "type of a struct expression operand shall equal the type of the "
41 "corresponding struct component",
43 subtype.pretty(),
44 op.type().pretty());
45
46 std::size_t subtype_width=boolbv_width(subtype);
47
48 if(subtype_width!=0)
49 {
50 const bvt &op_bv = convert_bv(op, subtype_width);
51
53 bit_idx + op_bv.size() <= width, "bit index shall be within bounds");
54
55 for(const auto &bit : op_bv)
56 {
57 bv[bit_idx] = bit;
58 bit_idx++;
59 }
60 }
61
62 ++op_it;
63 }
64
66 bit_idx == width, "all bits in the bitvector shall have been assigned");
67
68 return bv;
69}
const namespacet & ns
Definition arrays.h:56
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
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:99
virtual bvt convert_struct(const struct_exprt &expr)
Base class for all expressions.
Definition expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:165
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
Struct constructor from list of elements.
Definition std_expr.h:1722
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
The type of an expression, extends irept.
Definition type.h:29
std::vector< literalt > bvt
Definition literal.h:201
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition invariant.h:511
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308