Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"0 errors" when there is a (trivial) error blocking more verification #1180

Open
jaybosamiya-ms opened this issue Jun 26, 2024 · 0 comments
Open

Comments

@jaybosamiya-ms
Copy link
Contributor

This is fairly trivial, but if you run Verus on a library file and forget --crate-type=lib, then it throws an error, but still looks like 0 errors in its output, which at least for some tools (e.g., Veritas, verus-analyzer, ...) that parse that line, makes it seem like there have been 0 errors. We do get 0 verified, but it might be be good to say 1 error(s) or similar?

$ verus x.rs
error[E0601]: `main` function not found in crate `x`
 --> x.rs:9:2
  |
9 | }
  |  ^ consider adding a `main` function to `x.rs`

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0601`.
verification results:: 0 verified, 0 errors
@jaybosamiya-ms jaybosamiya-ms changed the title "0 errors" when there is an error "0 errors" when there is a (trivial) error blocking more verification Jun 26, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant