Skip to content

Commit 2d64aa8

Browse files
committed
ieee_floatt:one(...)
This adds ieee_floatt::one(...), as a convenience helper for generating an IEEE 754 number with the value one.
1 parent f9a7807 commit 2d64aa8

File tree

6 files changed

+29
-26
lines changed

6 files changed

+29
-26
lines changed

src/goto-programs/interpreter_evaluate.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -709,9 +709,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
709709
}
710710
else if(expr.type().id()==ID_floatbv)
711711
{
712-
ieee_floatt f(to_floatbv_type(expr.type()));
713-
f.from_integer(1);
714-
result=f.pack();
712+
result = ieee_floatt::one(to_floatbv_type(expr.type())).pack();
715713
}
716714
else
717715
result=1;

src/solvers/flattening/boolbv_typecast.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -204,10 +204,8 @@ bool boolbvt::type_conversion(
204204
// bool to float
205205

206206
// build a one
207-
ieee_floatt f(to_floatbv_type(dest_type));
208-
f.from_integer(1);
209-
210-
dest = convert_bv(f.to_expr());
207+
auto one = ieee_floatt::one(to_floatbv_type(dest_type));
208+
dest = convert_bv(one.to_expr());
211209

212210
INVARIANT(
213211
src_width == 1, "bitvector of type boolean shall have width one");

src/solvers/smt2/smt2_conv.cpp

Lines changed: 2 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -3066,29 +3066,12 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
30663066
{
30673067
constant_exprt val(irep_idt(), dest_type);
30683068

3069-
ieee_floatt a(dest_floatbv_type);
3070-
3071-
mp_integer significand;
3072-
mp_integer exponent;
3073-
30743069
out << "(ite ";
30753070
convert_expr(src);
30763071
out << " ";
3077-
3078-
significand = 1;
3079-
exponent = 0;
3080-
a.build(significand, exponent);
3081-
val.set_value(integer2bvrep(a.pack(), a.spec.width()));
3082-
3083-
convert_constant(val);
3072+
convert_constant(ieee_floatt::one(dest_floatbv_type).to_expr());
30843073
out << " ";
3085-
3086-
significand = 0;
3087-
exponent = 0;
3088-
a.build(significand, exponent);
3089-
val.set_value(integer2bvrep(a.pack(), a.spec.width()));
3090-
3091-
convert_constant(val);
3074+
convert_constant(ieee_floatt::zero(dest_floatbv_type).to_expr());
30923075
out << ")";
30933076
}
30943077
else if(src_type.id()==ID_c_bool)

src/util/ieee_float.cpp

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -470,6 +470,19 @@ void ieee_floatt::extract_base10(
470470
}
471471
}
472472

473+
ieee_floatt ieee_floatt::one(const ieee_float_spect &spec)
474+
{
475+
ieee_floatt result{spec};
476+
result.exponent = 0;
477+
result.fraction = power(2, result.spec.f);
478+
return result;
479+
}
480+
481+
ieee_floatt ieee_floatt::one(const floatbv_typet &type)
482+
{
483+
return one(ieee_float_spect{type});
484+
}
485+
473486
void ieee_floatt::build(
474487
const mp_integer &_fraction,
475488
const mp_integer &_exponent)

src/util/ieee_float.h

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -199,6 +199,16 @@ class ieee_floatt
199199
return result;
200200
}
201201

202+
static ieee_floatt zero(const ieee_float_spect &spec)
203+
{
204+
ieee_floatt result(spec);
205+
result.make_zero();
206+
return result;
207+
}
208+
209+
static ieee_floatt one(const floatbv_typet &);
210+
static ieee_floatt one(const ieee_float_spect &);
211+
202212
void make_NaN();
203213
void make_plus_infinity();
204214
void make_minus_infinity();

unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -150,6 +150,7 @@ SRC += analyses/ai/ai.cpp \
150150
util/get_base_name.cpp \
151151
util/graph.cpp \
152152
util/help_formatter.cpp \
153+
util/ieee_float.cpp \
153154
util/interval/add.cpp \
154155
util/interval/bitwise.cpp \
155156
util/interval/comparisons.cpp \

0 commit comments

Comments
 (0)