Marenz
5663fbb903
Merge branch 'develop' into breaking
...
Manual Resolved Conflicts:
Changelog.md
* Updated changelog
test/externalTests/ens.sh
* Merged fixes for upstream from both develop and breaking
test/libsolidity/semanticTests/inlineAssembly/external_identifier_access_shadowing.sol
* Removed in #11735 (breaking)
test/libsolidity/semanticTests/inlineAssembly/function_name_clash.sol
* Removed in #12209 (breaking)
test/libsolidity/semanticTests/storage/mappings_array2d_pop_delete.sol
* Removed in #11843 (breaking)
test/libsolidity/semanticTests/storage/mappings_array_pop_delete.sol
* Removed in #11843 (breaking)
test/libsolidity/syntaxTests/inlineAssembly/basefee_berlin_function.sol
* Used version of file from #11842 (breaking)
2022-08-30 18:07:20 +02:00
Leo Alt
16c0838f75
Update docker images and tests
2022-08-30 11:51:59 +02:00
Ishtiaque Zahid
61febbd249
formatNumberReadable now prints signed integers as well
2022-06-24 07:15:15 +06:00
chriseth
3c2cee5836
Merge pull request #13026 from ethereum/develop
...
Merge develop into breaking.
2022-05-16 15:29:39 +02:00
Leo Alt
6a126f6ccb
Update tests and hashes for z3 4.8.17
2022-05-13 15:25:10 +02:00
Leo Alt
cbaba6f913
update tests
2022-05-11 20:02:31 +02:00
chriseth
a137d42094
Merge pull request #13007 from ethereum/develop
...
Merge develop into breaking.
2022-05-11 16:39:24 +02:00
Kamil Śliwak
0e0d1972f9
Disable non-deterministic counterexamples in some SMT tests
...
- The counterexamples sometimes do appear and the tests fail.
2022-05-10 12:48:01 +02:00
Leo Alt
201c6c6819
fix smt flaky test
2022-05-05 11:38:16 +02:00
Leo Alt
cba3d18f66
adjust for osx nondeterminism
2022-05-04 19:04:54 +02:00
Leo Alt
4fd7de36f1
update smt tests z3 4.8.16
2022-05-03 14:23:27 +02:00
chriseth
a433511128
Merge remote-tracking branch 'origin/develop' into breaking
2022-04-13 17:08:27 +02:00
Leo Alt
f9fa76c9d3
smt encode call
2022-04-11 12:19:41 +02:00
chriseth
6b88e470ff
Merge remote-tracking branch 'origin/develop' into breaking
2022-03-07 16:34:55 +01:00
Leo Alt
bef69b595b
Ignore cex in SMT test
2022-02-28 18:56:20 +01:00
chriseth
814e233b67
Merge pull request #12604 from ethereum/develop
...
Merge develop into breaking
2022-01-31 17:59:03 +01:00
Leo Alt
098a3cb537
adjust tests for nondeterminism
2022-01-12 18:43:18 +01:00
Daniel Kirchner
1655626e0a
Remove counterexample from test.
2022-01-12 17:58:05 +01:00
Leo Alt
9f171c0f06
update smtchecker tests for new z3
2022-01-12 15:13:34 +01:00
Leo Alt
fb8c138b8b
Do not analyze unecessary contracts
2021-12-24 19:36:32 +01:00
chriseth
923d1cf2d2
Merge pull request #12423 from ethereum/develop
...
Merge develop into breaking.
2021-12-20 11:40:40 +01:00
Marenz
7a96953e78
Implement typechecked abi.encodeCall()
2021-12-16 17:35:58 +01:00
chriseth
c79ced0558
Merge pull request #12407 from ethereum/develop
...
Merge develop into breaking.
2021-12-14 18:54:25 +01:00
Leo Alt
316be7206f
Fix soundness of storage/memory pointers that were not erasing enough knowledge
2021-12-14 12:02:18 +01:00
chriseth
0bbf58ec5e
Merge pull request #12376 from ethereum/develop
...
Merge `develop` into `breaking`
2021-12-13 12:59:33 +01:00
Leo Alt
16535aae32
Fix ICE when unsafe targets are solved more than once and the cex is different
2021-12-03 00:21:38 +01:00
Leo Alt
a2588533e5
macos nondeterminism
2021-11-24 20:41:22 +01:00
Leo Alt
0c34d9df88
Adjust tests for nondeterminism
2021-11-24 20:41:22 +01:00
Leo Alt
ff5c842d67
update smtchecker tests
2021-11-24 20:41:22 +01:00
chriseth
88cc42230f
Merge remote-tracking branch 'origin/develop' into breaking
2021-11-09 18:26:34 +01:00
Leo Alt
dff280cadc
Fix ICE in CHC when using gas in the function options
2021-11-03 15:40:54 +01:00
Leo Alt
e40cf92b1d
[SMTChecker] Merge all entry points for a target
2021-11-03 11:12:58 +01:00
chriseth
8c6e5e501b
Merge remote-tracking branch 'origin/develop' into breaking
2021-10-27 18:09:13 +02:00
Leo Alt
38b0cf7f9c
SMTChecker tests
2021-10-26 11:30:30 +02:00
chriseth
8bcbe946c6
Merge remote-tracking branch 'origin/develop' into breaking
2021-10-06 12:00:17 +02:00
Leo Alt
4c2b661eaa
[SMTChecker] Report values for block, msg and tx variables in counterexamples
2021-10-05 15:19:10 +02:00
Leo Alt
d81ebe97c3
Fix magic access
2021-10-01 12:57:06 +02:00
Leo Alt
d25fb29178
Add isoltest option to ignore OS
2021-10-01 12:45:36 +02:00
Leo Alt
e74f853c6b
[SMTChecker] Support user types
2021-09-21 13:23:17 +02:00
Leo Alt
a1bea368cb
[SMTChecker] Support constants via modules
2021-09-16 14:35:05 +02:00
Leo Alt
b731957e65
Fix BMCs constraints on internal functions
2021-09-15 14:42:39 +02:00
Leo Alt
d91f75deb8
Fix ICE on unique errors
2021-09-09 16:37:43 +02:00
Leo Alt
6e2fe1e340
[SMTChecker] Cleanup spurious messages about TypeTypes
2021-09-07 16:55:25 +02:00
Leo Alt
106c591dde
Support the external call option
2021-09-01 20:18:37 +02:00
chriseth
e6b642699b
Merge remote-tracking branch 'origin/develop' into breaking
2021-08-31 10:36:23 +02:00
Leo Alt
ac528cfd1b
add static array length constraint
2021-08-30 17:15:16 +02:00
Leo Alt
16bc15acac
Fix false negative on storage array references returned by internal functions
2021-08-28 09:30:53 +02:00
Leo Alt
60b866f9d8
Fix ICE on multi-source use of abi.*
2021-08-27 18:55:36 +02:00
Leo Alt
0cc9162fb5
Update SMTChecker tests
2021-08-27 16:25:09 +02:00
Leo Alt
a9af63187e
Adjust tests for nondeterminism
2021-08-25 21:10:43 +02:00
