[PATCH] D103440: [WIP][analyzer] Introduce range-based reasoning for addition operator

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

I was wondering, if we could try something new with the tests. To increase our confidence that the expected behavior is correct, how about including a Z3 proof with each of the test cases?

For example:

  (declare-const a ( _ BitVec 32 ))
  (declare-const b ( _ BitVec 32 ))
  
  ; Assume 0 <= a, b, <= 5
  (assert (bvsge a #x00000000))
  (assert (bvsge b #x00000000))
  (assert (bvsle a #x00000005))
  (assert (bvsle b #x00000005))
  
  ; Check if 0 <= a + b  <= 10
  (assert (not (and (bvsle (bvadd a b) #x00000010) (bvsge (bvadd a b) #x00000000))))
  
  (check-sat)

Of course, the example above is obvious, but with overflows and other corner cases it is great to have a tool doublecheck our assumptions, and share how to reproduce the results.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103440/new/

https://reviews.llvm.org/D103440