various HTML fixes for the manual

Author: Daniel Kroening

doc/html-manual/api.shtml

@@ -299,17 +299,17 @@ extern unsigned char __CPROVER_memory[];
 This array models the contents of integer-addressed memory.
 </p>
 
-<h4>__CPROVER::unsignedbv<N> (C++ only)</h4>
+<h4>__CPROVER::unsignedbv&lt;N&gt; (C++ only)</h4>
 
 <p class="justified">This type is the equivalent of <b>unsigned __CPROVER_bitvector[N]</b> in the C++ front-end.
 </p>
 
-<h4>__CPROVER::signedbv<N> (C++ only)</h4>
+<h4>__CPROVER::signedbv&lt;N&gt; (C++ only)</h4>
 
 <p class="justified">This type is the equivalent of <b>signed __CPROVER_bitvector[N]</b> in the C++ front-end.
 </p>
 
-<h4>__CPROVER::fixedbv<N> (C++ only)</h4>
+<h4>__CPROVER::fixedbv&lt;N&gt; (C++ only)</h4>
 
 <p class="justified">This type is the equivalent of <b>__CPROVER_fixedbv[N,m]</b> in the C++ front-end.
 </p>

doc/html-manual/architecture.shtml

@@ -76,18 +76,18 @@ more subtle. Try the following program with <code>--big-endian</code>
 and <code>--little-endian</code>:</p>
 
 <hr>
-<code>
+<pre><code>
 #include &lt;stdio.h&gt;<br>
 #include &lt;assert.h&gt;<br>
 <br>
 int main() {<br>
 &nbsp;&nbsp;int i=0x01020304;<br>
-&nbsp;&nbsp;char *p=(char *)&i;<br>
+&nbsp;&nbsp;char *p=(char *)&amp;i;<br>
 &nbsp;&nbsp;printf("Bytes of i: %d, %d, %d, %d\n",<br>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;p[0], p[1], p[2], p[3]);<br>
 &nbsp;&nbsp;assert(0);<br>
 }
-</code>
+</code></pre>
 <hr>
 
 <!--#include virtual="footer.inc" -->

doc/html-manual/cbmc-loops.shtml

@@ -161,7 +161,7 @@ following loop-free program:
           <font color="#3030f0">BODY CODE COPY 4</font>
           if(cond) {
             <font color="#3030f0">BODY CODE COPY 5</font>
-            <font color=#ff3030">assert(!cond);</font>
+            <font color="#ff3030">assert(!cond);</font>
           }
         }
       }

doc/html-manual/cbmc.shtml

@@ -356,7 +356,6 @@ representation.
 <div class="box1">
 <div class="caption">Further Reading</div>
 
-<p>
 <ul>
 <li><a href="cbmc-loops.shtml">Understanding Loop Unwinding</a></li>
 <li><a target=_top href="http://www-2.cs.cmu.edu/~svc/papers/view-publications-ck03.html">
@@ -367,7 +366,6 @@ representation.
 <li><a target=_top href="http://www-2.cs.cmu.edu/~svc/papers/view-publications-ckl2004.html">A
     Tool for Checking ANSI-C Programs</a></li>
 </ul>
-</p>
 
 <p class="justified">
 We also have a <a href="http://www.cprover.org/cbmc/applications.shtml">list of

doc/html-manual/cover.shtml

@@ -215,7 +215,6 @@ Test 5.
   (iteration 5) desired_climb=-1.000000f, estimator_z_dot=1.000000f
   (iteration 6) desired_climb=-1.000000f, estimator_z_dot=1.000000f
 </code></pre>
-</p>
 
 <p class="justified">
 The option <code>--unwind 6</code> unwinds the loop inside the main

doc/html-manual/cprover-source.shtml

@@ -114,8 +114,8 @@ The excerpt below gives some details of the class <i>irept</i>:
 <pre><code class="c++">class irept
 {
 public:
-  typedef std::vector<irept> subt;
-  typedef std::map<irep_name_string, irept> named_subt;
+  typedef std::vector&lt;irept&gt; subt;
+  typedef std::map&lt;irep_name_string, irept&gt; named_subt;
   ...
 
 public:
@@ -134,7 +134,7 @@ protected:
   dt *data;
   ...
 };
