diff options
| author | Gabor Marton <gabor.marton@ericsson.com> | 2020-05-14 15:44:20 +0200 |
|---|---|---|
| committer | Gabor Marton <gabor.marton@ericsson.com> | 2020-05-14 15:46:13 +0200 |
| commit | 5fc05c376a3cc0fb9a532e41d12e51f3d9916692 (patch) | |
| tree | e4c7306b0ecaa0482f4a6a8a93c91f3622bbadd1 /clang/lib/Basic/SourceManager.cpp | |
| parent | ff4492c89feb54e6ddfd6edaea59c98776963208 (diff) | |
| download | llvm-5fc05c376a3cc0fb9a532e41d12e51f3d9916692.zip llvm-5fc05c376a3cc0fb9a532e41d12e51f3d9916692.tar.gz llvm-5fc05c376a3cc0fb9a532e41d12e51f3d9916692.tar.bz2 | |
Fix Z3 function calls regarding arithmetic operations
Summary:
The order of Z3_mk_fpa_mul, Z3_mk_fpa_div, Z3_mk_fpa_add and Z3_mk_fpa_sub functions' arguments is: context, rounding_mode, ast1, ast2.
See for example: https://github.com/Z3Prover/z3/blob/a14c2a30516003cd1a60f8b7deca029033d11c78/src/api/api_fpa.cpp#L433
At function calls from LLVM the argument order was different: rounding_mode was passed as last argument.
Unfortunately these Z3_ast and other function parameter types are technically like void* which are reinterpret_cast-ed to a specific class type. So there was no type error, but the assertions fail in runtime if something goes wrong. Such a crash happened during Z3 refutation while using StaticAnalyzer.
Reviewers: Szelethus, xazax.hun, baloghadamsoftware, steakhal, martong, mikhail.ramalho
Reviewed By: martong
Subscribers: hiraditya, rnkovacs, mikhail.ramalho, martong, llvm-commits
Tags: #llvm
Differential Revision: https://reviews.llvm.org/D79883
Patch by Tibor Brunner!
Diffstat (limited to 'clang/lib/Basic/SourceManager.cpp')
0 files changed, 0 insertions, 0 deletions