verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.06k stars 58 forks source link

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

Open jaybosamiya-ms opened 1 week ago

jaybosamiya-ms commented 1 week ago

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