Fixed cargo doc failing to compile (#1331)

Yoshiki Takashima · web-flow · commit 7cd1aeb6305b · 2022-07-05T14:09:27.000-04:00
* Resolved link formatting issue.

* Fixed escaping of brackets.

* Fixed intra dock links.

* Fixed broken link to rustc_middle::ty::layout::LayoutCx.

* More hyperlink formatting warning fixed.

* Fixed typo in struct. Mismatched curly braces.

* fixed links and brackets.

* Added gh action to build docs automatically.

* Added gh action to build docs automatically.

* Moved docs check to regressions script.
diff --git 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
@@ -118,7 +118,7 @@ pub enum ExprValue {
         op: SelfOperand,
         e: Expr,
     },
-    /// https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html
+    /// <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
+    /// <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: <https://github.com/model-checking/kani/issues/996>
         // 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
+    /// <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<Stmt>, typ: Type) -> Self {
diff --git 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
+/// <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: <https://github.com/model-checking/kani/issues/1>
 #[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
@@ -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
+/// <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
@@ -32,7 +32,7 @@ pub enum Type {
     /// `return_type x(parameters)`
     Code { parameters: Vec<Parameter>, return_type: Box<Type> },
     /// `__attribute__(constructor)`. Only valid as a function return type.
-    /// https://gcc.gnu.org/onlinedocs/gcc-4.7.0/gcc/Function-Attributes.html
+    /// <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<T: Into<InternedString>>(name: T, typ: Type) -> Self {
-        // TODO https://github.com/model-checking/kani/issues/1243
+        // TODO <https://github.com/model-checking/kani/issues/1243>
         // 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
+    /// <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<T>(self, size: T) -> Self
     where
         T: TryInto<u64>,
@@ -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<Parameter>, 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<Parameter>, 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
@@ -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
+/// <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
+    /// <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
@@ -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
+    /// <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<T>(i: T, width: u64, _signed: bool) -> IrepId
diff --git 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
+/// <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
+    /// <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
@@ -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
+/// <https://github.com/diffblue/cbmc/blob/develop/src/util/symbol_table.h>
 #[derive(Debug, PartialEq)]
 pub struct SymbolTable {
     pub symbol_table: BTreeMap<InternedString, Symbol>,
diff --git 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
@@ -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
+/// <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
@@ -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
+    /// <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
@@ -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. <https://doc.rust-lang.org/std/intrinsics/index.html>
     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
+    /// <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
+    ///     <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
+    ///     <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
+    ///     <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
+    ///     <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 <https://github.com/model-checking/kani/issues/1233> 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
+    /// <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
+    /// <https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html>
     fn codegen_ptr_offset_from(
         &mut self,
         fargs: Vec<Expr>,
@@ -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 <https://github.com/rust-lang/rust/issues/95892> for more details
     fn codegen_ptr_offset_from_unsigned(
         &mut self,
         fargs: Vec<Expr>,
@@ -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
+    /// <https://doc.rust-lang.org/std/intrinsics/fn.transmute.html>
     ///
     /// let bitpattern = unsafe {
     ///     std::mem::transmute::<f32, u32>(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
+    /// <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: <https://github.com/diffblue/cbmc/issues/6297>
     fn _codegen_intrinsic_simd_shuffle(
         &mut self,
         mut fargs: Vec<Expr>,
@@ -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
+    /// <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::<T>()` bytes of memory starting at `dst` to `val`
-    /// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
+    /// <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
@@ -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
@@ -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 <https://github.com/model-checking/kani/issues/327> 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
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
diff --git a/tools/bookrunner/src/books.rs b/tools/bookrunner/src/books.rs

Original file line number	Diff line number	Diff line change
`@@ -831,7 +831,7 @@ impl IrepId {`
`831`	`831`	`}`
`832`	`832`
`833`	`833`	`/// CBMC expects two's complement for negative numbers.`
`834`		`- /// https://github.com/diffblue/cbmc/blob/develop/src/util/arith_tools.cpp#L401..L424`
	`834`	`+ /// <https://github.com/diffblue/cbmc/blob/develop/src/util/arith_tools.cpp#L401..L424>`
`835`	`835`	`/// The bignum crate instead does sign/magnitude when making hex.`
`836`	`836`	`/// So for negatives, do the two's complement ourselves.`
`837`	`837`	`pub fn bitpattern_from_int<T>(i: T, width: u64, _signed: bool) -> IrepId`