 Matheus Aguiar
|
f3fc19080a
|
Override mobileType of MagicType to null
|
2023-07-18 10:56:02 +02:00 |
|
 Alexander Arlt
|
c5673278a7
|
Remove EWASM backend.
|
2023-05-11 10:56:55 -05:00 |
|
 Leo Alt
|
21c0f78650
|
Report safe properties in BMC and CHC
|
2023-03-09 14:59:32 +01:00 |
|
|
Leo Alt
|
8d91ccf028
|
[SMTChecker] Add a new trusted mode which assumes that code that is
available at compile time is trusted.
|
2023-02-06 17:02:33 +01:00 |
|
  
|
feba4de509
|
Add paris constraints to SMTChecker
Co-authored-by: Daniel <daniel@ekpyron.org>
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
Co-authored-by: Leo <leo@ethereum.org>
|
2023-01-31 11:03:04 +01:00 |
|
|
Leo Alt
|
504b70b6af
|
update smt tests
|
2022-11-24 13:08:06 +01:00 |
|
|
Leo Alt
|
16c0838f75
|
Update docker images and tests
|
2022-08-30 11:51:59 +02:00 |
|
|
Leo Alt
|
4fd7de36f1
|
update smt tests z3 4.8.16
|
2022-05-03 14:23:27 +02:00 |
|
|
Leo Alt
|
9f171c0f06
|
update smtchecker tests for new z3
|
2022-01-12 15:13:34 +01:00 |
|
|
Leo Alt
|
fb8c138b8b
|
Do not analyze unecessary contracts
|
2021-12-24 19:36:32 +01:00 |
|
|
Leo Alt
|
a2588533e5
|
macos nondeterminism
|
2021-11-24 20:41:22 +01:00 |
|
|
Leo Alt
|
ff5c842d67
|
update smtchecker tests
|
2021-11-24 20:41:22 +01:00 |
|
|
Leo Alt
|
38b0cf7f9c
|
SMTChecker tests
|
2021-10-26 11:30:30 +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
|
d81ebe97c3
|
Fix magic access
|
2021-10-01 12:57:06 +02:00 |
|
|
Leo Alt
|
b731957e65
|
Fix BMCs constraints on internal functions
|
2021-09-15 14:42:39 +02:00 |
|
|
Leo Alt
|
6e2fe1e340
|
[SMTChecker] Cleanup spurious messages about TypeTypes
|
2021-09-07 16:55:25 +02:00 |
|
|
Leo Alt
|
0cc9162fb5
|
Update SMTChecker tests
|
2021-08-27 16:25:09 +02:00 |
|
|
Leo Alt
|
85378b1770
|
Update existing tests
|
2021-08-25 21:10:08 +02:00 |
|
|
Leo Alt
|
3c1f555f71
|
Tests
|
2021-08-04 13:54:50 +02:00 |
|
|
Leo Alt
|
e46abd0ca1
|
Update tests due to nondeterminism
|
2021-07-19 15:20:11 +02:00 |
|
|
Leo Alt
|
20e23171da
|
Update tests to z3 4.8.12
|
2021-07-16 14:43:52 +02:00 |
|
 Alex Beregszaszi
|
1be07c2b36
|
Trivial isoltest updates: missing // ---- at the end
|
2021-04-20 17:38:29 +02:00 |
|
|
Alex Beregszaszi
|
84c05d35f3
|
Trivial isoltest updates: normalized whitespace
|
2021-04-20 17:38:29 +02:00 |
|
|
Leonardo Alt
|
0a4afa71bd
|
Update old tests
|
2021-04-08 21:03:39 +02:00 |
|
|
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
|
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
|
a49950cdf3
|
[SMTChecker] Added transaction constraints also for contract deployment
|
2021-02-01 16:46:34 +01:00 |
|
 Martin Blicha
|
deb90d84a6
|
[SMTChecker] added missing type constraints for Address
|
2021-01-27 20:39:24 +01:00 |
|
|
Leonardo Alt
|
a612daa783
|
Add msgvalue to cex
|
2021-01-21 19:05:44 +01:00 |
|
|
Alex Beregszaszi
|
e117c9516e
|
Replace "pragma experimental ABIEncoderV2" in tests where appropriate
And add a few tests for "pragma abicoder".
|
2021-01-15 19:57:09 +00:00 |
|
|
Leonardo Alt
|
007d39871b
|
[SMTChecker] Synthesize untrusted functions called externally
|
2021-01-15 11:56:26 +01:00 |
|
|
Leonardo Alt
|
b3c3836388
|
Output internal calls
|
2021-01-12 14:57:04 +01:00 |
|
|
Leonardo Alt
|
f1ae24abc7
|
Remove extra line breaks
|
2021-01-12 14:00:07 +01:00 |
|
|
Leonardo Alt
|
b02722ebda
|
Add contract name to called function in cex
|
2021-01-04 10:03:16 +01:00 |
|
|
Leonardo Alt
|
78d55e6b4a
|
[SMTChecker] Support check/unchecked
|
2020-12-30 12:14:30 +01:00 |
|
|
Martin Blicha
|
be0a0f4d90
|
[SMTChecker] Added constraints for block properties
|
2020-12-29 22:17:44 +01:00 |
|
|
Leonardo Alt
|
50be39fc21
|
Add and update tests
|
2020-12-17 14:42:49 +01:00 |
|
 chriseth
|
482bda6887
|
Merge remote-tracking branch 'origin/develop' into breaking
|
2020-12-10 12:15:52 +01:00 |
|
|
Leonardo Alt
|
3c142e0e94
|
Move CHC counterexamples to primary location
|
2020-12-09 19:55:18 +01:00 |
|
|
chriseth
|
d56a7bb89e
|
Merge pull request #10489 from ethereum/develop
Merge develop into breaking.
|
2020-12-03 18:11:12 +01:00 |
|
|
Leonardo Alt
|
fa561dbd0e
|
Add uncovered test and replace uncovered tests by asserts
|
2020-11-30 18:46:47 +01:00 |
|
|
chriseth
|
a0a02f2307
|
Merge remote-tracking branch 'origin/develop' into breaking
|
2020-11-23 19:28:08 +01:00 |
|
|
Martin Blicha
|
80d743426f
|
[SMTChecker] Added support for struct constructor.
|
2020-11-23 13:45:17 +01:00 |
|
|
chriseth
|
04195439b7
|
Merge remote-tracking branch 'origin/develop' into HEAD
|
2020-11-09 14:28:05 +01:00 |
|
|
Leonardo Alt
|
daf859c15b
|
[SMTChecker] report SMTEncoder warnings also via CHC
|
2020-11-03 16:06:17 +00:00 |
|
|
chriseth
|
5ffee049fa
|
Merge remote-tracking branch 'origin/develop' into breaking
|
2020-11-03 14:05:14 +01:00 |
|
|
Martin Blicha
|
c1a57ffbfe
|
[SMTChecker] More precise creation of verification targets.
|
2020-10-30 19:11:28 +01:00 |
|