remove the --fixedbv command-line option

The option was marked deprecated in January 2017.  A similar effect can be
achieved with #define float/double __CPROVER_fixedbv[].

Author: Daniel Kroening

regression/cbmc/Fixedbv4/main.c

@@ -1,61 +1,65 @@
+#include <assert.h>
+
+typedef __CPROVER_fixedbv[32][16] fbvt;
+
 int main()
 {
-  double f;
+  fbvt f;
 
   // addition
   assert(100.0+10==110);
   assert(0+f==f);
   assert(f+0==f);
   assert(100+0.5==100.5);
-  assert(0.0+0.0+f==f);
+  assert((fbvt)0.0+(fbvt)0.0+f==f);
 
   // subtraction
-  assert(100.0-10==90);
+  assert((fbvt)100.0-10==90);
   assert(0-f==-f);
   assert(f-0==f);
-  assert(100-0.5==99.5);
-  assert(0.0-0.0-f==-f);
+  assert((fbvt)100-(fbvt)0.5==(fbvt)99.5);
+  assert((fbvt)0.0-(fbvt)0.0-f==-f);
 
   // unary minus
-  assert(-(-100.0)==100);
-  assert(-(1-2.0)==1);
+  assert(-(fbvt)(-100.0)==100);
+  assert(-(1-(fbvt)2.0)==1);
   assert(-(-f)==f);
 
   // multiplication
-  assert(100.0*10==1000);
+  assert((fbvt)100.0*10==1000);
   assert(0*f==0);
   assert(f*0==0);
-  assert(100*0.5==50);
+  assert((fbvt)100*(fbvt)0.5==50);
   assert(f*1==f);
   assert(1*f==f);
-  assert(1.0*1.0*f==f);
+  assert((fbvt)1.0*(fbvt)1.0*f==f);
 
   // division
-  assert(100.0/1.0==100);
-  assert(100.1/1.0==100.1);
-  assert(100.0/2.0==50);
-  assert(100.0/0.5==200);
-  assert(0/1.0==0);
-  assert(f/1.0==f);
+  assert((fbvt)100.0/(fbvt)1.0==100);
+  assert((fbvt)100.1/(fbvt)1.0==(fbvt)100.1);
+  assert((fbvt)100.0/(fbvt)2.0==50);
+  assert((fbvt)100.0/(fbvt)0.5==200);
+  assert(0/(fbvt)1.0==0);
+  assert(f/(fbvt)1.0==f);
 
   // conversion
   assert(((double)(float)100)==100.0);
   assert(((unsigned int)100.0)==100.0);
   assert(100.0);
   assert(!0.0);
-  assert((int)0.5==0);
-  assert((int)0.49==0);
-  assert((int)-1.5==-1);
-  assert((int)-10.49==-10);
+  assert((int)(fbvt)0.5==0);
+  assert((int)(fbvt)0.49==0);
+  assert((int)(fbvt)-1.5==-1);
+  assert((int)(fbvt)-10.49==-10);
 
   // relations
-  assert(1.0<2.5);
-  assert(1.0<=2.5);
-  assert(1.01<=1.01);
-  assert(2.5>1.0);
-  assert(2.5>=1.0);
-  assert(1.01>=1.01);
-  assert(!(1.0>=2.5));
-  assert(!(1.0>2.5));
-  assert(1.0!=2.5);
+  assert((fbvt)1.0<(fbvt)2.5);
+  assert((fbvt)1.0<=(fbvt)2.5);
+  assert((fbvt)1.01<=(fbvt)1.01);
+  assert((fbvt)2.5>(fbvt)1.0);
+  assert((fbvt)2.5>=(fbvt)1.0);
+  assert((fbvt)1.01>=(fbvt)1.01);
+  assert(!((fbvt)1.0>=(fbvt)2.5));
+  assert(!((fbvt)1.0>(fbvt)2.5));
+  assert((fbvt)1.0!=(fbvt)2.5);
 }

regression/cbmc/Fixedbv4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---fixedbv
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Fixedbv6/main.c

