Open mmcloughlin opened 1 week ago
I'm not sure if this is a good idea, open to suggestions.
A simple alternative is something like a helper assert_one_fails_with_vir_error_msg
. This inline comment approach could be nice for the multi-error case though.
If we are going to support this kind of extended // FAILS
syntax, we might also want to think about enforcing a format for FAILS
comments. At the moment there are some comments with notes attached to them, for example:
Perhaps we support both an expectation and a note?
// FAIL
// FAIL: <expect_msg>
// FAIL (<note>)
// FAIL: <expect_msg> (<note>)
Hi @mmcloughlin. Thank you for the PR.
I have a fairly strong preference for the alternative approach:
A simple alternative is something like a helper assert_one_fails_with_vir_error_msg.
The FAILS
comment, in my mind, should just be a marker of the affected line, and I'd prefer we kept that as simple as possible. Multiple errors with FAILS are uncommon, because we generally will only reliably get one SMT failure (the earliest failing assertion), and so we don't generally write tests with multiple FAILS.
Support for info
or warning
would be useful, through the addition of other markers (there it would be more useful to have multiple -- and perhaps identify them by some "id" to match them with the expected message. In fact, we could also do this for "FAILS" in the uncommon case where there are multiple FAILS we want to handle, e.g.
use vstd::string::*;
fn get_char_fails() {
let x = new_strlit("hello world");
let val = x.get_char(0); // FAILS(0)
assert(val === 'h'); // FAILS(1)
}
uses:
assert_fails_with_vir_msgs(err, [
Level::Error, "invalid comparison operator `===`",
Level::Error, "expected function, found macro `assert`",
])
This PR extends the testing mechanism that checks for
FAILS
comments to additionally allow an expected error message.A comment of the form
// FAILS
just checks for an error. The form// FAILS: <expect>
also confirms that<expect>
appears in the diagnostic text.This PR demonstrates the feature by also updating some of the
integer_ring
tests.