Add test for printing different float values in the trace

Author: Thomas Kiley

regression/cbmc/float-trace/test.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+#include <stdbool.h>
+
+int main()
+{
+  float zero = 0.0f;
+  float one = 1.0f;
+  double dzero = 0.0;
+  float complex = 0x1p+37f;
+
+  assert(false);
+
+  return 0;
+}
+
+void test(float value)
+{
+  assert(value == 1.0f);
+  assert(value == 0.0f);
+}

regression/cbmc/float-trace/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--trace --xml-ui
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+<full_lhs_value binary="00000000000000000000000000000000">0.0f</full_lhs_value>
+<full_lhs_value binary="00111111100000000000000000000000">1.0f</full_lhs_value>
+<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">0.0</full_lhs_value>
+<full_lhs_value binary="01010010000000000000000000000000">1\.374390e\+11f</full_lhs_value>
+--
+--