Failure attributes

Sometimes, especially when writing regression tests, one wishes to check that certain top-level definition will not succeed. For this, we have a special set of attributes described in this page.

The simplest one is expect_failure, which "flips" the status of a definition. If the definition succeeds to typecheck, then F* will fail; if it fails, F* will succeed.

[@expect_failure] let test1 = assert False // this is accepted!
[@expect_failure] let test2 = 1 + 'a' // this too!

In either case the names bound by the definition in question (test1, test2) are not in scope for the rest of the program.

When we want to ensure that, beyond just failing, the definition fails for the right reasons, we can add a list of error codes to expect_failure. F* will then check that errors raised coincide exactly with the list, accounting for repetition, but not for ordering. (Note: we need to be careful to parenthesize the application, or these are in fact silently parsed as two attributes.)

[@(expect_failure [19])] let _ = assert False // succeeds!
[@(expect_failure [19;19])] let _ = assert False // fails: (Error) This top-level definition was expected to raise errors [19, 19], but it raised [19]. Error #19 was raised 1 times, instead of 2

When running with --lax, it is probably the case that many of the things expected to fail actually succeed since we are not fully checking them. Hence, definitions marked with expect_failure are actually just skipped when lax-checking.

However, we can check for things that are supposed to fail even lax-checking by using the expect_lax_failure attribute, which has pretty much the same semantics (and can take an optional error list), except that the definitions do not get skipped in lax mode.

#set-options "--lax"
[@expect_failure] let test5 = 1 + 'a' // ignored, so OK
[@expect_failure] let test6 = assert False // ignored, so OK
[@expect_lax_failure] let test7 = 1 + 'a' // fails lax-checking, so OK
[@expect_lax_failure] let test8 = assert False // succeeds lax-checking, so this raises an error