194 Commits

Author	SHA1	Message	Date
chriseth	9605b85c21	Merge pull request #9352 from ethereum/smt_cex ... [SMTChecker] CHC counterexamples	2020-07-27 19:21:04 +02:00
Leonardo Alt	b207222af7	Fix extra parens	2020-07-27 17:14:59 +02:00
Leonardo Alt	de4ae301c4	[SMTChecker] Fix ICE when tuples have extra effectless parens	2020-07-27 13:03:27 +02:00
Leonardo Alt	95484d9969	Fix tests after rebase	2020-07-23 18:49:03 +02:00
Leonardo Alt	d70ebbb62d	Remove problematic test	2020-07-23 18:49:03 +02:00
Leonardo Alt	5bb4e73693	Review 1	2020-07-23 18:49:03 +02:00
Leonardo Alt	003c9b9a5b	Update tests	2020-07-23 18:49:03 +02:00
Leonardo Alt	9d2a0947e9	Fix 1-tuple chain	2020-07-23 13:46:41 +02:00
chriseth	6bb6783d39	Merge remote-tracking branch 'origin/develop' into breaking	2020-07-22 15:26:44 +02:00
chriseth	9be5ed1220	Merge remote-tracking branch 'origin/develop' into breaking	2020-07-21 11:35:28 +02:00
Leonardo Alt	2c93278719	Fix push().push()	2020-07-20 17:17:35 +02:00
Leonardo Alt	2e1067a05a	Set type properly for event parameters	2020-07-17 11:17:27 +02:00
Leonardo Alt	672633af0a	[SMTChecker] Fix ICE on compound assignment to array index	2020-07-16 17:44:10 +02:00
chriseth	f945163909	Merge pull request #9432 from ethereum/develop ... Merge develop into breaking.	2020-07-16 17:14:45 +02:00
Leonardo Alt	46653b2d43	Fix ICE when bitwise operator on fixed bytes	2020-07-15 19:32:15 +02:00
chriseth	9743390a53	Update tests.	2020-07-07 12:16:18 +02:00
chriseth	ab68406006	Merge remote-tracking branch 'origin/develop' into breaking	2020-07-06 15:25:25 +02:00
Leonardo Alt	5517e817d5	Do not trust code of external functions	2020-07-01 18:20:46 +02:00
Leonardo Alt	5160f89c1b	[SMTChecker] Support to external calls to unknown code	2020-07-01 18:20:33 +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	8155ad2187	Merge remote-tracking branch 'origin/develop' into breaking	2020-06-15 17:11:41 +02:00
Leonardo Alt	3c4e286390	[SMTChecker] Replace wrap mod by slack vars	2020-06-12 14:57:21 +02:00
chriseth	6b3171c38b	Merge remote-tracking branch 'origin/develop' into breaking	2020-06-10 11:30:50 +02:00
Leonardo Alt	f49e2424b2	[SMTChecker] Erase knowledge when array variable is pushed	2020-06-08 10:23:06 +02:00
Leonardo	d243f5baac	Merge pull request #9045 from ethereum/smt_fix_tuple ... [SMTChecker] Fix internal error in tuples of tuples.	2020-06-05 14:21:32 +02:00
Leonardo	731e6466a0	Merge pull request #9067 from ethereum/smt_fix_fp_again ... [SMTChecker] Fix BMC targets with FP	2020-06-05 12:39:28 +02:00
Leonardo Alt	87ceb72b82	[SMTChecker] Fix internal error in tuples of tuples.	2020-06-05 12:20:47 +02:00
chriseth	c8b9d24eba	Merge pull request #9106 from ethereum/develop ... Merge develop into breaking.	2020-06-03 13:51:28 +02:00
Leonardo Alt	10162016ae	[SMTChecker] Fix internal error on try/catch	2020-06-02 16:51:53 +02:00
Leonardo	97cb091ada	Merge pull request #9068 from ethereum/smt_fix_state_var_init_call ... [SMTChecker] Relax assertion about callstack	2020-06-02 15:53:14 +02:00
Leonardo Alt	ede39fc2da	[SMTChecker] Relax assertion about callstack	2020-06-02 12:50:51 +02:00
Leonardo Alt	2128ff9f13	Fix ICE on push for member access	2020-05-29 19:13:27 +02:00
Leonardo Alt	e5d25692a5	[SMTChecker] Fix BMC targets with FP	2020-05-29 18:13:13 +02:00
chriseth	0b216f5771	Merge pull request #9050 from ethereum/smt_fix_nonvalue_asgn ... [SMTChecker] Fix ICE on index access assignment inside single branches	2020-05-28 16:25:46 +02:00
Leonardo	1051cea91c	Merge pull request #9052 from ethereum/smt_add_test_delete_m_d_array ... [SMTChecker] Add test that deletes arrays	2020-05-28 16:14:55 +02:00
Leonardo Alt	9b0146be42	Add test	2020-05-28 15:56:47 +02:00
Leonardo Alt	ec766958ea	Add test	2020-05-28 13:14:21 +02:00
Leonardo Alt	13f32268da	[SMTChecker] Add test that shows that deleting arrays takes the index into account	2020-05-28 13:08:16 +02:00
Leonardo Alt	9e9f0c52e1	[SMTChecker] Support to bitwise	2020-05-27 20:59:00 +02:00
chriseth	69a028b49c	Merge remote-tracking branch 'origin/develop' into breaking	2020-05-26 10:11:23 +02:00
Leonardo Alt	0fda5fe077	[SMTChecker] Add test that has an unused mapping	2020-05-25 10:24:48 +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	1ab6ad79d8	Update test expectation	2020-05-18 16:59:31 +02:00
Leonardo Alt	2435ab938c	Add verification target for empty pop	2020-05-18 16:35:56 +02:00
Leonardo Alt	d4d26c02e4	Assume that push will not overflow	2020-05-18 16:35:56 +02:00
Leonardo Alt	07bb1952a7	Test updates	2020-05-14 23:32:30 +02:00
Leonardo Alt	a0c605aa85	[SMTChecker] Support array length	2020-05-14 23:32:29 +02:00
chriseth	993a7941b1	Merge remote-tracking branch 'origin/develop' into breaking	2020-05-14 17:24:40 +02:00