CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
boolbv_if.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#include "boolbv.h"
11
13{
14 std::size_t width=boolbv_width(expr.type());
15
16 if(width==0)
17 return bvt(); // An empty bit-vector if.
18
19 literalt cond=convert(expr.cond());
20
21 const bvt &true_case_bv = convert_bv(expr.true_case(), width);
22 const bvt &false_case_bv = convert_bv(expr.false_case(), width);
23
25}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:39
virtual bvt convert_if(const if_exprt &expr)
Definition boolbv_if.cpp:12
bv_utilst bv_utils
Definition boolbv.h:118
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:103
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition bv_utils.cpp:95
typet & type()
Return the type of the expression.
Definition expr.h:84
The trinary if-then-else operator.
Definition std_expr.h:2497
exprt & cond()
Definition std_expr.h:2514
exprt & false_case()
Definition std_expr.h:2534
exprt & true_case()
Definition std_expr.h:2524
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
std::vector< literalt > bvt
Definition literal.h:201