Commit Graph

34 Commits

Author SHA1 Message Date
Leonardo Alt
c8cc73c80c Support array slices 2020-10-01 11:52:02 +02:00
Leonardo Alt
e6bd18525b [SMTChecker] Add engine prefix to verification target error messages 2020-09-25 19:09:06 +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
Alex Beregszaszi
c8c17b693b [SMTChecker] Support events and low-level logs 2020-09-16 11:50:39 +02:00
Leonardo Alt
00f6b303b1 [SMTChecker] Change warning message 2020-09-09 16:14:21 +02:00
Leonardo Alt
afcd44e77c Update current tests 2020-09-03 15:19:03 +02:00
Leonardo Alt
0a160b1ba0 Update remaining tests 2020-08-14 12:58:27 +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
d67734df6f Fix error IDs. 2020-06-22 18:56:32 +02:00
chriseth
1441b97131 Merge remote-tracking branch 'origin/develop' into breaking 2020-06-22 18:40:20 +02:00
a3d4
e04cedafc5 Added error codes to SyntaxTest expectations (updated tests) 2020-06-22 16:51:47 +02:00
chriseth
d422a406ba
Merge pull request #8983 from ethereum/develop
Merge develop into breaking.
2020-05-19 18:05:28 +02:00
Leonardo Alt
a0c605aa85 [SMTChecker] Support array length 2020-05-14 23:32:29 +02:00
Harikrishnan Mulackal
92cf61d4f9 fixed compilation tests and upgraded ext. tests branch 2020-05-05 21:11:15 +05:30
Leonardo Alt
07368c2e1e Add support to internal function calls 2020-03-11 16:29:07 +01:00
chriseth
2f11ac3590 Merge remote-tracking branch 'origin/develop' into develop_060 2019-12-03 21:17:15 +01:00
chriseth
96d777d7f1 Merge commit 'a7d481fb9' into develop_060 2019-12-03 20:47:30 +01:00
Leonardo Alt
b1577f5e46 [SMTChecker] Fix ICE in array of structs type 2019-12-03 01:12:30 +01:00
Leonardo Alt
9eda95caf9 [SMTChecker] Fix visit to IndexAccess that has type Type 2019-11-29 17:20:50 +01:00
chriseth
0973ae751a Do not warn about enabled ABIEncoderV2 anymore. 2019-11-26 15:49:42 +01:00
Leonardo Alt
d818746e0c [SMTChecker] Fix ICE in abi.decode 2019-11-18 13:15:10 +01:00
Leonardo Alt
dd1afeba52 [SMTChecker] Support this as address 2019-04-18 17:56:52 +02:00
Leonardo Alt
02d0e609b9 [SMTChecker] Support enums 2019-03-07 15:15:12 +01:00
Leonardo Alt
e74f58130e Add SMT type support to Solidity arrays 2019-03-06 11:29:26 +01:00
Leonardo Alt
34470f3549 [SMTChecker] Only check for overflow/underflow in the end of the function 2019-02-18 23:55:58 +01:00
Leonardo Alt
a10db051de [SMTChecker] Support basic typecast 2019-01-16 13:00:54 +01:00
Leonardo Alt
08737e43dc [SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions 2018-12-11 11:28:25 +01:00
Kevin Kelley
fb6fd1b3c2 add a 'readable' format for large hex values 2018-12-05 22:15:02 +01:00
Leonardo Alt
70bb0eaf95 [SMTChecker] Implement uninterpreted functions and use it for blockhash() 2018-11-15 09:12:42 +01:00
Leonardo Alt
d8cbf321da Grouping of symbolic variables in the same file and support to FixedBytes 2018-10-25 09:30:48 +02:00
Leonardo Alt
e2cf5f6ed9 Add gasleft constraint and use full member access name 2018-10-22 18:19:11 +02:00
Leonardo Alt
b46b827c30 [SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash 2018-10-19 15:52:16 +02:00