39 Commits

Author	SHA1	Message	Date
Mathias Baumann	e197ebbdd1	Replace TypePointer with Type const*	2021-03-23 11:47:19 +01:00
Alex Beregszaszi	bd641a5206	Enable more C++ compiler warnings	2020-12-10 21:03:58 +00:00
Martin Blicha	80d743426f	[SMTChecker] Added support for struct constructor.	2020-11-23 13:45:17 +01:00
Leonardo Alt	e38d0db683	[SMTChecker] Fix internal error when array.push() is used as LHS of assignment	2020-11-02 13:32:53 +00:00
Leonardo Alt	d3d77e482c	Fix ICE on conditions with tuples of rationals	2020-10-23 14:47:53 +01:00
Leonardo Alt	a2cdde1191	Add tx data to symbolic state	2020-10-13 17:49:04 +01:00
Leonardo Alt	7b3cd019d4	Make recursive structs unsupported	2020-09-03 15:19:33 +02:00
Leonardo Alt	e61b731647	[SMTChecker] Support structs	2020-09-03 15:19:03 +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
Djordje Mijovic	c6e4943089	Adding fixes for signedness warnings in libsolidity ... Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>	2020-06-10 10:41:55 +02:00
Leonardo Alt	9e9f0c52e1	[SMTChecker] Support to bitwise	2020-05-27 20:59:00 +02:00
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	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