 Tyler
|
047034544e
|
Merge branch 'develop' of github.com:tfire/solidity into fix/remove-namespace-ast-annotations
|
2022-03-09 18:55:22 -05:00 |
|
|
Tyler
|
519e1c9402
|
Specify namespaces
Fix references into solidity::util
|
2022-03-08 00:09:17 -05:00 |
|
 wechman
|
52dfccca98
|
Replace all locale-dependent operations with locale-agnostic counterparts
|
2022-03-07 17:23:08 +01:00 |
|
 Leo Alt
|
fb8c138b8b
|
Do not analyze unecessary contracts
|
2021-12-24 19:36:32 +01:00 |
|
|
Leo Alt
|
16535aae32
|
Fix ICE when unsafe targets are solved more than once and the cex is different
|
2021-12-03 00:21:38 +01:00 |
|
|
Leo Alt
|
dff280cadc
|
Fix ICE in CHC when using gas in the function options
|
2021-11-03 15:40:54 +01:00 |
|
|
Leo Alt
|
e40cf92b1d
|
[SMTChecker] Merge all entry points for a target
|
2021-11-03 11:12:58 +01:00 |
|
|
Leo Alt
|
d419c30ca6
|
Add errorCode list to invariants report
|
2021-10-26 11:30:30 +02:00 |
|
|
Leo Alt
|
49e7627bd3
|
Use invariants in CHC
|
2021-10-26 11:30:30 +02:00 |
|
 tcoyvwac
|
ba0c09e082
|
Prefer make_unique over new
|
2021-10-15 19:46:47 +02:00 |
|
|
Leo Alt
|
4c2b661eaa
|
[SMTChecker] Report values for block, msg and tx variables in counterexamples
|
2021-10-05 15:19:10 +02:00 |
|
|
Leo Alt
|
e74f853c6b
|
[SMTChecker] Support user types
|
2021-09-21 13:23:17 +02:00 |
|
|
Leo Alt
|
106c591dde
|
Support the external call option
|
2021-09-01 20:18:37 +02:00 |
|
|
Leo Alt
|
60b866f9d8
|
Fix ICE on multi-source use of abi.*
|
2021-08-27 18:55:36 +02:00 |
|
|
Leo Alt
|
8e81df1bd3
|
Do not show redundant unsupported errors in SMTChecker
|
2021-08-27 16:25:09 +02:00 |
|
|
Leo Alt
|
61160aa0e7
|
Add constraints correlating address(this).balance and msg.value
|
2021-08-25 21:10:08 +02:00 |
|
|
Leo Alt
|
a55685c04f
|
Erase balances when delegatecall is seen
|
2021-08-25 12:39:26 +02:00 |
|
|
Leo Alt
|
d89d63bf9c
|
Use the nondeterministic interface also for BARECALL
|
2021-08-19 16:34:01 +02:00 |
|
|
Leo Alt
|
6ee60aa628
|
Fix false positive on external calls from constructors
|
2021-08-12 18:51:55 +02:00 |
|
|
Leo Alt
|
10397e440c
|
Fix ICE in constants
|
2021-08-12 10:53:01 +02:00 |
|
|
Leo Alt
|
685d7a8c99
|
Bundle all unproved targets in a single message and only show all if setting chooses that
|
2021-08-04 13:54:50 +02:00 |
|
|
Leo Alt
|
6c8ecfa82c
|
Add option to choose solver
|
2021-07-27 17:14:21 +02:00 |
|
 chriseth
