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

Cargo doc not building. Errors from kani-compiler #1282

Closed
YoshikiTakashima opened this issue Jun 15, 2022 · 0 comments · Fixed by #1331
Closed

Cargo doc not building. Errors from kani-compiler #1282

YoshikiTakashima opened this issue Jun 15, 2022 · 0 comments · Fixed by #1331
Assignees
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@YoshikiTakashima
Copy link
Contributor

YoshikiTakashima commented Jun 15, 2022

I tried building cargo doc using the following command line invocation
at the root of the project.

cargo doc --workspace

with Kani version: 0.4.0 6184f0e (master/latest at the time)

I expected to see the doc-compile succeed and produce HTML docs.

Instead, this happened:

error: unresolved link to `codegen_place`
 --> kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:6:9
  |
6 | //! in [codegen_place] below.
  |         ^^^^^^^^^^^^^ no item named `codegen_place` in scope
error: this URL is not a hyperlink
   --> kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:121:9
    |
121 | ...// https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/Determine.20untupled.20closure.20args.20from.20Instance.3F
    |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: `<https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/Determine.20untupled.20closure.20args.20from.20Instance.3F>`
    |
    = note: `#[deny(rustdoc::bare_urls)]` implied by `#[deny(warnings)]`
    = note: bare URLs are not automatically turned into clickable links

... More errors below

The doc errors appear to be mostly comment formatting issues from
kani-compiler.

Since the error message is long, I only gave the one example per error message kind.

Click here for full error error: unresolved link to `codegen_place` --> kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:6:9 | 6 | //! in [codegen_place] below. | ^^^^^^^^^^^^^ no item named `codegen_place` in scope | note: the lint level is defined here --> kani-compiler/src/main.rs:9:9 | 9 | #![deny(warnings)] | ^^^^^^^^ = note: `#[deny(rustdoc::broken_intra_doc_links)]` implied by `#[deny(warnings)]` = help: to escape `[` and `]` characters, add '\' before them like `\[` or `\]`

error: unresolved link to codegen_pointer_cast
--> kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:614:22
|
614 | /// handled by [codegen_pointer_cast].
| ^^^^^^^^^^^^^^^^^^^^ no item named codegen_pointer_cast in scope
|
= help: to escape [ and ] characters, add '' before them like \[ or \]

error: unresolved link to codegen_misc_cast
--> kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:694:48
|
694 | /// many of which are instead handled by [codegen_misc_cast] instead.
| ^^^^^^^^^^^^^^^^^ no item named codegen_misc_cast in scope
|
= help: to escape [ and ] characters, add '' before them like \[ or \]

error: unresolved link to LayoutCx::layout_raw_uncached
--> kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:537:16
|
537 | /// check [LayoutCx::layout_raw_uncached] for LLVM codegen
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ no item named LayoutCx in scope

error: unresolved link to __nondet
--> kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs:5:27
|
5 | //! functions start with [__nondet] is silently replaced by nondeterministic values, and
| ^^^^^^^^ no item named __nondet in scope
|
= help: to escape [ and ] characters, add '' before them like \[ or \]

error: unresolved link to begin_panic
--> kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs:6:6
|
6 | //! [begin_panic] is replaced by [assert(false)], etc.
| ^^^^^^^^^^^ no item named begin_panic in scope
|
= help: to escape [ and ] characters, add '' before them like \[ or \]

error: unresolved link to <prefix>
--> kani-compiler/src/codegen_cprover_gotoc/utils/names.rs:114:10
|
114 | /// []
| ^^^^^^^^ missing type for generic parameters

error: unresolved link to KANI_REACHABILITY_CHECK
--> kani-compiler/src/codegen_cprover_gotoc/utils/names.rs:122:10
|
122 | /// [KANI_REACHABILITY_CHECK]
| ^^^^^^^^^^^^^^^^^^^^^^^ no item named KANI_REACHABILITY_CHECK in scope
|
= help: to escape [ and ] characters, add '' before them like \[ or \]

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:121:9
|
121 | ...// https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/Determine.20untupled.20closure.20args.20from.20Instance.3F
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/Determine.20untupled.20closure.20args.20from.20Instance.3F>
|
= note: #[deny(rustdoc::bare_urls)] implied by #[deny(warnings)]
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:130:14
|
130 | /// c.f. https://doc.rust-lang.org/std/intrinsics/index.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/intrinsics/index.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:756:9
|
756 | /// https://doc.rust-lang.org/std/intrinsics/fn.assert_inhabited.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/intrinsics/fn.assert_inhabited.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:757:9
|
757 | /// https://doc.rust-lang.org/std/intrinsics/fn.assert_uninit_valid.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/intrinsics/fn.assert_uninit_valid.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:758:9
|
758 | /// https://doc.rust-lang.org/std/intrinsics/fn.assert_zero_valid.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/intrinsics/fn.assert_zero_valid.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:907:13
|
907 | /// https://doc.rust-lang.org/core/intrinsics/fn.copy.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/core/intrinsics/fn.copy.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:909:13
|
909 | /// https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:981:13
|
981 | /// https://doc.rust-lang.org/std/intrinsics/fn.offset.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/intrinsics/fn.offset.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:983:13
|
983 | /// https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:988:13
|
988 | /// See #1233 for more details.
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://github.com/model-checking/kani/issues/1233>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:991:9
|
991 | /// https://doc.rust-lang.org/std/primitive.pointer.html#safety-2
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/primitive.pointer.html#safety-2>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:1026:9
|
1026 | /// https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:1051:13
|
1051 | /// See rust-lang/rust#95892 for more details
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://github.com/rust-lang/rust/issues/95892>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:1101:9
|
1101 | /// https://doc.rust-lang.org/std/intrinsics/fn.transmute.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/intrinsics/fn.transmute.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:1295:9
|
1295 | /// https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/c_expr.cpp
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/c_expr.cpp>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:1299:16
|
1299 | /// Issue: diffblue/cbmc#6297
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://github.com/diffblue/cbmc/issues/6297>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:1335:9
|
1335 | /// https://doc.rust-lang.org/std/ptr/fn.write_volatile.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/ptr/fn.write_volatile.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:1361:9
|
1361 | /// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/std/ptr/fn.write_bytes.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:35:13
|
35 | /// See #327 for more details.
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://github.com/model-checking/kani/issues/327>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:259:9
|
259 | /// https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/terminator/enum.TerminatorKind.html#variant.SwitchInt
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/terminator/enum.TerminatorKind.html#variant.SwitchInt>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:462:9
|
462 | /// #358
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://github.com/model-checking/kani/issues/358>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:539:19
|
539 | /// also c.f. https://www.ralfj.de/blog/2020/04/04/layout-debugging.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://www.ralfj.de/blog/2020/04/04/layout-debugging.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:540:19
|
540 | /// c.f. https://rust-lang.github.io/unsafe-code-guidelines/introduction.html
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://rust-lang.github.io/unsafe-code-guidelines/introduction.html>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:1059:14
|
1059 | /// c.f. https://rust-lang.github.io/unsafe-code-guidelines/layout/enums.html#layout-of-a-data-carrying-enums-without-a-repr-annotation
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://rust-lang.github.io/unsafe-code-guidelines/layout/enums.html#layout-of-a-data-carrying-enums-without-a-repr-annotation>
|
= note: bare URLs are not automatically turned into clickable links

