Add additional tests for more types

Author: Thomas Kiley

regression/cbmc/float-trace/test.c

@@ -1,12 +1,20 @@
 #include <assert.h>
+#include <math.h>
 #include <stdbool.h>
 
 int main()
 {
   float zero = 0.0f;
   float one = 1.0f;
-  double dzero = 0.0;
   float complex = 0x1p+37f;
+  float inf = INFINITY;
+  float nan = NAN;
+
+  double dzero = 0.0;
+  double done = 1.0;
+  double dinf = INFINITY;
+  double dnan = NAN;
+  double dcomplex = -5.56268e-309;
 
   assert(false);
 

regression/cbmc/float-trace/test.desc

@@ -4,10 +4,28 @@ test.c
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-<full_lhs_value binary="00000000000000000000000000000000">0.0f</full_lhs_value>
+<full_lhs>zero</full_lhs>
+<full_lhs_value binary="0{32}">0.0f</full_lhs_value>
+<full_lhs>one</full_lhs>
 <full_lhs_value binary="00111111100000000000000000000000">1.0f</full_lhs_value>
-<full_lhs_value binary="0000000000000000000000000000000000000000000000000000000000000000">0.0</full_lhs_value>
+<full_lhs>complex</full_lhs>
 <full_lhs_value binary="01010010000000000000000000000000">1\.374390e\+11f</full_lhs_value>
+<full_lhs>inf</full_lhs>
+<full_lhs_value binary="01{8}0{23}">\+INFINITY</full_lhs_value>
+<full_lhs>nan</full_lhs>
+<full_lhs_value binary="01{8}[01]*1[01]*">\+NAN</full_lhs_value>
+<full_lhs_value binary="[01]{32}">\+NAN</full_lhs_value>
+<full_lhs>dzero</full_lhs>
+<full_lhs_value binary="0{64}">0.0</full_lhs_value>
+<full_lhs>done</full_lhs>
+<full_lhs_value binary="001{10}0{52}">1.0</full_lhs_value>
+<full_lhs>dcomplex</full_lhs>
+<full_lhs_value binary="1000000000000011111111111111111111000111111100100110011101110111">-5\.562680e-309</full_lhs_value>
+<full_lhs>inf</full_lhs>
+<full_lhs_value binary="01{11}0{52}">\+INFINITY</full_lhs_value>
+<full_lhs>nan</full_lhs>
+<full_lhs_value binary="01{11}[01]*1[01]*">\+NAN</full_lhs_value>
+<full_lhs_value binary="[01]{64}">\+NAN</full_lhs_value>
 --
 --
 Checks that the binary value is printed for floating point types