Commit Graph

15 Commits

Author SHA1 Message Date
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