Smowton/merge/master 20170614

.gitignore

@@ -28,9 +28,16 @@ src/ansi-c/gcc_builtin_headers_alpha.inc
 src/ansi-c/gcc_builtin_headers_arm.inc
 src/ansi-c/gcc_builtin_headers_generic.inc
 src/ansi-c/gcc_builtin_headers_ia32-2.inc
+src/ansi-c/gcc_builtin_headers_ia32-3.inc
+src/ansi-c/gcc_builtin_headers_ia32-4.inc
 src/ansi-c/gcc_builtin_headers_ia32.inc
+src/ansi-c/gcc_builtin_headers_math.inc
+src/ansi-c/gcc_builtin_headers_mem_string.inc
+src/ansi-c/gcc_builtin_headers_omp.inc
+src/ansi-c/gcc_builtin_headers_tm.inc
 src/ansi-c/gcc_builtin_headers_mips.inc
 src/ansi-c/gcc_builtin_headers_power.inc
+src/ansi-c/gcc_builtin_headers_ubsan.inc
 
 # regression/test files
 *.out
@@ -68,6 +75,10 @@ src/xmllang/xml_lex.yy.cpp
 src/xmllang/xml_y.output
 src/xmllang/xml_y.tab.cpp
 src/xmllang/xml_y.tab.h
+src/memory-models/mm_lex.yy.cpp
+src/memory-models/mm_y.output
+src/memory-models/mm_y.tab.cpp
+src/memory-models/mm_y.tab.h
 
 # binaries
 src/cbmc/cbmc
@@ -99,3 +110,5 @@ src/ansi-c/library/converter
 src/ansi-c/library/converter.exe
 src/util/irep_ids_convert
 src/util/irep_ids_convert.exe
+
+*.pyc

CHANGELOG

@@ -7,6 +7,7 @@
 * GOTO-INSTRUMENT: New option --print-path-lenghts
 * GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
 * GOTO-INSTRUMENT: New option --undefined-function-is-assume-false
+* GOTO-INSTRUMENT: New option --remove-function-body
 
 
 5.7

CODING_STANDARD

@@ -158,6 +158,9 @@ C++ features:
 - Use the auto keyword if and only if one of the following
   - The type is explictly repeated on the RHS (e.g. a constructor call)
   - Adding the type will increase confusion (e.g. iterators, function pointers)
+- Avoid assert, if the condition is an actual invariant, use INVARIANT,
+  PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT.
+  If there are possible reasons why it might fail, throw an exception.
 
 Architecture-specific code:
 - Avoid if possible.

COMPILING

@@ -32,7 +32,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    The GNU Make needs to be version 3.81 or higher.
    On Debian-like distributions, do
 
-   apt-get install g++-6 gcc flex bison make git libwww-perl patch
+   apt-get install g++ gcc flex bison make git libwww-perl patch
 
    On Red Hat/Fedora or derivates, do
 
@@ -44,13 +44,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
    git clone https://github.com/diffblue/cbmc cbmc-git
 
-2) On Debian, do
-
-   cd cbmc-git/src
-   make minisat2-download
-   make CXX=g++-6
-
-   On Ubuntu, or other distributions with recent g++, do
+2) On Debian or Ubuntu, do
 
    cd cbmc-git/src
    make minisat2-download

appveyor.yml

@@ -75,6 +75,10 @@ test_script:
     cat goto-instrument-typedef/chain.sh || true
 
     rem HACK disable failing tests
+    rmdir /s /q ansi-c\arch_flags_mcpu_bad
+    rmdir /s /q ansi-c\arch_flags_mcpu_good
+    rmdir /s /q ansi-c\arch_flags_mthumb_bad
+    rmdir /s /q ansi-c\arch_flags_mthumb_good
     rmdir /s /q ansi-c\Forward_Declaration2
     rmdir /s /q ansi-c\Incomplete_Type1
     rmdir /s /q ansi-c\Union_Padding1

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

@@ -1,8 +1,8 @@
 <!--#include virtual="header.inc" -->
 
 <link rel="stylesheet" href="highlight/styles/default.css">
-<script src="highlight/highlight.pack.js"></script>
-<script>hljs.initHighlightingOnLoad();</script>
+<script src="highlight/highlight.pack.js" type="text/javascript"></script>
+<script type="text/javascript">hljs.initHighlightingOnLoad();</script>
 
 <p><a href="./">CPROVER Manual TOC</a></p>
 
@@ -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

@@ -1,8 +1,8 @@
 <!--#include virtual="header.inc" -->
 
 <link rel="stylesheet" href="highlight/styles/default.css">
-<script src="highlight/highlight.pack.js"></script>
-<script>hljs.initHighlightingOnLoad();</script>
+<script src="highlight/highlight.pack.js" type="text/javascript"></script>
+<script type="text/javascript">hljs.initHighlightingOnLoad();</script>
 
 <p><a href="./">CPROVER Manual TOC</a></p>
 
@@ -29,7 +29,7 @@ the program.
 <p class="justified">
 As an example, consider the following simple program, named
 <a href="file1.c">file1.c</a>:
-<p/>
+</p>
 
 <pre><code class="c">int puts(const char *s) { }
 
@@ -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,10 +366,9 @@ 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
+We also have a <a href="http://www.cprover.org/cbmc/applications/">list of
 interesting applications of CBMC</a>.</p>
 
 </div>

doc/html-manual/cover.shtml

@@ -1,8 +1,8 @@
 <!--#include virtual="header.inc" -->
 
 <link rel="stylesheet" href="highlight/styles/default.css">
-<script src="highlight/highlight.pack.js"></script>
-<script>hljs.initHighlightingOnLoad();</script>
+<script src="highlight/highlight.pack.js" type="text/javascript"></script>
+<script type="text/javascript">hljs.initHighlightingOnLoad();</script>
 
 <p><a href="./">CPROVER Manual TOC</a></p>
 
@@ -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

@@ -1,8 +1,8 @@
 <!--#include virtual="header.inc" -->
 
 <link rel="stylesheet" href="highlight/styles/default.css">
-<script src="highlight/highlight.pack.js"></script>
-<script>hljs.initHighlightingOnLoad();</script>
+<script src="highlight/highlight.pack.js" type="text/javascript"></script>
+<script type="text/javascript">hljs.initHighlightingOnLoad();</script>
 
 <p><a href="./">CPROVER Manual TOC</a></p>
 
@@ -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>