hevm: expand symbolic tests
- Dominant language
- Haskell
- Stars
- 2.1k
- Forks
- 320
- PR merge metrics
- No merged PRs in 30d
Description
This is a tracking issue containing ideas for expanding the test coverage of the symbolic execution modes of hevm.
- [ ] integrate the solc semanticTests (see [here](https://github.com/dapphub/dapptools/pull/467#issuecomment-668019856)).
- [ ] generate a set of negative tests for hevm equivalence by manually modifying the yul optimizer tests
- [ ] integrate hevm symbolic into the test suite [here](https://github.com/dddejan/solidity-semantics-tests)
- [ ] explore the contracts in the [solc-verify test suite](https://github.com/SRI-CSL/solidity/tree/boogie/test/solc-verify) and compare the results
- [ ] explore the contracts in the [verisol test suite](https://github.com/microsoft/verisol/tree/master/Test/regressions) and compare the results
- [ ] run `hevm equivalence` against optimized and unoptimized versions of all of the above contracts
- [ ] confirm the verification results in [`k-dss`](https://github.com/dapphub/k-dss) and [`k-uniswap-v2`](https://github.com/dapp-org/k-uniswap-v2) using `hevm symbolic` (requires integration with `act`)
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.