added a test for hexadecimal floating-point trace values

Author: Daniel Kroening

regression/cbmc/hex_trace/main.c

@@ -1,12 +1,15 @@
 int main()
 {
-	int a;
-	unsigned int b;
-	a = 0;
-	a = -100;
-	a = 2147483647;
-	b = a*2;
-	a = -2147483647;
-	__CPROVER_assert(0,"");
+  int a;
+  unsigned int b;
+  float f;
 
+  a = 0;
+  a = -100;
+  a = 2147483647;
+  b = a * 2;
+  a = -2147483647;
+  f = 0.1f;
+
+  __CPROVER_assert(0, "");
 }

regression/cbmc/hex_trace/test.desc

@@ -9,6 +9,7 @@ a=-100 \s*\(0xFFFFFF9C\)
 a=2147483647 \s*\(0x7FFFFFFF\)
 b=4294967294ul? \s*\(0xFFFFFFFE\)
 a=-2147483647 \s*\(0x80000001\)
+f=0\.1f \s*\(0x3DCCCCCD\)
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/solvers/floatbv/float_bv.cpp

@@ -105,7 +105,7 @@ exprt float_bvt::abs(const exprt &op, const ieee_float_spect &spec)
   // we mask away the sign bit, which is the most significant bit
   const mp_integer v = power(2, spec.width() - 1) - 1;
 
-  constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
+  const constant_exprt mask(integer2bvrep(v, spec.width()), op.type());
 
   return bitand_exprt(op, mask);
 }