Skip to content

Commit 75d4fac

Browse files
author
Thomas Kiley
committed
Draft version of adding flaot output
1 parent 1af207d commit 75d4fac

File tree

1 file changed

+18
-2
lines changed

1 file changed

+18
-2
lines changed

src/goto-programs/xml_goto_trace.cpp

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Author: Daniel Kroening
1919
#include <util/xml_irep.h>
2020

2121
#include <langapi/language_util.h>
22+
#include <util/arith_tools.h>
2223

2324
#include "printf_formatter.h"
2425
#include "xml_expr.h"
@@ -88,16 +89,31 @@ void convert(
8889
}
8990
}
9091

91-
std::string full_lhs_string, full_lhs_value_string;
92+
std::string full_lhs_string, full_lhs_value_string,
93+
full_lhs_value_binary_string;
9294

9395
if(step.full_lhs.is_not_nil())
9496
full_lhs_string = from_expr(ns, identifier, step.full_lhs);
9597

9698
if(step.full_lhs_value.is_not_nil())
99+
{
97100
full_lhs_value_string = from_expr(ns, identifier, step.full_lhs_value);
101+
if(can_cast_type<floatbv_typet>(step.full_lhs_value.type()))
102+
{
103+
const auto width =
104+
to_floatbv_type(step.full_lhs_value.type()).get_width();
105+
full_lhs_value_binary_string =
106+
integer2binary(bvrep2integer(step.full_lhs_value.get(ID_value),
107+
width,
108+
false), width);
109+
}
110+
}
98111

99112
xml_assignment.new_element("full_lhs").data = full_lhs_string;
100-
xml_assignment.new_element("full_lhs_value").data = full_lhs_value_string;
113+
xmlt &full_lhs_value_node = xml_assignment.new_element("full_lhs_value");
114+
if(full_lhs_value_binary_string != "")
115+
full_lhs_value_node.set_attribute("binary", full_lhs_value_binary_string);
116+
full_lhs_value_node.data = full_lhs_value_string;
101117

102118
xml_assignment.set_attribute_bool("hidden", step.hidden);
103119
xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));

0 commit comments

Comments
 (0)