We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent deeb26e commit 187395fCopy full SHA for 187395f
regression/cbmc/Float24/main.c
@@ -0,0 +1,6 @@
1
+int main()
2
+{
3
+ double d=5.1;
4
+ __CPROVER_assert(0, "");
5
+ return 0;
6
+}
regression/cbmc/Float24/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--win32 --xml-ui
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
7
+<full_lhs_value>5\.1</full_lhs_value>
8
+--
9
+^warning: ignoring
10
+<full_lhs_value>5\.1l</full_lhs_value>
src/ansi-c/expr2c.cpp
@@ -1847,7 +1847,8 @@ std::string expr2ct::convert_constant(
1847
// ANSI-C: double is default; float/long-double require annotation
1848
if(src.type()==float_type())
1849
dest+='f';
1850
- else if(src.type()==long_double_type())
+ else if(src.type()==long_double_type() &&
1851
+ double_type()!=long_double_type())
1852
dest+='l';
1853
}
1854
else if(dest.size()==4 &&
0 commit comments