"Coverage Required" annotation
- 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
Assessment
This issue has not been assessed yet.