20 Commits

Author	SHA1	Message	Date
Leo Alt	60b866f9d8	Fix ICE on multi-source use of abi.*	2021-08-27 18:55:36 +02:00
Leo Alt	61160aa0e7	Add constraints correlating address(this).balance and msg.value	2021-08-25 21:10:08 +02:00
chriseth	90c4623460	Some more base fees.	2021-08-12 16:37:21 +02:00
Mathias Baumann	e197ebbdd1	Replace TypePointer with Type const*	2021-03-23 11:47:19 +01:00
Martin Blicha	a49950cdf3	[SMTChecker] Added transaction constraints also for contract deployment	2021-02-01 16:46:34 +01:00
Leonardo Alt	a612daa783	Add msgvalue to cex	2021-01-21 19:05:44 +01:00
Martin Blicha	504e4c22b2	[SMTChecker] Fix in abi handling - tuple expression of size 1 has the type of the member and not TupleType	2021-01-14 14:53:56 +01:00
Martin Blicha	32a923c7ef	[SMTChecker] Fix in abi handling - abstracting expressions of type Function inside ABI functions when translating to SMT	2021-01-14 14:53:22 +01:00
Martin Blicha	be0a0f4d90	[SMTChecker] Added constraints for block properties	2020-12-29 22:17:44 +01:00
Leonardo Alt	2cbf33ca1c	SMTChecker support ABI functions as UFs	2020-12-17 14:03:17 +01:00
Alex Beregszaszi	2f899bbffa	[SMTChecker] Avoid implicit conversion	2020-11-11 16:29:03 +00:00
Leonardo Alt	54f76e081a	[SMTChecker] Support crypto functions in CHC	2020-10-16 14:57:13 +01:00
Leonardo Alt	a2cdde1191	Add tx data to symbolic state	2020-10-13 17:49:04 +01: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
Leonardo Alt	ac93ee1d08	Move error flag from CHC to SymbolicState	2020-09-28 12:37:57 +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	45eba27424	Rename namespace	2020-05-20 12:55:18 +02:00
Leonardo Alt	a0c605aa85	[SMTChecker] Support array length	2020-05-14 23:32:29 +02:00
Leonardo Alt	05a85461fe	Symbolic state	2020-04-06 12:27:53 +02:00