cerc-io/solidity
15
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
81b3a13333
solidity/test/libsolidity/smtCheckerTests
History
Martin Blicha 5ca7a24896 [SMTChecker] Added support for precise modeling of external calls to this. 
Modeling external calls to this, since we can trust these calls.

fixed problem with transaction data not being restored after trusted external call

update to the tests

additional tests

changelog entry

added tests for external getters of this
2020-11-13 11:49:09 +01:00
..
array_members [SMTChecker] Fix internal error when array.push() is used as LHS of assignment 2020-11-02 13:32:53 +00:00
blockchain_state Remove more tests because current Spacer crashes 2020-10-13 19:27:49 +01:00
bmc_coverage Isoltets SMTChecker option and BMC specific tests 2020-11-06 15:03:38 +00:00
complex Isoltets SMTChecker option and BMC specific tests 2020-11-06 15:03:38 +00:00
control_flow Fix CHC false positives when using branches inside modifiers 2020-11-04 21:47:07 +00:00
crypto Add unknown message to all verification targets 2020-10-19 20:54:13 +01:00
external_calls Update tests 2020-10-13 17:49:04 +01:00
function_selector [SMTChecker] report SMTEncoder warnings also via CHC 2020-11-03 16:06:17 +00:00
functions [SMTChecker] Added support for precise modeling of external calls to this. 2020-11-13 11:49:09 +01:00
imports [SMTChecker] report SMTEncoder warnings also via CHC 2020-11-03 16:06:17 +00:00
inheritance [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +02:00
inline_assembly [SMTChecker] report SMTEncoder warnings also via CHC 2020-11-03 16:06:17 +00:00
invariants Add unknown message to all verification targets 2020-10-19 20:54:13 +01:00
loops [SMTChecker] More precise creation of verification targets. 2020-10-30 19:11:28 +01:00
math [SMTChecker] Adding division by zero checks in the CHC engine 2020-10-21 14:48:33 +02:00
modifiers [SMTChecker] More precise creation of verification targets. 2020-10-30 19:11:28 +01:00
operators [SMTChecker] Fix internal error when array.push() is used as LHS of assignment 2020-11-02 13:32:53 +00:00
overflow [SMTChecker] More precise creation of verification targets. 2020-10-30 19:11:28 +01:00
simple [SMTChecker] Shortcut RationalNumber expressions 2019-03-11 12:53:49 +01:00
special [SMTChecker] report SMTEncoder warnings also via CHC 2020-11-03 16:06:17 +00:00
typecast Isoltets SMTChecker option and BMC specific tests 2020-11-06 15:03:38 +00:00
types Isoltets SMTChecker option and BMC specific tests 2020-11-06 15:03:38 +00:00
verification_target [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +02:00