File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed
cprover_bindings/src/goto_program
kani-compiler/src/codegen_cprover_gotoc/codegen Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -7,7 +7,7 @@ use std::fmt::Debug;
77/// A `Contract` represents a code contract type.
88/// A contract describes specifications (in the form of preconditions, postconditions, and invariants) of certain expressions.
99/// Further details about the CBMC implementation can be found here -
10- /// https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/contracts.md
10+ /// < https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/contracts.md>
1111
1212/// Represents a contract on a function, loop, etc.
1313#[ derive( Clone , Debug ) ]
Original file line number Diff line number Diff line change @@ -56,7 +56,7 @@ impl<'tcx> GotocCtx<'tcx> {
5656
5757 /// Generates a new contract symbol and adds it to the symbol table.
5858 /// See <https://github.com/diffblue/cbmc/pull/6799> for further details about the contract symbol.
59- /// The name of the contract symbol should be set to " contract::<function-name>" .
59+ /// The name of the contract symbol should be set to ` contract::<function-name>` .
6060 /// The type field of the contract symbol contains the `#spec_requires`, `#spec_ensures`, and `#spec_assigns` fields
6161 /// for specifying the preconditions, postconditions, and the modifies (assigns/write) set of the function respectively.
6262 /// The contract symbol serves as the entry point for CBMC to check the contract.
You can’t perform that action at this time.
0 commit comments