Don't report PASS when no assert is reachable due to e.g. always reverting calls

[acmLL]

Configuration: MacBook Pro, Apple M1 Pro, Sonoma 14.0, 32GB

hevm version: 0.52.0 (static version)

I don't know if this is in your plans, but I think this feature would be interesting to provide more security in the use of hevm test. When we run a prove (prefixed based test) in hevm test, we expect it to execute some assert to obtain a PASS or FAIL result. However, in some cases, due to conditions that cannot be satisfied or issues in the test design, no assert is reached, and hevm test reports PASS in such cases. I think it would be interesting for it to report that no assert was reached so that the user can be sure that there was a problem with their test and that it needs to be adjusted. In some scenarios I have encountered, hevm test doesn't reach the assert and reports PASS. It's okay that it didn't actually find any issues, but it didn't even reach the assert for the test case.

Thanks!

[acmLL]

Fixed this with an else revert(). Thanks!

[d-xo]

This should actually work already, can you post a test case that exhibits the buggy behaviour here.

[acmLL]

For example, @d-xo :

This is a small modification in one of the test cases that are automatically generated by "forge init"

function prove_Increment(uint256 val) public {
    if(val < 0) {
        counter.setNumber(val);
        counter.increment();
        assertEq(counter.number(), val);
    }
}

I would like to see hevm reporting the same message that it reports in other scenarios but in this case it reports PASS. If I change to

function prove_Increment(uint256 val) public {
    if(val < 0) {
        counter.setNumber(val);
        counter.increment();
        assertEq(counter.number(), val);
    }
    else revert();
}

Then it reports

[FAIL] prove_Increment(uint256)

Failure: prove_Increment(uint256)

No reachable assertion violations, but all branches reverted Prefix this testname with proveFail if this is expected

Thanks!

[msooseth]

Hi,

In the first example we can't detect it's a trivial test -- it's hard to find the right heuristic to distinguish this test from a valid test. It could ostensibly possible to assert some precondition with a require and then do a branch with if and that would then be also the same setup:

require(a>10);
if (a < 10) {
 ...blah..
}

This would be very similar, at the EVM level, to the first test that you wrote.

Closing this as #cantfix