18 Commits

Author	SHA1	Message	Date
Leonardo Alt	07368c2e1e	Add support to internal function calls	2020-03-11 16:29:07 +01:00
chriseth	2f11ac3590	Merge remote-tracking branch 'origin/develop' into develop_060	2019-12-03 21:17:15 +01:00
chriseth	96d777d7f1	Merge commit 'a7d481fb9' into develop_060	2019-12-03 20:47:30 +01:00
Leonardo Alt	b1577f5e46	[SMTChecker] Fix ICE in array of structs type	2019-12-03 01:12:30 +01:00
Leonardo Alt	9eda95caf9	[SMTChecker] Fix visit to IndexAccess that has type Type	2019-11-29 17:20:50 +01:00
chriseth	0973ae751a	Do not warn about enabled ABIEncoderV2 anymore.	2019-11-26 15:49:42 +01:00
Leonardo Alt	d818746e0c	[SMTChecker] Fix ICE in abi.decode	2019-11-18 13:15:10 +01:00
Leonardo Alt	dd1afeba52	[SMTChecker] Support this as address	2019-04-18 17:56:52 +02:00
Leonardo Alt	02d0e609b9	[SMTChecker] Support enums	2019-03-07 15:15:12 +01:00
Leonardo Alt	e74f58130e	Add SMT type support to Solidity arrays	2019-03-06 11:29:26 +01:00
Leonardo Alt	34470f3549	[SMTChecker] Only check for overflow/underflow in the end of the function	2019-02-18 23:55:58 +01:00
Leonardo Alt	a10db051de	[SMTChecker] Support basic typecast	2019-01-16 13:00:54 +01:00
Leonardo Alt	08737e43dc	[SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions	2018-12-11 11:28:25 +01:00
Kevin Kelley	fb6fd1b3c2	add a 'readable' format for large hex values	2018-12-05 22:15:02 +01:00
Leonardo Alt	70bb0eaf95	[SMTChecker] Implement uninterpreted functions and use it for blockhash()	2018-11-15 09:12:42 +01:00
Leonardo Alt	d8cbf321da	Grouping of symbolic variables in the same file and support to FixedBytes	2018-10-25 09:30:48 +02:00
Leonardo Alt	e2cf5f6ed9	Add gasleft constraint and use full member access name	2018-10-22 18:19:11 +02:00
Leonardo Alt	b46b827c30	[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash	2018-10-19 15:52:16 +02:00