cprover
boolbv_array_of.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/arith_tools.h>
12 #include <util/std_types.h>
13 
15 {
16  if(expr.type().id()!=ID_array)
17  throw "array_of must be array-typed";
18 
19  const array_typet &array_type=to_array_type(expr.type());
20 
21  if(is_unbounded_array(array_type))
22  return conversion_failed(expr);
23 
24  std::size_t width=boolbv_width(array_type);
25 
26  if(width==0)
27  {
28  // A zero-length array is acceptable;
29  // an element with unknown size is not.
30  if(boolbv_width(array_type.subtype())==0)
31  return conversion_failed(expr);
32  else
33  return bvt();
34  }
35 
36  const exprt &array_size=array_type.size();
37 
38  mp_integer size;
39 
40  if(to_integer(array_size, size))
41  return conversion_failed(expr);
42 
43  const bvt &tmp=convert_bv(expr.op0());
44 
45  bvt bv;
46  bv.resize(width);
47 
48  if(size*tmp.size()!=width)
49  throw "convert_array_of: unexpected operand width";
50 
51  std::size_t offset=0;
52 
53  for(mp_integer i=0; i<size; i=i+1)
54  {
55  for(std::size_t j=0; j<tmp.size(); j++, offset++)
56  bv[offset]=tmp[j];
57  }
58 
59  assert(offset==bv.size());
60 
61  return bv;
62 }
BigInt mp_integer
Definition: mp_arith.h:22
virtual bvt convert_array_of(const array_of_exprt &expr)
exprt & op0()
Definition: expr.h:72
boolbv_widtht boolbv_width
Definition: boolbv.h:90
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:259
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const exprt & size() const
Definition: std_types.h:1023
array constructor from single element
Definition: std_expr.h:1550
API to type classes.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
arrays with given size
Definition: std_types.h:1013
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
const typet & subtype() const
Definition: type.h:33
std::vector< literalt > bvt
Definition: literal.h:200