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

16 bvt boolbvt::convert_floatbv_fma(const floatbv_fma_exprt &expr)

17{

18 float_utilst float_utils(prop);

19

20 float_utils.set_rounding_mode(convert_bv(expr.rounding_mode()));

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

22

23 bvt multiply_lhs = convert_bv(expr.op_multiply_lhs());

24 bvt multiply_rhs = convert_bv(expr.op_multiply_rhs());

25 bvt addend = convert_bv(expr.op_add());

26

27 return float_utils.fma(multiply_lhs, multiply_rhs, addend);

28}

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

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

virtual bvt convert_floatbv_fma(const floatbv_fma_exprt &)

Definition boolbv_floatbv_fma.cpp:16

exprt::type

typet & type()

Return the type of the expression.

Definition expr.h:85

float_utilst

Definition float_utils.h:18

floatbv_fma_exprt

Fused multiply-add expression: round(op0 * op1 + op2) with a single rounding.

Definition floatbv_expr.h:574

floatbv_fma_exprt::op_multiply_lhs

exprt & op_multiply_lhs()

Definition floatbv_expr.h:584

floatbv_fma_exprt::op_add

exprt & op_add()

Definition floatbv_expr.h:602

floatbv_fma_exprt::op_multiply_rhs

exprt & op_multiply_rhs()

Definition floatbv_expr.h:593

floatbv_fma_exprt::rounding_mode

exprt & rounding_mode()

Definition floatbv_expr.h:611

ieee_float_spect

Definition ieee_float.h:22

prop_conv_solvert::prop

propt & prop

Definition prop_conv_solver.h:130

float_utils.h

floatbv_expr.h

API to expression classes for floating-point arithmetic.

bvt

std::vector< literalt > bvt

Definition literal.h:201