More precise bitwise AND

seahorn / crab

A library for building abstract interpretation-based analyses

Apache License 2.0

234 stars 32 forks source link

Closed elazarg closed 5 years ago

elazarg commented 6 years ago

x & K can at least be inferred to be <= K. This is not the case currently.

caballa commented 6 years ago

I'm assuming you mean that y = x & k implies that y <= k

E.g., given x = 10, k = -3 and bitwdith=4 we get y = 1010 & 1101 = 1000

which in decimal, y = 8. Thus, we cannot infer here that y <= -3