|
e3525b81d0
|
Supply scanner to model checker.
|
2021-07-14 15:12:10 +02:00 |
|
|
Leo Alt
|
547a6915ad
|
Fix ICE on external calls from constructor
|
2021-06-01 14:21:48 +02:00 |
|
|
Leo Alt
|
f7b045b886
|
review
|
2021-05-26 22:12:49 +02:00 |
|
|
Leo Alt
|
daea5f886d
|
Fix CHCSmtLib2Interface
|
2021-05-26 22:12:49 +02:00 |
|
|
Leonardo Alt
|
4b2ccf2f37
|
Abstract function smtchecker natspec
|
2021-05-11 15:30:19 +02:00 |
|
|
Leonardo Alt
|
dd1865873e
|
Choose contracts to be analyzed by the SMTChecker
|
2021-04-21 10:34:14 +02:00 |
|
|
Leonardo Alt
|
095d337140
|
Basic support to free constants
|
2021-04-19 19:23:18 +02:00 |
|
|
Leonardo Alt
|
4e34359063
|
Basic support to free functions
|
2021-04-19 19:23:18 +02:00 |
|
|
Leonardo Alt
|
b753cb6120
|
Deprecate pragma experimental SMTChecker
|
2021-04-08 21:03:38 +02:00 |
|
 anurag4u80
|
bbcdddeed9
|
Replaced keys, values and reverse with ranges
|
2021-03-31 23:33:04 +05:30 |
|
|
Leonardo Alt
|
ba97d6ac4e
|
Add local vars to cex
|
2021-03-30 17:55:21 +02:00 |
|
|
Leonardo Alt
|
dbd067d6db
|
Report out of bounds index access
|
2021-03-30 10:28:48 +02:00 |
|
|
Leonardo Alt
|
d1db41a5c8
|
Fix target warning order nondeterminism
|
2021-03-26 12:13:52 +01:00 |
|
 Martin Blicha
|
85358dfe30
|
[SMTChecker] Do not create targets for contracts that cannot be deployed
|
2021-03-25 15:38:37 +01:00 |
|
 Mathias Baumann
|
e197ebbdd1
|
Replace TypePointer with Type const*
|
2021-03-23 11:47:19 +01:00 |
|
|
Leonardo Alt
|
998346e599
|
Fix bug in virtual functions called by constructor.
|
2021-03-12 16:42:28 +01:00 |
|
|
Leonardo Alt
|
6fd76e830d
|
Fix CHC cex order
|
2021-03-11 10:36:40 +01:00 |
|
|
Martin Blicha
|
4285c2803b
|
[SMTChecker] Fix ICE on array.pop nested inside 1-tuple
|
2021-03-09 20:00:51 +01:00 |
|
|
Leonardo
|
7405dc5b7f
|
Merge pull request #10836 from ethereum/smt_fix_cex_inheritance
Fix inheritance bug in CHC cex
|
2021-02-03 18:49:25 +01:00 |
|
|
Martin Blicha
|
d99256aae7
|
[SMTChecker] refactoring of resetting storage variables
|
2021-02-03 15:53:58 +01:00 |
|
|
Martin Blicha
|
f1013427a7
|
[SMTChecker] refactoring the accessing the encoding state
|
2021-02-03 15:53:58 +01:00 |
|
|
Leonardo Alt
|
665ce27c18
|
Fix inheritance bug in CHC cex
|
2021-02-02 18:06:32 +01:00 |
|
 Martin Blicha
|
a49950cdf3
|
[SMTChecker] Added transaction constraints also for contract deployment
|
2021-02-01 16:46:34 +01:00 |
|
|
Leonardo Alt
|
545305a31f
|
[SMTChecker] Fix super and virtual
|
2021-01-28 18:51:29 +01:00 |
|
|
Leonardo Alt
|
3b23cadbdc
|
Add CLI and JSON option to select SMTChecker targets
|
2021-01-20 17:35:37 +01:00 |
|
|
Leonardo Alt
|
007d39871b
|
[SMTChecker] Synthesize untrusted functions called externally
|
2021-01-15 11:56:26 +01:00 |
|
|
Martin Blicha
|
7c6340fe4f
|
[SMTChecker] Refactoring expression to tuple assignment
|
2021-01-12 17:15:14 +01:00 |
|
|
Leonardo Alt
|
b3c3836388
|
Output internal calls
|
2021-01-12 14:57:04 +01:00 |
|