507 Commits

Author	SHA1	Message	Date
chriseth	da92fe548e	Merge remote-tracking branch 'origin/develop' into breaking	2020-11-10 13:48:32 +01:00
Leonardo	25b2a38d8b	Merge pull request #10202 from ethereum/smt_fix_modifiers_branches ... [SMTChecker] Fix CHC false positives when using branches inside modifiers	2020-11-09 16:42:30 +00:00
chriseth	04195439b7	Merge remote-tracking branch 'origin/develop' into HEAD	2020-11-09 14:28:05 +01:00
Leonardo Alt	00858c0ccf	Isoltets SMTChecker option and BMC specific tests	2020-11-06 15:03:38 +00:00
Leonardo Alt	89dce24f24	Force SMT variable creation order	2020-11-06 11:51:01 +00:00
Leonardo Alt	646be53f2f	Sort variables and expressions by AST id	2020-11-06 11:50:43 +00:00
Leonardo Alt	1dbd8f8d67	Fix CHC false positives when using branches inside modifiers	2020-11-04 21:47:07 +00:00
Leonardo	62535c2fd4	Merge pull request #10181 from ethereum/smt_user_timeout ... [SMTChecker] User timeout option	2020-11-04 10:55:28 +00:00
Leonardo Alt	daf859c15b	[SMTChecker] report SMTEncoder warnings also via CHC	2020-11-03 16:06:17 +00:00
chriseth	5ffee049fa	Merge remote-tracking branch 'origin/develop' into breaking	2020-11-03 14:05:14 +01:00
Leonardo Alt	d03ddeb0fa	[SMTChecker] User timeout option	2020-11-03 10:46:11 +00:00
Leonardo Alt	e38d0db683	[SMTChecker] Fix internal error when array.push() is used as LHS of assignment	2020-11-02 13:32:53 +00:00
Leonardo Alt	94e2506132	Fix inherited state vars for BMC	2020-11-02 11:42:39 +00:00
Martin Blicha	c1a57ffbfe	[SMTChecker] More precise creation of verification targets.	2020-10-30 19:11:28 +01:00
chriseth	e93a84ccd4	Merge remote-tracking branch 'origin/develop' into HEAD	2020-10-28 18:19:31 +01:00
Đorđe Mijović	1f50b86aad	Merge pull request #10073 from ethereum/smt_format_array_cex ... Format array cex	2020-10-28 12:39:19 +01:00
Leonardo Alt	25f75ce547	Remove nondet tests	2020-10-28 11:03:42 +00:00
Leonardo	07c454949f	Merge pull request #10127 from ethereum/fixIceSmtBitwise ... [SMTChecker] Fix ICE when using >>>	2020-10-28 09:28:18 +00:00
Djordje Mijovic	9cc37c3fa4	[SMTChecker] Fix ICE when using >>>	2020-10-28 09:25:14 +01:00
Leonardo Alt	f2f84a7f97	Format array cex	2020-10-27 16:32:43 +00:00
Leonardo Alt	446e46fe06	Use Expression instead of plain strings for counterexamples	2020-10-27 12:04:51 +00:00
Leonardo Alt	4755cfe157	Fix assignment to contract member access	2020-10-26 14:39:02 +00:00
Leonardo Alt	d3d77e482c	Fix ICE on conditions with tuples of rationals	2020-10-23 14:47:53 +01:00
chriseth	20f39ab6e9	Merge pull request #10097 from ethereum/develop ... Merge develop into breaking.	2020-10-23 10:30:24 +02:00
chriseth	bfc8e26007	Remove low-level log functions.	2020-10-22 17:50:14 +02:00
Martin Blicha	ade3b9951c	[SMTChecker] Added support for selector when expression's value is known at compile time	2020-10-22 14:18:52 +02:00
Leonardo Alt	b087fa9750	[SMTChecker] Fix ICE implicit conversion string literal -> byte	2020-10-21 22:03:01 +01:00
Martin Blicha	f0d81601db	[SMTChecker] Adding division by zero checks in the CHC engine	2020-10-21 14:48:33 +02:00
Leonardo Alt	cf35785328	Add unknown message to all verification targets	2020-10-19 20:54:13 +01:00
chriseth	6979952995	Merge remote-tracking branch 'origin/develop' into HEAD	2020-10-19 18:02:50 +02:00
Leonardo	a097f9f124	Merge pull request #10025 from ethereum/smt_crypto_functions ... [SMTChecker] Support crypto functions in CHC	2020-10-16 16:40:29 +01:00
Leonardo	8d7bdcaba7	Merge pull request #10036 from ethereum/smt_cli_option ... Add CLI option to choose model checker engine	2020-10-16 16:37:33 +01:00
Martin Blicha	78c8fbc7ce	[SMTChecker] encoding division and modulo operations using slack variables	2020-10-16 16:06:31 +02:00
Leonardo Alt	4e49135318	Add CLI option to choose model checker engine	2020-10-16 15:01:47 +01:00
Leonardo Alt	54f76e081a	[SMTChecker] Support crypto functions in CHC	2020-10-16 14:57:13 +01:00
chriseth	979d3062bc	Merge pull request #10033 from ethereum/develop ... Merge develop into breaking	2020-10-14 14:12:20 +02:00
Leonardo Alt	440e5b3935	[SMTChecker] Fix counterexample state reporting	2020-10-13 22:18:43 +01:00
Leonardo Alt	aec456021d	Add tx constraints to CHC	2020-10-13 17:49:04 +01:00
Leonardo Alt	a2cdde1191	Add tx data to symbolic state	2020-10-13 17:49:04 +01:00
chriseth	f6e57a0eec	Merge pull request #10023 from ethereum/develop ... Merge develop into breaking.	2020-10-13 18:18:53 +02:00
Mathias Baumann	006e5f2e1f	Allow path syntax for super constructor calls	2020-10-13 14:32:11 +02:00
Leonardo Alt	1e568d7dc6	[SMTChecker] Fix implicit constructor summary predicate	2020-10-13 09:38:58 +01:00
Djordje Mijovic	e23d8f5593	[SMTChecker] Supporting inline arrays.	2020-10-12 16:59:14 +02:00
Leonardo Alt	18cf01c187	Add this and state to CHC	2020-10-12 11:11:52 +01:00
Leonardo Alt	a86f656704	Refactor state as tuple	2020-10-12 11:11:52 +01:00
Alex Beregszaszi	fedbea46cd	[SMTChecker] Support type conversions	2020-10-02 10:26:02 +02:00
Leonardo Alt	c8cc73c80c	Support array slices	2020-10-01 11:52:02 +02:00
Leonardo Alt	352cce5fc8	[SMTChecker] Support addmod and mulmod.	2020-09-29 12:45:19 +02:00
Leonardo Alt	fa7c9a0dc6	Simplify internal function calls	2020-09-28 15:31:15 +02:00
Leonardo Alt	3519b38055	Move predicate functions from CHC to PredicateInstance	2020-09-28 12:43:19 +02:00