-</pre></code>
+</code></pre>
 
 <p class="justified">
 Every node of any tree is an object of class <i>irept</i>. Each node has a
@@ -692,20 +692,20 @@ declaration of the interface:
 {
 public:
                                  // Insert the symbol
-  bool add(const symbolt &symb);
+  bool add(const symbolt &amp;symb);
                                  // Insert symb into the
                                  // table and erase it.
                                  // New_symbol points to the
                                  // newly inserted element.
-  bool move(symbolt &symbol, symbolt *&new_symbol);
+  bool move(symbolt &amp;symbol, symbolt *&amp;new_symbol);
 
                                  // Insert symb into the
                                  // table. Then symb is erased.
-  bool move(symbolt &symb);
+  bool move(symbolt &amp;syb);
 
                                  // Return the entry of the
                                  // symbol with given name.
-  const irept &value(const std::string &name) const;
+  const irept &amp;value(const std::string &amp;name) const;
 };
 </code></pre>
 
@@ -815,7 +815,7 @@ public:
   instructionst instructions;
 
   typedef typename 
-    std::map<const_targett, unsigned> target_numberst;
+    std::map&lt;const_targett, unsigned&gt; target_numberst;
 
   //A map containing the unique number of each target
   target_numberst target_numbers;

doc/html-manual/goto-cc-variants.shtml

@@ -12,24 +12,23 @@ The goto-cc utility comes in several variants, summarised in the following table
 
 <center>
 <table cellpadding=5 cellspacing=0>
-<tr bgcolor=#e0e0e0>
+<tr bgcolor="#e0e0e0">
 <th>Executable</th><th>Environment</th><th>Preprocessor</th></tr>
-<tr bgcolor=#e0f0f0><td>goto-cc</td>
+<tr bgcolor="#e0f0f0"><td>goto-cc</td>
   <td><a href="http://gcc.gnu.org/">gcc</a> (control-flow graph only)</td>
   <td>gcc -E</td></tr>
-<tr bgcolor=#f0f0f0><td>goto-gcc</td>
+<tr bgcolor="#f0f0f0"><td>goto-gcc</td>
   <td><a href="http://gcc.gnu.org/">gcc</a> ("hybrid" executable)</td>
   <td>gcc -E</td></tr>
-<tr bgcolor=#e0f0f0><td>goto-armcc</td>
+<tr bgcolor="#e0f0f0"><td>goto-armcc</td>
   <td><a href="http://arm.com/products/tools/software-tools/rvds/index.php">ARM RVDS</a></td>
   <td>armcc -E</td></tr>
-<tr bgcolor=#f0f0f0><td>goto-cl</td>
+<tr bgcolor="#f0f0f0"><td>goto-cl</td>
   <td><a href="http://www.microsoft.com/visualstudio/">Visual Studio</a></td>
   <td>cl /E</td></tr>
-<tr bgcolor=#e0f0f0><td>goto-cw</td>
+<tr bgcolor="#e0f0f0"><td>goto-cw</td>
   <td><a href="http://www.freescale.com/webapp/sps/site/homepage.jsp?code=CW_HOME">Freescale CodeWarrior</a></td>
   <td>mwcceppc</td></tr>
-</tr>
 </table>
 </center>
 

doc/html-manual/hwsw.shtml

@@ -36,7 +36,7 @@ the consistency of the HDL implementation is highly desirable.
 <p class="justified">
 This motivates the verification problem: we want to verify the consistency
 of the HDL implementation, i.e., the product,
-<a href="http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=936243&userType=inst">
+<a href="http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&amp;arnumber=936243&amp;userType=inst">
 using the ANSI-C implementation as a reference</a>. Es&shy;ta&shy;bli&shy;shing the consistency
 does not re&shy;quire a formal specification. However, formal methods to verify
 either the hardware or software design are still desirable.
@@ -90,13 +90,12 @@ methodology allows arbitrary loop constructs.
 tutorial</a> and a description on <a href="hwsw-inputs.shtml">
 how to synchronize inputs between the C model and the Verilog model</a>.
 There is also a collection of <a href="http://www.cprover.org/hardware/sequential-equivalence/">
-benchmark problems</a> available.</a>
+benchmark problems</a> available.
 </p>
 
 <div class="box1">
 <div class="caption">Further Reading</div>
 
