146 Commits

Author	SHA1	Message	Date
Leo Alt	4c2b661eaa	[SMTChecker] Report values for block, msg and tx variables in counterexamples	2021-10-05 15:19:10 +02:00
Leo Alt	e74f853c6b	[SMTChecker] Support user types	2021-09-21 13:23:17 +02:00
Leo Alt	106c591dde	Support the external call option	2021-09-01 20:18:37 +02:00
Leo Alt	60b866f9d8	Fix ICE on multi-source use of abi.*	2021-08-27 18:55:36 +02:00
Leo Alt	8e81df1bd3	Do not show redundant unsupported errors in SMTChecker	2021-08-27 16:25:09 +02:00
Leo Alt	61160aa0e7	Add constraints correlating address(this).balance and msg.value	2021-08-25 21:10:08 +02:00
Leo Alt	a55685c04f	Erase balances when delegatecall is seen	2021-08-25 12:39:26 +02:00
Leo Alt	d89d63bf9c	Use the nondeterministic interface also for BARECALL	2021-08-19 16:34:01 +02:00
Leo Alt	6ee60aa628	Fix false positive on external calls from constructors	2021-08-12 18:51:55 +02:00
Leo Alt	10397e440c	Fix ICE in constants	2021-08-12 10:53:01 +02:00
Leo Alt	685d7a8c99	Bundle all unproved targets in a single message and only show all if setting chooses that	2021-08-04 13:54:50 +02:00
Leo Alt	6c8ecfa82c	Add option to choose solver	2021-07-27 17:14:21 +02:00
chriseth	e3525b81d0	Supply scanner to model checker.	2021-07-14 15:12:10 +02:00
Leo Alt	547a6915ad	Fix ICE on external calls from constructor	2021-06-01 14:21:48 +02:00
Leo Alt	f7b045b886	review	2021-05-26 22:12:49 +02:00
Leo Alt	daea5f886d	Fix CHCSmtLib2Interface	2021-05-26 22:12:49 +02:00
Leonardo Alt	4b2ccf2f37	Abstract function smtchecker natspec	2021-05-11 15:30:19 +02:00
Leonardo Alt	dd1865873e	Choose contracts to be analyzed by the SMTChecker	2021-04-21 10:34:14 +02:00
Leonardo Alt	095d337140	Basic support to free constants	2021-04-19 19:23:18 +02:00
Leonardo Alt	4e34359063	Basic support to free functions	2021-04-19 19:23:18 +02:00
Leonardo Alt	b753cb6120	Deprecate pragma experimental SMTChecker	2021-04-08 21:03:38 +02:00
anurag4u80	bbcdddeed9	Replaced keys, values and reverse with ranges	2021-03-31 23:33:04 +05:30
Leonardo Alt	ba97d6ac4e	Add local vars to cex	2021-03-30 17:55:21 +02:00
Leonardo Alt	dbd067d6db	Report out of bounds index access	2021-03-30 10:28:48 +02:00
Leonardo Alt	d1db41a5c8	Fix target warning order nondeterminism	2021-03-26 12:13:52 +01:00
Martin Blicha	85358dfe30	[SMTChecker] Do not create targets for contracts that cannot be deployed	2021-03-25 15:38:37 +01:00
Mathias Baumann	e197ebbdd1	Replace TypePointer with Type const*	2021-03-23 11:47:19 +01:00
Leonardo Alt	998346e599	Fix bug in virtual functions called by constructor.	2021-03-12 16:42:28 +01:00
Leonardo Alt	6fd76e830d	Fix CHC cex order	2021-03-11 10:36:40 +01:00
Martin Blicha	4285c2803b	[SMTChecker] Fix ICE on array.pop nested inside 1-tuple	2021-03-09 20:00:51 +01:00
Leonardo	7405dc5b7f	Merge pull request #10836 from ethereum/smt_fix_cex_inheritance ... Fix inheritance bug in CHC cex	2021-02-03 18:49:25 +01:00
Martin Blicha	d99256aae7	[SMTChecker] refactoring of resetting storage variables	2021-02-03 15:53:58 +01:00
Martin Blicha	f1013427a7	[SMTChecker] refactoring the accessing the encoding state	2021-02-03 15:53:58 +01:00
Leonardo Alt	665ce27c18	Fix inheritance bug in CHC cex	2021-02-02 18:06:32 +01:00
Martin Blicha	a49950cdf3	[SMTChecker] Added transaction constraints also for contract deployment	2021-02-01 16:46:34 +01:00
Leonardo Alt	545305a31f	[SMTChecker] Fix super and virtual	2021-01-28 18:51:29 +01:00
Leonardo Alt	3b23cadbdc	Add CLI and JSON option to select SMTChecker targets	2021-01-20 17:35:37 +01:00
Leonardo Alt	007d39871b	[SMTChecker] Synthesize untrusted functions called externally	2021-01-15 11:56:26 +01:00
Martin Blicha	7c6340fe4f	[SMTChecker] Refactoring expression to tuple assignment	2021-01-12 17:15:14 +01:00
Leonardo Alt	b3c3836388	Output internal calls	2021-01-12 14:57:04 +01:00
Leonardo Alt	f1ae24abc7	Remove extra line breaks	2021-01-12 14:00:07 +01:00
Martin Blicha	ff76c989ac	addressing review comments	2021-01-11 14:19:06 +01:00
Martin Blicha	dd43ce1578	fixing try/catch encoding for BMC, refactoring	2021-01-11 13:36:03 +01:00
Martin Blicha	0f3924186e	[SMTChecker] Support try-catch in CHC engine	2021-01-11 13:36:02 +01:00
Leonardo Alt	11f56861c3	Refactor cex loop	2021-01-07 23:13:02 +01:00
Leonardo Alt	78d55e6b4a	[SMTChecker] Support check/unchecked	2020-12-30 12:14:30 +01:00
Leonardo Alt	9482e7de23	[SMTChecker] Fix calls to virtual/overriden functions	2020-12-29 11:25:20 +01:00
Martin Blicha	bb0003f5ea	removed extra parameter from PredicateInstance::nondetInterface	2020-12-28 19:48:48 +01:00
Martin Blicha	f76ff35225	[SMTChecker] Detect errors caused by reentrancy	2020-12-28 14:32:53 +01:00
Martin Blicha	d90b9da4f0	[SMTChecker] Refactoring	2020-12-22 13:10:48 +01:00