crytic / crytic/echidna

"Coverage Required" annotation

Open
#880 3 comments 0 reactions 0 assignees View on GitHub
Dominant language
Haskell
Stars
3.2k
Forks
432
Avg merge
1d 20h
Merged PRs (30d)
5

Description

While writing assertion-based properties, sometimes you have a property that requires a function to be called before the property can be fully validated:

```
function deposit(uint256 assets) public {
vault.deposit(assets, address(this));
}

function verify_withdrawRoundingDirection(uint256 tokens) public {
require(tokens > 0);
uint256 sharesRedeemed = vault.withdraw(tokens);
assertGt(sharesRedeemed, 0, "withdraw() must not allow assets to be withdrawn at no cost");
}
```

In the example above, the verify_withdrawRoundingDirection prop cannot be fully "explored" unless deposit() is called first. Testers must verify that all the code in the property is reached using code coverage.

It would be nice to have some kind of annotation to mark a property as "not fully tested" if full coverage is not achieved. This would raise an error at the end of the run if the annotation was not reached:

```
function verify_withdrawRoundingDirection(uint256 tokens) public {
require(tokens > 0);
uint256 sharesRedeemed = vault.withdraw(tokens);
assertGt(sharesRedeemed, 0, "withdraw() must not allow assets to be withdrawn at no cost");
/// @coverageRequired
}
```

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.