Christian Parpart
|
6b23412fae
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
Leonardo Alt
|
f4f83690f3
|
Replace some shared_ptr by unique_ptr or raw pointers
|
2020-01-06 14:16:49 +01:00 |
|
chriseth
|
f6916a637e
|
Merge remote-tracking branch 'origin/develop' into develop_060
|
2019-12-09 17:16:58 +01:00 |
|
Leonardo Alt
|
225041738e
|
Add SMTCheckerTest for isoltest
|
2019-12-09 15:32:08 +01:00 |
|
chriseth
|
e061f1e743
|
Merge remote-tracking branch 'origin/develop' into HEAD
|
2019-12-05 16:44:26 +01:00 |
|
Leonardo Alt
|
48c3a5c225
|
[SMTChecker] Create options to choose SMT solver in runtime
|
2019-12-04 17:31:44 +01:00 |
|
chriseth
|
96d777d7f1
|
Merge commit 'a7d481fb9' into develop_060
|
2019-12-03 20:47:30 +01:00 |
|
Leonardo Alt
|
c09da092d2
|
[SMTChecker] Fix constructors with local vars
|
2019-11-29 16:59:15 +01:00 |
|
Leonardo Alt
|
a352abe00d
|
[SMTChecker] Add support to constructors
|
2019-11-28 14:43:23 +01:00 |
|
Leonardo Alt
|
ddc478e3e4
|
Add CallbackKind and use it for the SMT solver
|
2019-11-21 22:10:21 +00:00 |
|
chriseth
|
216e1749f4
|
Merge remote-tracking branch 'origin/develop' into develop_060
|
2019-11-14 13:42:46 +01:00 |
|
Leonardo Alt
|
e3652627fd
|
[SMTChecker] Fix ICE in CHC when function used as argument
|
2019-11-13 15:11:30 +01:00 |
|
chriseth
|
2e5a42836c
|
Merge pull request #7681 from ethereum/develop
Merge develop into develop_060
|
2019-11-11 16:42:03 +01:00 |
|
Leonardo Alt
|
6b10efff8c
|
Add CHCSmtLib2Interface
|
2019-11-07 11:12:11 +01:00 |
|
chriseth
|
21e65076b3
|
Merge pull request #7650 from ethereum/develop
Merge develop into develop_060
|
2019-11-06 21:56:55 +01:00 |
|
Leonardo Alt
|
10e70b8603
|
[SMTChecker] Support inheritance and resolve overrides
|
2019-11-06 11:00:06 +01:00 |
|
chriseth
|
4d99bf68f4
|
Merge pull request #7638 from ethereum/develop
Merge develop into develop_060
|
2019-11-05 17:33:54 +01:00 |
|
Leonardo Alt
|
c5e081dc8c
|
[SMTChecker] Refactor CHC loops and add if blocks
|
2019-11-05 09:28:59 +01:00 |
|
Daniel Kirchner
|
3321fc56ea
|
Split fallback function and introduce "fallback()" and "receive()" syntax.
|
2019-11-04 17:17:58 +01:00 |
|
Leonardo Alt
|
e1c238e25f
|
[SMTChecker] Add loop support
|
2019-09-13 12:40:53 +02:00 |
|
Leonardo Alt
|
1a70a46f9b
|
[CHC] Add function blocks and check asserts
|
2019-08-15 12:25:15 +02:00 |
|
Leonardo Alt
|
bef6228810
|
[SMTChecker] Create CHC constructor/interface/error blocks
|
2019-08-12 12:34:57 +02:00 |
|
Leonardo Alt
|
4214cd1354
|
[SMTChecker] Fix ICE when reporting cex concerning state vars from different source files
|
2019-08-10 20:56:52 +02:00 |
|
Leonardo Alt
|
369f8cd97f
|
[SMTChecker] CHC create function return variables
|
2019-08-05 12:36:51 +02:00 |
|
Leonardo Alt
|
b204f27047
|
[SMTChecker] EncodingContext config flag to accumulate assertions
|
2019-07-19 19:31:25 +02:00 |
|
Leonardo Alt
|
03cc124f32
|
Add CHC skeleton
|
2019-07-19 11:52:05 +02:00 |
|