Deploying to gh-pages from @ 60bb14c 🚀

adr/cpp-api-and-modularisation.html

@@ -99,7 +99,7 @@ <h2><a class="anchor" id="autotoc_md2"></a>
 <p>We are working towards addressing these teething problems, but while we are still operating on those, we have to accept some compromises in the architecture of the code while we are iterating or stabilising several of the new or refactored parts.</p>
 <p>Be advised that some constructs may pop up in some limited locations in the codebase that may appear questionable. We are only asking for some patience while we are working out the best way to refactor them into an architecture that is more cohesive with the long term vision for the platform.</p>
 <p>From our end, we will do our best to avoid any spillover effects to other areas of the codebase, and to avoid introducing any behavioural regressions while we are implementing the above plan. Any constructs that may feature "questionable" changes to parts will be marked as such and be followed with an explanation as to why the decision was made.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

adr/homebrew-tap-instructions.html

@@ -131,7 +131,7 @@ <h2><a class="anchor" id="autotoc_md6"></a>
 <div class="line">$ brew link --overwrite [email protected]</div>
 <div class="line">$ cbmc --version</div>
 <div class="line">5.55.0</div>
-</div><!-- fragment --><p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+</div><!-- fragment --><p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

adr/index.html

@@ -76,7 +76,7 @@ <h1><a class="anchor" id="autotoc_md9"></a>
 <li><a class="el" href="homebrew-tap-instructions.html">Homebrew tap instructions</a></li>
 <li><a class="el" href="cpp-api-and-modularisation.html">libcprover-cpp and Modularisation</a></li>
 </ul>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- PageDoc -->
 </div><!-- contents -->
 <!-- start footer part -->

adr/release-process.html

@@ -111,7 +111,7 @@ <h2><a class="anchor" id="autotoc_md13"></a>
 <p>Originally we wanted to automate this part, but we were limited by the fact that we needed to update <code>src/config.inc</code> before doing the release, and that couldn't be done in an automated fashion, as any update needs to go through a PR, and gets stuck on code-owners approvals, making the whole process more manual than intended.</p>
 <p>Following this original limitation, we decided to settle on doing manual releases every two weeks, but having the process being initiated by a developer manually making the change to <code>src/config.inc</code>, and after that has been merged, mark that specific commit as with a version tag, and push that version tag to Github. At that point, the rest of the process is automated.</p>
 <p>The change to the current implementation was part of <a href="https://github.com/diffblue/cbmc/pull/5517">https://github.com/diffblue/cbmc/pull/5517</a>.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

adr/symex-ready-goto.html

@@ -81,7 +81,7 @@
 <li><code>stop_on_fail_verifier_with_fault_localizationt</code>,</li>
 <li><code>stop_on_fail_verifiert</code>.</li>
 </ul>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

api/index.html

@@ -68,7 +68,7 @@
 <div class="textblock"><p><a class="anchor" id="md_README"></a></p><ul>
 <li><a class="el" href="piped-process.html"><code>src/util/piped_process.{cpp, h}</code></a></li>
 </ul>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- PageDoc -->
 </div><!-- contents -->
 <!-- start footer part -->

api/piped-process.html

@@ -93,7 +93,7 @@
 </ul>
 </li>
 </ul>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

assets/index.html

@@ -83,7 +83,7 @@ <h2><a class="anchor" id="autotoc_md1"></a>
 <li>texlive-latex-base</li>
 <li>texlive-latex-extra (for minted package)</li>
 </ul>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- PageDoc -->
 </div><!-- contents -->
 <!-- start footer part -->

assets/md_xml_spec.html

@@ -410,7 +410,7 @@ <h1><a class="anchor" id="autotoc_md4"></a>
 <h3><a class="anchor" id="autotoc_md8"></a>
 SSA to GOTO Trace</h3>
 <p>SSA steps are sorted by clocks and the following steps are skipped: PHI, GUARD assignments; shared-read, shared-write, constraint, spawn, atomic-begin, atomic-end.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

background-concepts.html

