Fixed cargo doc failing to compile (#1331)

* 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.

Author: Yoshiki Takashima

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;

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 {

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,

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 {

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) }

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)
     }

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

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

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>,

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;