Add test for printing different float values in the trace

Author: Thomas Kiley

regression/cbmc/float-trace/test.c

@@ -0,0 +1,21 @@
+#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>
+--
+--