error: this URL is not a hyperlink
--> kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:1444:5
|
1444 | /// #752
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ help: use an automatic link instead: <https://github.com/model-checking/kani/issues/752>
|
= note: bare URLs are not automatically turned into clickable links

error: could not document kani-compiler

Caused by:
process didn't exit successfully: rustdoc --edition=2021 --crate-type bin --crate-name kani_compiler kani-compiler/src/main.rs -o /Users/ytakashl/Desktop/kani/target/doc --cfg 'feature="ar"' --cfg 'feature="bitflags"' --cfg 'feature="cbmc"' --cfg 'feature="cprover"' --cfg 'feature="default"' --cfg 'feature="kani_metadata"' --cfg 'feature="libc"' --cfg 'feature="num"' --cfg 'feature="object"' --cfg 'feature="rustc-demangle"' --cfg 'feature="serde"' --cfg 'feature="serde_json"' --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --document-private-items '-Arustdoc::private-intra-doc-links' -C metadata=527085c67c642800 -L dependency=/Users/ytakashl/Desktop/kani/target/debug/deps --extern ar=/Users/ytakashl/Desktop/kani/target/debug/deps/libar-a97f6b4805ae9296.rmeta --extern atty=/Users/ytakashl/Desktop/kani/target/debug/deps/libatty-8d3b9df89a760fa1.rmeta --extern bitflags=/Users/ytakashl/Desktop/kani/target/debug/deps/libbitflags-89d21d19d5ca1122.rmeta --extern clap=/Users/ytakashl/Desktop/kani/target/debug/deps/libclap-14f41d53bbf9356d.rmeta --extern cbmc=/Users/ytakashl/Desktop/kani/target/debug/deps/libcprover_bindings-9f29e9ddfc91582b.rmeta --extern home=/Users/ytakashl/Desktop/kani/target/debug/deps/libhome-caebcd41c0c039ac.rmeta --extern kani_metadata=/Users/ytakashl/Desktop/kani/target/debug/deps/libkani_metadata-709315a34b09e9b1.rmeta --extern kani_queries=/Users/ytakashl/Desktop/kani/target/debug/deps/libkani_queries-574d486ee8bb0d7d.rmeta --extern libc=/Users/ytakashl/Desktop/kani/target/debug/deps/liblibc-e4808047fc491b1b.rmeta --extern num=/Users/ytakashl/Desktop/kani/target/debug/deps/libnum-bcc2e3d1f720ad8d.rmeta --extern object=/Users/ytakashl/Desktop/kani/target/debug/deps/libobject-2c2d33cac520c1e8.rmeta --extern rustc_demangle=/Users/ytakashl/Desktop/kani/target/debug/deps/librustc_demangle-c363574301d8a485.rmeta --extern serde=/Users/ytakashl/Desktop/kani/target/debug/deps/libserde-1feca9d10d3ee4fa.rmeta --extern serde_json=/Users/ytakashl/Desktop/kani/target/debug/deps/libserde_json-053ef1d5f05fddb9.rmeta --extern shell_words=/Users/ytakashl/Desktop/kani/target/debug/deps/libshell_words-2319a8d03c6898ea.rmeta --extern tracing=/Users/ytakashl/Desktop/kani/target/debug/deps/libtracing-11ced09703f4cbf8.rmeta --extern tracing_subscriber=/Users/ytakashl/Desktop/kani/target/debug/deps/libtracing_subscriber-a68033cd97dc0946.rmeta --extern tracing_tree=/Users/ytakashl/Desktop/kani/target/debug/deps/libtracing_tree-339ea9b387ad594d.rmeta --crate-version 0.4.0 (exit status: 1)
warning: build failed, waiting for other jobs to finish...

Compilation exited abnormally with code 101 at Tue Jun 14 19:52:59

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant