chriseth
|
f6916a637e
|
Merge remote-tracking branch 'origin/develop' into develop_060
|
2019-12-09 17:16:58 +01:00 |
|
Leonardo Alt
|
beed0f6a27
|
Set tests that CVC4 can't handle to Z3 only
|
2019-12-09 15:32:08 +01:00 |
|
chriseth
|
2f11ac3590
|
Merge remote-tracking branch 'origin/develop' into develop_060
|
2019-12-03 21:17:15 +01:00 |
|
chriseth
|
96d777d7f1
|
Merge commit 'a7d481fb9' into develop_060
|
2019-12-03 20:47:30 +01:00 |
|
Leonardo Alt
|
b1577f5e46
|
[SMTChecker] Fix ICE in array of structs type
|
2019-12-03 01:12:30 +01:00 |
|
Leonardo Alt
|
5adc2a40b9
|
[SMTChecker] Fix ICE for arrays and mappings of functions.
|
2019-11-29 18:06:44 +01:00 |
|
Erik K
|
94272d44aa
|
Merge pull request #7745 from ethereum/develop
Merge develop into develop_060
|
2019-11-19 15:30:31 +01:00 |
|
Leonardo Alt
|
e500a262ea
|
Fix SMTChecker tests for 060
|
2019-11-19 10:58:59 +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
|
8a42e3f87a
|
[SMTChecker] Support assignments to m-d arrays and mappings
|
2019-10-28 17:27:39 +01:00 |
|
Leonardo Alt
|
a774b2d905
|
[SMTChecker] Zero-initialize arrays
|
2019-09-02 22:37:30 +02:00 |
|
Leonardo Alt
|
214e5c6369
|
[SMTChecker] Fix index access type type error
|
2019-08-27 16:39:19 +02:00 |
|
Leonardo Alt
|
360f868836
|
[SMTChecker] Fix literal string type mismatch
|
2019-08-10 21:51:46 +02:00 |
|
Leonardo Alt
|
369f8cd97f
|
[SMTChecker] CHC create function return variables
|
2019-08-05 12:36:51 +02:00 |
|
Leonardo Alt
|
7b5863e583
|
Do not erase knowledge about storage pointers when another pointer is assigned
|
2019-08-02 13:09:06 +02:00 |
|
Leonardo Alt
|
847f574e22
|
[SMTChecker] Fix ICE when inlining function with tuple expression
|
2019-07-26 16:29:29 +02:00 |
|
Leonardo Alt
|
fb3c85633b
|
Always create symbolic expression
|
2019-07-01 16:25:33 +02:00 |
|
Leonardo Alt
|
a28b84fdc3
|
[SMTChecker] Add a more general VerificationTarget
|
2019-06-27 10:31:50 +02:00 |
|
Leonardo Alt
|
60a4f03d3d
|
[SMTChecker] Fix ice in unsupported functions with multi return values
|
2019-05-16 18:23:42 +02:00 |
|
Leonardo Alt
|
3ea5c112d3
|
[SMTChecker] Fix VariableUsage for IndexAccess
|
2019-05-10 11:28:10 +02:00 |
|
Leonardo Alt
|
3c7540ceb2
|
[SMTChecker] Support tuples with multiple var decls
|
2019-05-07 16:57:27 +02:00 |
|
Leonardo Alt
|
5440a53d4d
|
[SMTChecker] Support tuples as function calls with multiple return values
|
2019-05-03 06:10:22 +02:00 |
|
Leonardo Alt
|
204dcf1771
|
[SMTChecker] Support tuple assignments
|
2019-05-02 12:55:34 +02:00 |
|
Leonardo Alt
|
6c7527ac90
|
[SMTChecker] Support tuple type declaration
|
2019-05-02 12:05:21 +02:00 |
|
Leonardo Alt
|
fc482de695
|
[SMTChecker] Support address members
|
2019-04-25 16:24:36 +02:00 |
|
Leonardo Alt
|
ecd89393ee
|
[SMTChecker] Support contract type
|
2019-04-17 16:30:11 +02:00 |
|
Leonardo Alt
|
a8209e9899
|
[SMTChecker] Shortcut RationalNumber expressions
|
2019-03-11 12:53:49 +01:00 |
|
Leonardo Alt
|
02d0e609b9
|
[SMTChecker] Support enums
|
2019-03-07 15:15:12 +01:00 |
|
Leonardo Alt
|
29b2ab6f66
|
Handle aliasing
|
2019-03-06 11:29:54 +01:00 |
|
Leonardo Alt
|
cb6c2b33f8
|
Add tests
|
2019-03-06 11:29:26 +01:00 |
|
Leonardo Alt
|
e74f58130e
|
Add SMT type support to Solidity arrays
|
2019-03-06 11:29:26 +01:00 |
|
Leonardo Alt
|
22cdfb18d4
|
[SMTChecker] Assert type is not function when assigning
|
2019-02-14 13:32:56 +01:00 |
|
Leonardo Alt
|
9199718ec0
|
Clear all mapping knowledge after array variable assignment
|
2018-12-14 12:21:53 +01:00 |
|
Leonardo Alt
|
6a2809a582
|
[SMTChecker] Support to mapping
|
2018-12-14 12:21:53 +01:00 |
|
Leonardo Alt
|
08737e43dc
|
[SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions
|
2018-12-11 11:28:25 +01:00 |
|
Leonardo Alt
|
32fe4768a9
|
Organize smt tests in subdirectories
|
2018-11-22 13:33:28 +00:00 |
|
Leonardo Alt
|
d8cbf321da
|
Grouping of symbolic variables in the same file and support to FixedBytes
|
2018-10-25 09:30:48 +02:00 |
|