CBMC: /home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_floatbv_mod_rem.cpp Source File

15 bvt boolbvt::convert_floatbv_mod_rem(const binary_exprt &expr)

16{

17 // Note that the expressions do not have rounding modes

18 // but float_utils requires one.

19

20 float_utilst float_utils(prop);

21

22 auto rm = bv_utils.build_constant(ieee_floatt::ROUND_TO_EVEN, 32);

23 float_utils.set_rounding_mode(rm);

24

25 float_utils.spec = ieee_float_spect(to_floatbv_type(expr.type()));

26

27 bvt lhs_as_bv = convert_bv(expr.lhs());

28 bvt rhs_as_bv = convert_bv(expr.rhs());

29

30 // float_utilst::rem implements lhs-(lhs/rhs)*rhs, which matches

31 // neither fmod() nor IEEE

32 return float_utils.rem(lhs_as_bv, rhs_as_bv);

33}

bitvector_types.h

Pre-defined bitvector types.

to_floatbv_type

const floatbv_typet & to_floatbv_type(const typet &type)

Cast a typet to a floatbv_typet.

Definition bitvector_types.h:449

boolbv.h

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

binary_exprt

A base class for binary expressions.

Definition std_expr.h:649

binary_exprt::lhs

exprt & lhs()

Definition std_expr.h:679

binary_exprt::rhs

exprt & rhs()

Definition std_expr.h:689

boolbvt::convert_bv

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:40

boolbvt::bv_utils

bv_utilst bv_utils

Definition boolbv.h:121

boolbvt::convert_floatbv_mod_rem

virtual bvt convert_floatbv_mod_rem(const binary_exprt &)

Definition boolbv_floatbv_mod_rem.cpp:15

bv_utilst::build_constant

static bvt build_constant(const mp_integer &i, std::size_t width)

Definition bv_utils.cpp:16

exprt::type

typet & type()

Return the type of the expression.

Definition expr.h:85

float_utilst

Definition float_utils.h:18

ieee_float_spect

Definition ieee_float.h:22

ieee_floatt::ROUND_TO_EVEN

@ ROUND_TO_EVEN

Definition ieee_float.h:379

prop_conv_solvert::prop

propt & prop

Definition prop_conv_solver.h:130

float_utils.h

bvt

std::vector< literalt > bvt

Definition literal.h:201