Is this a bug from function kernel_int?

[Yue Cao <yuecao1990 at gmail dot com>]

Hi there,

Recently I find systemtap generates a wrong result when I use kernel_int to
print out the int value from the pointer. In my case, systemtap prints out
a huge value (18446744072649393666) with kernel_int. As you can see, this
value is larger than 2^32 (the maximal value for int). However, when I use
kernel_long, the result is within 2^32. The new value (3234809346) actually
is equal to what I expected by using kernel_int. I have tried multiple
times and the results are same. I wonder is it a bug. Could anyone tell me
how to fix it?

Here is another example that I have used to reproduce the error above. The
following two values are supposed to be same. But the first value returns
(18446744072649393666), while the second one returns (3234809346), which is
the expected value.
 *kernel_int(&*@cast($skb->cb, "tcp_skb_cb", "kernel<net/tcp.h>")->end_seq)
@cast($skb->cb, "tcp_skb_cb", "kernel<net/tcp.h>")->end_seq

Looking forward to your reply.

Best,
Yue