Nikola Matic
|
d0a5556fd0
|
Purge using namespace from libsolidity/formal
|
2023-08-15 14:40:27 +02:00 |
|
Marenz
|
f7cc29bec1
|
Add std:: qualifier to move() calls
|
2022-08-30 11:12:15 +02:00 |
|
TerranCivilian
|
c15501eea9
|
Remove unneeded include files
|
2021-06-07 12:53:18 -04:00 |
|
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 |
|