-<p>
 <ul>
 <li><a target=_top href="http://www-2.cs.cmu.edu/~svc/papers/view-publications-ck03.html">
     Hardware Verification using ANSI-C Programs as a Reference</a></li>
@@ -111,7 +110,7 @@ href="http://www.kroening.com/publications/view-publications-kc2004.html">Checki
 Consistency of C and Verilog using Predicate Abstraction and Induction</a></li>
 
 </ul>
-</p>
+</div> <!-- box1 -->
 
 <!--#include virtual="footer.inc" -->
 

doc/html-manual/introduction.shtml

@@ -151,13 +151,11 @@ SATABS are described <a href="hwsw.shtml">here</a>.
 
 <div class="box1">
 <div class="caption">Further Reading</div>
-<p>
 <ul>
 <li><a href="cbmc.shtml">Bounded Model Checking with CBMC</a></li>
 <li><a href="satabs.shtml">Predicate Abstraction with SATABS</a></li>
 <li><a href="hwsw.shtml">Hardware/Software Co-Verification</a></li>
 </ul>
-</p>
 </div>
 
 <!--#include virtual="footer.inc" -->

doc/html-manual/properties.shtml

@@ -185,7 +185,6 @@ we can obtain a counterexample trace for the NULL-pointer dereference:
 checks:
 </p>
 
-<p>
 <table>
 <tr><td><code>--no-assertions</code></td>           <td>ignore user assertions</td>
 <tr><td><code>--bounds-check</code></td>            <td>add array bounds checks</td></tr>
@@ -198,15 +197,12 @@ checks:
 <tr><td><code>--uninitialized-check</code></td>     <td>add checks for uninitialized locals (experimental)</td></tr>
 <tr><td><code>--error-label <i>label</i></code></td><td>check that given label is unreachable</td></tr>
 </table>
-</p>
 
 <div class="box1">
 <div class="caption">Further Reading</div>
-<p>
 <ul>
-<li><a href="goto-cc.shtml">Integration into Build Systems with goto-cc</li>
+<li><a href="goto-cc.shtml">Integration into Build Systems with goto-cc</a></li>
 </ul>
-</p>
 </div>
 
 <!--#include virtual="footer.inc" -->

doc/html-manual/satabs-aeon.shtml

@@ -181,7 +181,7 @@ same function:</p>
 Claim getConfig.7:<br>
 &nbsp;&nbsp;file lib_aeon.c line 19 function getConfig<br>
 &nbsp;&nbsp;dereference failure: array `home' upper bound<br>
-&nbsp;&nbsp;!(POINTER_OFFSET(dst) + (int)i >= 512) || !(SAME-OBJECT(dst, &home[0]))<br>
+&nbsp;&nbsp;!(POINTER_OFFSET(dst) + (int)i >= 512) || !(SAME-OBJECT(dst, &amp;home[0]))<br>
 </code></p>
 
 <p class="justified">
@@ -258,7 +258,7 @@ overflow:
 Violated property:<br>
 &nbsp;&nbsp;file stubs.c line 8 column 10 function c::strcpy<br>
 &nbsp;&nbsp;dereference failure: array `home' upper bound<br>
-&nbsp;&nbsp;!(dest == \&home[0]) $\vert\vert$ !(i $>$= 512)}
+&nbsp;&nbsp;!(dest == &amp;home[0]) $\vert\vert$ !(i $>$= 512)}
 </code>
 -->
 

doc/html-manual/satabs.shtml

@@ -165,8 +165,6 @@ validity of the properties if SATABS did not run to completion!
 
 <div class="box1">
 <div class="caption">Further Reading</div>
-
-<p>
 <ul>
 <li><a href="http://www.kroening.com/publications/view-publications-wbwk2007.html">
 Model Checking Concurrent Linux Device Drivers</a></li>
@@ -175,6 +173,6 @@ Model Checking Concurrent Linux Device Drivers</a></li>
 <li><a href="http://www-2.cs.cmu.edu/~svc/papers/view-publications-cksy2004.html">
     Predicate Abstraction of ANSI-C Programs using SAT</a></li>
 </ul>
-</p>
+</div>
 
 <!--#include virtual="footer.inc" -->