Merge pull request #3715 from diffblue/compile-time-rounding

test for compile-time rounding

Author: tautschnig

regression/cbmc/Float-rounding/compile_time_rounding.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+double THREE = 3;
+
+int main()
+{
+  // the rounding mode of the two '3' literals during
+  // the conversion to double should match
+  assert(THREE == 3);
+}

regression/cbmc/Float-rounding/compile_time_rounding.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+compile_time_rounding.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+the rounding mode of the two '3' literals during
+the conversion to double should match