Ishtiaque Zahid
|
61febbd249
|
formatNumberReadable now prints signed integers as well
|
2022-06-24 07:15:15 +06:00 |
|
Leo Alt
|
6a126f6ccb
|
Update tests and hashes for z3 4.8.17
|
2022-05-13 15:25:10 +02:00 |
|
Leo Alt
|
cbaba6f913
|
update tests
|
2022-05-11 20:02:31 +02:00 |
|
Kamil Śliwak
|
0e0d1972f9
|
Disable non-deterministic counterexamples in some SMT tests
- The counterexamples sometimes do appear and the tests fail.
|
2022-05-10 12:48:01 +02:00 |
|
Leo Alt
|
201c6c6819
|
fix smt flaky test
|
2022-05-05 11:38:16 +02:00 |
|
Leo Alt
|
cba3d18f66
|
adjust for osx nondeterminism
|
2022-05-04 19:04:54 +02:00 |
|
Leo Alt
|
4fd7de36f1
|
update smt tests z3 4.8.16
|
2022-05-03 14:23:27 +02:00 |
|
Leo Alt
|
f9fa76c9d3
|
smt encode call
|
2022-04-11 12:19:41 +02:00 |
|
Leo Alt
|
bef69b595b
|
Ignore cex in SMT test
|
2022-02-28 18:56:20 +01:00 |
|
Leo Alt
|
098a3cb537
|
adjust tests for nondeterminism
|
2022-01-12 18:43:18 +01:00 |
|
Daniel Kirchner
|
1655626e0a
|
Remove counterexample from test.
|
2022-01-12 17:58:05 +01: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 |
|
Marenz
|
7a96953e78
|
Implement typechecked abi.encodeCall()
|
2021-12-16 17:35:58 +01:00 |
|
Leo Alt
|
316be7206f
|
Fix soundness of storage/memory pointers that were not erasing enough knowledge
|
2021-12-14 12:02:18 +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
|
a2588533e5
|
macos nondeterminism
|
2021-11-24 20:41:22 +01:00 |
|
Leo Alt
|
0c34d9df88
|
Adjust tests for 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
|
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
|
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
|
d25fb29178
|
Add isoltest option to ignore OS
|
2021-10-01 12:45:36 +02:00 |
|
Leo Alt
|
e74f853c6b
|
[SMTChecker] Support user types
|
2021-09-21 13:23:17 +02:00 |
|
Leo Alt
|
a1bea368cb
|
[SMTChecker] Support constants via modules
|
2021-09-16 14:35:05 +02:00 |
|
Leo Alt
|
b731957e65
|
Fix BMCs constraints on internal functions
|
2021-09-15 14:42:39 +02:00 |
|
Leo Alt
|
d91f75deb8
|
Fix ICE on unique errors
|
2021-09-09 16:37:43 +02:00 |
|
Leo Alt
|
6e2fe1e340
|
[SMTChecker] Cleanup spurious messages about TypeTypes
|
2021-09-07 16:55:25 +02:00 |
|
Leo Alt
|
106c591dde
|
Support the external call option
|
2021-09-01 20:18:37 +02:00 |
|
Leo Alt
|
ac528cfd1b
|
add static array length constraint
|
2021-08-30 17:15:16 +02:00 |
|
Leo Alt
|
16bc15acac
|
Fix false negative on storage array references returned by internal functions
|
2021-08-28 09:30:53 +02:00 |
|
Leo Alt
|
60b866f9d8
|
Fix ICE on multi-source use of abi.*
|
2021-08-27 18:55:36 +02:00 |
|
Leo Alt
|
0cc9162fb5
|
Update SMTChecker tests
|
2021-08-27 16:25:09 +02:00 |
|
Leo Alt
|
a9af63187e
|
Adjust tests for nondeterminism
|
2021-08-25 21:10:43 +02:00 |
|
Leo Alt
|
4cf4ccafd7
|
New tests
|
2021-08-25 21:10:08 +02:00 |
|
Leo Alt
|
85378b1770
|
Update existing tests
|
2021-08-25 21:10:08 +02:00 |
|
Leo Alt
|
718f392849
|
Don't erase things for BMC if function call is staticcall
|
2021-08-25 14:09:46 +02:00 |
|
Leo Alt
|
a55685c04f
|
Erase balances when delegatecall is seen
|
2021-08-25 12:39:26 +02:00 |
|
Leo Alt
|
9ea4576664
|
Update tests
|
2021-08-19 16:34:01 +02:00 |
|
Leo Alt
|
937af7d722
|
Fix SMT test
|
2021-08-12 22:34:18 +02:00 |
|
chriseth
|
fe0d027d45
|
Merge pull request #11785 from ethereum/someMoreBaseFees
Some more base fees.
|
2021-08-12 19:48:10 +02:00 |
|
Leo Alt
|
6ee60aa628
|
Fix false positive on external calls from constructors
|
2021-08-12 18:51:55 +02:00 |
|
chriseth
|
c87c0f02bd
|
Test updates.
|
2021-08-12 16:56:12 +02:00 |
|
Leo Alt
|
10397e440c
|
Fix ICE in constants
|
2021-08-12 10:53:01 +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 |
|
chriseth
|
1f8f1a3db9
|
Merge pull request #11484 from ethereum/fix-unreachable-code-anaysis
Fix revert pruner modifying function flows wrong
|
2021-06-04 12:44:35 +02:00 |
|