Skip to content

Commit 492f5e4

Browse files
committed
Explain why it is ok to use false for is_signed
To answer the question of why this is not a bug when reading the code. Ideally there would exist a `bvrep2binary` function, but this is out of scope of this PR.
1 parent bceafb5 commit 492f5e4

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/goto-programs/xml_goto_trace.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,11 @@ xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
4343
if(bv_type && constant)
4444
{
4545
const auto width = bv_type->get_width();
46+
// It is fine to pass `false` into the `is_signed` parameter, even for
47+
// signed values, because the subsequent conversion to binary will result
48+
// in the same value either way. E.g. if the value is `-1` for a signed 8
49+
// bit value, this will convert to `255` which is `11111111` in binary,
50+
// which is the desired result.
4651
const auto binary_representation =
4752
integer2binary(bvrep2integer(constant->get_value(), width, false), width);
4853
xml.set_attribute("binary", binary_representation);

0 commit comments

Comments
 (0)