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: kroening

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:

src/util/c_types.cpp

@@ -184,99 +184,54 @@ unsignedbv_typet char32_t_type()
 
 bitvector_typet float_type()
 {
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(config.ansi_c.single_width);
-    result.set_integer_bits(config.ansi_c.single_width/2);
-    result.set(ID_C_c_type, ID_float);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::single_precision().to_type();
-    result.set(ID_C_c_type, ID_float);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::single_precision().to_type();
+  result.set(ID_C_c_type, ID_float);
+  return result;
 }
 
 bitvector_typet double_type()
 {
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(config.ansi_c.double_width);
-    result.set_integer_bits(config.ansi_c.double_width/2);
-    result.set(ID_C_c_type, ID_double);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::double_precision().to_type();
-    result.set(ID_C_c_type, ID_double);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::double_precision().to_type();
+  result.set(ID_C_c_type, ID_double);
+  return result;
 }
 
 bitvector_typet long_double_type()
 {
-  if(config.ansi_c.use_fixed_for_float)
+  floatbv_typet result;
+  if(config.ansi_c.long_double_width==128)
+    result=ieee_float_spect::quadruple_precision().to_type();
+  else if(config.ansi_c.long_double_width==64)
+    result=ieee_float_spect::double_precision().to_type();
+  else if(config.ansi_c.long_double_width==80)
   {
-    fixedbv_typet result;
-    result.set_width(config.ansi_c.long_double_width);
-    result.set_integer_bits(config.ansi_c.long_double_width/2);
-    result.set(ID_C_c_type, ID_long_double);
-    return result;
+    // x86 extended precision has 80 bits in total, and
+    // deviating from IEEE, does not use a hidden bit.
+    // We use the closest we have got, but the below isn't accurate.
+    result=ieee_float_spect(63, 15).to_type();
   }
-  else
+  else if(config.ansi_c.long_double_width==96)
   {
-    floatbv_typet result;
-    if(config.ansi_c.long_double_width==128)
-      result=ieee_float_spect::quadruple_precision().to_type();
-    else if(config.ansi_c.long_double_width==64)
-      result=ieee_float_spect::double_precision().to_type();
-    else if(config.ansi_c.long_double_width==80)
-    {
-      // x86 extended precision has 80 bits in total, and
-      // deviating from IEEE, does not use a hidden bit.
-      // We use the closest we have got, but the below isn't accurate.
-      result=ieee_float_spect(63, 15).to_type();
-    }
-    else if(config.ansi_c.long_double_width==96)
-    {
-      result=ieee_float_spect(80, 15).to_type();
-      // not quite right. The extra bits beyond 80 are usually padded.
-    }
-    else
-      INVARIANT(false, "width of long double");
-
-    result.set(ID_C_c_type, ID_long_double);
-
-    return result;
+    result=ieee_float_spect(80, 15).to_type();
+    // not quite right. The extra bits beyond 80 are usually padded.
   }
+  else
+    INVARIANT(false, "width of long double");
+
+  result.set(ID_C_c_type, ID_long_double);
+
+  return result;
 }
 
 bitvector_typet gcc_float128_type()
 {
   // not same as long double!
-
-  if(config.ansi_c.use_fixed_for_float)
-  {
-    fixedbv_typet result;
-    result.set_width(128);
-    result.set_integer_bits(128/2);
-    result.set(ID_C_c_type, ID_gcc_float128);
-    return result;
-  }
-  else
-  {
-    floatbv_typet result=
-      ieee_float_spect::quadruple_precision().to_type();
-    result.set(ID_C_c_type, ID_gcc_float128);
-    return result;
-  }
+  floatbv_typet result=
+    ieee_float_spect::quadruple_precision().to_type();
+  result.set(ID_C_c_type, ID_gcc_float128);
+  return result;
 }
 
 signedbv_typet pointer_diff_type()

src/util/config.cpp

@@ -739,7 +739,6 @@ bool configt::set(const cmdlinet &cmdline)
   ansi_c.single_precision_constant=false;
   ansi_c.for_has_scope=true; // C99 or later
   ansi_c.c_standard=ansi_ct::default_c_standard();
-  ansi_c.use_fixed_for_float=false;
   ansi_c.endianness=ansi_ct::endiannesst::NO_ENDIANNESS;
   ansi_c.os=ansi_ct::ost::NO_OS;
   ansi_c.arch="none";
@@ -791,12 +790,6 @@ bool configt::set(const cmdlinet &cmdline)
   if(cmdline.isset("include"))
     ansi_c.include_files=cmdline.get_values("include");
 
-  if(cmdline.isset("floatbv"))
-    ansi_c.use_fixed_for_float=false;
-
-  if(cmdline.isset("fixedbv"))
-    ansi_c.use_fixed_for_float=true;
-
   // the default architecture is the one we run on
   irep_idt this_arch=this_architecture();
   irep_idt arch=this_arch;
@@ -1142,7 +1135,6 @@ void configt::set_from_symbol_table(
 
   ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
   ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
-  ansi_c.use_fixed_for_float=unsigned_from_ns(ns, "fixed_for_float")!=0;
   // for_has_scope, single_precision_constant, rounding_mode not
   // stored in namespace
 

src/util/config.h

@@ -41,7 +41,6 @@ class configt
 
     // various language options
     bool char_is_unsigned, wchar_t_is_unsigned;
-    bool use_fixed_for_float;
     bool for_has_scope;
     bool single_precision_constant;
     enum class c_standardt { C89, C99, C11 } c_standard;