forked from OSchip/llvm-project
53ac1a2ed4
The refutation manager is removing a true bug from the test in this patch.
The problem is that the following constraint:
```
(conj_$1{struct o *}) - (reg_$3<int * r>): [-9223372036854775808, 0]
```
is encoded as:
```
(and (bvuge (bvsub $1 $3) #x8000000000000000)
(bvule (bvsub $1 $3) #x0000000000000000))
```
The issue is that unsigned comparisons (bvuge and bvule) are being generated instead of signed comparisons (bvsge and bvsle).
When generating the expressions:
```
(conj_$1{p *}) - (reg_$3<int * r>) >= -9223372036854775808
```
and
```
(conj_$1{p *}) - (reg_$3<int * r>) <= 0
```
both -9223372036854775808 and 0 are casted to pointer type and `LTy->isSignedIntegerOrEnumerationType()` in `Z3ConstraintManager::getZ3BinExpr` only checks if the type is signed, not if it's a pointer.
Reviewers: NoQ, george.karpenkov, ddcc
Subscribers: rnkovacs, NoQ, george.karpenkov, ddcc, xazax.hun, szepet, a.sidorin
Differential Revision: https://reviews.llvm.org/D48324
llvm-svn: 335926
|
||
|---|---|---|
| clang | ||
| clang-tools-extra | ||
| compiler-rt | ||
| debuginfo-tests | ||
| libclc | ||
| libcxx | ||
| libcxxabi | ||
| libunwind | ||
| lld | ||
| lldb | ||
| llgo | ||
| llvm | ||
| openmp | ||
| parallel-libs | ||
| polly | ||
| README.md | ||
README.md
Low Level Virtual Machine (LLVM)
This directory and its subdirectories contain source code for LLVM, a toolkit for the construction of highly optimized compilers, optimizers, and runtime environments.