Deploying to gh-pages from @ 05ccb75 🚀

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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+</div><!-- fragment --><p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </p>
 </div></div><!-- PageDoc -->
 </div><!-- contents -->
 <!-- start footer part -->

api/piped-process.html

@@ -93,7 +93,7 @@
 </ul>
 </li>
 </ul>
-<p>Last modified: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 </div><!-- doc-content -->

cbmc-architecture.html

@@ -132,7 +132,7 @@ <h3><a class="anchor" id="autotoc_md178"></a>
 <h3><a class="anchor" id="autotoc_md179"></a>
 goto-analyzer</h3>
 <p>To be documented.</p>
-<p>Last modified: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 </div><!-- doc-content -->

central-data-structures.html

@@ -157,7 +157,7 @@ <h2><a class="anchor" id="autotoc_md185"></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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 </div><!-- doc-content -->

classstruct__encodingt.html

@@ -130,7 +130,7 @@
 <tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-methods"></a>
 Private Member Functions</h2></td></tr>
 <tr class="memitem:a88179d5b2392421dfa49da6af7834067"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classexprt.html">exprt</a>&#160;</td><td class="memItemRight" valign="bottom"><a class="el" href="classstruct__encodingt.html#a88179d5b2392421dfa49da6af7834067">encode_member</a> (const <a class="el" href="classmember__exprt.html">member_exprt</a> &amp;member_expr) const</td></tr>
-<tr class="memdesc:a88179d5b2392421dfa49da6af7834067"><td class="mdescLeft">&#160;</td><td class="mdescRight">The member expression selects the value of a field from a struct.  <a href="classstruct__encodingt.html#a88179d5b2392421dfa49da6af7834067">More...</a><br /></td></tr>
+<tr class="memdesc:a88179d5b2392421dfa49da6af7834067"><td class="mdescLeft">&#160;</td><td class="mdescRight">The member expression selects the value of a field from a struct or union.  <a href="classstruct__encodingt.html#a88179d5b2392421dfa49da6af7834067">More...</a><br /></td></tr>
 <tr class="separator:a88179d5b2392421dfa49da6af7834067"><td class="memSeparator" colspan="2">&#160;</td></tr>
 </table><table class="memberdecls">
 <tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-attribs"></a>
@@ -247,7 +247,7 @@ <h2 class="memtitle"><span class="permalink"><a href="#a7a60cb1f47f247dafe049135
 
 <p>Reconstructs a struct expression of the <code>original_type</code> using the data from the bit vector <code>encoded</code> expression. </p>
 
-<p class="definition">Definition at line <a class="el" href="struct__encoding_8cpp_source.html#l00237">237</a> of file <a class="el" href="struct__encoding_8cpp_source.html">struct_encoding.cpp</a>.</p>
+<p class="definition">Definition at line <a class="el" href="struct__encoding_8cpp_source.html#l00244">244</a> of file <a class="el" href="struct__encoding_8cpp_source.html">struct_encoding.cpp</a>.</p>
 
 </div>
 </div>
@@ -267,7 +267,7 @@ <h2 class="memtitle"><span class="permalink"><a href="#a95c06cf3804956acc32eab0a
       </table>
 </div><div class="memdoc">
 
-<p class="definition">Definition at line <a class="el" href="struct__encoding_8cpp_source.html#l00199">199</a> of file <a class="el" href="struct__encoding_8cpp_source.html">struct_encoding.cpp</a>.</p>
+<p class="definition">Definition at line <a class="el" href="struct__encoding_8cpp_source.html#l00206">206</a> of file <a class="el" href="struct__encoding_8cpp_source.html">struct_encoding.cpp</a>.</p>
 
 </div>
 </div>
@@ -315,10 +315,10 @@ <h2 class="memtitle"><span class="permalink"><a href="#a88179d5b2392421dfa49da6a
 </table>
 </div><div class="memdoc">
 
-<p>The member expression selects the value of a field from a struct. </p>
-<p>The struct is encoded as a single bitvector where the first field is stored in the highest bits. The second field is stored in the next highest set of bits and so on. As offsets are indexed from the lowest bit, any field can be selected by extracting the range of bits starting from an offset based on the combined width of the fields which follow the field being selected. </p>
+<p>The member expression selects the value of a field from a struct or union. </p>
+<p>Both structs and unions are encoded into a single large bit vector. The fields of a union are encoded into the lowest bits, with padding in the highest bits if needed. Structs are encoded as a single bitvector where the first field is stored in the highest bits. The second field is stored in the next highest set of bits and so on. As offsets are indexed from the lowest bit, any field can be selected by extracting the range of bits starting from an offset based on the combined width of the fields which follow the field being selected. </p>
 
-<p class="definition">Definition at line <a class="el" href="struct__encoding_8cpp_source.html#l00185">185</a> of file <a class="el" href="struct__encoding_8cpp_source.html">struct_encoding.cpp</a>.</p>
+<p class="definition">Definition at line <a class="el" href="struct__encoding_8cpp_source.html#l00188">188</a> of file <a class="el" href="struct__encoding_8cpp_source.html">struct_encoding.cpp</a>.</p>
 
 </div>
 </div>

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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+</div><!-- fragment --><p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->

cprover-manual/md_goto_cc.html

@@ -160,7 +160,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: 2023-10-12 21:13:08 +0200 </p>
+</div><!-- fragment --><p>Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+</pre><p> Last modified: 2023-10-16 10:18:17 +0100 </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: 2023-10-12 21:13:08 +0200 </p>
+<p>Last modified: 2023-10-16 10:18:17 +0100 </p>
 </div></div><!-- contents -->
 </div><!-- PageDoc -->
 <!-- start footer part -->