Merge pull request #1320 from tautschnig/double-output

Do not add an "l" prefix to double constants when double==long double

Author: Daniel Kroening

regression/cbmc/Float24/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  double d=5.1;
+  __CPROVER_assert(0, "");
+  return 0;
+}

regression/cbmc/Float24/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--win32 --xml-ui
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+<full_lhs_value>5\.1</full_lhs_value>
+--
+^warning: ignoring
+<full_lhs_value>5\.1l</full_lhs_value>

src/ansi-c/expr2c.cpp

@@ -1859,7 +1859,8 @@ std::string expr2ct::convert_constant(
       // ANSI-C: double is default; float/long-double require annotation
       if(src.type()==float_type())
         dest+='f';
-      else if(src.type()==long_double_type())
+      else if(src.type()==long_double_type() &&
+              double_type()!=long_double_type())
         dest+='l';
     }
     else if(dest.size()==4 &&