Run locally
git clone -- https://github.com/MasWag/crate-proofs report-22-source-1
git -C report-22-source-1 checkout --detach ce78df957d982a6049e602a5083bee5b3636b5ea
git -C report-22-source-1 submodule update --init --recursive --checkout
cd report-22-source-1/unindent/0.2.4/creusot
cargo creusot --no-cache --why3find-arg=--no-autodetect-provers --why3find-arg=-P '--why3find-arg=z3,cvc5,alt-ergo' --why3find-arg=-j --why3find-arg=2 --why3find-arg=--fast --why3find-arg=1 --why3find-arg=--time --why3find-arg=10 --why3find-arg=-d --why3find-arg=6Source on GitHub · SARIF with logs (.json)
Recorded run
Completed · 4 checks passed · 0 failed
| Check | Result | Claim |
|---|---|---|
| vc_do_unindent | Passed | Claim #1 |
| vc_unindent | Passed | Claim #1 |
| vc_do_unindent_bytes | Passed | Claim #2 |
| vc_unindent_bytes | Passed | Claim #2 |
Execution details
- Started
- 2026-11-04T16:49:50.972967303+00:00
- Finished
- 2026-11-04T16:52:28.889989975+00:00
- Platform
- linux x86_64
- Rust compiler
- rustc 1.91.0 (f8297e351 2025-10-28) binary: rustc commit-hash: f8297e351a40c1439a467bbbb6879088047f50b3 commit-date: 2025-10-28 host: x86_64-unknown-linux-gnu release: 1.91.0 LLVM version: 21.1.2
- Working directory
- unindent/0.2.4/creusot
- Environment overrides
- None recorded
- Git repository
- https://github.com/MasWag/crate-proofs
- Git commit
- ce78df957d982a6049e602a5083bee5b3636b5ea
Diagnostics & logs
=== stdout ===
Proved (36 files) ✔
=== stderr ===
warning: patch `creusot-std v0.15.0-dev (/home/lab8/mwaga/creusot/creusot-std)` was not used in the crate graph
help: Check that the patched package version and available features are compatible
with the dependency requirements. If the patch has a different version from
what is locked in the Cargo.lock file, run `cargo update` to use the new
version. This may also occur with an optional dependency that is not enabled.
Compiling proc-macro2 v1.0.107
Compiling unicode-ident v1.0.27
Compiling quote v1.0.47
Compiling libc v0.2.191
Compiling getrandom v0.4.3
Compiling cfg-if v1.0.5
Compiling syn v2.0.119
Compiling uuid v1.29.0
Compiling pearlite-syn v0.13.0
Compiling creusot-std-proc v0.13.0
Checking creusot-std v0.13.0
Checking unindent v0.2.4 (./unindent/0.2.4/creusot)
warning: unnecessary parentheses around function argument
--> src/lib.rs:56:20
|
56 | (found ==> (exists<a: Int,k: Int> a < bound && spec::later_candidate(s,a,k) && k-a == margin)) &&
| ^ ^
|
= note: `#[warn(unused_parens)]` (part of `#[warn(unused)]`) on by default
help: remove these parentheses
|
56 - (found ==> (exists<a: Int,k: Int> a < bound && spec::later_candidate(s,a,k) && k-a == margin)) &&
56 + (found ==> exists<a: Int,k: Int> a < bound && spec::later_candidate(s,a,k) && k-a == margin ) &&
|
warning: unused variable: `k`
--> src/lemmas.rs:48:24
|
48 | if a > 0 { let k = first_nonwhite(s,a,a,i); }
| ^ help: if this is intentional, prefix it with an underscore: `_k`
|
= note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default
warning: function `append_range` is never used
--> src/lib.rs:40:4
|
40 | fn append_range(s: &[u8], start: usize, end: usize, initial: Vec<u8>) -> Vec<u8> {
| ^^^^^^^^^^^^
|
= note: `#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default
warning: `unindent` (lib) generated 3 warnings (run `cargo fix --lib -p unindent` to apply 2 suggestions)
Finished `dev` profile [unoptimized + debuginfo] target(s) in 28.48s