remove the --fixedbv command-line option

CHANGELOG

@@ -4,6 +4,9 @@
   generate bodies for functions that don't have a body
   in the goto code. This supercedes the functionality
   of --undefined-function-is-assume-false
+* The --fixedbv command-line option has been removed
+  (it was marked deprecated in January 2017)
+
 
 5.8
 ===

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,8 +1,11 @@
-CORE
+KNOWNBUG
 main.c
---fixedbv --no-simplify
+--no-simplify
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+To make this work, conversion from floating-point numbers to fixed-point
+numbers is required in solvers/flattening/boolbv_typecast.cpp. Issue #2158.

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)+"]["+