@@ -624,7 +624,7 @@ <h2><a class="anchor" id="flattening_lowering_subsection"></a>
 <h2><a class="anchor" id="verification_condition_subsection"></a>
 Verification Condition</h2>
 <p>In the CPROVER framework, the term <b>verification condition</b> is used in a somewhat non-standard way. Let a program and a set of assertions be given. We transform the program into an (acyclic) SSA (i.e., an SSA with all loops unrolled a finite number of times) and turn it into a logical formula, as described above. Note that in this case, the formula will also contain information about what the program does after the assertion is reached: this part of the formula, is, in fact, irrelevant for deciding whether the program can satisfy the assertion or not. The <em>verification condition</em> is the part of the formula that only covers the program execution until the line that checks the assertion has been executed, with everything that comes after it removed.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 </div><!-- doc-content -->

cbmc-architecture.html

@@ -132,7 +132,7 @@ <h3><a class="anchor" id="autotoc_md183"></a>
 <h3><a class="anchor" id="autotoc_md184"></a>
 goto-analyzer</h3>
 <p>To be documented.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 </div><!-- doc-content -->

central-data-structures.html

@@ -157,7 +157,7 @@ <h2><a class="anchor" id="autotoc_md190"></a>
 <p><code>irep</code>s are the underlying data structure used to implement many of the data structures in CBMC and the assorted tools. These include the <code>exprt</code>, <code>typet</code>, <code>codet</code> and <code><a class="el" href="classsource__locationt.html">source_locationt</a></code> classes. This is a tree data structure where each node is expected to contain a string/ID and may have child nodes stored in both a sequence of child nodes and a map of strings/IDs to child nodes. This enables the singular <code>irept</code> data structure to be used to model graphs such as ASTs, CFGs, etc.</p>
 <p>The classes extending <code>irept</code> define how the higher level concepts are mapped onto the underlying tree data structure. For this reason it is usually advised that the member functions of the sub-classes should be used to access the data held, rather than the member functions of the base <code>irept</code> class. This aids potential future restructuring and associates accesses of the data with the member functions which have the doxygen explaining what the data is.</p>
 <p>The strings/IDs held within <code>irept</code> are of type <code>irep_idt</code>. These can be converted to <code>std::string</code> using the <code>id2string</code> function. There is a mechanism provided for casting expressions and types in <a href="../../src/util/expr_cast.h"><code>src/util/expr_cast.h</code></a>. In depth documentation of the <code>irept</code> class itself can be found in <a href="../../src/util/irep.h"><code>src/util/irep.h</code></a>.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 </div><!-- doc-content -->

code-walkthrough.html

@@ -129,7 +129,7 @@ <h1><a class="anchor" id="solvers-infrastructure-section"></a>
 <h1><a class="anchor" id="static-analysis-apis-section"></a>
 Static analysis APIs</h1>
 <p>See <a class="el" href="group__analyses.html">analyses</a> and <a class="el" href="group__pointer-analysis.html">pointer-analysis</a>.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 </div><!-- doc-content -->

compilation-and-development.html

@@ -182,7 +182,7 @@ <h1><a class="anchor" id="compilation-and-development-section-time-profiling"></
 <p>Run <code>gprof &lt;path-to-binary&gt; &lt;path-to-gmon.out&gt;</code> and redirect the output to a file. This will take a while to run - e.g. 12 minutes for test-gen run on a trivial function.</p>
 <p>The output file will now be a large text file. There are two sections: the "flat
 profile", which ignores context, and just tells you how much time was spent in each function; and the "call graph", which includes context, and tells you how much time was spent within each call stack. For more information see online tutorials, like <a href="https://ftp.gnu.org/old-gnu/Manuals/gprof-2.9.1/html_chapter/gprof_5.html">https://ftp.gnu.org/old-gnu/Manuals/gprof-2.9.1/html_chapter/gprof_5.html</a></p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 </div><!-- doc-content -->

contributing_documentation.html

