expr2java/floating point output: Lossless-test needs to use is_float

tautschnig · tautschnig · commit 8b4ba92d5bc0 · 2018-09-03T09:00:42.000Z
diff --git a/jbmc/src/java_bytecode/expr2java.h b/jbmc/src/java_bytecode/expr2java.h
@@ -81,7 +81,10 @@ std::string floating_point_to_java_string(float_type value)
       return true;
     try
     {
-      return std::stod(decimal) == value;
+      if(is_float)
+        return std::stof(decimal) == value;
+      else
+        return std::stod(decimal) == value;
     }
     catch(std::out_of_range &)
     {

Original file line number	Diff line number	Diff line change
`@@ -81,7 +81,10 @@ std::string floating_point_to_java_string(float_type value)`
`81`	`81`	`return true;`
`82`	`82`	`try`
`83`	`83`	`{`
`84`		`- return std::stod(decimal) == value;`
	`84`	`+ if(is_float)`
	`85`	`+ return std::stof(decimal) == value;`
	`86`	`+ else`
	`87`	`+ return std::stod(decimal) == value;`
`85`	`88`	`}`
`86`	`89`	`catch(std::out_of_range &)`
`87`	`90`	`{`