cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #13939 from pgebal/fix_handling_bitwise_operators_when_parsing_z3_call_result

Browse Source 
Fixes handling bitwise operators for z3 model checker
This commit is contained in:
Leo 2023-02-09 12:16:28 +01:00 committed by GitHub
commit 59f9ab4dee
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 19 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -10,6 +10,7 @@ Compiler Features:
Bugfixes: Bugfixes:
* SMTChecker: Fix internal error when using the custom NatSpec annotation to abstract free functions. * SMTChecker: Fix internal error when using the custom NatSpec annotation to abstract free functions.
* TypeChecker: Also allow external library functions in ``using for``. * TypeChecker: Also allow external library functions in ``using for``.
* SMTChecker: Fix internal error caused by unhandled ``z3`` expressions that come from the solver when bitwise operators are used.
### 0.8.18 (2023-02-01) ### 0.8.18 (2023-02-01)

6
libsmtutil/Z3Interface.cpp
View File

@ -344,6 +344,12 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
return arguments[0] % arguments[1]; return arguments[0] % arguments[1];
else if (kind == Z3_OP_XOR) else if (kind == Z3_OP_XOR)
return arguments[0] ^ arguments[1]; return arguments[0] ^ arguments[1];
else if (kind == Z3_OP_BOR)
return arguments[0] | arguments[1];
else if (kind == Z3_OP_BAND)
return arguments[0] & arguments[1];
else if (kind == Z3_OP_BXOR)
return arguments[0] ^ arguments[1];
else if (kind == Z3_OP_BNOT) else if (kind == Z3_OP_BNOT)
return !arguments[0]; return !arguments[0];
else if (kind == Z3_OP_BSHL) else if (kind == Z3_OP_BSHL)

12
test/libsolidity/smtCheckerTests/operators/bitwise_operators_do_not_throw_exceptions.sol Normal file
View File

@ -0,0 +1,12 @@
contract C {
// tests that bitwise operators are parsed from z3 answer
function test(uint x, uint y) public pure {
x | y;
x & y;
x ^ y;
assert(true);
}
}
// ====
// SMTEngine: all
// ----