@@ -100,7 +100,7 @@
 <p>When you contribute a module <code>mymodule.c</code> to the source code, there are probably at least two kinds of documentation you want to contribute. One is user documentation to help people use your feature. One is developer documentation to help people debug or extend your work. We recommend that you put files <code>mymodule-user.md</code> and <code>mymodule-developer.md</code> next to <code>mymodule.c</code> in the repository. Then you can use the <code>\page</code> and <code>\subpage</code> mechanism described above into the appropriate parts of the user guide and developer guide.</p>
 <p>When you contribute documentation, it may not be clear whether it should go into the user guide or the developer guide. We recommend that you put into the user guide everything a user needs to know to use the tool. For example, put a description of the CBMC memory model into the user guide. Then the developer guide can link to that description of the memory model in the user guide, and say, "This is the memory model, and
 this is how we implement the memory model."</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 </div><!-- doc-content -->

cprover-manual/index.html

@@ -100,7 +100,7 @@
 <li><a class="el" href="md_smt2_incr.html">Incremental SMT solver</a></li>
 <li><a class="el" href="md_unsound_options.html">Unsound options</a></li>
 </ul>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- PageDoc -->
 </div><!-- contents -->
 <!-- start footer part -->

cprover-manual/md_api.html

@@ -240,7 +240,7 @@ <h3><a class="anchor" id="cproverfixedbvn-c-only"></a>
 <h2><a class="anchor" id="concurrency"></a>
 Concurrency</h2>
 <p>Asynchronous threads are created by preceding an instruction with a label with the prefix **__CPROVER_ASYNC_**.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_cbmc_assertions.html

@@ -103,7 +103,7 @@ <h2><a class="anchor" id="assertion-checking"></a>
 <p>Future CPROVER releases will support explicit quantifiers with a syntax that resembles Spec#:</p>
 <div class="fragment"><div class="line">__CPROVER_forall { *type identifier* ; *expression* }</div>
 <div class="line">__CPROVER_exists { *type identifier* ; *expression* }</div>
-</div><!-- fragment --><p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+</div><!-- fragment --><p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_cbmc_tutorial.html

@@ -220,7 +220,7 @@ <h2><a class="anchor" id="further-reading"></a>
 <li><a href="http://www-2.cs.cmu.edu/~svc/papers/view-publications-ckl2004.html">A Tool for Checking ANSI-C Programs</a></li>
 </ul>
 <p>We also have a <a href="http://www.cprover.org/cbmc/applications/">list of interesting applications of CBMC</a>.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_cbmc_unwinding.html

@@ -147,7 +147,7 @@ <h3><a class="anchor" id="depth-based-unwinding"></a>
 Depth-based Unwinding</h3>
 <p>The loop-based unwinding bound is not always appropriate. In particular, it is often difficult to control the size of the generated formula when using the <code>--unwind</code> option. The option: </p><pre class="fragment">--depth nr
 </pre><p> specifies an unwinding bound in terms of the number of instructions that are executed on a given path, irrespective of the number of loop iterations. Note that CBMC uses the number of instructions in the control-flow graph as the criterion, not the number of instructions in the source code.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_goto_analyzer.html

@@ -150,7 +150,7 @@ <h2><a class="anchor" id="other-options"></a>
 Other Options</h2>
 <p><code>goto-analyzer</code> supports a number of other options for the C/C++ frontend, the platform, displaying program representations and instrumentation. These all function exactly the same as CBMC does.</p>
 <p>It also supports specific analyses which do not fit into the configurable scheme above. At the time of writing this is just <code>--taint</code> which performs a configurable taint analysis.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_goto_cc.html

@@ -158,7 +158,7 @@ <h2><a class="anchor" id="architectural-settings"></a>
 <div class="line">  printf(<span class="stringliteral">&quot;Bytes of i: %d, %d, %d, %d\n&quot;</span>, p[0], p[1], p[2], p[3]);</div>
 <div class="line">  assert(0);</div>
 <div class="line">}</div>
-</div><!-- fragment --><p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+</div><!-- fragment --><p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_goto_harness.html

@@ -399,7 +399,7 @@ <h3><a class="anchor" id="the-function-call-harness-generator"></a>
 
 ** 0 of 1 failed (1 iterations)
 VERIFICATION SUCCESSFUL
-</pre><p> Last modified: 2024-09-29 16:08:10 -0400 </p>
+</pre><p> Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_installation.html

