Skip to content

Commit 5834261

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #7149 from markrtuttle/publish-documentation
Publish documentation
2 parents 54bb53d + ee0a06d commit 5834261

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

45 files changed

+13489
-55
lines changed

‎.github/workflows/publish.yaml

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
name: Publish CBMC documentation
2+
on: [push, pull_request]
3+
4+
jobs:
5+
publish:
6+
runs-on: ubuntu-latest
7+
steps:
8+
- name: Checkout repository
9+
uses: actions/checkout@v2
10+
11+
- name: Install doxygen
12+
run: sudo apt install doxygen graphviz pandoc
13+
14+
- name: Install python modules
15+
run: sudo python3 -m pip install gitpython pandocfilters
16+
17+
- name: Build documentation
18+
run: cd doc/doxygen-root && make && touch html/.nojekyll
19+
20+
- name: Publish documentation
21+
if: ${{ github.event_name == 'push' && startsWith('refs/heads/develop', github.ref) }}
22+
uses: JamesIves/[email protected]
23+
with:
24+
branch: gh-pages
25+
folder: doc/doxygen-root/html

‎doc/ADR/README.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,5 @@ of the system and the surrounding infrastructure.
88

99
## Release & Packaging
1010

11-
* [Release Process](release_process.md)
12-
* [Homebrew tap](homebrew_tap.md)
11+
* \subpage release-process
12+
* \subpage homebrew-tap-instructions

‎doc/ADR/homebrew_tap.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
# Homebrew tap instructions
1+
\page homebrew-tap-instructions Homebrew tap instructions
22

33
CBMC archives versions into a tap which you can use to quickly download and
44
build various historical versions.

‎doc/ADR/release_process.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
# Release Process
1+
\page release-process Release Process
22

33
**Date**: 2020-10-08
44
**Updated**: 2022-06-23
@@ -9,7 +9,7 @@
99

1010
The current process we follow through to make a new release is the following:
1111

12-
1. At the point in time we want to make the release, we make a change to
12+
1. At the point in time we want to make the release, we make a change to
1313
`src/config.inc`, and update the configuration variable `CBMC_VERSION`.
1414
This is important as it informs the various tools of the current version
1515
of CBMC.

‎doc/API/README.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# CPROVER APIs
2+
3+
* \subpage piped-process

‎doc/API/util/piped_process.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
# `src/util/piped_process.{cpp, h}`
1+
\page piped-process `src/util/piped_process.{cpp, h}`
22

33
To utilise the `piped_process` API for interprocess communication with any binary:
44

‎doc/architectural/background-concepts.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
\ingroup module_hidden
2+
23
\page background-concepts Background Concepts
34

45
\author Martin Brain, Peter Schrammel, Johannes Kloos

‎doc/architectural/cbmc-architecture.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
\ingroup module_hidden
2+
23
\page cbmc-architecture CBMC Architecture
34

45
\author Martin Brain, Peter Schrammel

‎doc/architectural/code-walkthrough.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
\ingroup module_hidden
2+
23
\page code-walkthrough Code Walkthrough
34

45
\author Cesar Rodriguez, Owen Jones

‎doc/architectural/compilation-and-development.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
\ingroup module_hidden
2+
23
\page compilation-and-development Compilation and Development
34

45
\author Martin Brain, Peter Schrammel, Owen Jones

‎doc/architectural/folder-walkthrough.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
\ingroup module_hidden
2+
23
\page folder-walkthrough Folder Walkthrough
34

45
\author Martin Brain, Peter Schrammel

‎doc/architectural/front-page.md

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
1-
CProver Developer Documentation
2-
=====================
1+
\page cprover_documentation CProver documentation
32

43
These pages contain user tutorials, automatically-generated API
54
documentation, and higher-level architectural overviews for the
@@ -66,6 +65,10 @@ Overview of Documentation
6665
you can access it <a href=
6766
"https://svn.cprover.org/wiki/doku.php?id=cprover_tutorial">here</a>.
6867

68+
* \subpage memory-analyzer
69+
* \subpage memory-bounds-checking
70+
* \subpage satabs
71+
6972
### For contributors:
7073

