search

seahorn / crab

A library for building abstract interpretation-based analyses
Apache License 2.0
234 stars 32 forks source link

Valgrind warnings #25

Closed elazarg closed 5 years ago

elazarg commented 6 years ago

Running valgrind when using the sdbm domain I get a warning about "use of uninitialized value of size 8" and "Conditional jump depends on uninitialized value" in this line.

I'm not sure which of the variables triggers this error; I would guess it's the dense field since it is of size 8.

(I used the file samples/self/accept_DIV32_overflow_check_1.3 in the bpf verifier)

gkgange commented 6 years ago

This is expected behaviour; see the comment on line 195. Valgrind is right, in that the read sparse[k] can go outside the bounds of k. But I think it should be safe, because when that happens, one of the cross-reference tests on line 216 will fail.

On Mon, Nov 12, 2018 at 3:53 AM Elazar Gershuni notifications@github.com wrote:

Running valgrind when using the sdbm domain I get a warning about "use of uninitialized value of size 8" and "Conditional jump depends on uninitialized value" in this line https://github.com/seahorn/crab/blob/f5d77edb67375a3d01b309b88731fa2ad9510409/include/crab/domains/graphs/adapt_sgraph.hpp#L216 .

I'm not sure which of the variables triggers this error; I would guess it's the dense field since it is of size 8.

(I used the file samples/self/accept_DIV32_overflow_check_1.3 in the bpf verifier)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/seahorn/crab/issues/25, or mute the thread https://github.com/notifications/unsubscribe-auth/AOWOWTyUeDhFlznwgKY_HT8z5s7Aty0Hks5uuFYhgaJpZM4YYkvt .