Commit Graph
81 Commits
Author SHA1 Message Date
Leonardo Alt 50be39fc21 Add and update tests 2020-12-17 14:42:49 +01:00
chriseth ffaf40950a Merge pull request #10605 from ethereum/develop
Merge develop into breaking.
2020-12-15 14:01:01 +01:00
Alex Beregszaszi edbdff8619 Update tests 2020-12-14 19:32:31 +00:00
Martin Blicha 0be325dc0d [SMTChecker] Fix handling of function calls where the function identifier is nested in a tuple. 2020-12-14 16:19:24 +01:00
chriseth 561280a5cc Merge remote-tracking branch 'origin/develop' into breaking 2020-12-14 11:33:40 +01:00
Martin Blicha 8927015e5a [SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine 2020-12-11 17:41:50 +01:00
chriseth 482bda6887 Merge remote-tracking branch 'origin/develop' into breaking 2020-12-10 12:15:52 +01:00
Leonardo Alt 3c142e0e94 Move CHC counterexamples to primary location 2020-12-09 19:55:18 +01:00
chriseth 329b8f2a60 Merge remote-tracking branch 'origin/develop' into breaking 2020-12-07 13:04:14 +01:00
Leonardo Alt 7490ffbe13 Use nonlinear clauses instead of inlining for base constructors 2020-12-04 13:25:56 +01:00
chriseth d56a7bb89e Merge pull request #10489 from ethereum/develop
Merge develop into breaking.
2020-12-03 18:11:12 +01:00
Martin Blicha 2ee633f404 [SMTChecker] Added support for public getters through this. 2020-12-02 16:06:48 +01:00
hrkrshnn a834476de6 Tests/Docs after disallowing super, this and _ as declaration names 2020-11-25 11:14:13 +01:00
chriseth 253889cbf1 Merge remote-tracking branch 'origin/develop' into breaking 2020-11-24 16:22:03 +01:00
chriseth 79669ecd48 Use new abicoder pragma. 2020-11-24 14:57:45 +01:00
chriseth a0a02f2307 Merge remote-tracking branch 'origin/develop' into breaking 2020-11-23 19:28:08 +01:00
Martin Blicha 66125b79d6 [SMTChecker] Do not report warning when encountered a Type identifier. The operations are supported now. 2020-11-23 15:41:57 +01:00
chriseth e8a278eefa Merge remote-tracking branch 'origin/develop' into breaking 2020-11-17 18:51:57 +01:00
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
chriseth 04195439b7 Merge remote-tracking branch 'origin/develop' into HEAD 2020-11-09 14:28:05 +01:00
Leonardo Alt daf859c15b [SMTChecker] report SMTEncoder warnings also via CHC 2020-11-03 16:06:17 +00:00
chriseth 5ffee049fa Merge remote-tracking branch 'origin/develop' into breaking 2020-11-03 14:05:14 +01:00
Martin Blicha c1a57ffbfe [SMTChecker] More precise creation of verification targets. 2020-10-30 19:11:28 +01:00
hrkrshnn 0e30fbbae1 Fix failing SMTChecker test on breaking 2020-10-26 14:01:40 +01:00
chriseth 979d3062bc Merge pull request #10033 from ethereum/develop
Merge develop into breaking
2020-10-14 14:12:20 +02:00
Leonardo Alt aec456021d Add tx constraints to CHC 2020-10-13 17:49:04 +01:00
chriseth f6e57a0eec Merge pull request #10023 from ethereum/develop
Merge develop into breaking.
2020-10-13 18:18:53 +02:00
Mathias Baumann 006e5f2e1f Allow path syntax for super constructor calls 2020-10-13 14:32:11 +02:00
Mathias Baumann 32b4f18023 Print warning for unnamed return parameters and no return statement 2020-10-13 13:11:29 +02:00
Leonardo Alt 3d2e6252f0 Add/update tests 2020-10-12 11:11:52 +01:00
Leonardo Alt e6bd18525b [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +02:00
Leonardo Alt 0223571987 [SMTChecker] Do not report error when rlimit 2020-09-25 18:43:10 +02:00
Alex Beregszaszi 6edfdff187 [SMTChecker] Do not warn on "abi" as an identifer
There is an approprate warning for the function call.
2020-09-24 13:57:42 +01:00
Leonardo Alt f4ee4cd479 Update tests 2020-09-22 20:51:28 +02:00
Leonardo Alt fd6c665548 Update SMTChecker tests with z3 4.8.9 2020-09-14 19:04:13 +02:00
Leonardo Alt 00f6b303b1 [SMTChecker] Change warning message 2020-09-09 16:14:21 +02:00
Leonardo Alt 0a160b1ba0 Update remaining tests 2020-08-14 12:58:27 +02:00
Leonardo Alt 8df8c6e14f [SMTChecker] Fix ICE in BMC function inlining 2020-08-05 11:47:25 +02:00
Leonardo Alt 95484d9969 Fix tests after rebase 2020-07-23 18:49:03 +02:00
Leonardo Alt 003c9b9a5b Update tests 2020-07-23 18:49:03 +02:00
chriseth 9743390a53 Update tests. 2020-07-07 12:16:18 +02:00
Leonardo Alt 5517e817d5 Do not trust code of external functions 2020-07-01 18:20:46 +02:00
Leonardo Alt 5160f89c1b [SMTChecker] Support to external calls to unknown code 2020-07-01 18:20:33 +02:00
a3d4 e04cedafc5 Added error codes to SyntaxTest expectations (updated tests) 2020-06-22 16:51:47 +02:00
Leonardo Alt 3c4e286390 [SMTChecker] Replace wrap mod by slack vars 2020-06-12 14:57:21 +02:00
Leonardo Alt ede39fc2da [SMTChecker] Relax assertion about callstack 2020-06-02 12:50:51 +02:00
Leonardo Alt ec766958ea Add test 2020-05-28 13:14:21 +02:00
Leonardo Alt 059d0bdebb Revert "Use Spacer option to improve performance of constant arrays"
This reverts commit 92059fa848.
2020-04-24 11:55:58 +02:00
Leonardo Alt 92059fa848 Use Spacer option to improve performance of constant arrays 2020-04-23 10:45:02 +02:00
Leonardo Alt e3ec22124e [SMTChecker] Fix ICE in CHC internal calls 2020-04-07 01:09:03 +02:00