Repository navigation
_fail tests should fail if compilation fails #338
Description
Activity
Oh oh, we should totally distinguish between compilation and verification failures (I thought we did, unless a test was
_ignoreor_fixme).- changed the title
[-]Test `src/test/cbmc/DynTrait/main_fail.rs` uses wrong name for `__VERIFIER_expect_fail`.[/-][+]`_fail` tests should fail if compilation fails[/+]on Jul 21, 2021 You're both right. We don't currently check for the kind of errors we get from tests. I happen to need this feature for the dashboard as well. So, I will make it a priority.
Reacted by Alexa VanHattum
Metadata
Metadata
Assignees
Labels
No labels
The test at
src/test/cbmc/DynTrait/main_fail.rsuses_VERIFIER_expect_failinstead of__VERIFIER_expect_fail, causing it to have a rust compile error.I expect it went by unnoticed because we (accidentally?) left in the
_failsuffix, when really it shouldn't fail, and we don't distinguish between compilation failure and verification failure.