22215 Commits

This Branch

This Branch

All Branches

Author	SHA1	Message	Date
Leo Alt	673e9fc0e2	Update tests and hashes for z3 4.8.17	2022-05-15 19:00:21 +02:00
Daniel Kirchner	16f58bca72	Increase CircleCI node size for soltest_all runs.	2022-05-15 19:00:08 +02:00
Daniel Kirchner	824b71c5e5	Bug list entry, changelog entry and tests.	2022-05-15 19:00:08 +02:00
Daniel Kirchner	cee2427771	Bugfix.	2022-05-15 19:00:08 +02:00
Daniel Kirchner	634c7f036c	Test case for the buggy behaviour.	2022-05-15 19:00:08 +02:00
Leo Alt	b5a1de909a	fixup Changelog	2022-05-15 18:59:45 +02:00
Leo Alt	321bf8a595	Increase memory for clang tests	2022-05-12 17:37:03 +02:00
Leo Alt	d85494a77d	adjust nondet	2022-05-12 17:35:44 +02:00
Leo Alt	0d0add2afc	more smtchecker tests	2022-05-12 15:52:29 +02:00
Leo Alt	98930344e8	new tests with address state variables	2022-05-12 15:19:51 +02:00
Leo Alt	ff01c7275c	fixup new tests external calls	2022-05-12 15:19:51 +02:00
Leo Alt	5daa97f417	fixup external low calls	2022-05-12 15:19:51 +02:00
Leo Alt	7092caf6bf	Adjust tests for nondeterminism	2022-05-12 15:19:51 +02:00
Leo Alt	17add47a27	Fix compilation after rebase	2022-05-12 15:19:51 +02:00
Leo Alt	671adfb644	Havoc the state when state variables of reference type contain contract type	2022-05-12 15:19:51 +02:00
Leo Alt	43e08ba243	Fix getters to this	2022-05-12 15:19:51 +02:00
Leo Alt	e7dede36d0	adjust old tests	2022-05-12 15:19:51 +02:00
Leo Alt	d982e1613c	commandline tests	2022-05-12 15:19:51 +02:00
Leo Alt	ba4173cd8a	Add new tests with semantic this and indirect storage changes	2022-05-12 15:19:51 +02:00
Leo Alt	8234e238b2	Docs	2022-05-12 15:19:51 +02:00
Leo Alt	8cb5f04356	Changelog	2022-05-12 15:19:51 +02:00
Leo Alt	154e7619e0	Add smtchecker isoltest options for contract and trusted external calls	2022-05-12 15:19:51 +02:00
Leo Alt	9c7e1bbbb5	Support getters in trusted mode too	2022-05-12 15:19:51 +02:00
Leo Alt	4b1cfcd54e	Adjust tests/tools	2022-05-12 15:19:51 +02:00
Leo Alt	397bd7da4f	Add CLI option for smtchecker trusted external calls	2022-05-12 15:19:51 +02:00
Leo Alt	d4e4189a85	Adjust counterexamples for synthesized calls to external contracts that are state variables in the analyzed contract	2022-05-12 15:19:51 +02:00
Leo Alt	a66ba81dad	State variables of contract type may have their state changed between txs of the analyzed contract in trusted mode	2022-05-12 15:19:51 +02:00
Leo Alt	99e7622a89	Support external calls as trusted code	2022-05-12 15:19:51 +02:00
Leo Alt	4fa765172c	Refactor usesStaticCall	2022-05-12 15:19:51 +02:00
Leo Alt	e0cda47603	Support deployment	2022-05-12 15:19:51 +02:00
Leo Alt	287ea63cde	Create setting for trusted/untrusted external calls	2022-05-12 15:19:51 +02:00
Leo Alt	37f6dc1f88	Add storage to state	2022-05-12 15:19:51 +02:00
Leo Alt	08781eb8f5	Extract contractAddressValue into own function	2022-05-12 15:19:51 +02:00
Leo	2aba061bde	Merge pull request #12967 from ethereum/update_z3_docker ... Update docker z3 version 4.8.16	2022-05-12 15:23:03 +02:00
Leo	96bf85b35b	Merge pull request #13012 from ethereum/z3-use-rebuilt-buildpack-images ... Switch to newly built buildpack-deps images with Z3 4.8.16 in CI	2022-05-12 15:16:12 +02:00
Leo	80a055103e	Merge pull request #13009 from ethereum/smt_support_z3_16 ... Support new z3 AST node	2022-05-12 14:28:38 +02:00
Kamil Śliwak	c0cc8ff7e7	Switch to newly built buildpack-deps images in CI	2022-05-12 14:26:07 +02:00
Leo Alt	2fe143f7d0	add changelog entry and docs note	2022-05-12 13:43:28 +02:00
Leo Alt	60b405aaa9	Support new z3 AST node	2022-05-12 10:50:30 +02:00
Leo	0c0ff4fce6	Merge pull request #13000 from ethereum/smt_fix_recursive ... [SMTChecker] Fix check that solver is available	2022-05-11 21:52:52 +02:00
Leo Alt	4c00815c53	Changelog entry	2022-05-11 20:02:31 +02:00
Leo Alt	cbaba6f913	update tests	2022-05-11 20:02:31 +02:00
Leo Alt	93f9638a1b	Add error id to script	2022-05-11 20:02:31 +02:00
Leo Alt	75d08ea924	Check early if solvers are available.	2022-05-11 20:02:31 +02:00
Daniel Kirchner	1d7b4704bb	Merge pull request #13006 from ethereum/initializationOrderFix ... Fix asorted compilation issues with GCC 12.	2022-05-11 17:19:45 +02:00
Daniel Kirchner	cf311e5780	Disable maybe-unitialized warning for boost headers using a pragma.	2022-05-11 16:21:53 +02:00
Daniel Kirchner	cbf9a4f1ed	Add bogus return to switch.	2022-05-11 13:58:06 +02:00
Daniel Kirchner	ece547204a	Reorder member variables of unique error reporter to ensure proper initialization order.	2022-05-11 13:40:02 +02:00
Kamil Śliwak	c64fb7a258	docker_upgrade.sh: Workaround for git refusing to work with a repo in attached volume	2022-05-10 18:24:21 +02:00
Leo Alt	571d94b051	Update docker z3 version	2022-05-10 18:24:21 +02:00