Skip to content

Commit e6f81cf

Browse files
author
kroening
committed
more float_bvt
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3251 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
1 parent 21de424 commit e6f81cf

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/solvers/floatbv/float_bv.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ exprt float_bvt::convert_abs(const abs_exprt &src)
6060

6161
constant_exprt mask(mask_str, src.type());
6262

63-
// return bitand_exprt(src.op(), mask);
63+
return bitand_exprt(src.op(), mask);
6464
}
6565

6666
/*******************************************************************\
@@ -87,7 +87,7 @@ exprt float_bvt::convert_unary_minus(const unary_minus_exprt &src)
8787

8888
constant_exprt mask(mask_str, src.type());
8989

90-
// return bitxor_exprt(src.op(), mask);
90+
return bitxor_exprt(src.op(), mask);
9191
}
9292

9393
/*******************************************************************\
@@ -104,6 +104,7 @@ Function: float_bvt::convert_ieee_float_equal
104104

105105
exprt float_bvt::convert_ieee_float_equal(const ieee_float_equal_exprt &src)
106106
{
107+
return nil_exprt();
107108
}
108109

109110
/*******************************************************************\

0 commit comments

Comments
 (0)