Ability to ignore tests

[thedavidmeister]

As per #15 and #30 there are certain features that halmos doesn't currently support.

Refactoring fuzz tests to a form that halmos supports is not always beneficial or possible, for example in #30 the suggestion was to avoid dynamic arrays and use fixed size arrays instead. In the code I was testing this would result in loss of generality of the space the fuzz tester is scanning from all possible length arrays to one or several examples of specific length arrays.

I'd like to be able to keep my more general fuzz test, that can go more places that halmos can, albeit with weaker guarantees, but then tell halmos to ignore those tests.

I could then use halmos to provide stronger proofs for the tests that it does support, which is better than not being able to use halmos at all (seems to be current state of things) if i fuzz something unsupported anywhere in my repo.

[karmacoma-eth]

The way I would recommend doing this is by explicitly calling halmos with the function name prefix you want, e.g.:

• halmos --function test: testXYZ would be executed/fuzzed by both forge and halmos
• halmos --function check: checkXYZ would be executed by halmos only and ignored by forge

Does that work for you?

[thedavidmeister]

@karmacoma-eth hmm, ok is that just a regex style matcher that halmos already has?

[karmacoma-eth]

@thedavidmeister yes, although at the moment it's prefix only (rather than full regex)