diffblue · NlightNFotis · Sep 26, 2022 · Sep 22, 2022 · Sep 22, 2022 · Sep 22, 2022
@@ -0,0 +1,25 @@
+name: Publish CBMC documentation
+on: [push, pull_request]
+
+jobs:
+  publish:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v2
+
+      - name: Install doxygen
+        run: sudo apt install doxygen graphviz pandoc
+
+      - name: Install python modules
+        run: sudo python3 -m pip install gitpython pandocfilters
+
+      - name: Build documentation
+        run: cd doc/doxygen-root && make && touch html/.nojekyll
+
+      - name: Publish documentation
+        if: ${{ github.event_name == 'push' && startsWith('refs/heads/develop', github.ref) }}
+        uses: JamesIves/[email protected]
+        with:
+          branch: gh-pages
+          folder: doc/doxygen-root/html
@@ -8,5 +8,5 @@ of the system and the surrounding infrastructure.
 
 ## Release & Packaging
 
-* [Release Process](release_process.md)
-* [Homebrew tap](homebrew_tap.md)
+* \subpage release-process
+* \subpage homebrew-tap-instructions
@@ -1,4 +1,4 @@
-# Homebrew tap instructions
+\page homebrew-tap-instructions Homebrew tap instructions
 
 CBMC archives versions into a tap which you can use to quickly download and
 build various historical versions.

@@ -1,4 +1,4 @@
-# Release Process
+\page release-process Release Process
 
 **Date**: 2020-10-08
 **Updated**: 2022-06-23
@@ -9,7 +9,7 @@
 
 The current process we follow through to make a new release is the following:
 
-1. At the point in time we want to make the release, we make a change to 
+1. At the point in time we want to make the release, we make a change to
    `src/config.inc`, and update the configuration variable `CBMC_VERSION`.
    This is important as it informs the various tools of the current version
    of CBMC.

@@ -0,0 +1,3 @@
+# CPROVER APIs
+
+* \subpage piped-process
@@ -1,4 +1,4 @@
-# `src/util/piped_process.{cpp, h}`
+\page piped-process `src/util/piped_process.{cpp, h}`
 
 To utilise the `piped_process` API for interprocess communication with any binary:
 

@@ -1,4 +1,5 @@
 \ingroup module_hidden 
+
 \page background-concepts Background Concepts
 
 \author Martin Brain, Peter Schrammel, Johannes Kloos

@@ -1,4 +1,5 @@
 \ingroup module_hidden
+
 \page cbmc-architecture CBMC Architecture
 
 \author Martin Brain, Peter Schrammel

@@ -1,4 +1,5 @@
 \ingroup module_hidden 
+
 \page code-walkthrough Code Walkthrough
 
 \author Cesar Rodriguez, Owen Jones

@@ -1,4 +1,5 @@
 \ingroup module_hidden 
+
 \page compilation-and-development Compilation and Development
 
 \author Martin Brain, Peter Schrammel, Owen Jones

@@ -1,4 +1,5 @@
 \ingroup module_hidden 
+
 \page folder-walkthrough Folder Walkthrough
 
 \author Martin Brain, Peter Schrammel

@@ -1,5 +1,4 @@
-CProver Developer Documentation
-=====================
+\page cprover_documentation CProver documentation
 
 These pages contain user tutorials, automatically-generated API
 documentation, and higher-level architectural overviews for the
@@ -66,6 +65,10 @@ Overview of Documentation
 you can access it <a href=
 "https://svn.cprover.org/wiki/doku.php?id=cprover_tutorial">here</a>.
 
+* \subpage memory-analyzer
+* \subpage memory-bounds-checking
+* \subpage satabs
+
 ### For contributors:
 
 The following pages attempt to provide the information that a developer needs to

@@ -1,4 +1,5 @@
 \ingroup module_hidden
+
 \page tutorial Tutorials
 
 \section cbmc_tutorial CBMC Developer Tutorial

@@ -1,6 +1,5 @@
-[CPROVER Manual TOC](../../)
 
-## Memory Analyzer
+\page memory-analyzer Memory Analyzer
 
 The memory analyzer is a front-end that runs and queries GDB in order to obtain
 a snapshot of the state of the input program at a particular program location.

@@ -1,4 +1,5 @@
 \ingroup module_hidden
