Commit Graph

7 Commits

Author SHA1 Message Date
Ted Kremenek
34bfd8a490 Fixed logic error in BasicConstraintManager pointed out by Zhongxing Xu.
For checking if a symbol >= value, we need to check if symbol == value || symbol
> value. When checking symbol > value and we know that symbol != value, the path
is infeasible only if value == maximum integer.

For checking if a symbol <= value, we need to check if symbol == value || symbol
< value. When checking symbol < value and we know that symbol != value, the path
is infeasible only if value == minimum integer.

Updated test case exercising this logic: we only prune paths if the values are
unsigned.

llvm-svn: 56354
2008-09-19 18:00:36 +00:00
Zhongxing Xu
a8e88ecda6 Add an omitted case for AssumeSymInt.
llvm-svn: 56334
2008-09-19 06:07:59 +00:00
Ted Kremenek
8782716c4a Minor pass-sensitivity improvement:
if we know that 'len != 0' and know that 'i == 0' then we know that
  'i < len' must evaluate to true and cannot evaluate to false

llvm-svn: 56260
2008-09-16 23:24:45 +00:00
Daniel Dunbar
c62cf79290 Add newline at end of file.
llvm-svn: 55559
2008-08-30 02:06:22 +00:00
Zhongxing Xu
4c23963de8 Added LLVM comment header.
llvm-svn: 55537
2008-08-29 15:09:12 +00:00
Zhongxing Xu
c1bd3a5f8b Migrate the rest symbolic analysis stuff to BasicConstraintManager.
llvm-svn: 55536
2008-08-29 14:52:36 +00:00
Zhongxing Xu
f71b5f39bb Refactor Assume logic into a separate class ConstraintManager.
llvm-svn: 55412
2008-08-27 14:03:33 +00:00