Commit Graph
5253 Commits
Author SHA1 Message Date
Daniel Kirchner 32bcbc6cfb slightly broken 2023-07-03 00:01:34 +02:00
Daniel Kirchner 987278385e tmp 2023-06-29 02:42:10 +02:00
Daniel Kirchner 5adc255b3c Separate approach of AST transform. 2023-06-28 16:45:51 +02:00
Daniel Kirchner f9b424418c tmp 2023-06-27 16:49:39 +02:00
Daniel Kirchner 9120737f57 tmp 2023-06-27 02:18:00 +02:00
Daniel Kirchner ea9dfca1ae tmp 2023-06-27 01:39:18 +02:00
Daniel Kirchner 156d5c7cb7 tmp 2023-06-27 00:41:11 +02:00
Daniel Kirchner 8135e28821 tmp 2023-06-27 00:16:28 +02:00
Daniel Kirchner 48b35bd921 tmp 2023-06-25 09:03:15 +02:00
Daniel Kirchner 2e9b844d65 tmp 2023-06-25 08:48:48 +02:00
Daniel Kirchner 58b7344c5a tmp 2023-06-25 08:33:45 +02:00
Daniel Kirchner fd1db21d64 tmp 2023-06-25 07:50:09 +02:00
Daniel Kirchner 5bfe862bc4 tmp 2023-06-25 07:04:50 +02:00
Daniel Kirchner 6f352cbcbe tmp 2023-06-25 04:22:13 +02:00
Daniel Kirchner 947deaec96 tmp 2023-06-25 03:53:03 +02:00
Daniel Kirchner d882a08582 tmp 2023-06-25 03:44:37 +02:00
Daniel Kirchner 1bc8caf54a tmp 2023-06-24 19:30:05 +02:00
Daniel Kirchner 423972883c tmp 2023-06-24 19:12:14 +02:00
Daniel Kirchner 955ada39e5 tmp 2023-06-24 18:53:47 +02:00
Daniel Kirchner f9d6e805ba tmp 2023-06-24 18:38:55 +02:00
Daniel Kirchner bd4be335d4 tmp 2023-06-24 10:10:00 +02:00
Daniel Kirchner 60e1e53f20 tmp 2023-06-24 07:55:10 +02:00
Daniel Kirchner 4a84818669 tmp 2023-06-24 07:47:33 +02:00
Daniel Kirchner 0d1679cee0 tmp 2023-06-24 06:24:28 +02:00
Daniel Kirchner 62a5291bbd tmp 2023-06-24 01:45:56 +02:00
Daniel Kirchner 7d094b3be6 tmp 2023-06-24 01:21:14 +02:00
Daniel Kirchner 315270f3bb tmp 2023-06-23 18:37:58 +02:00
Daniel Kirchner 14a34ae088 tmp 2023-06-21 02:15:01 +02:00
Daniel Kirchner 7a8c997438 tmp 2023-06-21 01:50:00 +02:00
Daniel Kirchner 3286d1cec2 tmp 2023-06-21 01:08:34 +02:00
Daniel Kirchner 1c1110f734 tmp 2023-06-20 22:26:52 +02:00
Daniel Kirchner 3249979969 tmp 2023-06-20 04:45:30 +02:00
Daniel Kirchner bd0e0fcdbe tmp 2023-06-20 04:08:23 +02:00
Daniel Kirchner 4357b0316b tmp 2023-06-19 22:06:36 +02:00
Daniel Kirchner 71f7bf7206 tmp 2023-06-19 16:24:07 +02:00
Daniel Kirchner fb959b3066 Scanner hack. 2023-06-13 20:42:59 +02:00
Daniel Kirchner d2cde10388 tmp 2023-06-13 17:38:46 +02:00
Daniel Kirchner 17eeef6369 Use separate instances of the stateless DocStringTagParser during analysis. 2023-06-13 17:31:10 +02:00
Daniel Kirchner 33c12e2195 Do not assume successful analysis on fatal error. 2023-06-13 17:31:10 +02:00
Kamil Śliwak b1a773be2f IRGenerator: Leave IR optimization up to the caller to avoid unnecessarily doing it twice 2023-06-07 19:44:40 +02:00
Kamil Śliwak 25be38905f YulStack: When Yul optimization is not requested, run Yul optimizer with a minimal sequence instead of disabling it 2023-06-07 12:13:38 +02:00
Nikola Matic 47969adf91 Experimental standard library
Change import syntax and cover with tests
2023-06-06 17:16:23 +02:00
Pawel Gebal f15b826431 Add optional bounds to unroll loops in BMC model checker 2023-06-02 18:32:38 +02:00
Leo a0933fa80a Merge pull request #14276 from ethereum/smtchecker-fix-ice
SMTChecker: External function call with struct member is not getter
2023-05-30 13:46:35 +02:00
Leo ceab4dfee5 Merge pull request #14269 from blishko/smtchecker-fix-analysis-external-calls
[SMTChecker] Remember verification targets from trusted external calls
2023-05-30 13:45:37 +02:00
Martin Blicha 8ca453f82e SMTChecker: External function call with struct member is not getter
if a struct has a member that is a function pointer with `external`
attribute, and such a member is called, it is currently incorrectly
treated as a public getter in SMTEncoder.

The proposed fix is to make SMTEncoder::publicGetter more strict in
deciding whether an expression is a public getter.
The added condition, that the access happens on a state variable, is
exactly what is checked later with an assertion that is currently
failing.
2023-05-26 14:23:45 +02:00
Nikola Matić 477b621f2e Merge pull request #14274 from ethereum/enable-access-to-foreign-events 2023-05-26 13:49:13 +02:00
Martin Blicha b0419da654 [SMTChecker] Remember verification targets from trusted external calls
Previously, we did not remember trusted external calls for later phase
when we compute possible verification targets for each function.
This led to false negative in cases where verification target can be
violated, but not by calling a public function directly, but only when
it is called as an external function from other function.

The added test cases witnesses this behaviour. The underflow in
`dec` cannot happen in any other way except what the `dec` is called
from `f`.

The same problem did not occur when the functions are called internally,
because for such cases, we have already been remembering these calls in
the callgraph in the CHC engine.
2023-05-26 13:03:44 +02:00
Nikola Matic 5893e099fe Allow qualified access to events from other contracts 2023-05-26 12:52:52 +02:00
GiokaMarkella 28a1abf89a Yul AST output on the CLI and in Standard JSON 2023-05-26 12:35:31 +02:00