cprover
Loading...
Searching...
No Matches
boolbv_array_of.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/arith_tools.h>
12#include <util/invariant.h>
13#include <util/std_types.h>
14
17{
19 expr.type().id() == ID_array, "array_of expression shall have array type");
20
21 const array_typet &array_type = expr.type();
22
23 if(is_unbounded_array(array_type))
24 return conversion_failed(expr);
25
26 std::size_t width=boolbv_width(array_type);
27
28 if(width==0)
29 {
30 // A zero-length array is acceptable;
31 // an element with unknown size is not.
32 if(boolbv_width(array_type.element_type()) == 0)
33 return conversion_failed(expr);
34 else
35 return bvt();
36 }
37
38 const exprt &array_size=array_type.size();
39
40 const auto size = numeric_cast<mp_integer>(array_size);
41
42 if(!size.has_value())
43 return conversion_failed(expr);
44
45 const bvt &tmp = convert_bv(expr.what());
46
48 *size * tmp.size() == width,
49 "total array bit width shall equal the number of elements times the "
50 "element bit with");
51
52 bvt bv;
53 bv.resize(width);
54
55 auto b_it = tmp.begin();
56
57 for(auto &b : bv)
58 {
59 b = *b_it;
60
61 b_it++;
62
63 if(b_it == tmp.end())
64 b_it = tmp.begin();
65 }
66
67 return bv;
68}
Array constructor from single element.
Definition std_expr.h:1411
const array_typet & type() const
Definition std_expr.h:1418
exprt & what()
Definition std_expr.h:1428
Arrays with given size.
Definition std_types.h:763
const exprt & size() const
Definition std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:777
bool is_unbounded_array(const typet &type) const override
Definition boolbv.cpp:547
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 bvt convert_array_of(const array_of_exprt &expr)
Flatten arrays constructed from a single element.
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition boolbv.cpp:84
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:99
Base class for all expressions.
Definition expr.h:54
const irep_idt & id() const
Definition irep.h:396
std::vector< literalt > bvt
Definition literal.h:201
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Pre-defined types.