Skip to content

Commit 7e785d0

Browse files
committed
show bit-pattern of pointers in trace
This commit adds output for the bit-pattern of pointers.
1 parent 39c3460 commit 7e785d0

File tree

3 files changed

+12
-0
lines changed

3 files changed

+12
-0
lines changed

regression/cbmc/hex_trace/main.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,15 @@ int main()
33
int a;
44
unsigned int b;
55
float f;
6+
char *p;
67

78
a = 0;
89
a = -100;
910
a = 2147483647;
1011
b = a * 2;
1112
a = -2147483647;
1213
f = 0.1f;
14+
p = (char *)123;
1315

1416
__CPROVER_assert(0, "");
1517
}

regression/cbmc/hex_trace/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ a=2147483647 \s*\(0x7FFFFFFF\)
1010
b=4294967294ul? \s*\(0xFFFFFFFE\)
1111
a=-2147483647 \s*\(0x80000001\)
1212
f=0\.1f \s*\(0x3DCCCCCD\)
13+
p=.* \(0x7B\)
1314
^VERIFICATION FAILED$
1415
--
1516
^warning: ignoring

src/goto-programs/goto_trace.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,15 @@ std::string trace_numeric_value(
242242
}
243243
}
244244
}
245+
else if(expr.id() == ID_annotated_pointer_constant)
246+
{
247+
const auto &annotated_pointer_constant =
248+
to_annotated_pointer_constant_expr(expr);
249+
auto width = to_pointer_type(expr.type()).get_width();
250+
auto &value = annotated_pointer_constant.get_value();
251+
auto c = constant_exprt(value, unsignedbv_typet(width));
252+
return numeric_representation(c, ns, options);
253+
}
245254
else if(expr.id()==ID_array)
246255
{
247256
std::string result;

0 commit comments

Comments
 (0)