+
 \page memory-bounds-checking Memory Bounds Checking
 
 cbmc provides means to verify that pointers are within the bounds of (statically

@@ -1,4 +1,5 @@
 \ingroup module_hidden 
+
 \page other-tools Other Tools
 
 \author Martin Brain, Peter Schrammel

@@ -176,7 +176,7 @@ the `for` loop in the program. As CBMC performs Bounded Model Checking,
 all loops have to have a finite upper run-time bound in order to
 guarantee that all bugs are found. CBMC can optionally check that enough
 unwinding is performed. As an example, consider the program
-[binsearch.c](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/cprover-manual/binsearch1.c):
+[binsearch.c](https://raw.githubusercontent.com/diffblue/cbmc/develop/doc/cprover-manual/binsearch.c):
 
 ```C
 int binsearch(int x)
@@ -333,7 +333,7 @@ comes with a small set of definitions, which includes functions such as
 
 ### Further Reading
 
--   [Understanding Loop Unwinding](../unwinding/)
+-   [Understanding Loop Unwinding](../../cbmc/unwinding/)
 -   [Hardware Verification using ANSI-C Programs as a
     Reference](http://www-2.cs.cmu.edu/~svc/papers/view-publications-ck03.html)
 -   [Behavioral Consistency of C and Verilog Programs Using Bounded

@@ -3,6 +3,7 @@
 # Loop Contracts
 
 CBMC offers support for loop contracts, which includes three basic clauses:
+
 - _invariant_ clause for establishing safety properties
 - _decreases_ clause for establishing termination, and
 - _assigns_ clause for declaring the subset of variables that is modifiable in the loop.

@@ -15,6 +15,7 @@ Design](https://www.georgefairbanks.com/york-university-contract-based-design-20
 by George Fairbanks.
 
 CBMC currently supports contracts on functions and loops:
+
 - [Function Contracts](../contracts/functions/)
 - [Loop Contracts](../contracts/loops/)
 

@@ -18,6 +18,7 @@ iterations or B. possibly false.  In this sense, each tool has its own
 strengths and weaknesses.
 
 To use `goto-analyzer` you need to give options for:
+
 * What [task](#task) to perform after the abstract interpreter has run.
 * How to format the [output](#output).
 * Which [abstract interpreter](#abstractinterpreter) is used.
@@ -48,7 +49,7 @@ goto-analyzer  --verify --three-way-merge --vsd --vsd-values set-of-constants --
 
 I want to discharge obvious conditions and remove unreachable code:
 ```
-goto-analyzer --simplify out.gb --three-way-merge --vsd 
+goto-analyzer --simplify out.gb --three-way-merge --vsd
 ```
 
 
@@ -182,7 +183,7 @@ will likely become the default at some point in the future.
 : This extends `--recursive-interprocedural` by performing a
 "modification aware" merge after function calls.  At the time of
 writing only `--vsd` supports the necessary differential reasoning.
-If you are using `--vsd` this is recommended as it is more accurate 
+If you are using `--vsd` this is recommended as it is more accurate
 with little extra cost.
 
 
@@ -412,7 +413,7 @@ location will use the same domain.  Setting this means that the
 results of other histories will be similar to setting
 `--ahistorical`.  One difference is how and when widening occurs.
 `--one-domain-per-location --loop-unwind n` will wait until `n`
-iterations of a loop have been completed and then will start to widen. 
+iterations of a loop have been completed and then will start to widen.
 
 `--one-domain-per-history`
 : 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.
 It also supports specific analyses which do not fit into the
 configurable scheme above.  At the time of writing this is just
 `--taint` which performs a configurable taint analysis.
-
@@ -1,34 +1,34 @@
 # The CPROVER Manual
 
-## 1. [Introduction](introduction/)
+1. [Introduction](introduction/)
 
-## 2. [Installation](installation/)
+2. [Installation](installation/)
 
-## 3. CBMC &ndash; Bounded Model Checking
+3. CBMC &ndash; Bounded Model Checking
 
-[A Short Tutorial](cbmc/tutorial/),
-[Loop Unwinding](cbmc/unwinding/),
-[Assertion Checking](cbmc/assertions/)
+   * [A Short Tutorial](cbmc/tutorial/)
+   * [Loop Unwinding](cbmc/unwinding/)
+   * [Assertion Checking](cbmc/assertions/)
 
-## 4. [Compositional Reasoning using Code Contracts](contracts/)
+4. [Compositional Reasoning using Code Contracts](contracts/)
 
-## 5. [Goto-Analyzer &ndash; Abstract Interpretation](goto-analyzer/)
+5. [Goto-Analyzer &ndash; Abstract Interpretation](goto-analyzer/)
 
-## 6. [Test Suite Generation](test-suite/)
+6. [Test Suite Generation](test-suite/)
 
-## 7. [Program Properties](properties/)
+7. [Program Properties](properties/)
 
-## 8. Modeling
+8. Modeling
 
-[Nondeterminism](modeling/nondeterminism/),
-[Assumptions](modeling/assumptions/),
-[Pointers](modeling/pointers/),
-[Floating Point](modeling/floating-point/)
-[Generating Environments](goto-harness/)
+   * [Nondeterminism](modeling/nondeterminism/)
+   * [Assumptions](modeling/assumptions/)
+   * [Pointers](modeling/pointers/)
+   * [Floating Point](modeling/floating-point/)
+   * [Generating Environments](goto-harness/)
 
-## 9. Build Systems
+9. Build Systems
 
-[Integration into Build Systems with goto-cc](goto-cc/),
-[Integration with Visual Studio builds](visual-studio/)
+   * [Integration into Build Systems with goto-cc](goto-cc/)
+   * [Integration with Visual Studio builds](visual-studio/)
 
-## 10. [The CPROVER API Reference](api/)
+10. [The CPROVER API Reference](api/)
@@ -133,14 +133,15 @@ The goto-instrument program supports these checks:
 | `--error-label label`        |  check that given label is unreachable               |
 
 As all of these checks apply across the entire input program, we may wish to
-disable or enable them for selected statements in the program. 
-For example, unsigned overflows can be expected and acceptable in certain 
-instructions even when elsewhere we do not expect them. 
+disable or enable them for selected statements in the program.
+For example, unsigned overflows can be expected and acceptable in certain
+instructions even when elsewhere we do not expect them.
 As of version 5.12, CBMC supports selectively disabling or enabling
 automatically generated properties using pragmas.
 
 
 CPROVER pragmas are handled using a stack:
+
 - `#pragma CPROVER check push` pushes a new level on the pragma stack
 - `#pragma CPROVER check disable "<name_of_check>"` adds a disable pragma
   at the top of the stack

@@ -0,0 +1 @@
+html/