482 Commits

Author	SHA1	Message	Date
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
Leo Alt	4cf4ccafd7	New tests	2021-08-25 21:10:08 +02:00
Leo Alt	85378b1770	Update existing tests	2021-08-25 21:10:08 +02:00
Alex Beregszaszi	9803b62a50	Merge pull request #11840 from ethereum/develop ... Merge develop to breaking	2021-08-25 15:37:08 +01:00
Leo Alt	718f392849	Don't erase things for BMC if function call is staticcall	2021-08-25 14:09:46 +02:00
Leo Alt	a55685c04f	Erase balances when delegatecall is seen	2021-08-25 12:39:26 +02:00
Leo Alt	9ea4576664	Update tests	2021-08-19 16:34:01 +02:00
chriseth	aeb2438eab	Fix shadowing error for inline assembly.	2021-08-17 12:12:56 +02:00
Leo Alt	937af7d722	Fix SMT test	2021-08-12 22:34:18 +02:00
chriseth	fe0d027d45	Merge pull request #11785 from ethereum/someMoreBaseFees ... Some more base fees.	2021-08-12 19:48:10 +02:00
Leo Alt	6ee60aa628	Fix false positive on external calls from constructors	2021-08-12 18:51:55 +02:00
chriseth	c87c0f02bd	Test updates.	2021-08-12 16:56:12 +02:00
Leo Alt	10397e440c	Fix ICE in constants	2021-08-12 10:53:01 +02:00
Leo Alt	3c1f555f71	Tests	2021-08-04 13:54:50 +02:00
Leo Alt	e46abd0ca1	Update tests due to nondeterminism	2021-07-19 15:20:11 +02:00
Leo Alt	20e23171da	Update tests to z3 4.8.12	2021-07-16 14:43:52 +02:00