Skip to content

Commit

Permalink
test: add early fail() test
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Jul 16, 2024
1 parent 362494f commit b5eeb05
Show file tree
Hide file tree
Showing 2 changed files with 27 additions and 0 deletions.
11 changes: 11 additions & 0 deletions tests/expected/all.json
Original file line number Diff line number Diff line change
Expand Up @@ -777,6 +777,17 @@
"num_bounded_loops": null
}
],
"test/Foundry.t.sol:EarlyFailTest": [
{
"name": "check_early_fail_cheatcode(uint256)",
"exitcode": 1,
"num_models": 1,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
}
],
"test/Foundry.t.sol:FoundryTest": [
{
"name": "check_assume(uint256)",
Expand Down
16 changes: 16 additions & 0 deletions tests/regression/test/Foundry.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,22 @@ contract DeepFailer is Test {
}
}

contract EarlyFailTest is Test {
function do_fail() external {
fail();
}

function check_early_fail_cheatcode(uint x) public {
address(this).call(abi.encodeWithSelector(this.do_fail.selector, ""));

// this shouldn't be reached due to the early fail() semantics.
// if this assertion is executed, two counterexamples will be generated:
// - counterexample caused by fail(): x > 0
// - counterexample caused by assert(x > 0): x == 0
assert(x > 0);
}
}

contract FoundryTest is Test {
/* TODO: support checkFail prefix
function checkFail() public {
Expand Down

0 comments on commit b5eeb05

Please sign in to comment.