diff --git a/cprover_bindings/src/env.rs b/cprover_bindings/src/env.rs index 594af6ea60a5..6e285e1bf206 100644 --- a/cprover_bindings/src/env.rs +++ b/cprover_bindings/src/env.rs @@ -6,7 +6,7 @@ //! the current compilation instance's session information. //! //! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp]. -//! One possible invocation of this insertion in CBMC can be found in [ansi_c_languaget::parse]. +//! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\]. use super::goto_program::{Expr, Location, Symbol, Type}; use super::MachineModel; diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 6b7891bd970e..80fc0c4d937e 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -118,7 +118,7 @@ pub enum ExprValue { op: SelfOperand, e: Expr, }, - /// https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html + /// /// e.g. `({ int y = foo (); int z; if (y > 0) z = y; else z = - y; z; })` /// `({ op1; op2; ...})` StatementExpression { @@ -326,7 +326,7 @@ impl Expr { /// What typecasts are legal. Based off the C standard, plus some additional types /// that don't appear in the standard, like `bool` - /// https://docs.microsoft.com/en-us/cpp/c-language/type-cast-conversions?view=msvc-160 + /// pub fn can_cast_from(source: &Type, target: &Type) -> bool { let source = source.unwrap_typedef(); let target = target.unwrap_typedef(); @@ -544,7 +544,7 @@ impl Expr { { assert!(typ.is_integer()); let i = i.into(); - // TODO: https://github.com/model-checking/kani/issues/996 + // TODO: // if i != 0 && i != 1 { // assert!( // typ.min_int() <= i && i <= typ.max_int(), @@ -622,7 +622,7 @@ impl Expr { expr!(PointerConstant(c), typ) } - /// https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html + /// /// e.g. `({ int y = foo (); int z; if (y > 0) z = y; else z = - y; z; })` /// `({ op1; op2; ...})` pub fn statement_expression(ops: Vec, typ: Type) -> Self { diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs index 13c6e9f369f7..1125b615be67 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/cprover_bindings/src/goto_program/symbol.rs @@ -5,7 +5,7 @@ use super::{DatatypeComponent, Expr, Location, Parameter, Stmt, Type}; use crate::{InternStringOption, InternedString}; /// Based off the CBMC symbol implementation here: -/// https://github.com/diffblue/cbmc/blob/develop/src/util/symbol.h +/// #[derive(Clone, Debug)] pub struct Symbol { /// Unique identifier. Mangled name from compiler `foo12_bar17_x@1` @@ -45,7 +45,7 @@ pub struct Symbol { } /// Currently, only C is understood by CBMC. -// TODO: https://github.com/model-checking/kani/issues/1 +// TODO: #[derive(Clone, Debug)] pub enum SymbolModes { C, diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs index 62fec3bf0b98..2c12a00a80ca 100644 --- a/cprover_bindings/src/goto_program/symbol_table.rs +++ b/cprover_bindings/src/goto_program/symbol_table.rs @@ -5,7 +5,7 @@ use super::{BuiltinFn, Stmt, Symbol}; use crate::InternedString; use std::collections::BTreeMap; /// This is a typesafe implementation of the CBMC symbol table, based on the CBMC code at: -/// https://github.com/diffblue/cbmc/blob/develop/src/util/symbol_table.h +/// /// Since the field is kept private, with only immutable references handed out, elements can only #[derive(Clone, Debug)] pub struct SymbolTable { diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index fbbb0adac33a..6661351349b9 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -32,7 +32,7 @@ pub enum Type { /// `return_type x(parameters)` Code { parameters: Vec, return_type: Box }, /// `__attribute__(constructor)`. Only valid as a function return type. - /// https://gcc.gnu.org/onlinedocs/gcc-4.7.0/gcc/Function-Attributes.html + /// Constructor, /// `double` Double, @@ -185,7 +185,7 @@ impl DatatypeComponent { } pub fn field>(name: T, typ: Type) -> Self { - // TODO https://github.com/model-checking/kani/issues/1243 + // TODO // assert!( // Self::typecheck_datatype_field(&typ), // "Illegal field.\n\tName: {}\n\tType: {:?}", @@ -813,13 +813,13 @@ impl Type { /// But, `struct foo` is not structurally equivalent to: /// ``` /// __attribute__((packed)) - /// struct baz {} + /// struct baz { /// char x; /// int y; /// } /// ``` /// Since they have different padding. - /// https://github.com/diffblue/cbmc/blob/develop/src/solvers/lowering/byte_operators.cpp#L1093..L1136 + /// pub fn is_structurally_equivalent_to(&self, other: &Type, st: &SymbolTable) -> bool { let concrete_other = other.unwrap_typedef(); let concrete_self = self.unwrap_typedef(); @@ -898,7 +898,7 @@ impl Type { } } - /// elem_t[size] + /// elem_t\[size\] pub fn array_of(self, size: T) -> Self where T: TryInto, @@ -959,7 +959,7 @@ impl Type { CInteger(CIntType::SSizeT) } - /// corresponds to [code_typet] in CBMC, representing a function type + /// corresponds to \[code_typet\] in CBMC, representing a function type /// ret (params ..) pub fn code(parameters: Vec, return_type: Type) -> Self { Code { parameters, return_type: Box::new(return_type) } @@ -1155,7 +1155,7 @@ impl Type { Unsignedbv { width } } - /// corresponds to [code_typet] in CBMC, representing a function type + /// corresponds to \[code_typet\] in CBMC, representing a function type /// ret (params, ... ) pub fn variadic_code(parameters: Vec, return_type: Type) -> Self { VariadicCode { parameters, return_type: Box::new(return_type) } diff --git a/cprover_bindings/src/irep/irep.rs b/cprover_bindings/src/irep/irep.rs index d9b9c80afb59..8cb6cc2e2079 100644 --- a/cprover_bindings/src/irep/irep.rs +++ b/cprover_bindings/src/irep/irep.rs @@ -12,7 +12,7 @@ use std::fmt::Debug; /// The CBMC serialization format for goto-programs. /// CBMC implementation code is at: -/// https://github.com/diffblue/cbmc/blob/develop/src/util/irep.h +/// #[derive(Clone, Debug, PartialEq)] pub struct Irep { pub id: IrepId, @@ -85,7 +85,7 @@ impl Irep { /// Constructors impl Irep { /// `__attribute__(constructor)`. Only valid as a function return type. - /// https://gcc.gnu.org/onlinedocs/gcc-4.7.0/gcc/Function-Attributes.html + /// pub fn constructor() -> Irep { Irep::just_id(IrepId::Constructor) } diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index cebf99769174..41cd7718f947 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/cprover_bindings/src/irep/irep_id.rs @@ -831,7 +831,7 @@ impl IrepId { } /// CBMC expects two's complement for negative numbers. - /// https://github.com/diffblue/cbmc/blob/develop/src/util/arith_tools.cpp#L401..L424 + /// /// The bignum crate instead does sign/magnitude when making hex. /// So for negatives, do the two's complement ourselves. pub fn bitpattern_from_int(i: T, width: u64, _signed: bool) -> IrepId diff --git a/cprover_bindings/src/irep/symbol.rs b/cprover_bindings/src/irep/symbol.rs index 2707103f2569..a7ea418b7cfe 100644 --- a/cprover_bindings/src/irep/symbol.rs +++ b/cprover_bindings/src/irep/symbol.rs @@ -3,7 +3,7 @@ use super::Irep; use crate::InternedString; /// A direct implementation of the CBMC serilization format for symbols implemented in -/// https://github.com/diffblue/cbmc/blob/develop/src/util/symbol.h +/// // TODO: do we want these members to be public? #[derive(Clone, Debug, PartialEq)] pub struct Symbol { @@ -19,7 +19,7 @@ pub struct Symbol { /// Almost always the same as base_name, but with name mangling can be relevant pub pretty_name: InternedString, /// Currently set to C. Consider creating a "rust" mode and using it in cbmc - /// https://github.com/model-checking/kani/issues/1 + /// pub mode: InternedString, // global properties diff --git a/cprover_bindings/src/irep/symbol_table.rs b/cprover_bindings/src/irep/symbol_table.rs index 77e63c98fa4b..7e1ae6b40ec6 100644 --- a/cprover_bindings/src/irep/symbol_table.rs +++ b/cprover_bindings/src/irep/symbol_table.rs @@ -5,7 +5,7 @@ use crate::InternedString; use std::collections::BTreeMap; /// A direct implementation of the CBMC serilization format for symbol tables implemented in -/// https://github.com/diffblue/cbmc/blob/develop/src/util/symbol_table.h +/// #[derive(Debug, PartialEq)] pub struct SymbolTable { pub symbol_table: BTreeMap, diff --git a/cprover_bindings/src/lib.rs b/cprover_bindings/src/lib.rs index 30a1fd531ded..4b8b1508bd3f 100644 --- a/cprover_bindings/src/lib.rs +++ b/cprover_bindings/src/lib.rs @@ -6,24 +6,28 @@ //! in CBMC's documentation. All these representations precisely replicate ones in CBMC. //! //! In short, CBMC's AST has three levels: -//! 1. [SymbolTable] is the top level symbol table. -//! 2. [Symbol] is a symbol in the symbol table. -//! 3. [Irep] represents all trees (code, expression, metadata, etc). +//! 1. [irep::SymbolTable] is the top level symbol table. +//! 2. [irep::Symbol] is a symbol in the symbol table. +//! 3. [irep::Irep] represents all trees (code, expression, metadata, etc). //! -//! Each tree represented by [Irep] has three nodes: -//! 1. [id] for identity, -//! 2. [sub] for a (potentially empty) list of unnamed subtrees as [Irep], -//! 3. [named_sub] for a (potentially empty) map of named subtrees as [Irep]. +//! Each tree represented by [irep::Irep] has three nodes: +//! 1. [irep::Irep::id] for identity, +//! 2. [irep::Irep::sub] for a (potentially empty) list of unnamed subtrees as [irep::Irep], +//! 3. [irep::Irep::named_sub] for a (potentially empty) map of named subtrees as [irep::Irep]. //! -//! The function of a tree is usually (but not always) recognized by its [id], and thus the aggregation -//! of all recognized [id]s are represented by [IrepId]. [sub] usually contains operands and [named_sub] -//! usually contains other flags or metadata. For example, for a binary operation [a + b], the [id] of -//! this tree is ["plus"] denoting the tree being a plus operation. [sub] contains two [Irep]s -//! representing [a] and [b] respectively. [named_sub] contains other information include the type of -//! the expression, location information, and so on. +//! The function of a tree is usually (but not always) recognized by +//! its [irep::Irep::id], and thus the aggregation of all recognized +//! [irep::Irep::id]s are represented by [irep::IrepId]. [irep::Irep::sub] usually +//! contains operands and [irep::Irep::named_sub] usually contains +//! other flags or metadata. For example, for a binary operation [a + +//! b], the [irep::Irep::id] of this tree is ["plus"] denoting the +//! tree being a plus operation. [irep::Irep::sub] contains two [irep::Irep]s +//! representing \[a\] and \[b\] respectively. [irep::Irep::named_sub] +//! contains other information include the type of the expression, +//! location information, and so on. //! -//! Speical [id]s include: -//! 1. [Empty] and [Nil] behaves like [null]. +//! Speical [irep::Irep::id]s include: +//! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\]. mod env; pub mod goto_program; diff --git a/cprover_bindings/src/machine_model.rs b/cprover_bindings/src/machine_model.rs index fa506701d877..31427a83a629 100644 --- a/cprover_bindings/src/machine_model.rs +++ b/cprover_bindings/src/machine_model.rs @@ -38,7 +38,7 @@ impl MachineModel { } /// The different rounding modes supported by cbmc. -/// https://github.com/diffblue/cbmc/blob/2bc93c24ea6c09b5fc99b31df682ec5b31c4b162/src/ansi-c/library/fenv.c#L7 +/// #[derive(Clone, Copy, Debug)] pub enum RoundingMode { ToNearest = 0, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 9ab4d1412941..eca7cf4c6d72 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -118,7 +118,7 @@ impl<'tcx> GotocCtx<'tcx> { /// back to the tuple local for use in the body. /// /// See: - /// https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/Determine.20untupled.20closure.20args.20from.20Instance.3F + /// fn codegen_function_prelude(&mut self) { let mir = self.current_fn().mir(); if mir.spread_arg.is_none() { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index a6e2427214f2..2ec2278dd44e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -125,7 +125,7 @@ impl<'tcx> GotocCtx<'tcx> { /// c.f. rustc_codegen_llvm::intrinsic impl IntrinsicCallMethods<'tcx> for Builder<'a, 'll, 'tcx> /// fn codegen_intrinsic_call - /// c.f. https://doc.rust-lang.org/std/intrinsics/index.html + /// c.f. fn codegen_intrinsic( &mut self, instance: Instance<'tcx>, @@ -743,9 +743,9 @@ impl<'tcx> GotocCtx<'tcx> { /// These are intrinsics that statically compile to panics if the type /// layout is invalid so we get a message that mentions the offending type. /// - /// https://doc.rust-lang.org/std/intrinsics/fn.assert_inhabited.html - /// https://doc.rust-lang.org/std/intrinsics/fn.assert_uninit_valid.html - /// https://doc.rust-lang.org/std/intrinsics/fn.assert_zero_valid.html + /// + /// + /// fn codegen_assert_intrinsic( &mut self, instance: Instance<'tcx>, @@ -894,9 +894,9 @@ impl<'tcx> GotocCtx<'tcx> { /// /// Note that this function handles code generation for: /// 1. The `copy` intrinsic. - /// https://doc.rust-lang.org/core/intrinsics/fn.copy.html + /// /// 2. The `CopyNonOverlapping` statement. - /// https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html + /// /// /// Undefined behavior if any of these conditions are violated: /// * Both `src`/`dst` must be properly aligned (done by alignment checks) @@ -968,17 +968,17 @@ impl<'tcx> GotocCtx<'tcx> { /// /// Note that this function handles code generation for: /// 1. The `offset` intrinsic. - /// https://doc.rust-lang.org/std/intrinsics/fn.offset.html + /// /// 2. The `arith_offset` intrinsic. - /// https://doc.rust-lang.org/std/intrinsics/fn.arith_offset.html + /// /// /// Note(std): We don't check that the starting or resulting pointer stay /// within bounds of the object they point to. Doing so causes spurious /// failures due to the usage of these intrinsics in the standard library. - /// See https://github.com/model-checking/kani/issues/1233 for more details. + /// See for more details. /// Also, note that this isn't a requirement for `arith_offset`, but it's /// one of the safety conditions specified for `offset`: - /// https://doc.rust-lang.org/std/primitive.pointer.html#safety-2 + /// fn codegen_offset( &mut self, intrinsic: &str, @@ -1013,7 +1013,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// ptr_offset_from returns the offset between two pointers - /// https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html + /// fn codegen_ptr_offset_from( &mut self, fargs: Vec, @@ -1038,7 +1038,7 @@ impl<'tcx> GotocCtx<'tcx> { /// `ptr_offset_from_unsigned` returns the offset between two pointers where the order is known. /// The logic is similar to `ptr_offset_from` but the return value is a `usize`. - /// See https://github.com/rust-lang/rust/issues/95892 for more details + /// See for more details fn codegen_ptr_offset_from_unsigned( &mut self, fargs: Vec, @@ -1088,7 +1088,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// A transmute is a bitcast from the argument type to the return type. - /// https://doc.rust-lang.org/std/intrinsics/fn.transmute.html + /// /// /// let bitpattern = unsafe { /// std::mem::transmute::(1.0) @@ -1282,11 +1282,11 @@ impl<'tcx> GotocCtx<'tcx> { /// choosing values according to an input array of indexes. /// /// This code mimics CBMC's `shuffle_vector_exprt::lower()` here: - /// https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/c_expr.cpp + /// /// /// We can't use shuffle_vector_exprt because it's not understood by the CBMC backend, /// it's immediately lowered by the C frontend. - /// Issue: https://github.com/diffblue/cbmc/issues/6297 + /// Issue: fn _codegen_intrinsic_simd_shuffle( &mut self, mut fargs: Vec, @@ -1322,7 +1322,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// A volatile write of a memory location: - /// https://doc.rust-lang.org/std/ptr/fn.write_volatile.html + /// /// /// Undefined behavior if any of these conditions are violated: /// * `dst` must be valid for writes (done by `--pointer-check`) @@ -1348,7 +1348,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// Sets `count * size_of::()` bytes of memory starting at `dst` to `val` - /// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html + /// /// /// Undefined behavior if any of these conditions are violated: /// * `dst` must be valid for writes (done by memset writable check) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 10b81428dcc3..40051137ff19 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -3,7 +3,7 @@ //! responsible for handling codegening places. //! //! a place is an expression of specifying a location in memory, like a left value. check the cases -//! in [codegen_place] below. +//! in [GotocCtx::codegen_place] below. use super::typ::TypeExt; use crate::codegen_cprover_gotoc::utils::slice_fat_ptr; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 6dc72c99856f..3360d4d02ab1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -32,7 +32,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Since vtable pointer comparison is not well defined and it has many nuances, we decided to /// fail if the user code performs such comparison. /// - /// See https://github.com/model-checking/kani/issues/327 for more details. + /// See for more details. fn codegen_comparison_fat_ptr( &mut self, op: &BinOp, @@ -608,7 +608,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// This handles all kinds of casts, except a limited subset that are instead - /// handled by [`codegen_pointer_cast`]. + /// handled by [`Self::codegen_pointer_cast`]. fn codegen_misc_cast(&mut self, src: &Operand<'tcx>, dst_t: Ty<'tcx>) -> Expr { let src_t = self.operand_ty(src); debug!( @@ -688,7 +688,7 @@ impl<'tcx> GotocCtx<'tcx> { /// "Pointer casts" are particular kinds of pointer-to-pointer casts. /// See the [`PointerCast`] type for specifics. /// Note that this does not include all casts involving pointers, - /// many of which are instead handled by [`codegen_misc_cast`] instead. + /// many of which are instead handled by [`Self::codegen_misc_cast`] instead. pub fn codegen_pointer_cast( &mut self, k: &PointerCast, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 23adc483c9aa..42e76bfbf9db 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -251,7 +251,7 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::block(block, Location::none()) } - /// https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/terminator/enum.TerminatorKind.html#variant.SwitchInt + /// /// Operand evaluates to an integer; /// jump depending on its value to one of the targets, and otherwise fallback to otherwise. /// The otherwise value is stores as the last value of targets. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index ad518b73329c..5bcc1a8893f6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -458,7 +458,7 @@ impl<'tcx> GotocCtx<'tcx> { /// TODO: to handle trait upcasting, this will need to use a /// poly existential trait type as a part of the key as well. /// See compiler/rustc_middle/src/ty/vtable.rs - /// https://github.com/model-checking/kani/issues/358 + /// pub fn vtable_name(&self, t: Ty<'tcx>) -> String { format!("{}::vtable", self.normalized_trait_name(t)) } @@ -533,10 +533,10 @@ impl<'tcx> GotocCtx<'tcx> { /// codegen for types. it finds a C type which corresponds to a rust type. /// that means [ty] has to be monomorphized. /// - /// check [LayoutCx::layout_raw_uncached] for LLVM codegen + /// check [rustc_middle::ty::layout::LayoutCx::layout_of_uncached] for LLVM codegen /// - /// also c.f. https://www.ralfj.de/blog/2020/04/04/layout-debugging.html - /// c.f. https://rust-lang.github.io/unsafe-code-guidelines/introduction.html + /// also c.f. + /// c.f. pub fn codegen_ty(&mut self, ty: Ty<'tcx>) -> Type { let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), ty); let goto_typ = self.codegen_ty_inner(normalized); @@ -1055,7 +1055,7 @@ impl<'tcx> GotocCtx<'tcx> { /// struct Option<&i32> { /// u8 *_0; /// } - /// c.f. https://rust-lang.github.io/unsafe-code-guidelines/layout/enums.html#layout-of-a-data-carrying-enums-without-a-repr-annotation + /// c.f. fn codegen_enum( &mut self, ty: Ty<'tcx>, @@ -1440,7 +1440,7 @@ pub fn is_repr_c_adt(mir_type: Ty) -> bool { /// This is a place holder function that should normalize the given type. /// /// TODO: We should normalize the type projection here. For more details, see -/// https://github.com/model-checking/kani/issues/752 +/// fn normalize_type(ty: Ty) -> Ty { ty } diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 444283885417..9f52828770de 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -2,8 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! this module contains various codegen hooks for functions. //! e.g. -//! functions start with [__nondet] is silently replaced by nondeterministic values, and -//! [begin_panic] is replaced by [assert(false)], etc. +//! functions start with \[__nondet\] is silently replaced by nondeterministic values, and +//! \[begin_panic\] is replaced by \[assert(false)\], etc. //! //! It would be too nasty if we spread around these sort of undocumented hooks in place, so //! this module addresses this issue. diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index b7d1075bf0ef..8a875e6d6506 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -111,7 +111,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// Add a prefix of the form: - /// [] + /// \[\] /// to the provided message pub fn add_prefix_to_msg(msg: &str, prefix: &str) -> String { format!("[{}] {}", prefix, msg) @@ -119,7 +119,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Generate a message for the reachability check of an assert with ID /// `check_id`. The message is of the form: - /// [KANI_REACHABILITY_CHECK] + /// \[KANI_REACHABILITY_CHECK\] /// The check_id is generated using the GotocCtx::next_check_id method and /// is a unique string identifier for that check. pub fn reachability_check_message(check_id: &str) -> String { diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs index 4758d27ecb59..dbbcc87d474a 100644 --- a/library/kani/src/invariant.rs +++ b/library/kani/src/invariant.rs @@ -5,7 +5,7 @@ use std::num::*; /// Types that implement a check to ensure its value is valid and safe to be used. See -/// https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html for examples of valid values. +/// for examples of valid values. /// /// Implementations of Invariant traits must ensure that the current bit values of the given type /// is valid and that all its invariants hold. @@ -61,7 +61,7 @@ unsafe impl Invariant for bool { } /// Validate that a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] -/// Ref: https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html +/// Ref: unsafe impl Invariant for char { #[inline(always)] fn is_valid(&self) -> bool { diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index ff1acedb9425..19ffbba6752c 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -88,6 +88,9 @@ time "$SCRIPT_DIR"/codegen-firecracker.sh # dependency2 time "$KANI_DIR"/tests/kani-dependency-test/diamond-dependency/run-dependency-test.sh +# Check that documentation compiles. +cargo doc --workspace + echo echo "All Kani regression tests completed successfully." echo diff --git a/tools/bookrunner/src/books.rs b/tools/bookrunner/src/books.rs index a9c233f04e0b..98c0f1c8b0d3 100644 --- a/tools/bookrunner/src/books.rs +++ b/tools/bookrunner/src/books.rs @@ -456,7 +456,7 @@ fn paths_to_string(paths: HashSet) -> String { f } -/// Creates a new [`Tree`] from `path`, and a test `result`. +/// Creates a new [`bookrunner::Tree`] from `path`, and a test `result`. fn tree_from_path(mut path: Vec, result: bool) -> bookrunner::Tree { assert!(!path.is_empty(), "Error: `path` must contain at least 1 element."); let mut tree = bookrunner::Tree::new(