26 Commits

Author	SHA1	Message	Date
Leonardo Alt	5d9dd654cf	[SMTChecker] Add and use tuple sort	2020-04-08 18:26:03 +02:00
Leonardo Alt	2cfa44bba3	Allow constructing symbolic arrays from smt sort	2020-04-06 10:50:00 +02:00
Christian Parpart	6b23412fae	C++ namespace cleanup (except tests).	2020-01-07 15:51:50 +01:00
Leonardo Alt	d818746e0c	[SMTChecker] Fix ICE in abi.decode	2019-11-18 13:15:10 +01:00
Leonardo Alt	e3652627fd	[SMTChecker] Fix ICE in CHC when function used as argument	2019-11-13 15:11:30 +01:00
Leonardo Alt	360f868836	[SMTChecker] Fix literal string type mismatch	2019-08-10 21:51:46 +02:00
Leonardo Alt	6bcbeb1d23	[SMTChecker] Reset SSA index to 0 instead of increasing in context reset	2019-07-25 14:16:34 +02:00
Leonardo Alt	4aebdcc442	[SMTChecker] Allow FunctionSort to be created via sort and not type	2019-07-04 12:00:24 +02:00
Leonardo Alt	934e00d235	[SMTChecker] SymbolicVariables use EncodingContext to declare SMT vars	2019-07-03 16:05:56 +02:00
Leonardo Alt	fac383a233	Move SMT specific code into smt namespace	2019-05-10 20:03:11 +02:00
Leonardo Alt	c8a017ccd6	[SMTChecker] Use unique_ptr instead of shared_ptr where applicable.	2019-05-09 16:34:22 +02:00
Leonardo Alt	6c7527ac90	[SMTChecker] Support tuple type declaration	2019-05-02 12:05:21 +02:00
Christian Parpart	58a45f2cb6	[libsolidity] TypeProvider: adds explicit uint256() accessor and removes default params in integerType(...).	2019-04-16 18:28:40 +02:00
Christian Parpart	bf43eebea9	libsolidity: Introducing TypeProvider API, for clear type system ownership.	2019-04-16 18:26:45 +02:00
Leonardo Alt	07fac9e381	[SMTChecker] Allow SymbolicVariable from smt::Sort	2019-04-15 14:52:46 +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
Daniel Kirchner	8ca6715e18	More style checks.	2019-02-14 11:41:20 +01:00
Leonardo Alt	cce377833a	Sort includes in libsolidity/formal	2018-12-17 18:26:10 +01:00
Leonardo Alt	6a2809a582	[SMTChecker] Support to mapping	2018-12-14 12:21:53 +01:00
Leonardo Alt	de46bb2c42	[SMTChecker] Introduce SymbolicFunctionVariable	2018-12-10 11:34:29 +01:00
Leonardo Alt	b9f424e373	[SMTChecker] Simplify symbolic variables	2018-12-05 09:56:52 +01:00
Leonardo Alt	ec84a7dc9b	[SMTChecker] Refactor setZeroValue and setUnknownValue	2018-11-22 16:42:51 +01:00
Leonardo Alt	13a142b039	[SMTChecker] Add FunctionSort and refactors the solver interface to create variables	2018-11-22 10:04:04 +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