Experience report: running Prusti against chrono

[djc]

After trying on rustls, I tried running Prusti on chrono. However, running it on current main generated 452 problems, practically all of which seem to be internal errors. A sample:

date.rs[Ln 109, Col 5]: Details: cannot generate fold-unfold Viper statements. Failed to subtract fractional permissions: invalid substraction: read - write.

[Prusti: unsupported feature] Prusti encountered an unexpected internal error

[Prusti: unsupported feature] unsupported constant type Ref(_#5r, offset::utcLLUtc, Not) [Ln 418, Col 9] (src/datetime/mod.rs`)

[Prusti: unsupported feature] access to reference-typed fields is not supported [Ln 579, Col 5] (src/datetime/mod.rs)

[Prusti: unsupported feature] cast statements that crate loans are not supported [Ln 348, Col 10] (src/format/mod.rs)

(A bunch of these seem to happen in compiler-internal derives like PartialEq or Debug, maybe those should be disabled by default?)

I naively ran Prusti on all of chrono (clicking the Verify with Prusti button in VS Code's status bar) -- maybe that's not the recommended method? It would be nice if there was some better sense of progress, maybe just the number of functions left to check or something?

Of the 452 issues, 39 are "attempt to [op] with overflow", so will be looking into these in more detail!