cprover
boolbv_union.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/config.h
>
13
14
#include "
bv_endianness_map.h
"
15
16
bvt
boolbvt::convert_union
(
const
union_exprt
&expr)
17
{
18
std::size_t width=
boolbv_width
(expr.
type
());
19
20
if
(width==0)
21
return
conversion_failed
(expr);
22
23
const
bvt
&op_bv=
convert_bv
(expr.
op
());
24
25
INVARIANT
(
26
op_bv.size() <= width,
27
"operand bitvector width shall not be larger than the width indicated by "
28
"the union type"
);
29
30
bvt
bv;
31
bv.resize(width);
32
33
if
(
config
.
ansi_c
.
endianness
==
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
)
34
{
35
for
(std::size_t i=0; i<op_bv.size(); i++)
36
bv[i]=op_bv[i];
37
38
// pad with nondets
39
for
(std::size_t i=op_bv.size(); i<bv.size(); i++)
40
bv[i]=
prop
.
new_variable
();
41
}
42
else
43
{
44
INVARIANT
(
45
config
.
ansi_c
.
endianness
==
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
,
46
"endianness should be set to either little endian or big endian"
);
47
48
bv_endianness_mapt
map_u(expr.
type
(),
false
,
ns
,
boolbv_width
);
49
bv_endianness_mapt
map_op(expr.
op
().
type
(),
false
,
ns
,
boolbv_width
);
50
51
for
(std::size_t i=0; i<op_bv.size(); i++)
52
bv[map_u.
map_bit
(i)]=op_bv[map_op.
map_bit
(i)];
53
54
// pad with nondets
55
for
(std::size_t i=op_bv.size(); i<bv.size(); i++)
56
bv[map_u.
map_bit
(i)]=
prop
.
new_variable
();
57
}
58
59
return
bv;
60
}
arith_tools.h
bv_endianness_map.h
bvt
std::vector< literalt > bvt
Definition:
literal.h:201
bv_endianness_mapt
Map bytes according to the configured endianness.
Definition:
bv_endianness_map.h:21
union_exprt
Union constructor from single element.
Definition:
std_expr.h:1567
propt::new_variable
virtual literalt new_variable()=0
boolbvt::convert_union
virtual bvt convert_union(const union_exprt &expr)
Definition:
boolbv_union.cpp:16
configt::ansi_c
struct configt::ansi_ct ansi_c
exprt::type
typet & type()
Return the type of the expression.
Definition:
expr.h:81
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition:
boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition:
boolbv.h:113
arrayst::ns
const namespacet & ns
Definition:
arrays.h:51
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition:
endianness_map.h:48
unary_exprt::op
const exprt & op() const
Definition:
std_expr.h:281
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
config
configt config
Definition:
config.cpp:24
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
config.h
boolbv.h
configt::ansi_ct::endianness
endiannesst endianness
Definition:
config.h:77
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition:
prop_conv_solver.h:131
solvers
flattening
boolbv_union.cpp
Generated by
1.8.20