@@ -97,7 +97,7 @@ <h2><a class="anchor" id="requirements-1"></a>
 <h2><a class="anchor" id="installing-the-eclipse-plugin-1"></a>
 Installing the Eclipse Plugin</h2>
 <p>The installation instructions for the Eclipse Plugin, including the link to the download site, are available <a href="http://www.cprover.org/eclipse-plugin/">here</a>. This includes a short tutorial on the Eclipse plugin.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_introduction.html

@@ -82,7 +82,7 @@ <h2><a class="anchor" id="bounded-model-checking-with-cbmc"></a>
 <p>CBMC implements a technique called <em>Bounded Model Checking</em> (BMC). In BMC, the transition relation for a complex state machine and its specification are jointly unwound to obtain a Boolean formula, which is then checked for satisfiability by using an efficient SAT procedure. If the formula is satisfiable, a counterexample is extracted from the output of the SAT procedure. If the formula is not satisfiable, the program can be unwound more to determine if a longer counterexample exists.</p>
 <p>In many engineering domains, real-time guarantees are a strict requirement. An example is software embedded in automotive controllers. As a consequence, the loop constructs in these types of programs often have a strict bound on the number of iterations. CBMC is able to formally verify such bounds by means of <em>unwinding assertions</em>. Once this bound is established, CBMC is able to prove the absence of errors.</p>
 <p>A more detailed description of how to apply CBMC to verify programs is in our <a class="el" href="md_cbmc_tutorial.html">CBMC Tutorial</a>.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_jbmc_user_manual.html

@@ -196,7 +196,7 @@ <h2><a class="anchor" id="java-library-support"></a>
 <h2><a class="anchor" id="further-documentation"></a>
 Further documentation</h2>
 <p>JBMC has a wealth of other options that can either constrain the model (to cope with complexity issues), or output more relevant information. The list of all available options is printed by running: </p><pre class="fragment">$ jbmc --help
-</pre><p> Last modified: 2024-09-29 16:08:10 -0400 </p>
+</pre><p> Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_memory_primitives.html

@@ -182,7 +182,7 @@ <h3><a class="anchor" id="checking-if-a-memory-segment-has-at-least-a-given-size
 </ul>
 <p>Using them on invalid pointers, however, may still be unintended in user programs.</p>
 <p><sup>1</sup> Pointers with negative offsets never point to memory objects. Negative values are used internally to detect pointer underflows.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_modeling_assumptions.html

@@ -124,7 +124,7 @@ <h2><a class="anchor" id="coverage"></a>
 <div class="line">[main.3] file assume_assert.c line 7 function main assert(false) before assume(x &lt; 0): SATISFIED</div>
 <div class="line">[main.4] file assume_assert.c line 7 function main assert(false) after assume(x &lt; 0): FAILED</div>
 </div><!-- fragment --><p>When an <code>assert(false)</code> statement before the assume has the property status <code>SATISFIED</code>, but is followed by an <code>assert(false)</code> statement <em>after</em> the assume statement that has status <code>FAILED</code>, this is an indication that this specific assume statement (on the line reported) is one that is emptying the search space for model checking.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_modeling_floating_point.html

@@ -92,7 +92,7 @@ <h3><a class="anchor" id="math-library"></a>
 <h3><a class="anchor" id="fixed-point-arithmetic"></a>
 Fixed-point Arithmetic</h3>
 <p>CPROVER also has support for fixed-point types. The <code>--fixedbv</code> flag switches <code>float</code>, <code>double</code>, and <code>long double</code> to fixed-point types. The length of these types is platform specific. The upper half of each type is the integer component and the lower half is the fractional part.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_modeling_mmio.html

@@ -89,7 +89,7 @@ <h3><a class="anchor" id="device-behavior"></a>
 <div class="line">    <span class="keywordflow">return</span> nondet_char();</div>
 <div class="line">}</div>
 </div><!-- fragment --><p>will return the value 2 upon any access at address 0x1000, and return a non-deterministic value in all other cases.</p>
-<p>Last modified: 2024-09-29 16:08:10 -0400 </p>
+<p>Last modified: 2024-10-22 05:58:08 -0700 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->