@@ -1,27 +1,29 @@
+typedef __CPROVER_fixedbv[32][16] fbvt;
+
 int main()
 {
   // constants
-  assert(1.0!=2.0);
-  assert(1.0==1.0);
-  assert(1.0<2.0);
-  assert(!(-1.0<-2.0));
-  assert(2.0>1.0);
-  assert(!(-2.0>-1.0));
-  assert(!(2.0<2.0));
-  assert(!(-2.0<-2.0));
-  assert(!(2.0>2.0));
-  assert(!(-2.0>-2.0));
-  assert(2.0<=2.0);
-  assert(-2.0<=-2.0);
-  assert(2.0>=2.0);
-  assert(-2.0>=-2.0);
-  assert(1.0<=2.0);
-  assert(!(-1.0<=-2.0));
-  assert(2.0>=1.0);
-  assert(!(-2.0>=-1.0));
+  assert((fbvt)1.0!=(fbvt)2.0);
+  assert((fbvt)1.0==(fbvt)1.0);
+  assert((fbvt)1.0<(fbvt)2.0);
+  assert(!((fbvt)-1.0<(fbvt)-2.0));
+  assert((fbvt)2.0>(fbvt)1.0);
+  assert(!((fbvt)-2.0>(fbvt)-1.0));
+  assert(!((fbvt)2.0<(fbvt)2.0));
+  assert(!((fbvt)-2.0<(fbvt)-2.0));
+  assert(!((fbvt)2.0>(fbvt)2.0));
+  assert(!((fbvt)-2.0>(fbvt)-2.0));
+  assert((fbvt)2.0<=(fbvt)2.0);
+  assert((fbvt)-2.0<=(fbvt)-2.0);
+  assert((fbvt)2.0>=(fbvt)2.0);
+  assert((fbvt)-2.0>=(fbvt)-2.0);
+  assert((fbvt)1.0<=(fbvt)2.0);
+  assert(!((fbvt)-1.0<=(fbvt)-2.0));
+  assert((fbvt)2.0>=(fbvt)1.0);
+  assert(!((fbvt)-2.0>=(fbvt)-1.0));
 
   // variables
-  float a, b, _a=a, _b=b;
+  fbvt a, b, _a=a, _b=b;
   __CPROVER_assume(a==1 && b==2);
 
   assert(a!=b);

regression/cbmc/Fixedbv6/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---fixedbv
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Fixedbv7/main.c

@@ -1,61 +1,65 @@
+#include <assert.h>
+
+typedef __CPROVER_fixedbv[32][16] fbvt;
+
 int main()
 {
-  double f;
+  fbvt f;
 
   // addition
-  assert(100.0+10==110);
+  assert((fbvt)100.0+10==110);
   assert(0+f==f);
   assert(f+0==f);
-  assert(100+0.5==100.5);
-  assert(0.0+0.0+f==f);
+  assert(100+(fbvt)0.5==(fbvt)100.5);
+  assert((fbvt)0.0+(fbvt)0.0+f==f);
 
   // subtraction
-  assert(100.0-10==90);
+  assert((fbvt)100.0-10==90);
   assert(0-f==-f);
   assert(f-0==f);
-  assert(100-0.5==99.5);
-  assert(0.0-0.0-f==-f);
+  assert(100-(fbvt)0.5==(fbvt)99.5);
+  assert((fbvt)0.0-(fbvt)0.0-f==-f);
 
   // unary minus
-  assert(-(-100.0)==100);
-  assert(-(1-2.0)==1);
+  assert(-(fbvt)(-100.0)==100);
+  assert(-(1-(fbvt)2.0)==1);
   assert(-(-f)==f);
 
   // multiplication
-  assert(100.0*10==1000);
+  assert((fbvt)100.0*10==1000);
   assert(0*f==0);
   assert(f*0==0);
-  assert(100*0.5==50);
+  assert(100*(fbvt)0.5==50);
   assert(f*1==f);
   assert(1*f==f);
-  assert(1.0*1.0*f==f);
+  assert((fbvt)1.0*(fbvt)1.0*f==f);
 
   // division
-  assert(100.0/1.0==100);
-  assert(100.1/1.0==100.1);
-  assert(100.0/2.0==50);
-  assert(100.0/0.5==200);
-  assert(0/1.0==0);
-  assert(f/1.0==f);
+  assert((fbvt)100.0/(fbvt)1.0==100);
+  assert((fbvt)100.1/(fbvt)1.0==(fbvt)100.1);
+  assert((fbvt)100.0/(fbvt)2.0==50);
+  assert((fbvt)100.0/(fbvt)0.5==200);
+  assert(0/(fbvt)1.0==0);
+  assert(f/(fbvt)1.0==f);
 
   // conversion
-  assert(((double)(float)100)==100.0);
-  assert(((unsigned int)100.0)==100.0);
+  assert(((__CPROVER_fixedbv[40][16])(fbvt)100)==(__CPROVER_fixedbv[40][16])100.0);
+  assert(((unsigned int)(fbvt)100.0)==100.0);
   assert(100.0);
   assert(!0.0);
-  assert((int)0.5==0);
-  assert((int)0.49==0);
-  assert((int)-1.5==-1);
-  assert((int)-10.49==-10);
+  assert((int)(fbvt)0.5==0);
+  assert((int)(fbvt)0.49==0);
+  assert((int)(fbvt)-1.5==-1);
+  assert((int)(fbvt)-10.49==-10);
 
   // relations
-  assert(1.0<2.5);
-  assert(1.0<=2.5);
-  assert(1.01<=1.01);
-  assert(2.5>1.0);
-  assert(2.5>=1.0);
-  assert(1.01>=1.01);
-  assert(!(1.0>=2.5));
-  assert(!(1.0>2.5));
-  assert(1.0!=2.5);
+  assert((fbvt)1.0<(fbvt)2.5);
+  assert((fbvt)1.0<=(fbvt)2.5);
+  assert((fbvt)1.01<=(fbvt)1.01);
+  assert((fbvt)2.5>(fbvt)1.0);
+  assert((fbvt)2.5>=(fbvt)1.0);
+  assert((fbvt)1.01>=(fbvt)1.01);
+  assert(!((fbvt)1.0>=(fbvt)2.5));
+  assert(!((fbvt)1.0>(fbvt)2.5));
+  assert((fbvt)1.0!=(fbvt)2.5);
 }

regression/cbmc/Fixedbv7/test.desc

@@ -1,6 +1,6 @@
-CORE
+KNOWNBUG
 main.c
---fixedbv --no-simplify
+--no-simplify
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/ansi-c/ansi_c_internal_additions.cpp

@@ -243,7 +243,6 @@ void ansi_c_architecture_strings(std::string &code)
   code+=architecture_string(config.ansi_c.wchar_t_width, "wchar_t_width");
   code+=architecture_string(config.ansi_c.char_is_unsigned, "char_is_unsigned");
   code+=architecture_string(config.ansi_c.wchar_t_is_unsigned, "wchar_t_is_unsigned"); // NOLINT(whitespace/line_length)
-  code+=architecture_string(config.ansi_c.use_fixed_for_float, "fixed_for_float"); // NOLINT(whitespace/line_length)
   code+=architecture_string(config.ansi_c.alignment, "alignment");
   code+=architecture_string(config.ansi_c.memory_operand_size, "memory_operand_size"); // NOLINT(whitespace/line_length)
   code+=architecture_string(static_cast<int>(config.ansi_c.endianness), "endianness"); // NOLINT(whitespace/line_length)

src/ansi-c/expr2c.cpp

@@ -219,15 +219,6 @@ std::string expr2ct::convert_rec(
   {
     const std::size_t width=to_fixedbv_type(src).get_width();
 
-    if(config.ansi_c.use_fixed_for_float)
-    {
-      if(width==config.ansi_c.single_width)
-        return q+"float"+d;
-      if(width==config.ansi_c.double_width)
-        return q+"double"+d;
-      if(width==config.ansi_c.long_double_width)
-        return q+"long double"+d;
-    }
     const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();
     return
       q+"__CPROVER_fixedbv["+std::to_string(width)+"]["+

src/ansi-c/literals/convert_float_literal.cpp

@@ -80,60 +80,18 @@ exprt convert_float_literal(const std::string &src)
     // but these aren't handled anywhere
   }
 
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    unsigned width=result.type().get_int(ID_width);
-    unsigned fraction_bits;
-    const irep_idt integer_bits=result.type().get(ID_integer_bits);
-
-    assert(width!=0);
+  ieee_floatt a(to_floatbv_type(result.type()));
 
-    if(integer_bits==irep_idt())
-      fraction_bits=width/2; // default
-    else
-      fraction_bits=width-std::stoi(id2string(integer_bits));
-
-    mp_integer factor=mp_integer(1)<<fraction_bits;
-    mp_integer value=significand*factor;
-
-    if(value!=0)
-    {
-      if(exponent<0)
-        value/=power(base, -exponent);
-      else
-      {
-        value*=power(base, exponent);
-
-        if(value>=power(2, width-1))
-        {
-          // saturate: use "biggest value"
-          value=power(2, width-1)-1;
-        }
-        else if(value<=-power(2, width-1)-1)
-        {
-          // saturate: use "smallest value"
-          value=-power(2, width-1);
-        }
-      }
-    }
-
-    result.set(ID_value, integer2binary(value, width));
-  }
+  if(base==10)
+    a.from_base10(significand, exponent);
+  else if(base==2) // hex
+    a.build(significand, exponent);
   else
-  {
-    ieee_floatt a(to_floatbv_type(result.type()));
-
-    if(base==10)
-      a.from_base10(significand, exponent);
-    else if(base==2) // hex
-      a.build(significand, exponent);
-    else
-      assert(false);
+    assert(false);
 
-    result.set(
-      ID_value,
-      integer2binary(a.pack(), a.spec.width()));
-  }
+  result.set(
+    ID_value,
+    integer2binary(a.pack(), a.spec.width()));
 
   if(is_imaginary)
   {

src/cbmc/cbmc_parse_options.h

@@ -74,7 +74,7 @@ class optionst;
   OPT_FLUSH \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
-  "(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
+  "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 
 class cbmc_parse_optionst: