264 Commits

Author	SHA1	Message	Date
Leo Alt	316be7206f	Fix soundness of storage/memory pointers that were not erasing enough knowledge	2021-12-14 12:02:18 +01:00
Leo Alt	d81ebe97c3	Fix magic access	2021-10-01 12:57:06 +02:00
chriseth	1531863835	Split Common.h into Numeric.h.	2021-09-23 15:27:29 +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	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
Marenz	2b28f87abf	Add type().min/max for enums	2021-09-01 15:02:02 +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	8e81df1bd3	Do not show redundant unsupported errors in SMTChecker	2021-08-27 16:25:09 +02:00
Leonardo	6e6bbb2f83	Merge pull request #11837 from soroosh-sdi/use-range-v3-part2 ... Using range-v3 instead of boost	2021-08-26 09:38:27 +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
soroosh-sdi	b0ce98bcb2	Using range-v3 instead of boost ... Signed-off-by: soroosh-sdi <soroosh.sardari@gmail.com>	2021-08-24 23:50:23 +04:30
Leo Alt	d89d63bf9c	Use the nondeterministic interface also for BARECALL	2021-08-19 16:34:01 +02:00
Leo Alt	10397e440c	Fix ICE in constants	2021-08-12 10:53:01 +02:00
Leo Alt	08c065ee04	Add option divModWithSlacks	2021-08-06 15:50:25 +02:00
chriseth	e3525b81d0	Supply scanner to model checker.	2021-07-14 15:12:10 +02:00
Leo Alt	bf21cd400c	Fix conversion from bytes to fixed bytes	2021-06-01 17:55:18 +02:00
Leo Alt	95f973e08a	Fix gasleft variable name	2021-05-26 22:12:49 +02:00
Martin Blicha	9c98ab59f0	SMTChecker: fixed struct constructor where FixedBytes member is initialized with a string literal	2021-05-17 13:52:37 +02:00
Leonardo Alt	4b2ccf2f37	Abstract function smtchecker natspec	2021-05-11 15:30:19 +02:00
Leo Alt	e2959ce55c	Assign cast from constants directly	2021-05-11 14:07:09 +02:00
Leo Alt	1642c10f6e	Fix ICE in free functions	2021-05-03 10:57:11 +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
chriseth	98a8640928	Merge pull request #11203 from anurag-git/issue_10738-1 ... Use range-v3 loops (reverse, keys, values)	2021-04-01 12:19:40 +02:00
anurag4u80	bbcdddeed9	Replaced keys, values and reverse with ranges	2021-03-31 23:33:04 +05:30
Martin Blicha	330fb8f4d0	[SMTChecker] Assignment refactoring	2021-03-31 13:36:50 +02:00
Leonardo	78d94737a4	Merge pull request #11188 from blishko/issue-11181 ... [SMTChecker] Fix crash when analysing try-catch clauses with function call.	2021-03-31 11:24:36 +02:00
chriseth	b04b189959	Syntax for custom errors.	2021-03-30 21:15:18 +02:00
Martin Blicha	2d231f1859	[SMTChecker] Changed SMTEncoder::mergeVariables to work regardless which branch has been visited first	2021-03-30 20:35:44 +02:00
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
Martin Blicha	5293f05ee3	[SMTChecker] Fix ICE on ABI functions with no arguments	2021-03-25 13:28:29 +01:00
Martin Blicha	98446782e2	[SMTChecker] Fix compound assignment to push	2021-03-24 14:54:13 +01:00
Martin Blicha	852e877ae7	[SMTChecker] Handle InaccessibleDynamicType	2021-03-24 11:53:06 +01:00
Mathias Baumann	e197ebbdd1	Replace TypePointer with Type const*	2021-03-23 11:47:19 +01:00
Leonardo	25b31111df	Merge pull request #11040 from ethereum/smt_fix_virtual_one_more_time ... [SMTChecker] Fix bug in virtual functions called by constructor	2021-03-17 16:54:36 +01:00
Martin Blicha	432944d0b4	[SMTChecker] Small refactoring of defining SMT expressions for structs/tuples	2021-03-16 15:34:43 +01:00
Martin Blicha	2f52affcc2	[SMTChecker] Correctly resolve current scope contract in VariableUsage.	2021-03-15 13:55:14 +01:00
Martin Blicha	6aa6c5f5f9	[SMTChecker] Reset reference variables on assignment to a variable of reference type	2021-03-12 19:51:31 +01:00
Leonardo Alt	998346e599	Fix bug in virtual functions called by constructor.	2021-03-12 16:42:28 +01:00
Martin Blicha	0cb75293f9	[SMTChecker] fix handling of assignments of array/mapping state variable accessed using contract name	2021-03-12 14:01:07 +01:00
Martin Blicha	4285c2803b	[SMTChecker] Fix ICE on array.pop nested inside 1-tuple	2021-03-09 20:00:51 +01:00
Martin Blicha	385a664f3c	[SMTChecker] Fix public getter for array of structs.	2021-03-08 17:34:20 +01:00
Martin Blicha	0340510c53	[SMTChecker] correct handling of FixedBytes constants initialized with string literal	2021-03-04 15:14:47 +01:00
Martin Blicha	41fc59f00f	[SMTChecker] Ensure that push to a string casted to bytes is registered in the original string	2021-03-03 17:11:42 +01:00