413 Commits

Author	SHA1	Message	Date
Jason Cobb	888d7037cd	Make FunctionCallAnnotation::kind a SetOnce	2020-08-12 11:57:01 -04:00
Leonardo Alt	ec31d971e6	[SMTChecker] Fix tuple name for arrays	2020-08-07 12:28:10 +02:00
Leonardo Alt	8df8c6e14f	[SMTChecker] Fix ICE in BMC function inlining	2020-08-05 11:47:25 +02:00
Leonardo Alt	ad1798b000	[SMTChecker] Fix ICE on fixed bytes access	2020-07-28 17:59:42 +02:00
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	d5f00842d9	cex2dot debug	2020-07-23 18:49:03 +02:00
Leonardo Alt	5bb4e73693	Review 1	2020-07-23 18:49:03 +02:00
Leonardo Alt	51721c3080	Double SAT run for cex	2020-07-23 18:49:03 +02:00
Leonardo Alt	694ec92688	Generate counterexample message based on cex graph	2020-07-23 18:49:03 +02:00
Leonardo Alt	744905525f	Convert z3 cex graph into STL	2020-07-23 18:49:03 +02:00
Leonardo Alt	a7a069c74a	Refactor constructor exit	2020-07-23 18:49:03 +02:00
Leonardo Alt	9d2a0947e9	Fix 1-tuple chain	2020-07-23 13:46:41 +02:00
Leonardo Alt	2c93278719	Fix push().push()	2020-07-20 17:17:35 +02:00
Sachin Grover	b7adb2aa42	Add SPDX license identifier if not present already in source file ... Fixes: #9220	2020-07-17 20:24:12 +05:30
Leonardo Alt	672633af0a	[SMTChecker] Fix ICE on compound assignment to array index	2020-07-16 17:44:10 +02:00
Leonardo Alt	46653b2d43	Fix ICE when bitwise operator on fixed bytes	2020-07-15 19:32:15 +02:00
chriseth	b3566ad0d5	Merge pull request #9082 from ethereum/conversionWarnings ... Adding `-Wsign-conversion` flag and fixing errors	2020-07-13 11:28:09 +02:00
Leonardo Alt	88030c6568	[SMTChecker] Refactor verification targets	2020-07-10 10:28:49 +02:00
Alex Beregszaszi	a0300835eb	Change CHC to avoid sign mismatch	2020-07-09 17:22:52 +02:00
Djordje Mijovic	547590b972	Fixing additional signedness errors after adding -Wsign-conversion flag ... Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>	2020-07-09 17:22:45 +02:00
Leonardo Alt	f97fa9b520	[SMTChecker] Add current input variables to the function summary	2020-07-02 15:30:29 +02:00
Leonardo Alt	5517e817d5	Do not trust code of external functions	2020-07-01 18:20:46 +02:00
Leonardo Alt	56e7d43384	Rename var	2020-07-01 18:20:34 +02:00
Leonardo Alt	5160f89c1b	[SMTChecker] Support to external calls to unknown code	2020-07-01 18:20:33 +02:00
Leonardo Alt	3c4e286390	[SMTChecker] Replace wrap mod by slack vars	2020-06-12 14:57:21 +02:00
Djordje Mijovic	c6e4943089	Adding fixes for signedness warnings in libsolidity ... Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>	2020-06-10 10:41:55 +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
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
Leonardo Alt	b90fb1cab6	[SMTChecker] Fix ICE on index access assignment inside single branches	2020-05-28 15:56:46 +02:00
Leonardo Alt	a73ec6a82f	[SMTChecker] Fix ICE in inlining function calls while short circuiting	2020-05-28 13:14:19 +02:00
Leonardo Alt	cb1cbbc1f1	[SMTChecker] Fix fixed point inc/dec	2020-05-28 10:56:06 +02:00
Leonardo Alt	9e9f0c52e1	[SMTChecker] Support to bitwise	2020-05-27 20:59:00 +02:00
chriseth	9604174151	Rename asCallableFunction.	2020-05-26 11:35:12 +02:00
Leonardo Alt	7a91c9b971	Remove Type from SolverInterface	2020-05-20 12:55:19 +02:00
Leonardo Alt	45eba27424	Rename namespace	2020-05-20 12:55:18 +02:00
Leonardo Alt	087605ea02	Create libsmtutil	2020-05-20 12:55:18 +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	82db35e563	[SMTChecker] Support array push/pop	2020-05-18 16:33:34 +02:00
Leonardo Alt	a0c605aa85	[SMTChecker] Support array length	2020-05-14 23:32:29 +02:00
a3d4	7cae074b8a	Add error IDs to BMC	2020-05-12 11:39:18 +02:00