Merge pull request #3262 from diffblue/smt2-integer

tautschnig · web-flow · commit 11a98d8b1f5e · 2018-11-05T13:09:10.000Z
goto_trace: unbounded integers are now shown like other numbers
diff --git a/regression/cbmc/integer-assignments1/test.desc b/regression/cbmc/integer-assignments1/test.desc
@@ -3,5 +3,5 @@ main.c
 --trace --smt2
 ^EXIT=10$
 ^SIGNAL=0$
-^  b=100
+^  b=100 \(0b1100100\)$
 --
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
@@ -205,7 +205,12 @@ std::string trace_numeric_value(
     {
       mp_integer i;
       if(!to_integer(expr, i) && i>=0)
-        return integer2string(i, 2);
+      {
+        if(options.hex_representation)
+          return "0x" + integer2string(i, 16);
+        else
+          return "0b" + integer2string(i, 2);
+      }
     }
   }
   else if(expr.id()==ID_array)

Original file line number	Diff line number	Diff line change
`@@ -205,7 +205,12 @@ std::string trace_numeric_value(`
`205`	`205`	`{`
`206`	`206`	`mp_integer i;`
`207`	`207`	`if(!to_integer(expr, i) && i>=0)`
`208`		`- return integer2string(i, 2);`
	`208`	`+ {`
	`209`	`+ if(options.hex_representation)`
	`210`	`+ return "0x" + integer2string(i, 16);`
	`211`	`+ else`
	`212`	`+ return "0b" + integer2string(i, 2);`
	`213`	`+ }`
`209`	`214`	`}`
`210`	`215`	`}`
`211`	`216`	`else if(expr.id()==ID_array)`