Skip to content

Commit 5b055f0

Browse files
committed
1 parent a47ec3f commit 5b055f0

File tree

3 files changed

+23
-2
lines changed

3 files changed

+23
-2
lines changed

src/halmos/__main__.py

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1390,9 +1390,10 @@ def resolve_target_selectors(
13901390
or fun_sig.startswith("check_")
13911391
or fun_sig.startswith("prove_")
13921392
or fun_sig.startswith("invariant_")
1393-
or fun_sig.startswith("setUp")
1393+
or fun_sig == "setUp()"
1394+
or fun_sig == "afterInvariant()"
13941395
):
1395-
debug(f"Skipping special function {fun_sig}")
1396+
debug(f"Skipping {fun_sig} (reserved function)")
13961397
continue
13971398

13981399
yield (fun_sig, fun_selector)

tests/expected/all.json

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3338,6 +3338,15 @@
33383338
"time": null,
33393339
"num_bounded_loops": null
33403340
},
3341+
{
3342+
"name": "invariant_targets_inception_afterInvariant_included()",
3343+
"exitcode": 1,
3344+
"num_models": 1,
3345+
"models": null,
3346+
"num_paths": null,
3347+
"time": null,
3348+
"num_bounded_loops": null
3349+
},
33413350
{
33423351
"name": "invariant_targets_inception_check_included()",
33433352
"exitcode": 1,

tests/regression/test/InvariantTargetThis.t.sol

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ contract InvariantTargetBase {
1010
bool public test_foo_called;
1111
bool public check_foo_called;
1212
bool public setUpSymbolic_called;
13+
bool public afterInvariant_called;
1314

1415
function setUp() public virtual {
1516
setUp_called = true;
@@ -27,6 +28,10 @@ contract InvariantTargetBase {
2728
_invariant_this_called = true;
2829
}
2930

31+
function afterInvariant() public {
32+
afterInvariant_called = true;
33+
}
34+
3035
// should be included
3136
function foo() public {
3237
foo_called = true;
@@ -63,6 +68,7 @@ contract InvariantTargetThis is InvariantTargetBase, Test {
6368
assertEq(setUpSymbolic_called, false);
6469
assertEq(test_foo_called, false);
6570
assertEq(_invariant_this_called, false);
71+
assertEq(afterInvariant_called, false);
6672
}
6773

6874
// we expect a counterexample, showing that setUp is called
@@ -85,6 +91,11 @@ contract InvariantTargetThis is InvariantTargetBase, Test {
8591
assertEq(inception.check_foo_called(), false);
8692
}
8793

94+
// we expect a counterexample, showing that afterInvariant is called
95+
function invariant_targets_inception_afterInvariant_included() public view {
96+
assertEq(inception.afterInvariant_called(), false);
97+
}
98+
8899
// we expect a counterexample, showing that foo is indeed called
89100
function invariant_targets_foo_included() public view {
90101
assertEq(foo_called, false);

0 commit comments

Comments
 (0)