expr2c: Allow custom __CPROVER_fixedbv types together with double/float when using --fixedbv.

Pascal Kesseli · Pascal Kesseli · commit 48bfc7e8dad3 · 2016-10-06T10:29:02.000+01:00
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -276,24 +276,19 @@ std::string expr2ct::convert_rec(
   }
   else if(src.id()==ID_fixedbv)
   {
-    std::size_t width=to_fixedbv_type(src).get_width();
+    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;
-      else if(width==config.ansi_c.double_width)
+      if(width==config.ansi_c.double_width)
         return q+"double"+d;
-      else if(width==config.ansi_c.long_double_width)
+      if(width==config.ansi_c.long_double_width)
         return q+"long double"+d;
-      else
-        assert(false);
-    }
-    else
-    {
-      std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();
-      return q+"__CPROVER_fixedbv["+i2string(width)+"]["+i2string(fraction_bits)+"]";
     }
+    const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();
+    return q+"__CPROVER_fixedbv["+i2string(width)+"]["+i2string(fraction_bits)+"]"+d;
   }
   else if(src.id()==ID_c_bit_field)
   {

Original file line number	Diff line number	Diff line change
`@@ -276,24 +276,19 @@ std::string expr2ct::convert_rec(`
`276`	`276`	`}`
`277`	`277`	`else if(src.id()==ID_fixedbv)`
`278`	`278`	`{`
`279`		`- std::size_t width=to_fixedbv_type(src).get_width();`
	`279`	`+ const std::size_t width=to_fixedbv_type(src).get_width();`
`280`	`280`
`281`	`281`	`if(config.ansi_c.use_fixed_for_float)`
`282`	`282`	`{`
`283`	`283`	`if(width==config.ansi_c.single_width)`
`284`	`284`	`return q+"float"+d;`
`285`		`- else if(width==config.ansi_c.double_width)`
	`285`	`+ if(width==config.ansi_c.double_width)`
`286`	`286`	`return q+"double"+d;`
`287`		`- else if(width==config.ansi_c.long_double_width)`
	`287`	`+ if(width==config.ansi_c.long_double_width)`
`288`	`288`	`return q+"long double"+d;`
`289`		`- else`
`290`		`- assert(false);`
`291`		`- }`
`292`		`- else`
`293`		`- {`
`294`		`- std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();`
`295`		`- return q+"__CPROVER_fixedbv["+i2string(width)+"]["+i2string(fraction_bits)+"]";`
`296`	`289`	`}`
	`290`	`+ const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();`
	`291`	`+ return q+"__CPROVER_fixedbv["+i2string(width)+"]["+i2string(fraction_bits)+"]"+d;`
`297`	`292`	`}`
`298`	`293`	`else if(src.id()==ID_c_bit_field)`
`299`	`294`	`{`