7174
The following pages attempt to provide the information that a developer needs to

‎doc/architectural/howto.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
\ingroup module_hidden
2+
23
\page tutorial Tutorials
34

45
\section cbmc_tutorial CBMC Developer Tutorial

‎doc/architectural/memory-analyzer.md

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
1-
[CPROVER Manual TOC](../../)
21

3-
## Memory Analyzer
2+
\page memory-analyzer Memory Analyzer
43

54
The memory analyzer is a front-end that runs and queries GDB in order to obtain
65
a snapshot of the state of the input program at a particular program location.

‎doc/architectural/memory-bounds-checking.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
\ingroup module_hidden
2+
23
\page memory-bounds-checking Memory Bounds Checking
34

45
cbmc provides means to verify that pointers are within the bounds of (statically

‎doc/architectural/other-tools.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
\ingroup module_hidden
2+
23
\page other-tools Other Tools
34

45
\author Martin Brain, Peter Schrammel

‎doc/cprover-manual/cbmc-tutorial.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,7 @@ the `for` loop in the program. As CBMC performs Bounded Model Checking,
176176
all loops have to have a finite upper run-time bound in order to
177177
guarantee that all bugs are found. CBMC can optionally check that enough
178178
unwinding is performed. As an example, consider the program
179-
[binsearch.c](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/cprover-manual/binsearch1.c):
179+
[binsearch.c](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/cprover-manual/binsearch.c):
180180

181181
```C
182182
int binsearch(int x)
@@ -333,7 +333,7 @@ comes with a small set of definitions, which includes functions such as
333333

334334
### Further Reading
335335

336-
- [Understanding Loop Unwinding](../unwinding/)
336+
- [Understanding Loop Unwinding](../../cbmc/unwinding/)
337337
- [Hardware Verification using ANSI-C Programs as a
338338
Reference](http://www-2.cs.cmu.edu/~svc/papers/view-publications-ck03.html)
339339
- [Behavioral Consistency of C and Verilog Programs Using Bounded

‎doc/cprover-manual/contracts-loops.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
# Loop Contracts
44

55
CBMC offers support for loop contracts, which includes three basic clauses:
6+
67
- _invariant_ clause for establishing safety properties
78
- _decreases_ clause for establishing termination, and
89
- _assigns_ clause for declaring the subset of variables that is modifiable in the loop.

‎doc/cprover-manual/contracts.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Design](https://www.georgefairbanks.com/york-university-contract-based-design-20
1515
by George Fairbanks.
1616

1717
CBMC currently supports contracts on functions and loops:
18+
1819
- [Function Contracts](../contracts/functions/)
1920
- [Loop Contracts](../contracts/loops/)
2021

‎doc/cprover-manual/goto-analyzer.md

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ iterations or B. possibly false. In this sense, each tool has its own
1818
strengths and weaknesses.
1919

2020
To use `goto-analyzer` you need to give options for:
21+
2122
* What [task](#task) to perform after the abstract interpreter has run.
2223
* How to format the [output](#output).
2324
* Which [abstract interpreter](#abstractinterpreter) is used.
@@ -48,7 +49,7 @@ goto-analyzer --verify --three-way-merge --vsd --vsd-values set-of-constants --
4849

4950
I want to discharge obvious conditions and remove unreachable code:
5051
```
51-
goto-analyzer --simplify out.gb --three-way-merge --vsd
52+
goto-analyzer --simplify out.gb --three-way-merge --vsd
5253
```
5354

5455

@@ -182,7 +183,7 @@ will likely become the default at some point in the future.
182183
: This extends `--recursive-interprocedural` by performing a
183184
"modification aware" merge after function calls. At the time of
184185
writing only `--vsd` supports the necessary differential reasoning.
185-
If you are using `--vsd` this is recommended as it is more accurate
186+
If you are using `--vsd` this is recommended as it is more accurate
186187
with little extra cost.
187188

188189

@@ -412,7 +413,7 @@ location will use the same domain. Setting this means that the
412413
results of other histories will be similar to setting
413414
`--ahistorical`. One difference is how and when widening occurs.
414415
`--one-domain-per-location --loop-unwind n` will wait until `n`
415-
iterations of a loop have been completed and then will start to widen.
416+
iterations of a loop have been completed and then will start to widen.
416417

417418
`--one-domain-per-history`
418419
: This is the best option to use if you are using a history other than
@@ -430,4 +431,3 @@ instrumentation. These all function exactly the same as CBMC does.
430431
It also supports specific analyses which do not fit into the
431432
configurable scheme above. At the time of writing this is just
432433
`--taint` which performs a configurable taint analysis.
433-

‎doc/cprover-manual/index.md

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,34 +1,34 @@
11
# The CPROVER Manual
22

3-
## 1. [Introduction](introduction/)
3+
1. [Introduction](introduction/)
44

5-
## 2. [Installation](installation/)
5+
2. [Installation](installation/)
66

7-
## 3. CBMC &ndash; Bounded Model Checking
7+
3. CBMC &ndash; Bounded Model Checking
88

9-
[A Short Tutorial](cbmc/tutorial/),
10-
[Loop Unwinding](cbmc/unwinding/),
11-
[Assertion Checking](cbmc/assertions/)
9+
* [A Short Tutorial](cbmc/tutorial/)
10+
* [Loop Unwinding](cbmc/unwinding/)
11+
* [Assertion Checking](cbmc/assertions/)
1212

13-
## 4. [Compositional Reasoning using Code Contracts](contracts/)
13+
4. [Compositional Reasoning using Code Contracts](contracts/)
1414

15-
## 5. [Goto-Analyzer &ndash; Abstract Interpretation](goto-analyzer/)
15+
5. [Goto-Analyzer &ndash; Abstract Interpretation](goto-analyzer/)
1616

17-
## 6. [Test Suite Generation](test-suite/)
17+
6. [Test Suite Generation](test-suite/)
1818

19-
## 7. [Program Properties](properties/)
19+
7. [Program Properties](properties/)
2020

21-
## 8. Modeling
21+
8. Modeling
2222

23-
[Nondeterminism](modeling/nondeterminism/),
24-
[Assumptions](modeling/assumptions/),
25-
[Pointers](modeling/pointers/),
26-
[Floating Point](modeling/floating-point/)
27-
[Generating Environments](goto-harness/)
23+
* [Nondeterminism](modeling/nondeterminism/)
24+
* [Assumptions](modeling/assumptions/)
25+
* [Pointers](modeling/pointers/)
26+
* [Floating Point](modeling/floating-point/)
27+
* [Generating Environments](goto-harness/)
2828

29-
## 9. Build Systems
29+
9. Build Systems
3030

31-
[Integration into Build Systems with goto-cc](goto-cc/),
32-
[Integration with Visual Studio builds](visual-studio/)
31+
* [Integration into Build Systems with goto-cc](goto-cc/)
32+
* [Integration with Visual Studio builds](visual-studio/)
3333

34-
## 10. [The CPROVER API Reference](api/)
34+
10. [The CPROVER API Reference](api/)

‎doc/cprover-manual/properties.md

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -133,14 +133,15 @@ The goto-instrument program supports these checks:
133133
| `--error-label label` | check that given label is unreachable |
134134
135135
As all of these checks apply across the entire input program, we may wish to
136-
disable or enable them for selected statements in the program.
137-
For example, unsigned overflows can be expected and acceptable in certain
138-
instructions even when elsewhere we do not expect them.
136+
disable or enable them for selected statements in the program.
137+
For example, unsigned overflows can be expected and acceptable in certain
138+
instructions even when elsewhere we do not expect them.
139139
As of version 5.12, CBMC supports selectively disabling or enabling
140140
automatically generated properties using pragmas.
141141
142142
143143
CPROVER pragmas are handled using a stack:
144+
144145
- `#pragma CPROVER check push` pushes a new level on the pragma stack
145146
- `#pragma CPROVER check disable "<name_of_check>"` adds a disable pragma
146147
at the top of the stack

‎doc/doxygen-root/.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
html/

0 commit comments

Comments
 (0)