From 60e2e0e0ebc6fd9c16b902995aaa0583557536bb Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Thu, 10 Nov 2016 12:30:00 +0000 Subject: [PATCH 01/58] adjusted the command line for the pid controller case study with a better look output test suites --- doc/html-manual/cover.shtml | 16 +- doc/html-manual/pid_test_suites.xml | 500 ++++++++++++++++++++++++++++ 2 files changed, 510 insertions(+), 6 deletions(-) create mode 100644 doc/html-manual/pid_test_suites.xml diff --git a/doc/html-manual/cover.shtml b/doc/html-manual/cover.shtml index 45a3fb82143..5e3bfaffad8 100644 --- a/doc/html-manual/cover.shtml +++ b/doc/html-manual/cover.shtml @@ -149,7 +149,7 @@ To demonstrate the automatic test suite generation in CBMC, we call the following command and we are going to explain the command line options one by one.

-
cbmc pid.c --cover mcdc --unwind 6 --trace --xml-ui
+
cbmc pid.c --cover mcdc --unwind 6 --xml-ui
 

 
 

@@ -173,11 +173,11 @@ pprz >= (float)0 && pprz <= (float)(16 * 600)     id="climb_pid_run.coverage.3"
 
 

 The "id" of each coverage goal is automatically assigned by CBMC.  For every
-coverage goal, a trace (if there exists) of the program execution that
-satisfies such a goal is printed out in XML format, as the parameters
---trace --xml-ui are given.  Multiple coverage goals can share a
-trace, when the corresponding execution of the program satisfies all these
-goals at the same time.  Each trace corresponds to a test case. 
+coverage goal, a test suite (if there exists) that 
+satisfies such a goal is printed out in XML format, as the parameter
+--xml-ui is given.  Multiple coverage goals can share a
+test suite, when the corresponding execution of the program satisfies all these
+goals at the same time.  
 

 
 

@@ -185,6 +185,10 @@ In the end, the following test suites are automatically generated for testing th
 A test suite consists of a sequence of input parameters that are
 passed to the PID function climb_pid_run at each loop iteration. 
 For example, Test 1 covers the MC/DC goal with id="climb_pid_run.coverage.1".
+The complete output from CBMC is in
+pid_test_suites.xml, where every test suite and the coverage goals it is for
+are clearly described.
+
 
Test suite:
 Test 1. 
   (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
diff --git a/doc/html-manual/pid_test_suites.xml b/doc/html-manual/pid_test_suites.xml
new file mode 100644
index 00000000000..014fea12294
--- /dev/null
+++ b/doc/html-manual/pid_test_suites.xml
@@ -0,0 +1,500 @@
+
+
+CBMC 5.5
+
+  CBMC version 5.5 64-bit x86_64 macos
+
+
+
+  Parsing pid.c
+
+
+
+  Converting
+
+
+
+  Type-checking pid
+
+
+
+  
+  function `nondet_float' is not declared
+
+
+
+  Generating GOTO Program
+
+
+
+  Adding CPROVER library (x86_64)
+
+
+
+  Removal of function pointers and virtual functions
+
+
+
+  Partial Inlining
+
+
+
+  Generic Property Instrumentation
+
+
+criterion: mcdc
+
+
+  Instrumenting coverage goals
+
+
+
+  Starting Bounded Model Checking
+
+
+
+  Unwinding loop main.0 iteration 1 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  Unwinding loop main.0 iteration 2 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  Unwinding loop main.0 iteration 3 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  Unwinding loop main.0 iteration 4 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  Unwinding loop main.0 iteration 5 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  Not unwinding loop main.0 iteration 6 (6 max) file pid.c line 56 function main thread 0
+
+
+
+  size of program expression: 416 steps
+
+
+
+  Generated 114 VCC(s), 108 remaining after simplification
+
+
+
+  Passing problem to propositional reduction
+
+
+
+  converting SSA
+
+
+
+  Aiming to cover 19 goal(s)
+
+
+
+  Running propositional reduction
+
+
+
+  Post-processing
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 553801 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered decision/condition `1 != 0' true
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 395675 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered MC/DC independence condition `!(pprz >= (float)0) && pprz <= (float)(16 * 600)'
+
+
+
+  Covered decision `pprz >= (float)0 && pprz <= (float)(16 * 600)' false
+
+
+
+  Covered condition `pprz >= (float)0' false
+
+
+
+  Covered decision/condition `pprz > (float)(16 * 600)' false
+
+
+
+  Covered condition `pprz <= (float)(16 * 600)' true
+
+
+
+  Covered decision/condition `desired_climb > (float)0' false
+
+
+
+  Covered decision/condition `climb_sum_err > (float)10' false
+
+
+
+  Covered decision/condition `climb_sum_err < (float)-10' false
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 393279 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered MC/DC independence condition `pprz >= (float)0 && !(pprz <= (float)(16 * 600))'
+
+
+
+  Covered condition `pprz >= (float)0' true
+
+
+
+  Covered decision/condition `pprz > (float)(16 * 600)' true
+
+
+
+  Covered condition `pprz <= (float)(16 * 600)' false
+
+
+
+  Covered decision/condition `desired_climb > (float)0' true
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 391285 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered MC/DC independence condition `pprz >= (float)0 && pprz <= (float)(16 * 600)'
+
+
+
+  Covered decision `pprz >= (float)0 && pprz <= (float)(16 * 600)' true
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 390122 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered decision/condition `climb_sum_err < (float)-10' true
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 390121 clauses
+
+
+
+  SAT checker: instance is SATISFIABLE
+
+
+
+  Covered decision/condition `climb_sum_err > (float)10' true
+
+
+
+  Solving with MiniSAT 2.2.1 with simplifier
+
+
+
+  131818 variables, 387493 clauses
+
+
+
+  SAT checker inconsistent: instance is UNSATISFIABLE
+
+
+
+  Runtime decision procedure: 3.806s
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+
+
+
+  
+  
+
+
+
+  
+    
+      -1.000000
+    
+    
+      1.000000
+    
+  
+  
+  
+  
+  
+  
+  
+  
+  
+
+
+
+  
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+  
+  
+  
+  
+  
+  
+
+
+
+  
+    
+      0.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+  
+  
+  
+
+
+
+  
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      0.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+  
+  
+
+
+
+  
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+    
+      -1.000000
+    
+    
+      1.000000
+    
+  
+  
+
+
+
+  ** 18 of 19 covered (94.7%)
+
+
+
+  ** Used 7 iterations
+
+
+

From fbdf29a9420eae70ff7c66dc3462d61e21e2c6b9 Mon Sep 17 00:00:00 2001
From: reuk 
Date: Thu, 16 Mar 2017 13:48:29 +0000
Subject: [PATCH 02/58] Remove DEBUG ifdefs which broke the debug build

---
 .travis.yml                                   |  2 ++
 src/analyses/constant_propagator.cpp          |  2 --
 src/analyses/natural_loops.cpp                |  2 --
 src/analyses/natural_loops.h                  |  6 ----
 src/cpp/parse.cpp                             | 29 -------------------
 src/goto-instrument/accelerate/accelerate.cpp |  2 --
 .../accelerate/acceleration_utils.cpp         |  2 --
 .../accelerate/all_paths_enumerator.cpp       |  2 --
 .../accelerate/cone_of_influence.cpp          |  2 --
 .../disjunctive_polynomial_acceleration.cpp   |  3 --
 .../enumerating_loop_acceleration.cpp         |  2 --
 .../accelerate/overflow_instrumenter.cpp      |  2 --
 .../accelerate/polynomial_accelerator.cpp     |  3 --
 .../accelerate/sat_path_enumerator.cpp        |  2 --
 .../accelerate/scratch_program.cpp            | 11 -------
 .../accelerate/trace_automaton.cpp            | 16 ----------
 src/goto-programs/goto_inline_class.cpp       |  2 --
 src/linking/linking.cpp                       | 10 -------
 src/path-symex/path_symex.cpp                 |  2 --
 src/path-symex/path_symex_state.cpp           |  2 --
 src/path-symex/path_symex_state_read.cpp      |  2 --
 src/path-symex/var_map.cpp                    |  2 --
 src/pointer-analysis/dereference.cpp          |  2 --
 .../value_set_dereference.cpp                 |  2 --
 src/solvers/flattening/arrays.cpp             |  2 --
 src/solvers/flattening/boolbv.cpp             |  9 ------
 src/solvers/flattening/boolbv_get.cpp         |  2 --
 src/solvers/flattening/boolbv_map.cpp         |  2 --
 src/solvers/flattening/equality.cpp           |  7 -----
 src/solvers/flattening/functions.cpp          |  2 --
 src/solvers/prop/prop_conv.cpp                |  2 --
 src/solvers/sat/satcheck_limmat.cpp           |  2 --
 src/solvers/sat/satcheck_zchaff.cpp           |  2 --
 33 files changed, 2 insertions(+), 140 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index d74ec93f7e3..3fc29224575 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -68,6 +68,8 @@ matrix:
 
 script:
   - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
+    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O0 -ggdb3 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DDEBUG\" -j2" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
     COMMAND="make -C src minisat2-download" &&
     eval ${PRE_COMMAND} ${COMMAND} &&
     COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare\" -j2" &&
diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 1fe89a7b8f6..189048994b8 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -6,8 +6,6 @@ Author: Peter Schrammel
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp
index 16985daa5e9..593fc78006d 100644
--- a/src/analyses/natural_loops.cpp
+++ b/src/analyses/natural_loops.cpp
@@ -10,8 +10,6 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
 
 #include "natural_loops.h"
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: show_natural_loops
diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h
index 327ebbdf112..3408aba68db 100644
--- a/src/analyses/natural_loops.h
+++ b/src/analyses/natural_loops.h
@@ -81,8 +81,6 @@ Function: natural_loops_templatet::compute
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
@@ -92,10 +90,6 @@ void natural_loops_templatet::compute(P &program)
 {
   cfg_dominators(program);
 
-#ifdef DEBUG
-  cfg_dominators.output(std::cout);
-#endif
-
   // find back-edges m->n
   for(T m_it=program.instructions.begin();
       m_it!=program.instructions.end();
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index 5a7d2095a58..b15b486c248 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -21,8 +21,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_member_spec.h"
 #include "cpp_enum_type.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 
@@ -639,12 +637,6 @@ bool Parser::rDefinition(cpp_itemt &item)
 {
   int t=lex.LookAhead(0);
 
-  #ifdef DEBUG
-  indenter _i;
-  std::cout << std::string(__indent, ' ') << "Parser::rDefinition 1 " << t
-            << "\n";
-  #endif
-
   if(t==';')
     return rNullDeclaration(item.make_declaration());
   else if(t==TOK_TYPEDEF)
@@ -1237,12 +1229,6 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl)
   switch(kind)
   {
   case tdk_decl:
-    #ifdef DEBUG
-    std::cout << std::string(__indent, ' ') << "BODY: " << body << std::endl;
-    std::cout << std::string(__indent, ' ') << "TEMPLATE_TYPE: "
-              << template_type << std::endl;
-    #endif
-
     body.add(ID_template_type).swap(template_type);
     body.set(ID_is_template, true);
     decl.swap(body);
@@ -1909,12 +1895,6 @@ bool Parser::rIntegralDeclaration(
 
     if(lex.LookAhead(0)==';')
     {
-      #ifdef DEBUG
-      std::cout << std::string(__indent, ' ')
-                << "Parser::rIntegralDeclaration 8 "
-                << declaration << "\n";
-      #endif
-
       lex.get_token(tk);
       return true;
     }
@@ -5119,11 +5099,6 @@ bool Parser::rClassBody(exprt &body)
       return true;        // error recovery
     }
 
-    #ifdef DEBUG
-    std::cout << std::string(__indent, ' ') << "Parser::rClassBody " << member
-              << std::endl;
-    #endif
-
     members.move_to_operands(
       static_cast(static_cast(member)));
   }
@@ -9244,10 +9219,6 @@ bool Parser::rExprStatement(codet &statement)
 
     if(rDeclarationStatement(statement))
     {
-      #ifdef DEBUG
-      std::cout << std::string(__indent, ' ') << "rDe: " << statement
-                << std::endl;
-      #endif
       return true;
     }
     else
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 93d0ca0dfd7..bb86d5a4d75 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -27,8 +27,6 @@ Author: Matt Lewis
 #include "overflow_instrumenter.h"
 #include "util.h"
 
-#define DEBUG
-
 goto_programt::targett acceleratet::find_back_jump(
   goto_programt::targett loop_header)
 {
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index d90357d2246..1d42ebf1945 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -42,8 +42,6 @@ Author: Matt Lewis
 #include "cone_of_influence.h"
 #include "overflow_instrumenter.h"
 
-#define DEBUG
-
 void acceleration_utilst::gather_rvalues(
   const exprt &expr,
   expr_sett &rvalues)
diff --git a/src/goto-instrument/accelerate/all_paths_enumerator.cpp b/src/goto-instrument/accelerate/all_paths_enumerator.cpp
index cfc1c3ae2ed..8b1038d426d 100644
--- a/src/goto-instrument/accelerate/all_paths_enumerator.cpp
+++ b/src/goto-instrument/accelerate/all_paths_enumerator.cpp
@@ -10,8 +10,6 @@ Author: Matt Lewis
 
 #include "all_paths_enumerator.h"
 
-// #define DEBUG
-
 bool all_paths_enumeratort::next(patht &path)
 {
   if(last_path.empty())
diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-instrument/accelerate/cone_of_influence.cpp
index a1914756698..0f0b969e342 100644
--- a/src/goto-instrument/accelerate/cone_of_influence.cpp
+++ b/src/goto-instrument/accelerate/cone_of_influence.cpp
@@ -12,8 +12,6 @@ Author: Matt Lewis
 
 #include "cone_of_influence.h"
 
-// #define DEBUG
-
 void cone_of_influencet::cone_of_influence(
   const expr_sett &targets,
   expr_sett &cone)
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index 6f91824a8e7..29d5ac0f81b 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -43,9 +43,6 @@ Author: Matt Lewis
 #include "cone_of_influence.h"
 #include "overflow_instrumenter.h"
 
-#define DEBUG
-
-
 bool disjunctive_polynomial_accelerationt::accelerate(
   path_acceleratort &accelerator)
 {
diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp
index 1590eb6c127..d47c0c6287a 100644
--- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp
+++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.cpp
@@ -10,8 +10,6 @@ Author: Matt Lewis
 
 #include "enumerating_loop_acceleration.h"
 
-// #define DEBUG
-
 bool enumerating_loop_accelerationt::accelerate(
   path_acceleratort &accelerator)
 {
diff --git a/src/goto-instrument/accelerate/overflow_instrumenter.cpp b/src/goto-instrument/accelerate/overflow_instrumenter.cpp
index 2bad8d1283b..6e126aeb581 100644
--- a/src/goto-instrument/accelerate/overflow_instrumenter.cpp
+++ b/src/goto-instrument/accelerate/overflow_instrumenter.cpp
@@ -18,8 +18,6 @@ Author: Matt Lewis
 #include "overflow_instrumenter.h"
 #include "util.h"
 
-// #define DEBUG
-
 /*
  * This code is copied wholesale from analyses/goto_check.cpp.
  */
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index a9dbb2ff58f..ccf24d6e475 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -39,9 +39,6 @@ Author: Matt Lewis
 #include "cone_of_influence.h"
 #include "overflow_instrumenter.h"
 
-#define DEBUG
-
-
 bool polynomial_acceleratort::accelerate(
   patht &loop,
   path_acceleratort &accelerator)
diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
index 17bc94ecce0..d8067ec3640 100644
--- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp
+++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp
@@ -42,8 +42,6 @@ Author: Matt Lewis
 #include "util.h"
 #include "overflow_instrumenter.h"
 
-#define DEBUG
-
 bool sat_path_enumeratort::next(patht &path)
 {
   scratch_programt program(symbol_table);
diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index f42cad26e0d..9f3ac61584d 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -15,8 +15,6 @@ Author: Matt Lewis
 
 #include "scratch_program.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
@@ -30,11 +28,6 @@ bool scratch_programt::check_sat(bool do_slice)
   remove_skip(*this);
   update();
 
-#ifdef DEBUG
-  std::cout << "Checking following program for satness:" << endl;
-  output(ns, "scratch", cout);
-#endif
-
   symex.constant_propagation=constant_propagation;
   goto_symex_statet::propagationt::valuest constants;
 
@@ -56,10 +49,6 @@ bool scratch_programt::check_sat(bool do_slice)
 
   equation.convert(*checker);
 
-#ifdef DEBUG
-  cout << "Finished symex, invoking decision procedure." << endl;
-#endif
-
   return (checker->dec_solve()==decision_proceduret::D_SATISFIABLE);
 }
 
diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp
index 228048552e8..9cd8bef2247 100644
--- a/src/goto-instrument/accelerate/trace_automaton.cpp
+++ b/src/goto-instrument/accelerate/trace_automaton.cpp
@@ -12,8 +12,6 @@ Author: Matt Lewis
 #include "trace_automaton.h"
 #include "path.h"
 
-// #define DEBUG
-
 void trace_automatont::build()
 {
 #ifdef DEBUG
@@ -76,9 +74,6 @@ void trace_automatont::add_path(patht &path)
   for(const auto &step : path)
   {
     goto_programt::targett l=step.loc;
-#ifdef DEBUG
-      std::cout << ", " << l->location_number << ":" << l->location;
-#endif
 
     if(in_alphabet(l))
     {
@@ -108,13 +103,6 @@ void trace_automatont::add_path(patht &path)
  */
 void trace_automatont::determinise()
 {
-#ifdef DEBUG
-  std::cout << "Determinising automaton with " << nta.num_states
-            << " states and " << nta.accept_states.size()
-            << " accept states and " << nta.count_transitions()
-            << " transitions" << endl;
-#endif
-
   dstates.clear();
   unmarked_dstates.clear();
   dta.clear();
@@ -123,10 +111,6 @@ void trace_automatont::determinise()
   init_states.insert(nta.init_state);
   epsilon_closure(init_states);
 
-#ifdef DEBUG
-  std::cout << "There are " << init_states.size() << " init states" << endl;
-#endif
-
   dta.init_state=add_dstate(init_states);
 
   while(!unmarked_dstates.empty())
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
index 5afb49f7ae3..d4db1576817 100644
--- a/src/goto-programs/goto_inline_class.cpp
+++ b/src/goto-programs/goto_inline_class.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index b66c0591b4b..927e78aba7b 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -936,11 +936,6 @@ bool linkingt::adjust_object_type_rec(
   else if(t1.id()!=t2.id())
   {
     // type classes do not match and can't be fixed
-    #ifdef DEBUG
-    str << "LINKING: cannot join " << t1.id() << " vs. " << t2.id();
-    debug_msg();
-    #endif
-
     return true;
   }
 
@@ -1041,11 +1036,6 @@ bool linkingt::adjust_object_type(
   const symbolt &new_symbol,
   bool &set_to_new)
 {
-  #ifdef DEBUG
-  str << "LINKING: trying to adjust types of " << old_symbol.name;
-  debug_msg();
-  #endif
-
   const typet &old_type=follow_tags_symbols(ns, old_symbol.type);
   const typet &new_type=follow_tags_symbols(ns, new_symbol.type);
 
diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp
index d8c5e0ea3de..eb58b330ab6 100644
--- a/src/path-symex/path_symex.cpp
+++ b/src/path-symex/path_symex.cpp
@@ -22,8 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "path_symex.h"
 #include "path_symex_class.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp
index 2ce47fedc0f..3dfc319d6d6 100644
--- a/src/path-symex/path_symex_state.cpp
+++ b/src/path-symex/path_symex_state.cpp
@@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "path_symex_state.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #include 
diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp
index df3621ee290..3aea2c24983 100644
--- a/src/path-symex/path_symex_state_read.cpp
+++ b/src/path-symex/path_symex_state_read.cpp
@@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "path_symex_state.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #include 
diff --git a/src/path-symex/var_map.cpp b/src/path-symex/var_map.cpp
index 8f18b3f9726..d981cf1cca9 100644
--- a/src/path-symex/var_map.cpp
+++ b/src/path-symex/var_map.cpp
@@ -14,8 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "var_map.h"
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: var_mapt::var_infot::operator()
diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp
index b21313f85bf..507830063c8 100644
--- a/src/pointer-analysis/dereference.cpp
+++ b/src/pointer-analysis/dereference.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #include 
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 98e6ab2cb2a..04598ac67fa 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index 9c710fc3737..9f72a8e3475 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #include 
 #include 
 
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index f5e9aad9f8b..aaa63e69fd2 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -27,8 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "../floatbv/float_utils.h"
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: boolbvt::literal
@@ -144,9 +142,6 @@ const bvt &boolbvt::convert_bv(const exprt &expr)
     bv_cache.insert(std::make_pair(expr, bvt()));
   if(!cache_result.second)
   {
-    #ifdef DEBUG
-    std::cout << "Cache hit on " << expr << "\n";
-    #endif
     return cache_result.first->second;
   }
 
@@ -205,10 +200,6 @@ Function: boolbvt::convert_bitvector
 
 bvt boolbvt::convert_bitvector(const exprt &expr)
 {
-  #ifdef DEBUG
-  std::cout << "BV: " << expr.pretty() << std::endl;
-  #endif
-
   if(expr.type().id()==ID_bool)
   {
     bvt bv;
diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp
index 3e74ec872c1..943ef98b19c 100644
--- a/src/solvers/flattening/boolbv_get.cpp
+++ b/src/solvers/flattening/boolbv_get.cpp
@@ -17,8 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv.h"
 #include "boolbv_type.h"
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: boolbvt::get
diff --git a/src/solvers/flattening/boolbv_map.cpp b/src/solvers/flattening/boolbv_map.cpp
index dbbb097e7b2..6c6e647a31c 100644
--- a/src/solvers/flattening/boolbv_map.cpp
+++ b/src/solvers/flattening/boolbv_map.cpp
@@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv_map.h"
 #include "boolbv_width.h"
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
diff --git a/src/solvers/flattening/equality.cpp b/src/solvers/flattening/equality.cpp
index 208a4510a35..63ca7e2e147 100644
--- a/src/solvers/flattening/equality.cpp
+++ b/src/solvers/flattening/equality.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #ifdef DEBUG
 #include 
 #endif
@@ -110,11 +108,6 @@ literalt equalityt::equality2(const exprt &e1, const exprt &e2)
       l=result->second;
   }
 
-  #ifdef DEBUG
-  std::cout << "EQUALITY " << l << "<=>"
-            << e1 << "=" << e2 << std::endl;
-  #endif
-
   return l;
 }
 
diff --git a/src/solvers/flattening/functions.cpp b/src/solvers/flattening/functions.cpp
index 37380aa323b..6b23229c958 100644
--- a/src/solvers/flattening/functions.cpp
+++ b/src/solvers/flattening/functions.cpp
@@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-// #define DEBUG
-
 #include 
 
 #include 
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index 01ae3fcd841..33a572191c0 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -18,8 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "prop_conv.h"
 #include "literal_expr.h"
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: prop_convt::is_in_conflict
diff --git a/src/solvers/sat/satcheck_limmat.cpp b/src/solvers/sat/satcheck_limmat.cpp
index a1aadbbff39..a8393cf30e8 100644
--- a/src/solvers/sat/satcheck_limmat.cpp
+++ b/src/solvers/sat/satcheck_limmat.cpp
@@ -16,8 +16,6 @@ extern "C"
 #include "limmat.h"
 }
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: satcheck_limmatt::satcheck_limmatt
diff --git a/src/solvers/sat/satcheck_zchaff.cpp b/src/solvers/sat/satcheck_zchaff.cpp
index 5a94615e221..6697d6b3c6c 100644
--- a/src/solvers/sat/satcheck_zchaff.cpp
+++ b/src/solvers/sat/satcheck_zchaff.cpp
@@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include 
 
-// #define DEBUG
-
 /*******************************************************************\
 
 Function: satcheck_zchaff_baset::satcheck_zchaff_baset

From 0314b2450aa38630c7e5b86d27f004af0d52b49c Mon Sep 17 00:00:00 2001
From: Cristina 
Date: Thu, 16 Mar 2017 17:15:35 +0000
Subject: [PATCH 03/58] Remove the disable-runtime-checks flag for Java

This was not visible from the outside and therefore could not be set.
---
 .../java_bytecode_convert_class.cpp           |   6 -
 .../java_bytecode_convert_class.h             |   1 -
 .../java_bytecode_convert_method.cpp          | 122 ++++++++----------
 .../java_bytecode_convert_method.h            |   3 -
 .../java_bytecode_convert_method_class.h      |   3 -
 src/java_bytecode/java_bytecode_language.cpp  |   4 -
 src/java_bytecode/java_bytecode_language.h    |   6 -
 7 files changed, 51 insertions(+), 94 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp
index f21b0bb1ce2..0330794a8e7 100644
--- a/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -27,14 +27,12 @@ class java_bytecode_convert_classt:public messaget
   java_bytecode_convert_classt(
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
-    bool _disable_runtime_checks,
     size_t _max_array_length,
     lazy_methodst& _lazy_methods,
     lazy_methods_modet _lazy_methods_mode,
     bool _string_refinement_enabled):
     messaget(_message_handler),
     symbol_table(_symbol_table),
-    disable_runtime_checks(_disable_runtime_checks),
     max_array_length(_max_array_length),
     lazy_methods(_lazy_methods),
     lazy_methods_mode(_lazy_methods_mode),
@@ -60,7 +58,6 @@ class java_bytecode_convert_classt:public messaget
 
 protected:
   symbol_tablet &symbol_table;
-  const bool disable_runtime_checks;
   const size_t max_array_length;
   lazy_methodst &lazy_methods;
   lazy_methods_modet lazy_methods_mode;
@@ -169,7 +166,6 @@ void java_bytecode_convert_classt::convert(const classt &c)
         method,
         symbol_table,
         get_message_handler(),
-        disable_runtime_checks,
         max_array_length);
     }
     else
@@ -364,7 +360,6 @@ bool java_bytecode_convert_class(
   const java_bytecode_parse_treet &parse_tree,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   lazy_methodst &lazy_methods,
   lazy_methods_modet lazy_methods_mode,
@@ -373,7 +368,6 @@ bool java_bytecode_convert_class(
   java_bytecode_convert_classt java_bytecode_convert_class(
     symbol_table,
     message_handler,
-    disable_runtime_checks,
     max_array_length,
     lazy_methods,
     lazy_methods_mode,
diff --git a/src/java_bytecode/java_bytecode_convert_class.h b/src/java_bytecode/java_bytecode_convert_class.h
index 0d2be3d8202..9ce5cc8c7cc 100644
--- a/src/java_bytecode/java_bytecode_convert_class.h
+++ b/src/java_bytecode/java_bytecode_convert_class.h
@@ -19,7 +19,6 @@ bool java_bytecode_convert_class(
   const java_bytecode_parse_treet &parse_tree,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   lazy_methodst &,
   lazy_methods_modet,
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 0912ec8b22a..e479423ed9b 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1084,20 +1084,17 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       assert(op.size()==1 && results.size()==1);
       code_blockt block;
-      if(!disable_runtime_checks)
-      {
-        // TODO throw NullPointerException instead
-        const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
-        const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
-        const exprt not_equal_null(
-          binary_relation_exprt(lhs, ID_notequal, rhs));
-        code_assertt check(not_equal_null);
-        check.add_source_location()
-          .set_comment("Throw null");
-        check.add_source_location()
-          .set_property_class("null-pointer-exception");
-        block.move_to_operands(check);
-      }
+      // TODO throw NullPointerException instead
+      const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));
+      const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type())));
+      const exprt not_equal_null(
+        binary_relation_exprt(lhs, ID_notequal, rhs));
+      code_assertt check(not_equal_null);
+      check.add_source_location()
+        .set_comment("Throw null");
+      check.add_source_location()
+        .set_property_class("null-pointer-exception");
+      block.move_to_operands(check);
 
       side_effect_expr_throwt throw_expr;
       throw_expr.add_source_location()=i_it->source_location;
@@ -1110,20 +1107,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="checkcast")
     {
-      if(!disable_runtime_checks)
-      {
-        // checkcast throws an exception in case a cast of object
-        // on stack to given type fails.
-        // The stack isn't modified.
-        // TODO: convert assertions to exceptions.
-        assert(op.size()==1 && results.size()==1);
-        binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
-        c=code_assertt(check);
-        c.add_source_location().set_comment("Dynamic cast check");
-        c.add_source_location().set_property_class("bad-dynamic-cast");
-      }
-      else
-        c=code_skipt();
+      // checkcast throws an exception in case a cast of object
+      // on stack to given type fails.
+      // The stack isn't modified.
+      // TODO: convert assertions to exceptions.
+      assert(op.size()==1 && results.size()==1);
+      binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
+      c=code_assertt(check);
+      c.add_source_location().set_comment("Dynamic cast check");
+      c.add_source_location().set_property_class("bad-dynamic-cast");
 
       results[0]=op[0];
     }
@@ -1308,13 +1300,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const dereference_exprt element(data_plus_offset, element_type);
 
       c=code_blockt();
-      if(!disable_runtime_checks)
-      {
-        codet bounds_check=
-          get_array_bounds_check(deref, op[1], i_it->source_location);
-        bounds_check.add_source_location()=i_it->source_location;
-        c.move_to_operands(bounds_check);
-      }
+      codet bounds_check=
+        get_array_bounds_check(deref, op[1], i_it->source_location);
+      bounds_check.add_source_location()=i_it->source_location;
+      c.move_to_operands(bounds_check);
       code_assignt array_put(element, op[2]);
       array_put.add_source_location()=i_it->source_location;
       c.move_to_operands(array_put);
@@ -1354,11 +1343,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       typet element_type=data_ptr.type().subtype();
       dereference_exprt element(data_plus_offset, element_type);
 
-      if(!disable_runtime_checks)
-      {
-        c=get_array_bounds_check(deref, op[1], i_it->source_location);
-        c.add_source_location()=i_it->source_location;
-      }
+      c=get_array_bounds_check(deref, op[1], i_it->source_location);
+      c.add_source_location()=i_it->source_location;
       results[0]=java_bytecode_promotion(element);
     }
     else if(statement==patternt("?load"))
@@ -1899,17 +1885,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
         java_new_array.add_source_location()=i_it->source_location;
 
       c=code_blockt();
-      if(!disable_runtime_checks)
-      {
-        // TODO make this throw NegativeArrayIndexException instead.
-        constant_exprt intzero=from_integer(0, java_int_type());
-        binary_relation_exprt gezero(op[0], ID_ge, intzero);
-        code_assertt check(gezero);
-        check.add_source_location().set_comment("Array size < 0");
-        check.add_source_location()
-          .set_property_class("array-create-negative-size");
-        c.move_to_operands(check);
-      }
+      // TODO make this throw NegativeArrayIndexException instead.
+      constant_exprt intzero=from_integer(0, java_int_type());
+      binary_relation_exprt gezero(op[0], ID_ge, intzero);
+      code_assertt check(gezero);
+      check.add_source_location().set_comment("Array size < 0");
+      check.add_source_location()
+        .set_property_class("array-create-negative-size");
+      c.move_to_operands(check);
+
       if(max_array_length!=0)
       {
         constant_exprt size_limit=
@@ -1941,26 +1925,24 @@ codet java_bytecode_convert_methodt::convert_instructions(
         java_new_array.add_source_location()=i_it->source_location;
 
       code_blockt checkandcreate;
-      if(!disable_runtime_checks)
+      // TODO make this throw NegativeArrayIndexException instead.
+      constant_exprt intzero=from_integer(0, java_int_type());
+      binary_relation_exprt gezero(op[0], ID_ge, intzero);
+      code_assertt check(gezero);
+      check.add_source_location().set_comment("Array size < 0");
+      check.add_source_location()
+        .set_property_class("array-create-negative-size");
+      checkandcreate.move_to_operands(check);
+
+      if(max_array_length!=0)
       {
-        // TODO make this throw NegativeArrayIndexException instead.
-        constant_exprt intzero=from_integer(0, java_int_type());
-        binary_relation_exprt gezero(op[0], ID_ge, intzero);
-        code_assertt check(gezero);
-        check.add_source_location().set_comment("Array size < 0");
-        check.add_source_location()
-          .set_property_class("array-create-negative-size");
-        checkandcreate.move_to_operands(check);
-
-        if(max_array_length!=0)
-        {
-          constant_exprt size_limit=
-            from_integer(max_array_length, java_int_type());
-          binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
-          code_assumet assume_le_max_size(le_max_size);
-          checkandcreate.move_to_operands(assume_le_max_size);
-        }
+        constant_exprt size_limit=
+          from_integer(max_array_length, java_int_type());
+        binary_relation_exprt le_max_size(op[0], ID_le, size_limit);
+        code_assumet assume_le_max_size(le_max_size);
+        checkandcreate.move_to_operands(assume_le_max_size);
       }
+
       const exprt tmp=tmp_variable("newarray", ref_type);
       c=code_assignt(tmp, java_new_array);
       results[0]=tmp;
@@ -2428,7 +2410,6 @@ void java_bytecode_convert_method(
   const java_bytecode_parse_treet::methodt &method,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   safe_pointer > needed_methods,
   safe_pointer > needed_classes)
@@ -2436,7 +2417,6 @@ void java_bytecode_convert_method(
   java_bytecode_convert_methodt java_bytecode_convert_method(
     symbol_table,
     message_handler,
-    disable_runtime_checks,
     max_array_length,
     needed_methods,
     needed_classes);
diff --git a/src/java_bytecode/java_bytecode_convert_method.h b/src/java_bytecode/java_bytecode_convert_method.h
index e81881f44e1..bc25eccb0c7 100644
--- a/src/java_bytecode/java_bytecode_convert_method.h
+++ b/src/java_bytecode/java_bytecode_convert_method.h
@@ -22,7 +22,6 @@ void java_bytecode_convert_method(
   const java_bytecode_parse_treet::methodt &,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length,
   safe_pointer > needed_methods,
   safe_pointer > needed_classes);
@@ -33,7 +32,6 @@ inline void java_bytecode_convert_method(
   const java_bytecode_parse_treet::methodt &method,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  bool disable_runtime_checks,
   size_t max_array_length)
 {
   java_bytecode_convert_method(
@@ -41,7 +39,6 @@ inline void java_bytecode_convert_method(
     method,
     symbol_table,
     message_handler,
-    disable_runtime_checks,
     max_array_length,
     safe_pointer >::create_null(),
     safe_pointer >::create_null());
diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h
index 4fb24c47b84..60b69a60f34 100644
--- a/src/java_bytecode/java_bytecode_convert_method_class.h
+++ b/src/java_bytecode/java_bytecode_convert_method_class.h
@@ -30,13 +30,11 @@ class java_bytecode_convert_methodt:public messaget
   java_bytecode_convert_methodt(
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
-    bool _disable_runtime_checks,
     size_t _max_array_length,
     safe_pointer > _needed_methods,
     safe_pointer > _needed_classes):
     messaget(_message_handler),
     symbol_table(_symbol_table),
-    disable_runtime_checks(_disable_runtime_checks),
     max_array_length(_max_array_length),
     needed_methods(_needed_methods),
     needed_classes(_needed_classes)
@@ -56,7 +54,6 @@ class java_bytecode_convert_methodt:public messaget
 
 protected:
   symbol_tablet &symbol_table;
-  const bool disable_runtime_checks;
   const size_t max_array_length;
   safe_pointer > needed_methods;
   safe_pointer > needed_classes;
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 0e2eb25d0ec..ce52cfcece3 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -42,7 +42,6 @@ Function: java_bytecode_languaget::get_language_options
 
 void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 {
-  disable_runtime_checks=cmd.isset("disable-runtime-check");
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
   string_refinement_enabled=cmd.isset("string-refine");
   if(cmd.isset("java-max-input-array-length"))
@@ -518,7 +517,6 @@ bool java_bytecode_languaget::typecheck(
          c_it->second,
          symbol_table,
          get_message_handler(),
-         disable_runtime_checks,
          max_user_array_length,
          lazy_methods,
          lazy_methods_mode,
@@ -639,7 +637,6 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
           *parsed_method.second,
           symbol_table,
           get_message_handler(),
-          disable_runtime_checks,
           max_user_array_length,
           safe_pointer >::create_non_null(
             &method_worklist2),
@@ -754,7 +751,6 @@ void java_bytecode_languaget::convert_lazy_method(
     *lazy_method_entry.second,
     symtab,
     get_message_handler(),
-    disable_runtime_checks,
     max_user_array_length);
 }
 
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index 77689d6e12a..3c889322daf 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -94,12 +94,6 @@ class java_bytecode_languaget:public languaget
   std::vector main_jar_classes;
   java_class_loadert java_class_loader;
   bool assume_inputs_non_null;      // assume inputs variables to be non-null
-
-  bool disable_runtime_checks;      // disable run-time checks for java, i.e.,
-                                    // ASSERTS for
-                                    //  - checkcast / instanceof
-                                    //  - array bounds check
-                                    //  - array size for newarray
   size_t max_nondet_array_length;   // maximal length for non-det array creation
   size_t max_user_array_length;     // max size for user code created arrays
   lazy_methodst lazy_methods;

From 6c5303635e112259fc569e21ecabfcdc295d797a Mon Sep 17 00:00:00 2001
From: reuk 
Date: Fri, 17 Mar 2017 09:22:15 +0000
Subject: [PATCH 04/58] Fix errors when -Wall -Werror flags are set

---
 .travis.yml                                     | 6 ++++--
 src/cbmc/bmc.cpp                                | 2 +-
 src/java_bytecode/java_local_variable_table.cpp | 8 --------
 src/util/union_find.h                           | 3 ++-
 4 files changed, 7 insertions(+), 12 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 3fc29224575..f3147e89e53 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -68,8 +68,6 @@ matrix:
 
 script:
   - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O0 -ggdb3 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DDEBUG\" -j2" &&
-    eval ${PRE_COMMAND} ${COMMAND} &&
     COMMAND="make -C src minisat2-download" &&
     eval ${PRE_COMMAND} ${COMMAND} &&
     COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare\" -j2" &&
@@ -77,4 +75,8 @@ script:
     COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
     eval ${PRE_COMMAND} ${COMMAND} &&
     COMMAND="make -C src CXX=$COMPILER CXXFLAGS=$FLAGS -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src clean" &&
+    eval ${PRE_COMMAND} ${COMMAND} &&
+    COMMAND="make -C src CXX=$COMPILER CXXFLAGS=\"-Wall -O0 -ggdb3 -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DDEBUG\" -j2" &&
     eval ${PRE_COMMAND} ${COMMAND}
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 2f39d97b1ce..f1e005a46a1 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -687,7 +687,7 @@ void bmct::setup_unwind()
 
   for(auto &val : unwindset_loops)
   {
-    unsigned thread_nr;
+    unsigned thread_nr=0;
     bool thread_nr_set=false;
 
     if(!val.empty() &&
diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp
index 33e8a39f5db..83ace02276b 100644
--- a/src/java_bytecode/java_local_variable_table.cpp
+++ b/src/java_bytecode/java_local_variable_table.cpp
@@ -546,14 +546,6 @@ static void merge_variable_table_entries(
   merge_into.var.start_pc=found_dominator;
   merge_into.var.length=last_pc-found_dominator;
 
-#ifdef DEBUG
-  debug_out << "Merged " << merge_vars.size() << " variables named "
-            << merge_into.var.name << "; new live range "
-            << merge_into.var.start_pc << "-"
-            << merge_into.var.start_pc + merge_into.var.length
-            << messaget::eom;
-#endif
-
   // Nuke the now-subsumed var-table entries:
   for(auto &v : merge_vars)
     if(v!=&merge_into)
diff --git a/src/util/union_find.h b/src/util/union_find.h
index 5b2ff2504e4..2fee15e495b 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -157,7 +157,8 @@ class union_find:public numbering
   // are 'a' and 'b' in the same set?
   bool same_set(const T &a, const T &b) const
   {
-    typename subt::number_type na, nb;
+    typedef typename subt::number_type subt_number_typet;
+    subt_number_typet na=subt_number_typet(), nb=subt_number_typet();
     bool have_na=!subt::get_number(a, na),
          have_nb=!subt::get_number(b, nb);
 

From 0662dd0ab93efbe54e1fa2eea6bfd4ceb985a810 Mon Sep 17 00:00:00 2001
From: Vojtech Forejt 
Date: Wed, 8 Mar 2017 20:26:38 +0000
Subject: [PATCH 05/58] Fix several test problems on Windows

- strip  from end of lines in test.pl
- tests for test-script do not depend on gcc
- Makefile in regression/goto-analyser has the same structure as other test Makefiles
- remove tests for empty lines
---
 regression/cbmc/Quantifiers-assertion/test.desc        |  1 -
 regression/cbmc/Quantifiers-assignment/test.desc       |  1 -
 regression/cbmc/Quantifiers-copy/test.desc             |  1 -
 regression/cbmc/Quantifiers-if/test.desc               |  1 -
 regression/cbmc/Quantifiers-initialisation/test.desc   |  1 -
 regression/cbmc/Quantifiers-initialisation2/test.desc  |  1 -
 .../cbmc/Quantifiers-invalid-var-range/test.desc       |  1 -
 regression/cbmc/Quantifiers-not-exists/test.desc       |  1 -
 regression/cbmc/Quantifiers-not/test.desc              |  1 -
 .../cbmc/Quantifiers-two-dimension-array/test.desc     |  1 -
 regression/cbmc/Quantifiers-type/test.desc             |  1 -
 regression/goto-analyzer/Makefile                      | 10 ++++++++--
 regression/test-script/excluded-line/program.c         |  7 -------
 regression/test-script/excluded-line/test.desc         |  2 +-
 regression/test-script/excluded-line/test.txt          |  3 +++
 regression/test-script/failing-excluded-line/program.c |  7 -------
 regression/test-script/failing-excluded-line/test.desc |  2 +-
 regression/test-script/failing-excluded-line/test.txt  |  3 +++
 regression/test-script/failing-multi-line/program.c    |  7 -------
 regression/test-script/failing-multi-line/test.desc    |  2 +-
 regression/test-script/failing-multi-line/test.txt     |  3 +++
 regression/test-script/failing-single-line/program.c   |  7 -------
 regression/test-script/failing-single-line/test.desc   |  2 +-
 regression/test-script/failing-single-line/test.txt    |  3 +++
 regression/test-script/multi-line/program.c            |  7 -------
 regression/test-script/multi-line/test.desc            |  2 +-
 regression/test-script/multi-line/test.txt             |  3 +++
 regression/test-script/program_runner.sh               |  3 +--
 .../single-line-windows-line-ends/test.desc            |  5 +++++
 .../test-script/single-line-windows-line-ends/test.txt |  3 +++
 regression/test-script/single-line/program.c           |  7 -------
 regression/test-script/single-line/test.desc           |  2 +-
 regression/test-script/single-line/test.txt            |  3 +++
 regression/test.pl                                     |  4 +++-
 34 files changed, 44 insertions(+), 64 deletions(-)
 delete mode 100755 regression/test-script/excluded-line/program.c
 create mode 100755 regression/test-script/excluded-line/test.txt
 delete mode 100755 regression/test-script/failing-excluded-line/program.c
 create mode 100755 regression/test-script/failing-excluded-line/test.txt
 delete mode 100755 regression/test-script/failing-multi-line/program.c
 create mode 100755 regression/test-script/failing-multi-line/test.txt
 delete mode 100755 regression/test-script/failing-single-line/program.c
 create mode 100755 regression/test-script/failing-single-line/test.txt
 delete mode 100755 regression/test-script/multi-line/program.c
 create mode 100755 regression/test-script/multi-line/test.txt
 create mode 100644 regression/test-script/single-line-windows-line-ends/test.desc
 create mode 100755 regression/test-script/single-line-windows-line-ends/test.txt
 delete mode 100755 regression/test-script/single-line/program.c
 create mode 100755 regression/test-script/single-line/test.txt

diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
index 5b4797b9b00..555f7b0e61f 100644
--- a/regression/cbmc/Quantifiers-assertion/test.desc
+++ b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -8,6 +8,5 @@ main.c
 ^\[main.assertion.4\] NotExists-Forall: failed: FAILURE$
 ^\[main.assertion.5\] NotForall-Forall: successful: SUCCESS$
 ^\[main.assertion.6\] NotForall-NotForall: successful: SUCCESS$
-
 ^\*\* 2 of 6 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
index cfc835ce948..289e8a47efc 100644
--- a/regression/cbmc/Quantifiers-assignment/test.desc
+++ b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -6,6 +6,5 @@ main.c
 ^\[main.assertion.2\] assertion y: FAILURE$
 ^\[main.assertion.3\] assertion z1: SUCCESS$
 ^\[main.assertion.4\] assertion z2: SUCCESS$
-
 ^\*\* 1 of 4 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-copy/test.desc b/regression/cbmc/Quantifiers-copy/test.desc
index 5682d588b9c..993061a5b3a 100644
--- a/regression/cbmc/Quantifiers-copy/test.desc
+++ b/regression/cbmc/Quantifiers-copy/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion b\[.*\] == 2: SUCCESS$
 ^\[main.assertion.4\] assertion b\[.*\] == 3: SUCCESS$
 ^\[main.assertion.5\] assertion b\[.*\] == 4: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-if/test.desc b/regression/cbmc/Quantifiers-if/test.desc
index e121e2e1955..be4945b25ef 100644
--- a/regression/cbmc/Quantifiers-if/test.desc
+++ b/regression/cbmc/Quantifiers-if/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] success 1: SUCCESS$
 ^\[main.assertion.4\] failure 3: FAILURE$
 ^\[main.assertion.5\] success 2: SUCCESS$
-
 ^\*\* 3 of 5 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-initialisation/test.desc b/regression/cbmc/Quantifiers-initialisation/test.desc
index b10b600c308..d0e4c279e1f 100644
--- a/regression/cbmc/Quantifiers-initialisation/test.desc
+++ b/regression/cbmc/Quantifiers-initialisation/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\] == 3: SUCCESS$
 ^\[main.assertion.4\] assertion a\[.*\] == 4: SUCCESS$
 ^\[main.assertion.5\] assertion a\[.*\] == 5: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-initialisation2/test.desc b/regression/cbmc/Quantifiers-initialisation2/test.desc
index ad5913e4d92..0f309d9332d 100644
--- a/regression/cbmc/Quantifiers-initialisation2/test.desc
+++ b/regression/cbmc/Quantifiers-initialisation2/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\] > a\[.*\]: FAILURE$
 ^\[main.assertion.4\] forall c\[\]: SUCCESS$
 ^\[main.assertion.5\] assertion c\[.*\] >= c\[.*\]: SUCCESS$
-
 ^\*\* 1 of 5 failed \(2 iterations\)$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
index e38af4ddbdb..a3e1bce313f 100644
--- a/regression/cbmc/Quantifiers-invalid-var-range/test.desc
+++ b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
@@ -2,6 +2,5 @@ CORE
 main.c
 
 ^\*\* Results:$
-
 ^\*\* 0 of 1 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc
index 51feeae3b08..630e54eb224 100644
--- a/regression/cbmc/Quantifiers-not-exists/test.desc
+++ b/regression/cbmc/Quantifiers-not-exists/test.desc
@@ -8,6 +8,5 @@ main.c
 ^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$
 ^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
 ^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
-
 ^\*\* 0 of 6 failed \(1 iteration\)$
 ^\VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-not/test.desc b/regression/cbmc/Quantifiers-not/test.desc
index b1b6a0d1d60..2e862045758 100644
--- a/regression/cbmc/Quantifiers-not/test.desc
+++ b/regression/cbmc/Quantifiers-not/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] failure 1: FAILURE$
 ^\[main.assertion.4\] success 3: SUCCESS$
 ^\[main.assertion.5\] failure 2: FAILURE$
-
 ^\*\* 2 of 5 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc
index 2874b9dc0eb..b8501be880e 100644
--- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc
+++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc
@@ -7,6 +7,5 @@ main.c
 ^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
 ^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
-
 ^\*\* 0 of 5 failed \(1 iteration\)$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
index 3bc8a8d2a5f..b0b25cc9903 100644
--- a/regression/cbmc/Quantifiers-type/test.desc
+++ b/regression/cbmc/Quantifiers-type/test.desc
@@ -4,6 +4,5 @@ main.c
 ^\*\* Results:$
 ^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
 ^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
-
 ^\*\* 1 of 2 failed \(2 iterations\)$
 ^\VERIFICATION FAILED$
diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile
index 5701431a37e..2630bf17097 100644
--- a/regression/goto-analyzer/Makefile
+++ b/regression/goto-analyzer/Makefile
@@ -1,10 +1,16 @@
 default: tests.log
 
 test:
-	@../test.pl -c ../../../src/goto-analyzer/goto-analyzer
+	@if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 tests.log: ../test.pl
-	@../test.pl -c ../../../src/goto-analyzer/goto-analyzer
+	@if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 show:
 	@for dir in *; do \
diff --git a/regression/test-script/excluded-line/program.c b/regression/test-script/excluded-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/excluded-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/excluded-line/test.desc b/regression/test-script/excluded-line/test.desc
index 2384efe0828..7fa478ad232 100644
--- a/regression/test-script/excluded-line/test.desc
+++ b/regression/test-script/excluded-line/test.desc
@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 ^Hello$
 --
diff --git a/regression/test-script/excluded-line/test.txt b/regression/test-script/excluded-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/excluded-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/failing-excluded-line/program.c b/regression/test-script/failing-excluded-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/failing-excluded-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/failing-excluded-line/test.desc b/regression/test-script/failing-excluded-line/test.desc
index 36668db5a5f..3c8b8bc9f72 100644
--- a/regression/test-script/failing-excluded-line/test.desc
+++ b/regression/test-script/failing-excluded-line/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 ^Hello$
 --
diff --git a/regression/test-script/failing-excluded-line/test.txt b/regression/test-script/failing-excluded-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/failing-excluded-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/failing-multi-line/program.c b/regression/test-script/failing-multi-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/failing-multi-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/failing-multi-line/test.desc b/regression/test-script/failing-multi-line/test.desc
index cf4fcf3034b..b3b2f171842 100644
--- a/regression/test-script/failing-multi-line/test.desc
+++ b/regression/test-script/failing-multi-line/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 activate-multi-line-match
 Hello\nAnother\nWorld
diff --git a/regression/test-script/failing-multi-line/test.txt b/regression/test-script/failing-multi-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/failing-multi-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/failing-single-line/program.c b/regression/test-script/failing-single-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/failing-single-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/failing-single-line/test.desc b/regression/test-script/failing-single-line/test.desc
index 604682ecbdb..973b5aa464b 100644
--- a/regression/test-script/failing-single-line/test.desc
+++ b/regression/test-script/failing-single-line/test.desc
@@ -1,5 +1,5 @@
 KNOWNBUG
-program.c
+test.txt
 
 ^Goodbye$
 --
diff --git a/regression/test-script/failing-single-line/test.txt b/regression/test-script/failing-single-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/failing-single-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/multi-line/program.c b/regression/test-script/multi-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/multi-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/multi-line/test.desc b/regression/test-script/multi-line/test.desc
index cf9bb072880..2ef644c2082 100644
--- a/regression/test-script/multi-line/test.desc
+++ b/regression/test-script/multi-line/test.desc
@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 activate-multi-line-match
 Hello\nWorld
diff --git a/regression/test-script/multi-line/test.txt b/regression/test-script/multi-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/multi-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/program_runner.sh b/regression/test-script/program_runner.sh
index 8e09b75f0ab..851f1716b12 100755
--- a/regression/test-script/program_runner.sh
+++ b/regression/test-script/program_runner.sh
@@ -2,5 +2,4 @@
 
 set -e
 
-gcc $1 -o a.out
-./a.out
+cat $1
diff --git a/regression/test-script/single-line-windows-line-ends/test.desc b/regression/test-script/single-line-windows-line-ends/test.desc
new file mode 100644
index 00000000000..d7c83bd851e
--- /dev/null
+++ b/regression/test-script/single-line-windows-line-ends/test.desc
@@ -0,0 +1,5 @@
+CORE
+test.txt
+
+^Hello$
+--
diff --git a/regression/test-script/single-line-windows-line-ends/test.txt b/regression/test-script/single-line-windows-line-ends/test.txt
new file mode 100755
index 00000000000..7c9ae46963c
--- /dev/null
+++ b/regression/test-script/single-line-windows-line-ends/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test-script/single-line/program.c b/regression/test-script/single-line/program.c
deleted file mode 100755
index 882fedcc2fd..00000000000
--- a/regression/test-script/single-line/program.c
+++ /dev/null
@@ -1,7 +0,0 @@
-#include 
-
-int main(void) {
-  printf("Hello\n");
-  printf("World\n");
-  return 0;
-}
diff --git a/regression/test-script/single-line/test.desc b/regression/test-script/single-line/test.desc
index 2507fd6a412..d7c83bd851e 100644
--- a/regression/test-script/single-line/test.desc
+++ b/regression/test-script/single-line/test.desc
@@ -1,5 +1,5 @@
 CORE
-program.c
+test.txt
 
 ^Hello$
 --
diff --git a/regression/test-script/single-line/test.txt b/regression/test-script/single-line/test.txt
new file mode 100755
index 00000000000..0ac4c9a8b57
--- /dev/null
+++ b/regression/test-script/single-line/test.txt
@@ -0,0 +1,3 @@
+Hello
+World
+
diff --git a/regression/test.pl b/regression/test.pl
index a2ac088d0e0..d27c663b0aa 100755
--- a/regression/test.pl
+++ b/regression/test.pl
@@ -73,7 +73,7 @@ ($$$$$)
   $options =~ s/$ign//g if(defined($ign));
 
   my $output = $input;
-  $output =~ s/\.(c|i|gb|cpp|ii|xml|class|jar)$/.out/;
+  $output =~ s/\.[^.]*$/.out/;
 
   if($output eq $input) {
     print("Error in test file -- $test\n");
@@ -125,6 +125,7 @@ ($$$$$)
             local $/ = undef;
             binmode $fh;
             my $whole_file = <$fh>;
+            $whole_file =~ s/\r\n/\n/g;
             my $is_match = $whole_file =~ /$result/;
             $r = ($included ? !$is_match : $is_match);
           }
@@ -132,6 +133,7 @@ ($$$$$)
           {
             my $found_line = 0;
             while(my $line = <$fh>) {
+              $line =~ s/\r$//;
               if($line =~ /$result/) {
                 # We've found the line, therefore if it is included we set
                 # the result to 0 (OK) If it is excluded, we set the result

From 1a5c69d733971266279954926d14e474f374ff14 Mon Sep 17 00:00:00 2001
From: reuk 
Date: Mon, 20 Mar 2017 21:14:56 +0000
Subject: [PATCH 06/58] Fix DEBUG blocks based on feedback

---
 src/analyses/cfg_dominators.h                 |  9 ++++++-
 src/analyses/natural_loops.h                  |  4 +++
 src/cpp/parse.cpp                             | 27 ++++++++++++++++++-
 .../accelerate/scratch_program.cpp            | 11 +++++++-
 .../accelerate/trace_automaton.cpp            | 20 ++++++++++++--
 .../java_local_variable_table.cpp             | 11 ++++++--
 6 files changed, 75 insertions(+), 7 deletions(-)

diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h
index 1a4d6090f47..930d0ae69b9 100644
--- a/src/analyses/cfg_dominators.h
+++ b/src/analyses/cfg_dominators.h
@@ -224,6 +224,13 @@ void dominators_pretty_print_node(const T &node, std::ostream &out)
   out << node;
 }
 
+inline void dominators_pretty_print_node(
+  const goto_programt::targett& target,
+  std::ostream& out)
+{
+  out << target->code.pretty();
+}
+
 /*******************************************************************\
 
 Function: cfg_dominators_templatet::output
@@ -241,7 +248,7 @@ void cfg_dominators_templatet::output(std::ostream &out) const
 {
   for(const auto &node : cfg.entry_map)
   {
-    T n=node.first;
+    auto n=node.first;
 
     dominators_pretty_print_node(n, out);
     if(post_dom)
diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h
index 3408aba68db..ff56c687c93 100644
--- a/src/analyses/natural_loops.h
+++ b/src/analyses/natural_loops.h
@@ -90,6 +90,10 @@ void natural_loops_templatet::compute(P &program)
 {
   cfg_dominators(program);
 
+#ifdef DEBUG
+  cfg_dominators.output(std::cout);
+#endif
+
   // find back-edges m->n
   for(T m_it=program.instructions.begin();
       m_it!=program.instructions.end();
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index b15b486c248..b16340c3eef 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -637,6 +637,12 @@ bool Parser::rDefinition(cpp_itemt &item)
 {
   int t=lex.LookAhead(0);
 
+  #ifdef DEBUG
+  indenter _i;
+  std::cout << std::string(__indent, ' ') << "Parser::rDefinition 1 " << t
+            << '\n';
+  #endif
+
   if(t==';')
     return rNullDeclaration(item.make_declaration());
   else if(t==TOK_TYPEDEF)
@@ -1229,6 +1235,12 @@ bool Parser::rTemplateDecl(cpp_declarationt &decl)
   switch(kind)
   {
   case tdk_decl:
+    #ifdef DEBUG
+    std::cout << std::string(__indent, ' ') << "BODY: "
+              << body.pretty() << '\n';
+    std::cout << std::string(__indent, ' ') << "TEMPLATE_TYPE: "
+              << template_type.pretty() << '\n';
+    #endif
     body.add(ID_template_type).swap(template_type);
     body.set(ID_is_template, true);
     decl.swap(body);
@@ -1895,6 +1907,11 @@ bool Parser::rIntegralDeclaration(
 
     if(lex.LookAhead(0)==';')
     {
+      #ifdef DEBUG
+      std::cout << std::string(__indent, ' ')
+                << "Parser::rIntegralDeclaration 8 "
+                << declaration.pretty() << '\n';
+      #endif
       lex.get_token(tk);
       return true;
     }
@@ -5098,6 +5115,10 @@ bool Parser::rClassBody(exprt &body)
       // body=Ptree::List(ob, nil, new Leaf(tk));
       return true;        // error recovery
     }
+    #ifdef DEBUG
+    std::cout << std::string(__indent, ' ') << "Parser::rClassBody "
+              << member.pretty() << '\n';
+    #endif
 
     members.move_to_operands(
       static_cast(static_cast(member)));
@@ -7558,7 +7579,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
   #ifdef DEBUG
   indenter _i;
   std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 0 "
-            << lex.LookAhead(0) << " " << lex.current_token().text <<"\n";
+            << lex.LookAhead(0) << ' ' << lex.current_token().text << '\n';
   #endif
 
   switch(lex.LookAhead(0))
@@ -9219,6 +9240,10 @@ bool Parser::rExprStatement(codet &statement)
 
     if(rDeclarationStatement(statement))
     {
+      #ifdef DEBUG
+      std::cout << std::string(__indent, ' ') << "rDe "
+                << statement.pretty() << '\n';
+      #endif
       return true;
     }
     else
diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp
index 9f3ac61584d..8f7e1f40c2d 100644
--- a/src/goto-instrument/accelerate/scratch_program.cpp
+++ b/src/goto-instrument/accelerate/scratch_program.cpp
@@ -28,6 +28,11 @@ bool scratch_programt::check_sat(bool do_slice)
   remove_skip(*this);
   update();
 
+#ifdef DEBUG
+  std::cout << "Checking following program for satness:\n";
+  output(ns, "scratch", std::cout);
+#endif
+
   symex.constant_propagation=constant_propagation;
   goto_symex_statet::propagationt::valuest constants;
 
@@ -42,13 +47,17 @@ bool scratch_programt::check_sat(bool do_slice)
   {
     // Symex sliced away all our assertions.
 #ifdef DEBUG
-    std::cout << "Trivially unsat" << std::endl;
+    std::cout << "Trivially unsat\n";
 #endif
     return false;
   }
 
   equation.convert(*checker);
 
+#ifdef DEBUG
+  std::cout << "Finished symex, invoking decision procedure.\n";
+#endif
+
   return (checker->dec_solve()==decision_proceduret::D_SATISFIABLE);
 }
 
diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp
index 9cd8bef2247..10682862e7b 100644
--- a/src/goto-instrument/accelerate/trace_automaton.cpp
+++ b/src/goto-instrument/accelerate/trace_automaton.cpp
@@ -75,6 +75,11 @@ void trace_automatont::add_path(patht &path)
   {
     goto_programt::targett l=step.loc;
 
+#ifdef DEBUG
+    std::cout << ", " << l->location_number << ':'
+              << l->source_location.as_string();
+#endif
+
     if(in_alphabet(l))
     {
 #ifdef DEBUG
@@ -103,6 +108,13 @@ void trace_automatont::add_path(patht &path)
  */
 void trace_automatont::determinise()
 {
+#ifdef DEBUG
+  std::cout << "Determinising automaton with " << nta.num_states
+            << " states and " << nta.accept_states.size()
+            << " accept states and " << nta.count_transitions()
+            << " transitions\n";
+#endif
+
   dstates.clear();
   unmarked_dstates.clear();
   dta.clear();
@@ -111,6 +123,10 @@ void trace_automatont::determinise()
   init_states.insert(nta.init_state);
   epsilon_closure(init_states);
 
+#ifdef DEBUG
+  std::cout << "There are " << init_states.size() << " init states\n";
+#endif
+
   dta.init_state=add_dstate(init_states);
 
   while(!unmarked_dstates.empty())
@@ -371,7 +387,7 @@ void automatont::reverse(goto_programt::targett epsilon)
 
   std::cout << "Reversing automaton, old init=" << init_state
             << ", new init=" << new_init << ", old accept="
-            << *(accept_states.begin()) << "/" << accept_states.size()
+            << *(accept_states.begin()) << '/' << accept_states.size()
             << " new accept=" << init_state << std::endl;
 
   accept_states.clear();
@@ -455,7 +471,7 @@ void automatont::output(std::ostream &str)
   str << "Accept states: ";
 
   for(const auto &state : accept_states)
-    str << state << " ";
+    str << state << ' ';
 
   str << std::endl;
 
diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp
index 83ace02276b..85e9766d5ab 100644
--- a/src/java_bytecode/java_local_variable_table.cpp
+++ b/src/java_bytecode/java_local_variable_table.cpp
@@ -352,7 +352,7 @@ static void populate_predecessor_map(
             // handling is presently vague (any subroutine is assumed to
             // be able to return to any callsite)
             msg.warning() << "Local variable table: ignoring flow from "
-                          << "out of range for " << it->var.name << " "
+                          << "out of range for " << it->var.name << ' '
                           << pred << " -> " << amapit->first
                           << messaget::eom;
             continue;
@@ -375,7 +375,7 @@ static void populate_predecessor_map(
             // assumed to be able to return to any callsite)
             msg.warning() << "Local variable table: ignoring flow from "
                           << "clashing variable for "
-                          << it->var.name << " " << pred << " -> "
+                          << it->var.name << ' ' << pred << " -> "
                           << amapit->first << messaget::eom;
             continue;
           }
@@ -546,6 +546,13 @@ static void merge_variable_table_entries(
   merge_into.var.start_pc=found_dominator;
   merge_into.var.length=last_pc-found_dominator;
 
+#ifdef DEBUG
+  debug_out << "Merged " << merge_vars.size() << " variables named "
+            << merge_into.var.name << "; new live range "
+            << merge_into.var.start_pc << '-'
+            << merge_into.var.start_pc + merge_into.var.length << '\n';
+#endif
+
   // Nuke the now-subsumed var-table entries:
   for(auto &v : merge_vars)
     if(v!=&merge_into)

From 72052c7eef45dd56cd014a7c21ae4f6629b44217 Mon Sep 17 00:00:00 2001
From: Peter Schrammel 
Date: Wed, 22 Mar 2017 20:49:10 +0000
Subject: [PATCH 07/58] Auxiliary function to check whether source location is
 in built-in

---
 src/util/source_location.h | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/util/source_location.h b/src/util/source_location.h
index b24befcb8c4..b9cf434f3b0 100644
--- a/src/util/source_location.h
+++ b/src/util/source_location.h
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_UTIL_SOURCE_LOCATION_H
 
 #include "irep.h"
+#include "prefix.h"
 
 class source_locationt:public irept
 {
@@ -138,6 +139,18 @@ class source_locationt:public irept
     return get_bool(ID_hide);
   }
 
+  static bool is_built_in(const std::string &s)
+  {
+    std::string built_in1="";
+    std::string built_in2="";
+    return has_prefix(s, built_in1) || has_prefix(s, built_in2);
+  }
+
+  bool is_built_in() const
+  {
+    return is_built_in(id2string(get_file()));
+  }
+
   static const source_locationt &nil()
   {
     return static_cast(get_nil_irep());

From 32fcbbcdb95399eff80d4deeaf72992b3e9f9b14 Mon Sep 17 00:00:00 2001
From: Peter Schrammel 
Date: Wed, 22 Mar 2017 21:01:02 +0000
Subject: [PATCH 08/58] Replace built-in checks by is_built_in

---
 src/cbmc/symex_coverage.cpp           | 2 +-
 src/goto-instrument/count_eloc.cpp    | 2 +-
 src/goto-instrument/cover.cpp         | 4 +---
 src/goto-programs/graphml_witness.cpp | 4 ++--
 4 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp
index 8f64f9900a8..69af02e9e9e 100644
--- a/src/cbmc/symex_coverage.cpp
+++ b/src/cbmc/symex_coverage.cpp
@@ -318,7 +318,7 @@ void symex_coveraget::compute_overall_coverage(
       it!=file_records.end();
       ++it)
   {
-    if(has_prefix(id2string(it->first), "first)))
       continue;
 
     const coverage_recordt &f_cov=it->second;
diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp
index 2988b8637d2..96b21195a82 100644
--- a/src/goto-instrument/count_eloc.cpp
+++ b/src/goto-instrument/count_eloc.cpp
@@ -44,7 +44,7 @@ static void collect_eloc(
       const irep_idt &file=it->source_location.get_file();
 
       if(!file.empty() &&
-         !has_prefix(id2string(file), "source_location.is_built_in())
         files[file].insert(it->source_location.get_line());
     }
   }
diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp
index fa92bc27cc7..ede599b6d8b 100644
--- a/src/goto-instrument/cover.cpp
+++ b/src/goto-instrument/cover.cpp
@@ -1082,9 +1082,7 @@ void instrument_cover_goals(
 
   // ignore if built-in library
   if(!goto_program.instructions.empty() &&
-     has_prefix(
-       id2string(goto_program.instructions.front().source_location.get_file()),
-       "is_goto() && it->pc->guard.is_true()) ||
        source_location.is_nil() ||
        source_location.get_file().empty() ||
-       source_location.get_file()=="" ||
+       source_location.is_built_in() ||
        source_location.get_line().empty())
     {
       step_to_node[it->step_nr]=sink;
@@ -392,7 +392,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
        (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
        (it->is_goto() && it->source.pc->guard.is_true()) ||
        source_location.is_nil() ||
-       source_location.get_file()=="" ||
+       source_location.is_built_in() ||
        source_location.get_line().empty())
     {
       step_to_node[step_nr]=sink;

From c21d3ed4426a7b5d42e9f1a37f1e29af72c62877 Mon Sep 17 00:00:00 2001
From: Daniel Kroening 
Date: Thu, 23 Mar 2017 08:50:03 +0000
Subject: [PATCH 09/58] update instructions for g++ 6

---
 COMPILING | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/COMPILING b/COMPILING
index 93fc65c2938..8fe38eeea7e 100644
--- a/COMPILING
+++ b/COMPILING
@@ -44,12 +44,18 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
    git clone https://github.com/diffblue/cbmc cbmc-git
 
-2) Do
+2) On Debian/Ubuntu, do
 
    cd cbmc-git/src
    make minisat2-download
    make
 
+   On Redhat/Fedora etc., do
+
+   cd cbmc-git/src
+   make minisat2-download
+   make CXX=g++-6
+
 
 COMPILATION ON SOLARIS 11
 -------------------------

From 903d243eac50eb8172ab4e25343f4048aa30c4b8 Mon Sep 17 00:00:00 2001
From: jgwilson42 
Date: Thu, 23 Mar 2017 10:31:24 +0000
Subject: [PATCH 10/58] Updates for GCC 6

---
 COMPILING | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/COMPILING b/COMPILING
index 8fe38eeea7e..cfbb056c2e0 100644
--- a/COMPILING
+++ b/COMPILING
@@ -36,7 +36,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
    On Red Hat/Fedora or derivates, do
 
-   yum install gcc gcc-c++ flex bison perl-libwww-perl patch
+   yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6
 
    Note that you need g++ version 5.2 or newer.
 
@@ -48,13 +48,14 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
    cd cbmc-git/src
    make minisat2-download
-   make
+   make CXX=g++-6
 
    On Redhat/Fedora etc., do
 
    cd cbmc-git/src
    make minisat2-download
-   make CXX=g++-6
+   scl enable devtoolset-6 bash
+   make
 
 
 COMPILATION ON SOLARIS 11

From e843b724ec4c155e576a6551b24c0dc6e41c865e Mon Sep 17 00:00:00 2001
From: Chris Smowton 
Date: Mon, 20 Mar 2017 16:09:49 +0000
Subject: [PATCH 11/58] Correct pretty-printing of code_returnt

---
 src/ansi-c/expr2c.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index a6975bdab19..86bd4183b91 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -3337,7 +3337,7 @@ std::string expr2ct::convert_code_return(
   std::string dest=indent_str(indent);
   dest+="return";
 
-  if(src.operands().size()==1)
+  if(to_code_return(src).has_return_value())
     dest+=" "+convert(src.op0());
 
   dest+=';';

From 4473f0692f89d28fc2def116aed180c0006efbac Mon Sep 17 00:00:00 2001
From: Chris Smowton 
Date: Thu, 23 Mar 2017 12:36:17 +0000
Subject: [PATCH 12/58] Fix Java multinewarray

Simply assigning to a temporary symbol of the correct type and
amending the type passed to the elaboration of the sub-array seems
to suffice to properly initialise a multi-dimensional array.
---
 src/goto-programs/builtin_functions.cpp | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 615470b7f9e..1f9e790b9d9 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -851,13 +851,19 @@ void goto_convertt::do_java_new_array(
     goto_programt tmp;
 
     symbol_exprt tmp_i=
-      new_tmp_symbol(index_type(), "index", tmp, location).symbol_expr();
+      new_tmp_symbol(length.type(), "index", tmp, location).symbol_expr();
 
     code_fort for_loop;
 
     side_effect_exprt sub_java_new=rhs;
     sub_java_new.operands().erase(sub_java_new.operands().begin());
 
+    assert(rhs.type().id()==ID_pointer);
+    typet sub_type=
+      static_cast(rhs.type().subtype().find("#element_type"));
+    assert(sub_type.id()==ID_pointer);
+    sub_java_new.type()=sub_type;
+
     side_effect_exprt inc(ID_assign);
     inc.operands().resize(2);
     inc.op0()=tmp_i;
@@ -866,11 +872,21 @@ void goto_convertt::do_java_new_array(
     dereference_exprt deref_expr(
       plus_exprt(data, tmp_i), data.type().subtype());
 
+    code_blockt for_body;
+    symbol_exprt init_sym=
+      new_tmp_symbol(sub_type, "subarray_init", tmp, location).symbol_expr();
+
+    code_assignt init_subarray(init_sym, sub_java_new);
+    code_assignt assign_subarray(
+      deref_expr,
+      typecast_exprt(init_sym, deref_expr.type()));
+    for_body.move_to_operands(init_subarray);
+    for_body.move_to_operands(assign_subarray);
+
     for_loop.init()=code_assignt(tmp_i, from_integer(0, tmp_i.type()));
     for_loop.cond()=binary_relation_exprt(tmp_i, ID_lt, rhs.op0());
     for_loop.iter()=inc;
-    for_loop.body()=code_skipt();
-    for_loop.body()=code_assignt(deref_expr, sub_java_new);
+    for_loop.body()=for_body;
 
     convert(for_loop, tmp);
     dest.destructive_append(tmp);

From 0a53fbbb74ce7dfbb8177e159dc7520906fcba0b Mon Sep 17 00:00:00 2001
From: Chris Smowton 
Date: Thu, 23 Mar 2017 12:41:35 +0000
Subject: [PATCH 13/58] Amend test-case to complete in acceptable time

---
 .../cbmc-java/multinewarray/multinewarray.class | Bin 773 -> 771 bytes
 .../cbmc-java/multinewarray/multinewarray.java  |   4 ++--
 regression/cbmc-java/multinewarray/test.desc    |   2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/regression/cbmc-java/multinewarray/multinewarray.class b/regression/cbmc-java/multinewarray/multinewarray.class
index 09cb7711192f8203faf62662cb4b7ed4025996ce..6895eaa962b3d52d89596646be14ff9b8bebc37e 100644
GIT binary patch
delta 84
zcmZo=Yi8T9pON!B0}BH?0|P_Tdb82lIn8NwKZ8R8j47%~_{
k8A^e4HIU!PAjKdA)S=G6{)a(^oqYh~N8pONz?0}BH?0|P_L
Date: Wed, 22 Mar 2017 09:54:11 +0000
Subject: [PATCH 14/58] Add --drop-unused-functions option

The default behaviour of CBMC for the options --show-goto-functions,
--show-properties and --cover is to consider all functions. This
is particularly annoying for --cover where coverage goals are
reported from functions that are trivially unreachable from the entry point.
Also, --show-reachable-properties has been introduced in the past
to hide such properties.
We could change the default behaviour to slicing away everything
that is trivially unreachable from the entry point. However, this would
require an extra option to be able to view all functions and properties.
This commit preserves the default behaviour and enables focussing
the output of --show-goto-functions --show-properties and --cover
on functions that are not trivially unreachable using --drop-unused-functions.
---
 src/cbmc/cbmc_parse_options.cpp   | 9 ++++++++-
 src/cbmc/cbmc_parse_options.h     | 1 +
 src/symex/symex_parse_options.cpp | 9 +++++++++
 src/symex/symex_parse_options.h   | 1 +
 4 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index e33e700e0ca..f5241ed48b1 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -952,8 +952,14 @@ bool cbmc_parse_optionst::process_goto_program(
     // add loop ids
     goto_functions.compute_loop_numbers();
 
-    // instrument cover goals
+    if(cmdline.isset("drop-unused-functions"))
+    {
+      // Entry point will have been set before and function pointers removed
+      status() << "Removing Unused Functions" << eom;
+      remove_unused_functions(goto_functions, ui_message_handler);
+    }
 
+    // instrument cover goals
     if(cmdline.isset("cover"))
     {
       std::list criteria_strings=
@@ -1099,6 +1105,7 @@ void cbmc_parse_optionst::help()
     " --property id                only check one specific property\n"
     " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
     " --trace                      give a counterexample trace for failed properties\n" //NOLINT(*)
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"
     "C/C++ frontend options:\n"
     " -I path                      set include path (C/C++)\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index a3fc5e7e7d3..bcc3b8ac749 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -42,6 +42,7 @@ class optionst;
   "(show-goto-functions)(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
   "(show-claims)(claim):(show-properties)(show-reachable-properties)" \
+  "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 54aa9382759..04135b96d9c 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -34,6 +34,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include 
 #include 
 #include 
+#include 
 
 #include 
 #include 
@@ -383,6 +384,13 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     // add loop ids
     goto_model.goto_functions.compute_loop_numbers();
 
+    if(cmdline.isset("drop-unused-functions"))
+    {
+      // Entry point will have been set before and function pointers removed
+      status() << "Removing Unused Functions" << eom;
+      remove_unused_functions(goto_model.goto_functions, ui_message_handler);
+    }
+
     if(cmdline.isset("cover"))
     {
       std::string criterion=cmdline.get_value("cover");
@@ -683,6 +691,7 @@ void symex_parse_optionst::help()
     " --stop-on-fail               stop analysis once a failed property is detected\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --trace                      give a counterexample trace for failed properties\n"
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"
     "Frontend options:\n"
     " -I path                      set include path (C/C++)\n"
diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h
index a67469d71e5..5e178eec14e 100644
--- a/src/symex/symex_parse_options.h
+++ b/src/symex/symex_parse_options.h
@@ -41,6 +41,7 @@ class optionst;
   "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(show-locs)(show-vcc)(show-properties)" \
+  "(drop-unused-functions)" \
   OPT_SHOW_GOTO_FUNCTIONS \
   "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \
   "(no-simplify)(no-unwinding-assertions)(no-propagation)"

From a35731baa6e38343d75ece15a78acc5846e73875 Mon Sep 17 00:00:00 2001
From: Peter Schrammel 
Date: Thu, 23 Mar 2017 18:44:09 +0000
Subject: [PATCH 15/58] Remove -show-reachable-properties

The same effect can now be achieved by
--show-properties --drop-unused-functions
---
 src/cbmc/cbmc_parse_options.cpp | 13 -------------
 src/cbmc/cbmc_parse_options.h   |  2 +-
 2 files changed, 1 insertion(+), 14 deletions(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index f5241ed48b1..657e4531429 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -540,19 +540,6 @@ int cbmc_parse_optionst::doit()
     return 0; // should contemplate EX_OK from sysexits.h
   }
 
-  // may replace --show-properties
-  if(cmdline.isset("show-reachable-properties"))
-  {
-    const namespacet ns(symbol_table);
-
-    // Entry point will have been set before and function pointers removed
-    status() << "Removing Unused Functions" << eom;
-    remove_unused_functions(goto_functions, ui_message_handler);
-
-    show_properties(ns, get_ui(), goto_functions);
-    return 0; // should contemplate EX_OK from sysexits.h
-  }
-
   if(set_properties(goto_functions))
     return 7; // should contemplate EX_USAGE from sysexits.h
 
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index bcc3b8ac749..5fe9cdd9bf8 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -41,7 +41,7 @@ class optionst;
   "(little-endian)(big-endian)" \
   "(show-goto-functions)(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
-  "(show-claims)(claim):(show-properties)(show-reachable-properties)" \
+  "(show-claims)(claim):(show-properties)" \
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \

From 5e5bbca1d2f1ddf044c4e8d440bfe61ce64f864c Mon Sep 17 00:00:00 2001
From: Peter Schrammel 
Date: Wed, 22 Mar 2017 10:42:04 +0000
Subject: [PATCH 16/58] Correctly align description of option

---
 src/goto-programs/show_goto_functions.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/goto-programs/show_goto_functions.h b/src/goto-programs/show_goto_functions.h
index 5bb7320963e..a496682961e 100644
--- a/src/goto-programs/show_goto_functions.h
+++ b/src/goto-programs/show_goto_functions.h
@@ -19,7 +19,7 @@ class goto_modelt;
   "(show-goto-functions)"
 
 #define HELP_SHOW_GOTO_FUNCTIONS \
-  " --show-goto-functions         show goto program\n"
+  " --show-goto-functions        show goto program\n"
 
 void show_goto_functions(
   const namespacet &ns,

From 85a7566aa8e91be3348bc72bc800239e9dc02f99 Mon Sep 17 00:00:00 2001
From: Peter Schrammel 
Date: Wed, 22 Mar 2017 21:21:15 +0000
Subject: [PATCH 17/58] Option --no-built-in-assertions

This commit changes the behahaviour of --no-assertions so that
only user assertions are ignored.
Built-in assertions can be hidden by the new option
--no-built-in-assertions.
---
 src/analyses/goto_check.cpp             | 9 ++++++---
 src/cbmc/cbmc_parse_options.cpp         | 7 +++++++
 src/cbmc/cbmc_parse_options.h           | 1 +
 src/goto-programs/builtin_functions.cpp | 4 +++-
 4 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 4494aa33e76..7bba83bd298 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -55,6 +55,7 @@ class goto_checkt
     retain_trivial=_options.get_bool_option("retain-trivial");
     enable_assert_to_assume=_options.get_bool_option("assert-to-assume");
     enable_assertions=_options.get_bool_option("assertions");
+    enable_built_in_assertions=_options.get_bool_option("built-in-assertions");
     enable_assumptions=_options.get_bool_option("assumptions");
     error_labels=_options.get_list_option("error-label");
   }
@@ -125,6 +126,7 @@ class goto_checkt
   bool retain_trivial;
   bool enable_assert_to_assume;
   bool enable_assertions;
+  bool enable_built_in_assertions;
   bool enable_assumptions;
 
   typedef optionst::value_listt error_labelst;
@@ -1730,9 +1732,10 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
     }
     else if(i.is_assert())
     {
-      if(i.source_location.get_bool("user-provided") &&
-         i.source_location.get_property_class()!="error label" &&
-         !enable_assertions)
+      bool is_user_provided=i.source_location.get_bool("user-provided");
+      if((is_user_provided && !enable_assertions &&
+          i.source_location.get_property_class()!="error label") ||
+         (!is_user_provided && !enable_built_in_assertions))
         i.type=SKIP;
     }
     else if(i.is_assume())
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index e33e700e0ca..a8081e7c8a2 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -237,6 +237,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   else
     options.set_option("assertions", true);
 
+  // check built-in assertions
+  if(cmdline.isset("no-built-in-assertions"))
+    options.set_option("built-in-assertions", false);
+  else
+    options.set_option("built-in-assertions", true);
+
   // use assumptions
   if(cmdline.isset("no-assumptions"))
     options.set_option("assumptions", false);
@@ -1148,6 +1154,7 @@ void cbmc_parse_optionst::help()
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
     " --no-assertions              ignore user assertions\n"
+    " --no-built-in-assertions     ignore assertions in built-in library\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index a3fc5e7e7d3..fc2c578b69f 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -32,6 +32,7 @@ class optionst;
   "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
+  "(no-built-in-assertions)" \
   "(xml-ui)(xml-interface)(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
   "(no-sat-preprocessor)" \
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 615470b7f9e..1216f9891a9 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -1304,7 +1304,9 @@ void goto_convertt::do_function_call_symbol(
     goto_programt::targett t=dest.add_instruction(ASSERT);
     t->guard=arguments[0];
     t->source_location=function.source_location();
-    t->source_location.set("user-provided", true);
+    t->source_location.set(
+      "user-provided",
+      !function.source_location().is_built_in());
     t->source_location.set_property_class(ID_assertion);
     t->source_location.set_comment(description);
 

From 2b09c0b0b4d611937c48b00f7be74e3128dcf34d Mon Sep 17 00:00:00 2001
From: Owen Jones 
Date: Fri, 24 Mar 2017 11:04:21 +0000
Subject: [PATCH 18/58] Remove unused variable and braces

---
 src/java_bytecode/java_object_factory.cpp | 27 ++++++++++-------------
 1 file changed, 12 insertions(+), 15 deletions(-)

diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 088a25f7038..ea102a52996 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -250,20 +250,18 @@ void java_object_factoryt::gen_nondet_init(
     {
       exprt allocated=
         allocate_object(expr, subtype, loc, create_dynamic_objects);
-      {
-        exprt init_expr;
-        if(allocated.id()==ID_address_of)
-          init_expr=allocated.op0();
-        else
-          init_expr=dereference_exprt(allocated, allocated.type().subtype());
-        gen_nondet_init(
-          init_expr,
-          false,
-          "",
-          loc,
-          false,
-          create_dynamic_objects);
-      }
+      exprt init_expr;
+      if(allocated.id()==ID_address_of)
+        init_expr=allocated.op0();
+      else
+        init_expr=dereference_exprt(allocated, allocated.type().subtype());
+      gen_nondet_init(
+        init_expr,
+        false,
+        "",
+        loc,
+        false,
+        create_dynamic_objects);
     }
 
     if(!assume_non_null)
@@ -592,7 +590,6 @@ exprt object_factory(
 
     exprt object=aux_symbol.symbol_expr();
 
-    const namespacet ns(symbol_table);
     gen_nondet_init(
       object,
       init_code,

From a3f49a341b5e43a104e74feac28c33c574f68545 Mon Sep 17 00:00:00 2001
From: Owen Jones 
Date: Fri, 24 Mar 2017 11:19:20 +0000
Subject: [PATCH 19/58] Move function comments to the right place

---
 src/java_bytecode/java_object_factory.cpp | 53 ++++++++++++-----------
 1 file changed, 28 insertions(+), 25 deletions(-)

diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index ea102a52996..2c22d71e4ac 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -25,18 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_types.h"
 #include "java_utils.h"
 
-/*******************************************************************\
-
-Function: gen_nondet_init
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
 class java_object_factoryt:public messaget
 {
   code_blockt &init_code;
@@ -81,19 +69,15 @@ class java_object_factoryt:public messaget
     const typet &override_type=empty_typet());
 };
 
-
 /*******************************************************************\
 
-Function: gen_nondet_array_init
+Function: java_object_factoryt::allocate_object
 
-  Inputs: the target expression, desired object type, source location
-          and Boolean whether to create a dynamic object
+  Inputs:
 
- Outputs: the allocated object
+ Outputs:
 
- Purpose: Returns false if we can't figure out the size of allocate_type.
-          allocate_type may differ from target_expr, e.g. for target_expr
-          having type int* and allocate_type being an int[10].
+ Purpose:
 
 \*******************************************************************/
 
@@ -165,10 +149,29 @@ exprt java_object_factoryt::allocate_object(
   }
 }
 
-// Override type says to ignore the LHS' real type, and init it with the given
-// type regardless. Used at the moment for reference arrays, which are
-// implemented as void* arrays but should be init'd as their true type with
-// appropriate casts.
+/*******************************************************************\
+
+Function: java_object_factoryt::gen_nondet_init
+
+  Inputs:
+   expr -
+   is_sub -
+   class_identifier -
+   loc -
+   skip_classid -
+   create_dynamic_objects -
+   override - Ignore the LHS' real type. Used at the moment for
+              reference arrays, which are implemented as void*
+              arrays but should be init'd as their true type with
+              appropriate casts.
+   override_type - Type to use if ignoring the LHS' real type
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
 void java_object_factoryt::gen_nondet_init(
   const exprt &expr,
   bool is_sub,
@@ -343,7 +346,7 @@ void java_object_factoryt::gen_nondet_init(
 
 /*******************************************************************\
 
-Function: gen_nondet_array_init
+Function: java_object_factoryt::gen_nondet_array_init
 
   Inputs:
 

From 4c4ccc032919a94753e824c892155a8ca9d55f4a Mon Sep 17 00:00:00 2001
From: Owen Jones 
Date: Fri, 24 Mar 2017 12:04:19 +0000
Subject: [PATCH 20/58] Remove variable that is always false

skip_classid was always false, so there wasn't any point having it.
---
 src/java_bytecode/java_object_factory.cpp | 14 +-------------
 src/java_bytecode/java_object_factory.h   |  1 -
 2 files changed, 1 insertion(+), 14 deletions(-)

diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 2c22d71e4ac..602bc4bb497 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -63,7 +63,6 @@ class java_object_factoryt:public messaget
     bool is_sub,
     irep_idt class_identifier,
     const source_locationt &loc,
-    bool skip_classid,
     bool create_dynamic_objects,
     bool override=false,
     const typet &override_type=empty_typet());
@@ -158,7 +157,6 @@ Function: java_object_factoryt::gen_nondet_init
    is_sub -
    class_identifier -
    loc -
-   skip_classid -
    create_dynamic_objects -
    override - Ignore the LHS' real type. Used at the moment for
               reference arrays, which are implemented as void*
@@ -177,7 +175,6 @@ void java_object_factoryt::gen_nondet_init(
   bool is_sub,
   irep_idt class_identifier,
   const source_locationt &loc,
-  bool skip_classid,
   bool create_dynamic_objects,
   bool override,
   const typet &override_type)
@@ -263,7 +260,6 @@ void java_object_factoryt::gen_nondet_init(
         false,
         "",
         loc,
-        false,
         create_dynamic_objects);
     }
 
@@ -298,9 +294,6 @@ void java_object_factoryt::gen_nondet_init(
 
       if(name=="@class_identifier")
       {
-        if(skip_classid)
-          continue;
-
         irep_idt qualified_clsid="java::"+as_string(class_identifier);
         constant_exprt ci(qualified_clsid, string_typet());
         code_assignt code(me, ci);
@@ -328,7 +321,6 @@ void java_object_factoryt::gen_nondet_init(
           _is_sub,
           class_identifier,
           loc,
-          false,
           create_dynamic_objects);
       }
     }
@@ -380,7 +372,7 @@ void java_object_factoryt::gen_nondet_array_init(
   const auto &length_sym_expr=length_sym.symbol_expr();
 
   // Initialize array with some undetermined length:
-  gen_nondet_init(length_sym_expr, false, irep_idt(), loc, false, false);
+  gen_nondet_init(length_sym_expr, false, irep_idt(), loc, false);
 
   // Insert assumptions to bound its length:
   binary_relation_exprt
@@ -465,7 +457,6 @@ void java_object_factoryt::gen_nondet_array_init(
     false,
     irep_idt(),
     loc,
-    false,
     true,
     true,
     element_type);
@@ -495,7 +486,6 @@ void gen_nondet_init(
   code_blockt &init_code,
   symbol_tablet &symbol_table,
   const source_locationt &loc,
-  bool skip_classid,
   bool create_dyn_objs,
   bool assume_non_null,
   message_handlert &message_handler,
@@ -512,7 +502,6 @@ void gen_nondet_init(
     false,
     "",
     loc,
-    skip_classid,
     create_dyn_objs);
 }
 
@@ -599,7 +588,6 @@ exprt object_factory(
       symbol_table,
       loc,
       false,
-      false,
       !allow_null,
       message_handler,
       max_nondet_array_length);
diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h
index 6122d3e2780..5141ca45f42 100644
--- a/src/java_bytecode/java_object_factory.h
+++ b/src/java_bytecode/java_object_factory.h
@@ -27,7 +27,6 @@ void gen_nondet_init(
   code_blockt &init_code,
   symbol_tablet &symbol_table,
   const source_locationt &,
-  bool skip_classid,
   bool create_dynamic_objects,
   bool assume_non_null,
   message_handlert &message_handler,

From 9a1dae0323dad1f71ca7a946e4ee8c41596982b6 Mon Sep 17 00:00:00 2001
From: Owen Jones 
Date: Fri, 24 Mar 2017 15:05:50 +0000
Subject: [PATCH 21/58] Remove function that's only used once

gen_nondet_init() is only used once, and is only two lines long,
so get rid of it and just put those two lines. This also avoids
confusion with java_object_factory::gen_nondet_init().
---
 src/java_bytecode/java_object_factory.cpp | 51 ++++-------------------
 src/java_bytecode/java_object_factory.h   | 11 -----
 2 files changed, 9 insertions(+), 53 deletions(-)

diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 602bc4bb497..166be7827c9 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -471,42 +471,6 @@ void java_object_factoryt::gen_nondet_array_init(
 
 /*******************************************************************\
 
-Function: gen_nondet_init
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void gen_nondet_init(
-  const exprt &expr,
-  code_blockt &init_code,
-  symbol_tablet &symbol_table,
-  const source_locationt &loc,
-  bool create_dyn_objs,
-  bool assume_non_null,
-  message_handlert &message_handler,
-  size_t max_nondet_array_length)
-{
-  java_object_factoryt state(
-    init_code,
-    assume_non_null,
-    max_nondet_array_length,
-    symbol_table,
-    message_handler);
-  state.gen_nondet_init(
-    expr,
-    false,
-    "",
-    loc,
-    create_dyn_objs);
-}
-
-/*******************************************************************\
-
 Function: new_tmp_symbol
 
   Inputs:
@@ -582,15 +546,18 @@ exprt object_factory(
 
     exprt object=aux_symbol.symbol_expr();
 
-    gen_nondet_init(
-      object,
+    java_object_factoryt state(
       init_code,
+      !allow_null,
+      max_nondet_array_length,
       symbol_table,
-      loc,
+      message_handler);
+    state.gen_nondet_init(
+      object,
       false,
-      !allow_null,
-      message_handler,
-      max_nondet_array_length);
+      "",
+      loc,
+      false);
 
     return object;
   }
diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h
index 5141ca45f42..37ed40f0ec9 100644
--- a/src/java_bytecode/java_object_factory.h
+++ b/src/java_bytecode/java_object_factory.h
@@ -22,17 +22,6 @@ exprt object_factory(
   const source_locationt &,
   message_handlert &message_handler);
 
-void gen_nondet_init(
-  const exprt &expr,
-  code_blockt &init_code,
-  symbol_tablet &symbol_table,
-  const source_locationt &,
-  bool create_dynamic_objects,
-  bool assume_non_null,
-  message_handlert &message_handler,
-  size_t max_nondet_array_length=5);
-
-
 exprt get_nondet_bool(const typet &);
 
 symbolt &new_tmp_symbol(

From 27227ccd96e9318c0b35f5c3049a7f75f6db2096 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro 
Date: Fri, 24 Mar 2017 12:58:06 +0000
Subject: [PATCH 22/58] added support for array_copy in the full-slice option

Do not slice away array_copy expressions during the implicit call
in the full-slicert class. We do not process array_copy in value_set_fit.
---
 src/goto-instrument/full_slicer.cpp   | 4 ++++
 src/pointer-analysis/value_set_fi.cpp | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 59bda7f0af0..f7b42a0af3c 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -337,6 +337,10 @@ static bool implicit(goto_programt::const_targett target)
 {
   // some variables are used during symbolic execution only
 
+  const irep_idt &statement=target->code.get_statement();
+  if(statement==ID_array_copy)
+    return true;
+
   if(!target->is_assign())
     return false;
 
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 125a2cae58a..55542296c48 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -1729,6 +1729,9 @@ void value_set_fit::apply_code(
   else if(statement==ID_fence)
   {
   }
+  else if(statement==ID_array_copy)
+  {
+  }
   else if(statement==ID_input || statement==ID_output)
   {
     // doesn't do anything

From e70aa7d261f3b721d1844c5f4f498bb82b59ebc3 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro 
Date: Fri, 24 Mar 2017 12:55:12 +0000
Subject: [PATCH 23/58] added two test cases into goto-instrument regression
 for checking array_copy

added two test cases related to array copy in the goto-instrument
regression suite to further test the full-slice option
---
 regression/goto-instrument/slice22/main.c    | 19 +++++++++++++++
 regression/goto-instrument/slice22/test.desc |  6 +++++
 regression/goto-instrument/slice23/main.c    | 25 ++++++++++++++++++++
 regression/goto-instrument/slice23/test.desc |  6 +++++
 4 files changed, 56 insertions(+)
 create mode 100644 regression/goto-instrument/slice22/main.c
 create mode 100644 regression/goto-instrument/slice22/test.desc
 create mode 100644 regression/goto-instrument/slice23/main.c
 create mode 100644 regression/goto-instrument/slice23/test.desc

diff --git a/regression/goto-instrument/slice22/main.c b/regression/goto-instrument/slice22/main.c
new file mode 100644
index 00000000000..bac167b63d3
--- /dev/null
+++ b/regression/goto-instrument/slice22/main.c
@@ -0,0 +1,19 @@
+#include 
+#include 
+
+int main()
+{
+  int *ptr=malloc(sizeof(int));
+  *ptr=42;
+  ptr=realloc(ptr, 20);
+  assert(*ptr==42);
+
+  int *ptr2=malloc(2*sizeof(int));
+  *ptr2=42;
+  *(ptr2+1)=42;
+  ptr2=realloc(ptr2, 20);
+  assert(*ptr2==42);
+  assert(*(ptr2+1)==42);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice22/test.desc b/regression/goto-instrument/slice22/test.desc
new file mode 100644
index 00000000000..50181efa86b
--- /dev/null
+++ b/regression/goto-instrument/slice22/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/goto-instrument/slice23/main.c b/regression/goto-instrument/slice23/main.c
new file mode 100644
index 00000000000..d165e2c38b8
--- /dev/null
+++ b/regression/goto-instrument/slice23/main.c
@@ -0,0 +1,25 @@
+#include 
+#include 
+
+void foo(int argc)
+{
+  void* x=0;
+
+  if(argc>3)
+    x=malloc(4*sizeof(int));
+  else
+    x=malloc(3*sizeof(int));
+  *(int*)x=42;
+
+  x=realloc(x, sizeof(int));
+
+  assert(*(int*)x==42);
+}
+
+int main(int argc, char* argv[])
+{
+//__CPROVER_ASYNC_1:
+  foo(argc);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice23/test.desc b/regression/goto-instrument/slice23/test.desc
new file mode 100644
index 00000000000..50181efa86b
--- /dev/null
+++ b/regression/goto-instrument/slice23/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

From 83874c3624713ad5babd2238e06f9b7ada52864b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Fri, 24 Mar 2017 19:16:52 +0000
Subject: [PATCH 24/58] Release notes up to 5.6 from CProver Google group
 messages

---
 CHANGELOG | 69 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)

diff --git a/CHANGELOG b/CHANGELOG
index 4052fe87941..d0f6a04a558 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,72 @@
+5.6
+===
+
+Bugfixes in the C, C++, Java front-ends.
+
+
+5.5
+===
+
+This is a major release, with significant changes. The option
+--all-properties is now the default; to restore the previous behaviour,
+use --stop-on-fail. The primary area of attention was again the Java
+front-end. We have furthermore added test-suite generation for branch
+coverage, location coverage, condition coverage, decision coverage and
+MC/DC.
+
+
+5.4
+===
+
+This is a minor release, focused primarily on maintenance. The primary
+area of attention was again the Java front-end. We have also updated to
+Minisat 2.2.1.
+
+
+5.3
+===
+
+This is a minor release, focused primarily on maintenance. The primary
+area of attention is the Java front-end.
+
+
+5.2
+===
+
+This is a minor release, focused primarily on maintenance. The primary
+areas of attention are the full slicer, the Java frontend, test suite
+generation and support for the Glucose solver.
+
+
+5.1
+===
+
+This is a minor release, focused primarily on maintenance. Support for solving
+floating-point problems using for SMT-LIB2 solvers without support for the
+floating-point theory has been added.
+
+
+5.0
+===
+
+This is a major release, focused primarily on performance improvements.
+Furthermore, the support for the floating-point theory for SMT-LIB2 has been
+improved substantially. This release breaks compatibility with the goto-binary
+format used by earlier releases; i.e., you will need to rebuild your
+goto-binaries.
+
+
+4.9
+===
+
+This release is primarily for maintenance purposes and does not add any major
+new features. The support for SMT-LIB2 solvers has been improved substantially.
+
+
+4.8
+===
+
+
 4.7
 ===
 

From 81470f46b6aa1dd9e82b40226b44e3484db62968 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Fri, 24 Mar 2017 19:19:36 +0000
Subject: [PATCH 25/58] Initial version of release notes for 5.7

---
 CHANGELOG | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/CHANGELOG b/CHANGELOG
index d0f6a04a558..ba9ceda5549 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,27 @@
+5.7
+===
+
+* General: All tools now support the same set of --*-check options.
+* General: Added --conversion-check to catch type casts that cause loss of
+  information. Previously --(un)signed-overflow-check would report these.
+* CBMC: New option --symex-coverage-report to produce a Cobertura-compatible
+  statement- and branch coverage report.
+* CBMC/Java: New options --java-max-vla-length, --java-unwind-enum-static,
+  --java-cp-include-files, --lazy-methods.
+* GOTO-INSTRUMENT: Static loop unwinding via --unwind or via new options
+  --unwindset, --unwindset-file, --unwinding-assertions, --partial-loops,
+  --continue-as-loops, --log
+* GOTO-INSTRUMENT: New option --slice-global-inits
+* GOTO-INSTRUMENT: Inlining via --inline, --partial-inline, --function-inline,
+  --no-caching
+* GOTO-INSTRUMENT: New options --remove-function-pointers, --model-argc-argv,
+  --show-threaded
+* GOTO-CC: Additional drop-in replacement support for bcc, as, as86
+* GOTO-CC: GCC-style error/warning messages
+* GOTO-CC: New options --native-compiler and --native-linker to select the
+  compiler/linker to be used when building combined native/goto object files.
+
+
 5.6
 ===
 

From ad384f11927d08bf4f705fee8085942f4536a3a8 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro 
Date: Mon, 27 Mar 2017 14:37:19 +0100
Subject: [PATCH 26/58] kept consistency between parse options of cbmc and
 goto-instrument tools

Display the architecture information if the user intends to add the CPROVER
library for code instrumentation. As a result, the status message is now part
of the link_to_library implementation to avoid redundant code for the respective
library call.
---
 src/cbmc/cbmc_parse_options.cpp                       | 2 --
 src/clobber/clobber_parse_options.cpp                 | 1 -
 src/goto-analyzer/goto_analyzer_parse_options.cpp     | 2 --
 src/goto-diff/goto_diff_parse_options.cpp             | 2 --
 src/goto-instrument/goto_instrument_parse_options.cpp | 2 +-
 src/goto-programs/link_to_library.cpp                 | 7 +++++++
 src/musketeer/musketeer_parse_options.cpp             | 1 -
 src/symex/symex_parse_options.cpp                     | 1 -
 8 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index b69ab532204..caf0795e640 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -872,8 +872,6 @@ bool cbmc_parse_optionst::process_goto_program(
     remove_asm(symbol_table, goto_functions);
 
     // add the library
-    status() << "Adding CPROVER library ("
-             << config.ansi_c.arch << ")" << eom;
     link_to_library(symbol_table, goto_functions, ui_message_handler);
 
     if(cmdline.isset("string-abstraction"))
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 4ac42666639..803ab9db5b1 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -368,7 +368,6 @@ bool clobber_parse_optionst::get_goto_program(
 
     // finally add the library
     #if 0
-    status() << "Adding CPROVER library" << eom;
     link_to_library(symbol_table, goto_functions, ui_message_handler);
     #endif
 
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index e462740c1cc..bceddfadc54 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -378,8 +378,6 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     remove_asm(goto_model);
 
     // add the library
-    status() << "Adding CPROVER library ("
-             << config.ansi_c.arch << ")" << eom;
     link_to_library(goto_model, ui_message_handler);
     #endif
 
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index a405178652f..1ba3d96a9d4 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -480,8 +480,6 @@ bool goto_diff_parse_optionst::process_goto_program(
     remove_asm(symbol_table, goto_functions);
 
     // add the library
-    status() << "Adding CPROVER library ("
-             << config.ansi_c.arch << ")" << eom;
     link_to_library(symbol_table, goto_functions, ui_message_handler);
 
     // remove function pointers
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index b5486355277..d2173398e4f 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -983,7 +983,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
        cmdline.isset("custom-bitvector-analysis"))
       config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS");
 
-    status() << "Adding CPROVER library" << eom;
+    // add the library
     link_to_library(symbol_table, goto_functions, ui_message_handler);
   }
 
diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp
index 46cd45c36da..c3ead7e6ecb 100644
--- a/src/goto-programs/link_to_library.cpp
+++ b/src/goto-programs/link_to_library.cpp
@@ -6,6 +6,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
+#include 
+
 #include 
 
 #include "link_to_library.h"
@@ -54,6 +56,11 @@ void link_to_library(
   // this needs a fixedpoint, as library functions
   // may depend on other library functions
 
+  messaget message(message_handler);
+
+  message.status() << "Adding CPROVER library ("
+                   << config.ansi_c.arch << ")" << messaget::eom;
+
   std::set added_functions;
 
   while(true)
diff --git a/src/musketeer/musketeer_parse_options.cpp b/src/musketeer/musketeer_parse_options.cpp
index 707ec50bd0b..9114b8d7802 100644
--- a/src/musketeer/musketeer_parse_options.cpp
+++ b/src/musketeer/musketeer_parse_options.cpp
@@ -200,7 +200,6 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program(
 
   // we add the library, as some analyses benefit
 
-  status() << "Adding CPROVER library" << eom;
   link_to_library(symbol_table, goto_functions, ui_message_handler);
 
   namespacet ns(symbol_table);
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 04135b96d9c..2b3f00a9bed 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -355,7 +355,6 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
   try
   {
     // we add the library
-    status() << "Adding CPROVER library" << eom;
     link_to_library(goto_model, ui_message_handler);
 
     // do partial inlining

From 13dfd5abf748459da2ea7a59cceeaccab903ff59 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Tue, 1 Mar 2016 13:29:44 +0000
Subject: [PATCH 27/58] make_binary is not safe to use when types are mixed

Removed use of make_binary in pointer contexts, as pointer arithmetic
yields expressions that include pointer and non-pointer type operands,
with the overall expression type being that of the pointer.
---
 src/analyses/local_bitvector_analysis.cpp |  4 +++-
 src/analyses/local_may_alias.cpp          |  4 ++--
 src/pointer-analysis/dereference.cpp      | 14 ++++++++++----
 src/util/expr_util.cpp                    |  6 ++++++
 4 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index 43cb5c1d360..3fc0d10bb09 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -253,7 +253,9 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
   {
     if(rhs.operands().size()>=3)
     {
-      return get_rec(make_binary(rhs), loc_info_src);
+      assert(rhs.op0().type().id()==ID_pointer);
+      return get_rec(rhs.op0(), loc_info_src) |
+             flagst::mk_uses_offset();
     }
     else if(rhs.operands().size()==2)
     {
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index 53d089b9544..ffaefe73667 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include 
 #include 
 #include 
-#include 
 
 #include 
 #include 
@@ -309,7 +308,8 @@ void local_may_aliast::get_rec(
   {
     if(rhs.operands().size()>=3)
     {
-      get_rec(dest, make_binary(rhs), loc_info_src);
+      assert(rhs.op0().type().id()==ID_pointer);
+      get_rec(dest, rhs.op0(), loc_info_src);
     }
     else if(rhs.operands().size()==2)
     {
diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp
index b21313f85bf..bd9db73dfb4 100644
--- a/src/pointer-analysis/dereference.cpp
+++ b/src/pointer-analysis/dereference.cpp
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #endif
 
 #include 
-#include 
 #include 
 #include 
 #include 
@@ -279,11 +278,18 @@ exprt dereferencet::dereference_plus(
   const exprt &offset,
   const typet &type)
 {
+  exprt pointer=expr.op0();
+  exprt integer=expr.op1();
+
+  // need not be binary
   if(expr.operands().size()>2)
-    return dereference_rec(make_binary(expr), offset, type);
+  {
+    assert(expr.op0().type().id()==ID_pointer);
 
-  // binary
-  exprt pointer=expr.op0(), integer=expr.op1();
+    exprt::operandst plus_ops(
+      ++expr.operands().begin(), expr.operands().end());
+    integer.operands().swap(plus_ops);
+  }
 
   if(ns.follow(integer.type()).id()==ID_pointer)
     std::swap(pointer, integer);
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index f5abbc06c28..d5a28e4f5fa 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -55,13 +55,19 @@ exprt make_binary(const exprt &expr)
   if(operands.size()<=2)
     return expr;
 
+  // types must be identical for make_binary to be safe to use
+  const typet &type=expr.type();
+
   exprt previous=operands.front();
+  assert(previous.type()==type);
 
   for(exprt::operandst::const_iterator
       it=++operands.begin();
       it!=operands.end();
       ++it)
   {
+    assert(it->type()==type);
+
     exprt tmp=expr;
     tmp.operands().clear();
     tmp.operands().resize(2);

From b4ae91605603f8a4e5c086ee7141eed268d7bb4e Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro 
Date: Mon, 27 Mar 2017 13:09:13 +0100
Subject: [PATCH 28/58] Enabled test cases in goto-instrument after fixes in
 the full-slice

Enabled test cases slice01, slice13, and slice16 in the goto-instrument regression
suite after fixes related to commits 27227cc and 211cb90.
---
 regression/goto-instrument/slice01/test.desc | 4 ++--
 regression/goto-instrument/slice13/main.c    | 2 ++
 regression/goto-instrument/slice13/test.desc | 6 ++----
 regression/goto-instrument/slice16/test.desc | 4 +---
 4 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/regression/goto-instrument/slice01/test.desc b/regression/goto-instrument/slice01/test.desc
index 76cbcfa81bd..73b1ad786c4 100644
--- a/regression/goto-instrument/slice01/test.desc
+++ b/regression/goto-instrument/slice01/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---unwind 2 --full-slice
+--unwind 2 --full-slice --add-library
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/goto-instrument/slice13/main.c b/regression/goto-instrument/slice13/main.c
index 3354961512a..a24498017a7 100644
--- a/regression/goto-instrument/slice13/main.c
+++ b/regression/goto-instrument/slice13/main.c
@@ -17,7 +17,9 @@ void test (int mode, double d, float result) {
 
 int main (void)
 {
+#ifdef __GNUC__
   // Nearer to 0x1.fffffep+127 than to 0x1.000000p+128
   test(FE_UPWARD, 0x1.fffffe0000001p+127, +INFINITY);
+#endif
   return 1;
 }
diff --git a/regression/goto-instrument/slice13/test.desc b/regression/goto-instrument/slice13/test.desc
index cc8dd41ed5f..50181efa86b 100644
--- a/regression/goto-instrument/slice13/test.desc
+++ b/regression/goto-instrument/slice13/test.desc
@@ -1,8 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---floatbv --full-slice
+--full-slice --add-library
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/goto-instrument/slice16/test.desc b/regression/goto-instrument/slice16/test.desc
index 846baaf2a8b..ab6fd2dd827 100644
--- a/regression/goto-instrument/slice16/test.desc
+++ b/regression/goto-instrument/slice16/test.desc
@@ -1,8 +1,6 @@
-KNOWNBUG
+CORE
 main.c
 --full-slice --unwind 2
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring

From e333f8de80147b0d2145d75b3d9c37b6daf19170 Mon Sep 17 00:00:00 2001
From: Chris Smowton 
Date: Tue, 28 Mar 2017 15:57:42 +0100
Subject: [PATCH 29/58] Tolerate missing symbols in gather_needed_globals.
 Fixes #620

Symbols can be missing at this stage because they would be introduced during
typechecking when it notices they are undefined, which happens if the type
they were defined on is missing.
---
 src/java_bytecode/java_bytecode_language.cpp | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 0e2eb25d0ec..f94025bb57b 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -387,9 +387,16 @@ static void gather_needed_globals(
 {
   if(e.id()==ID_symbol)
   {
-    const auto &sym=symbol_table.lookup(to_symbol_expr(e).get_identifier());
-    if(sym.is_static_lifetime)
-      needed.add(sym);
+    // If the symbol isn't in the symbol table at all, then it is defined
+    // on an opaque type (i.e. we don't have the class definition at this point)
+    // and will be created during the typecheck phase.
+    // We don't mark it as 'needed' as it doesn't exist yet to keep.
+    auto findit=symbol_table.symbols.find(to_symbol_expr(e).get_identifier());
+    if(findit!=symbol_table.symbols.end() &&
+       findit->second.is_static_lifetime)
+    {
+      needed.add(findit->second);
+    }
   }
   else
     forall_operands(opit, e)

From a8a5eb138e0720d89a167f2e1fc981663f2c3474 Mon Sep 17 00:00:00 2001
From: reuk 
Date: Tue, 28 Mar 2017 16:00:32 +0100
Subject: [PATCH 30/58] Remove reserved identifier

Identifiers containing a double-underscore are reserved for the implementation.
---
 src/langapi/language_ui.cpp | 4 ++--
 src/langapi/language_ui.h   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index 95b5d104a4f..2c4019a253c 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -31,10 +31,10 @@ Function: language_uit::language_uit
 \*******************************************************************/
 
 language_uit::language_uit(
-  const cmdlinet &__cmdline,
+  const cmdlinet &cmdline,
   ui_message_handlert &_ui_message_handler):
   ui_message_handler(_ui_message_handler),
-  _cmdline(__cmdline)
+  _cmdline(cmdline)
 {
   set_message_handler(ui_message_handler);
 }
diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h
index 90c1de3e5cb..b82507f4c75 100644
--- a/src/langapi/language_ui.h
+++ b/src/langapi/language_ui.h
@@ -23,7 +23,7 @@ class language_uit:public messaget
   symbol_tablet symbol_table;
 
   language_uit(
-    const cmdlinet &__cmdline,
+    const cmdlinet &cmdline,
     ui_message_handlert &ui_message_handler);
   virtual ~language_uit();
 

From f9aac34f3b8e6387a3de5a2b3ddbada140979837 Mon Sep 17 00:00:00 2001
From: Chris Smowton 
Date: Tue, 28 Mar 2017 16:50:23 +0100
Subject: [PATCH 31/58] Avoid duplicate callee class-ids in virtual dispatch
 tables. Fixes #684

These were introduced because remove-virtual-functions' class hierarchy
walk assumed it was tree-structured, but Java interfaces show up in the
graph like multiple inheritence and falsify that assumption. This simply
truncates the walk when class IDs have been seen before.
---
 .../remove_virtual_functions.cpp              | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index c93b50a2500..fde2f5f8405 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -57,8 +57,11 @@ class remove_virtual_functionst
   typedef std::vector functionst;
   void get_functions(const exprt &, functionst &);
   void get_child_functions_rec(
-    const irep_idt &, const symbol_exprt &,
-    const irep_idt &, functionst &) const;
+    const irep_idt &,
+    const symbol_exprt &,
+    const irep_idt &,
+    functionst &,
+    std::set &visited) const;
   exprt get_method(
     const irep_idt &class_id,
     const irep_idt &component_name) const;
@@ -254,7 +257,8 @@ void remove_virtual_functionst::get_child_functions_rec(
   const irep_idt &this_id,
   const symbol_exprt &last_method_defn,
   const irep_idt &component_name,
-  functionst &functions) const
+  functionst &functions,
+  std::set &visited) const
 {
   auto findit=class_hierarchy.class_map.find(this_id);
   if(findit==class_hierarchy.class_map.end())
@@ -262,6 +266,8 @@ void remove_virtual_functionst::get_child_functions_rec(
 
   for(const auto &child : findit->second.children)
   {
+    if(!visited.insert(child).second)
+      continue;
     exprt method=get_method(child, component_name);
     functiont function(child);
     if(method.is_not_nil())
@@ -279,7 +285,8 @@ void remove_virtual_functionst::get_child_functions_rec(
       child,
       function.symbol_expr,
       component_name,
-      functions);
+      functions,
+      visited);
   }
 }
 
@@ -333,11 +340,13 @@ void remove_virtual_functionst::get_functions(
   }
 
   // iterate over all children, transitively
+  std::set visited;
   get_child_functions_rec(
     class_id,
     root_function.symbol_expr,
     component_name,
-    functions);
+    functions,
+    visited);
 
   if(root_function.symbol_expr!=symbol_exprt())
     functions.push_back(root_function);

From 02c77a424352099394bba795c7a2ef1121b63fc7 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis 
Date: Tue, 28 Mar 2017 18:20:27 +0100
Subject: [PATCH 32/58] Added tests that demonstrate the issue with static
 inline c functions.

---
 regression/ansi-c/static_inline1/main.c    | 11 +++++++++++
 regression/ansi-c/static_inline1/test.desc |  9 +++++++++
 regression/ansi-c/static_inline2/main.c    |  4 ++++
 regression/ansi-c/static_inline2/test.desc |  9 +++++++++
 4 files changed, 33 insertions(+)
 create mode 100644 regression/ansi-c/static_inline1/main.c
 create mode 100644 regression/ansi-c/static_inline1/test.desc
 create mode 100644 regression/ansi-c/static_inline2/main.c
 create mode 100644 regression/ansi-c/static_inline2/test.desc

diff --git a/regression/ansi-c/static_inline1/main.c b/regression/ansi-c/static_inline1/main.c
new file mode 100644
index 00000000000..ba8e8c6fb6b
--- /dev/null
+++ b/regression/ansi-c/static_inline1/main.c
@@ -0,0 +1,11 @@
+inline static int fun(int a)
+{
+    return a+1;
+}
+
+int main(int argc, char *argv[])
+{
+    fun(5);
+    return 0;
+}
+
diff --git a/regression/ansi-c/static_inline1/test.desc b/regression/ansi-c/static_inline1/test.desc
new file mode 100644
index 00000000000..5717777037a
--- /dev/null
+++ b/regression/ansi-c/static_inline1/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+
+--
+^warning: ignoring
diff --git a/regression/ansi-c/static_inline2/main.c b/regression/ansi-c/static_inline2/main.c
new file mode 100644
index 00000000000..c67e498b4f5
--- /dev/null
+++ b/regression/ansi-c/static_inline2/main.c
@@ -0,0 +1,4 @@
+inline static int fun(int a)
+{
+    return a+1;
+}
diff --git a/regression/ansi-c/static_inline2/test.desc b/regression/ansi-c/static_inline2/test.desc
new file mode 100644
index 00000000000..c5c5692745d
--- /dev/null
+++ b/regression/ansi-c/static_inline2/test.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--function fun
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+
+--
+^warning: ignoring

From 6824297fe8eac5294f53254366bb21e5967adc1e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Mon, 27 Jun 2016 12:50:25 +0000
Subject: [PATCH 33/58] Include --verbosity in help output of cbmc and symex

Signed-off-by: Michael Tautschnig 
CC: Norbert Manthey 

CR: https://cr.amazon.com/r/5473586/
---
 src/cbmc/cbmc_parse_options.cpp   | 1 +
 src/symex/symex_parse_options.cpp | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index caf0795e640..39a595e596d 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -1199,5 +1199,6 @@ void cbmc_parse_optionst::help()
     " --xml-ui                     use XML-formatted output\n"
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
+    " --verbosity #                verbosity level\n"
     "\n";
 }
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 2b3f00a9bed..5e547a19dff 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -738,5 +738,6 @@ void symex_parse_optionst::help()
     "Other options:\n"
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
+    " --verbosity #                verbosity level\n"
     "\n";
 }

From 090dfce65ead7fc913e16e3a8bc987a76f037bcb Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Mon, 27 Mar 2017 08:14:13 +0100
Subject: [PATCH 34/58] fixup! Add json->irep deserialization routine

---
 src/util/json_irep.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/util/json_irep.cpp b/src/util/json_irep.cpp
index 403247c1d04..2740228d1db 100644
--- a/src/util/json_irep.cpp
+++ b/src/util/json_irep.cpp
@@ -164,8 +164,8 @@ void json_irept::convert_from_json(const jsont &in, irept &out) const
   }
 
   for(const auto &named_sub : in["namedSub"].object)
-    convert_from_json(named_sub.second, out.get_named_sub()[named_sub.first]);
+    convert_from_json(named_sub.second, out.add(named_sub.first));
 
   for(const auto &comment : in["comment"].object)
-    convert_from_json(comment.second, out.get_comments()[comment.first]);
+    convert_from_json(comment.second, out.add(comment.first));
 }

From d658c0c0ec5e8352140b2f080e8ccf33d1c3d5a6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Mon, 27 Mar 2017 08:29:41 +0000
Subject: [PATCH 35/58] Throw when -DNDEBUG would cause missing return values

---
 src/solvers/flattening/boolbv_floatbv_op.cpp | 2 +-
 src/solvers/floatbv/float_utils.cpp          | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/solvers/flattening/boolbv_floatbv_op.cpp b/src/solvers/flattening/boolbv_floatbv_op.cpp
index 087faa0485a..e4926dc617e 100644
--- a/src/solvers/flattening/boolbv_floatbv_op.cpp
+++ b/src/solvers/flattening/boolbv_floatbv_op.cpp
@@ -138,7 +138,7 @@ bvt boolbvt::convert_floatbv_op(const exprt &expr)
     else if(expr.id()==ID_floatbv_rem)
       return float_utils.rem(bv0, bv1);
     else
-      assert(false);
+      throw "unexpected operator "+expr.id_string();
   }
   else if(type.id()==ID_vector || type.id()==ID_complex)
   {
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
index c277e51e6b0..a772ae0b8a7 100644
--- a/src/solvers/floatbv/float_utils.cpp
+++ b/src/solvers/floatbv/float_utils.cpp
@@ -206,7 +206,7 @@ bvt float_utilst::to_integer(
     return result;
   }
   else
-    assert(0);
+    throw "unsupported rounding mode";
 }
 
 /*******************************************************************\

From b5e97ae6ebdb2328d8383a593ce7351ceafada13 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Mon, 27 Mar 2017 09:32:49 +0100
Subject: [PATCH 36/58] fixup! Add --drop-unused-functions option

---
 CHANGELOG                                             | 2 ++
 src/cbmc/cbmc_parse_options.cpp                       | 4 ++--
 src/goto-instrument/goto_instrument_parse_options.cpp | 8 ++++++++
 src/goto-instrument/goto_instrument_parse_options.h   | 1 +
 src/symex/symex_parse_options.cpp                     | 4 ++--
 5 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG b/CHANGELOG
index ba9ceda5549..61489b8fb41 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -20,6 +20,8 @@
 * GOTO-CC: GCC-style error/warning messages
 * GOTO-CC: New options --native-compiler and --native-linker to select the
   compiler/linker to be used when building combined native/goto object files.
+* CBMC, SYMEX, GOTO-INSTRUMENT: New option --drop-unused-functions. Removed
+  ambiguous --show-reachable-properties.
 
 
 5.6
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 39a595e596d..721520e48fa 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -946,7 +946,7 @@ bool cbmc_parse_optionst::process_goto_program(
     if(cmdline.isset("drop-unused-functions"))
     {
       // Entry point will have been set before and function pointers removed
-      status() << "Removing Unused Functions" << eom;
+      status() << "Removing unused functions" << eom;
       remove_unused_functions(goto_functions, ui_message_handler);
     }
 
@@ -1096,7 +1096,6 @@ void cbmc_parse_optionst::help()
     " --property id                only check one specific property\n"
     " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
     " --trace                      give a counterexample trace for failed properties\n" //NOLINT(*)
-    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"
     "C/C++ frontend options:\n"
     " -I path                      set include path (C/C++)\n"
@@ -1142,6 +1141,7 @@ void cbmc_parse_optionst::help()
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index d2173398e4f..dda6b1ea302 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -744,6 +744,14 @@ int goto_instrument_parse_optionst::doit()
       return 0;
     }
 
+    if(cmdline.isset("drop-unused-functions"))
+    {
+      do_indirect_call_and_rtti_removal();
+
+      status() << "Removing unused functions" << eom;
+      remove_unused_functions(goto_functions, get_message_handler());
+    }
+
     // write new binary?
     if(cmdline.args.size()==2)
     {
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index d3efb975767..180eeb7a2f5 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -45,6 +45,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(stack-depth):(nondet-static)" \
   "(function-enter):(function-exit):(branch):" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  "(drop-unused-functions)" \
   "(show-value-sets)" \
   "(show-global-may-alias)" \
   "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 5e547a19dff..a3f671f0fd9 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -386,7 +386,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     if(cmdline.isset("drop-unused-functions"))
     {
       // Entry point will have been set before and function pointers removed
-      status() << "Removing Unused Functions" << eom;
+      status() << "Removing unused functions" << eom;
       remove_unused_functions(goto_model.goto_functions, ui_message_handler);
     }
 
@@ -690,7 +690,6 @@ void symex_parse_optionst::help()
     " --stop-on-fail               stop analysis once a failed property is detected\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --trace                      give a counterexample trace for failed properties\n"
-    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"
     "Frontend options:\n"
     " -I path                      set include path (C/C++)\n"
@@ -705,6 +704,7 @@ void symex_parse_optionst::help()
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     " --ppc-macos                  set MACOS/PPC architecture\n"
     " --mm model                   set memory model (default: sc)\n"
     " --arch                       set architecture (default: "

From 5aef4f2cdf20833ec2827039383bb25314c077d9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Mon, 27 Mar 2017 09:34:18 +0100
Subject: [PATCH 37/58] fixup! Option --no-built-in-assertions

---
 CHANGELOG | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGELOG b/CHANGELOG
index 61489b8fb41..0f15c3d5081 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -22,6 +22,7 @@
   compiler/linker to be used when building combined native/goto object files.
 * CBMC, SYMEX, GOTO-INSTRUMENT: New option --drop-unused-functions. Removed
   ambiguous --show-reachable-properties.
+* CBMC: New option --no-built-in-assertions
 
 
 5.6

From bfd57bac6e9482c84b46629caa17f242b7fc03be Mon Sep 17 00:00:00 2001
From: Daniel Kroening 
Date: Mon, 20 Jun 2016 17:02:12 -0400
Subject: [PATCH 38/58] missing assert.h

---
 regression/cbmc/Pointer_byte_extract9/main.c | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/regression/cbmc/Pointer_byte_extract9/main.c b/regression/cbmc/Pointer_byte_extract9/main.c
index 931f165c405..0b76b78021f 100644
--- a/regression/cbmc/Pointer_byte_extract9/main.c
+++ b/regression/cbmc/Pointer_byte_extract9/main.c
@@ -1,3 +1,5 @@
+#include 
+
 int main()
 {
   int N;

From 628d4e18253bbb9eb06c812f1f784cc1d546245d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Mon, 12 Dec 2016 10:07:04 +0000
Subject: [PATCH 39/58] Generalise witness as location numbers may vary

The previous regression test may fail dependent on the platform.
---
 regression/cbmc/graphml_witness1/test.desc | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
index 9e7f5b42724..bfd4cf4f3f4 100644
--- a/regression/cbmc/graphml_witness1/test.desc
+++ b/regression/cbmc/graphml_witness1/test.desc
@@ -46,29 +46,29 @@ main.c
   
     C
     
-    
+    
       true
     
     
       main.c
       21
     
-    
-    
+    
+    
       main.c
       29
       main
     
-    
-    
+    
+    
       main.c
       15
       remove_one
     
-    
+    
       true
     
-    
+    
       main.c
       31
     

From 753e7182606060cd180cfad3c6d63817aa58b538 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Sat, 25 Jun 2016 21:53:47 +0200
Subject: [PATCH 40/58] Minor code cleanup of irep.h

---
 src/util/irep.h | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/src/util/irep.h b/src/util/irep.h
index af0b68ac26e..6dd15df0983 100644
--- a/src/util/irep.h
+++ b/src/util/irep.h
@@ -283,11 +283,7 @@ class irept
 
     void clear()
     {
-      #ifdef USE_DSTRING
       data.clear();
-      #else
-      data="";
-      #endif
       sub.clear();
       named_sub.clear();
       comments.clear();

From 6755ecf50e1c2b7eea356b054e1997c76a757042 Mon Sep 17 00:00:00 2001
From: reuk 
Date: Wed, 29 Mar 2017 10:26:27 +0100
Subject: [PATCH 41/58] Fix really pedantic compiler errors

---
 src/analyses/reaching_definitions.h                | 2 +-
 src/java_bytecode/bytecode_info.cpp                | 2 +-
 src/java_bytecode/java_bytecode_convert_method.cpp | 6 ++++--
 src/util/std_types.h                               | 4 ++--
 src/xmllang/graphml.h                              | 2 +-
 5 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index 2ef4a549040..a48a271a9a6 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -160,7 +160,7 @@ class rd_range_domaint:public ai_domain_baset
   typedef std::map ranges_at_loct;
 
   const ranges_at_loct &get(const irep_idt &identifier) const;
-  const void clear_cache(const irep_idt &identifier) const
+  void clear_cache(const irep_idt &identifier) const
   {
     export_cache[identifier].clear();
   }
diff --git a/src/java_bytecode/bytecode_info.cpp b/src/java_bytecode/bytecode_info.cpp
index 556e208129c..87b1942b54e 100644
--- a/src/java_bytecode/bytecode_info.cpp
+++ b/src/java_bytecode/bytecode_info.cpp
@@ -218,5 +218,5 @@ struct bytecode_infot const bytecode_info[]=
 { "impdep1",        0xfe, ' ', 0, 0, ' ' }, // ; reserved for implementation-dependent operations within debuggers; should not appear in any class file  NOLINT(*)
 { "impdep2",        0xff, ' ', 0, 0, ' ' }, // ; reserved for implementation-dependent operations within debuggers; should not appear in any class file  NOLINT(*)
 { "wide",           0xc4, ' ', 0, 0, ' ' }, // modifier for others  NOLINT(*)
-{ 0, 0 }
+{ nullptr,          0x00, '\0',0, 0, '\0'}, // zero-initialized NOLINT (*)
 };
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 0912ec8b22a..cf879429972 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -2301,7 +2301,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
   // First create a simple flat list of basic blocks. We'll add lexical nesting
   // constructs as variable live-ranges require next.
   bool start_new_block=true;
-  int previous_address=-1;
+  bool has_seen_previous_address=false;
+  unsigned previous_address=0;
   for(const auto &address_pair : address_map)
   {
     const unsigned address=address_pair.first;
@@ -2316,7 +2317,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     if(!start_new_block)
       start_new_block=address_pair.second.predecessors.size()>1;
     // Start a new lexical block if we've just entered a try block
-    if(!start_new_block && previous_address!=-1)
+    if(!start_new_block && has_seen_previous_address)
     {
       for(const auto &exception_row : method.exception_table)
         if(exception_row.start_pc==previous_address)
@@ -2346,6 +2347,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     start_new_block=address_pair.second.successors.size()>1;
 
     previous_address=address;
+    has_seen_previous_address=true;
   }
 
   // Find out where temporaries are used:
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 11854535daf..02f4a3981a1 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -215,7 +215,7 @@ class struct_union_typet:public typet
       return set(ID_pretty_name, name);
     }
 
-    const bool get_anonymous() const
+    bool get_anonymous() const
     {
       return get_bool(ID_anonymous);
     }
@@ -225,7 +225,7 @@ class struct_union_typet:public typet
       return set(ID_anonymous, anonymous);
     }
 
-    const bool get_is_padding() const
+    bool get_is_padding() const
     {
       return get_bool(ID_C_is_padding);
     }
diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h
index 7a1050bcb00..1ef5aaedae1 100644
--- a/src/xmllang/graphml.h
+++ b/src/xmllang/graphml.h
@@ -49,7 +49,7 @@ class graphmlt:public grapht
     return false;
   }
 
-  const node_indext add_node_if_not_exists(std::string node_name)
+  node_indext add_node_if_not_exists(std::string node_name)
   {
     for(node_indext i=0; i
Date: Sat, 5 Nov 2016 12:14:57 +0000
Subject: [PATCH 42/58] String abstraction requires remove_returns

---
 src/goto-instrument/goto_instrument_parse_options.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index dda6b1ea302..21000a78da6 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1190,6 +1190,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(cmdline.isset("string-abstraction"))
   {
+    do_indirect_call_and_rtti_removal();
+    do_remove_returns();
+
     status() << "String Abstraction" << eom;
     string_abstraction(
       symbol_table,

From 80ba3cfcb7f56a7b48eee844c9c5d0dc82fb73f1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Sun, 26 Jun 2016 13:51:09 +0000
Subject: [PATCH 43/58] Make rename_symbol a no-op if its maps are empty

---
 src/util/rename_symbol.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp
index 55a9a7ff484..c6930a01d87 100644
--- a/src/util/rename_symbol.cpp
+++ b/src/util/rename_symbol.cpp
@@ -133,6 +133,9 @@ Function: rename_symbolt::have_to_rename
 
 bool rename_symbolt::have_to_rename(const exprt &dest) const
 {
+  if(expr_map.empty() && type_map.empty())
+    return false;
+
   // first look at type
 
   if(have_to_rename(dest.type()))
@@ -274,6 +277,9 @@ Function: rename_symbolt::have_to_rename
 
 bool rename_symbolt::have_to_rename(const typet &dest) const
 {
+  if(expr_map.empty() && type_map.empty())
+    return false;
+
   if(dest.has_subtype())
     if(have_to_rename(dest.subtype()))
       return true;

From 9c12efd69c827eaeee229c3b384d08629ea56a30 Mon Sep 17 00:00:00 2001
From: Daniel Kroening 
Date: Wed, 29 Mar 2017 18:24:47 +0100
Subject: [PATCH 44/58] use stat to determine whether a directory entry is a
 subdirectory; d_type is not POSIX

---
 src/util/file_util.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/util/file_util.cpp b/src/util/file_util.cpp
index 50dc06473f4..18634240141 100644
--- a/src/util/file_util.cpp
+++ b/src/util/file_util.cpp
@@ -16,6 +16,7 @@ Date: January 2012
     defined(__unix__) || \
     defined(__CYGWIN__) || \
     defined(__MACH__)
+#include 
 #include 
 #include 
 #include 
@@ -124,8 +125,13 @@ void delete_directory(const std::string &path)
       // Needed for Alpine Linux
       if(strcmp(ent->d_name, ".")==0 || strcmp(ent->d_name, "..")==0)
         continue;
+
       std::string sub_path=path+"/"+ent->d_name;
-      if(ent->d_type==DT_DIR)
+
+      struct stat stbuf;
+      stat(sub_path.c_str(), &stbuf);
+
+      if(S_ISDIR(stbuf.st_mode))
         delete_directory(sub_path);
       else
         remove(sub_path.c_str());

From cf42202a3597370c864e21867123d557975c5a6a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Tue, 21 Feb 2017 13:52:43 +0000
Subject: [PATCH 45/58] gcc_message_handlert must obey verbosity

---
 src/util/cout_message.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp
index af315c696c5..393ec62432f 100644
--- a/src/util/cout_message.cpp
+++ b/src/util/cout_message.cpp
@@ -211,5 +211,6 @@ void gcc_message_handlert::print(
   const std::string &message)
 {
   // gcc appears to send everything to cerr
-  std::cerr << message << '\n' << std::flush;
+  if(verbosity>=level)
+    std::cerr << message << '\n' << std::flush;
 }

From 943bdc8be4543145e6b29fd734e132e83ab8a9ae Mon Sep 17 00:00:00 2001
From: Daniel Kroening 
Date: Wed, 29 Mar 2017 18:39:52 +0100
Subject: [PATCH 46/58] Ubuntu has new g++

---
 COMPILING | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/COMPILING b/COMPILING
index cfbb056c2e0..fded90c50da 100644
--- a/COMPILING
+++ b/COMPILING
@@ -44,12 +44,18 @@ 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/Ubuntu, do
+2) On Debian, do
 
    cd cbmc-git/src
    make minisat2-download
    make CXX=g++-6
 
+   On Ubuntu, or other distributions with recent g++, do
+
+   cd cbmc-git/src
+   make minisat2-download
+   make
+
    On Redhat/Fedora etc., do
 
    cd cbmc-git/src

From 2d26cb7095972296a18086175ae2ddd565699794 Mon Sep 17 00:00:00 2001
From: Daniel Kroening 
Date: Wed, 29 Mar 2017 19:31:47 +0100
Subject: [PATCH 47/58] removed unnecessary newline

---
 regression/ansi-c/function_return1/test.desc | 1 -
 1 file changed, 1 deletion(-)

diff --git a/regression/ansi-c/function_return1/test.desc b/regression/ansi-c/function_return1/test.desc
index 78396740555..f49480a607f 100644
--- a/regression/ansi-c/function_return1/test.desc
+++ b/regression/ansi-c/function_return1/test.desc
@@ -3,7 +3,6 @@ main.c
 --verbosity 2
 ^main.c:3:1: warning: function has return void but a return statement returning signed int$
 ^SIGNAL=0$
-
 --
 ^warning: ignoring
 ^CONVERSION ERROR$

From 0983dbfdcaf32c7cad89476d7f6431c76d612759 Mon Sep 17 00:00:00 2001
From: Daniel Kroening 
Date: Wed, 29 Mar 2017 19:36:34 +0100
Subject: [PATCH 48/58] compile with Visual Studio 2017

---
 src/big-int/bigint-test.cc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/big-int/bigint-test.cc b/src/big-int/bigint-test.cc
index 6c8b9c84b64..5d506a89013 100644
--- a/src/big-int/bigint-test.cc
+++ b/src/big-int/bigint-test.cc
@@ -298,7 +298,7 @@ run_floorPow2_tests ()
 
   for (unsigned i = 0; i < 512; ++i) {
     unsigned x = 512 - i;
-    N = pow(2,x);
+    N = pow(BigInt(2),x);
     M.setPower2(x);
 
     if (!(N == M)) {
@@ -327,7 +327,7 @@ run_floorPow2_tests ()
 
   }
 
-  N = pow(2,0);  // 1
+  N = pow(BigInt(2),0);  // 1
   M.setPower2(0);
 
   if (!(N == M)) {

From 610e9e41ab52b7bae31f78f3ad942fb96998e224 Mon Sep 17 00:00:00 2001
From: Daniel Kroening 
Date: Wed, 29 Mar 2017 20:43:00 +0100
Subject: [PATCH 49/58] use std::size_t for counters

---
 src/musketeer/fencer.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/musketeer/fencer.cpp b/src/musketeer/fencer.cpp
index a787ce06393..4fc213908d4 100644
--- a/src/musketeer/fencer.cpp
+++ b/src/musketeer/fencer.cpp
@@ -87,9 +87,9 @@ void fence_weak_memory(
   {
     instrumenter.collect_cycles_by_SCCs(model);
     message.statistics() << "cycles collected: " << messaget::eom;
-    unsigned interesting_scc = 0;
-    unsigned total_cycles = 0;
-    for(unsigned i=0; i=4)
       {
         message.statistics() << "SCC #" << i << ": "

From 7fd6180188322498eddcbafbe5f59b0c75eecfab Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Sat, 25 Mar 2017 22:30:29 +0000
Subject: [PATCH 50/58] Fix concurrent traces generated via --trace

Traces had been cut off at the failing assertion without considering steps
performed in threads with a higher thread id. The behaviour of --stop-on-fail
was correct in this regard. The trace trimming must only be performed after
re-ordering of steps according to their time stamps.
---
 regression/cbmc-concurrency/trace1/main.c    | 28 ++++++++++++++++++++
 regression/cbmc-concurrency/trace1/test.desc |  9 +++++++
 src/goto-symex/build_goto_trace.cpp          | 23 ++++++++++++++--
 3 files changed, 58 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc-concurrency/trace1/main.c
 create mode 100644 regression/cbmc-concurrency/trace1/test.desc

diff --git a/regression/cbmc-concurrency/trace1/main.c b/regression/cbmc-concurrency/trace1/main.c
new file mode 100644
index 00000000000..7e1d3749edd
--- /dev/null
+++ b/regression/cbmc-concurrency/trace1/main.c
@@ -0,0 +1,28 @@
+// #include 
+#include 
+
+volatile unsigned x = 0, y = 0;
+volatile unsigned r1 = 0, r2 = 0;
+
+void* thr1(void* arg) {
+  x = 1;
+  r1 = y + 1;
+  return 0;
+}
+
+void* thr2(void* arg) {
+  y = 1;
+  r2 = x + 1;
+  return 0;
+}
+
+int main(){
+  // pthread_t t1, t2;
+  // pthread_create(&t1, NULL, thr1, NULL);
+  // pthread_create(&t2, NULL, thr2, NULL);
+__CPROVER_ASYNC_1: thr1(0);
+__CPROVER_ASYNC_2: thr2(0);
+  assert(r1 != 1 || r2 != 1);
+  return 0;
+}
+
diff --git a/regression/cbmc-concurrency/trace1/test.desc b/regression/cbmc-concurrency/trace1/test.desc
new file mode 100644
index 00000000000..a6f904e7a86
--- /dev/null
+++ b/regression/cbmc-concurrency/trace1/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--mm tso --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^[[:space:]]*r2=1u \(.*\)$
+--
+^warning: ignoring
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index 0e0a6f07dad..909a437bd9c 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -158,11 +158,17 @@ void build_goto_trace(
 
   mp_integer current_time=0;
 
+  const goto_trace_stept *end_ptr=nullptr;
+  bool end_step_seen=false;
+
   for(symex_target_equationt::SSA_stepst::const_iterator
       it=target.SSA_steps.begin();
-      it!=end_step;
+      it!=target.SSA_steps.end();
       it++)
   {
+    if(it==end_step)
+      end_step_seen=true;
+
     const symex_target_equationt::SSA_stept &SSA_step=*it;
 
     if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
@@ -221,6 +227,8 @@ void build_goto_trace(
     goto_tracet::stepst &steps=time_map[current_time];
     steps.push_back(goto_trace_stept());
     goto_trace_stept &goto_trace_step=steps.back();
+    if(!end_step_seen)
+      end_ptr=&goto_trace_step;
 
     goto_trace_step.thread_nr=SSA_step.source.thread_nr;
     goto_trace_step.pc=SSA_step.source.pc;
@@ -286,6 +294,17 @@ void build_goto_trace(
   for(auto &t_it : time_map)
     goto_trace.steps.splice(goto_trace.steps.end(), t_it.second);
 
+  // cut off the trace at the desired end
+  for(goto_tracet::stepst::iterator
+      s_it1=goto_trace.steps.begin();
+      s_it1!=goto_trace.steps.end();
+      ++s_it1)
+    if(end_step_seen && end_ptr==&(*s_it1))
+    {
+      goto_trace.trim_after(s_it1);
+      break;
+    }
+
   // produce the step numbers
   unsigned step_nr=0;
 
@@ -321,7 +340,7 @@ void build_goto_trace(
       s_it1++)
     if(s_it1->is_assert() && !s_it1->cond_value)
     {
-      goto_trace.steps.erase(++s_it1, goto_trace.steps.end());
+      goto_trace.trim_after(s_it1);
       break;
     }
 }

From 66481ab4d43bc7d8ae166a5920124363a45fa5a3 Mon Sep 17 00:00:00 2001
From: Marius Melemciuc 
Date: Tue, 14 Mar 2017 16:42:06 +0000
Subject: [PATCH 51/58] Removed the dynamic_object_exprt's instance()

Removed the dynamic_object_exprt's instance() methods and
replaced its usages with set_instance() and get_instance().

Added the dynamic_object_id_sett data structure into the
value_sett class. It is used as expr_sett but only for
dynamic-objects.
---
 src/pointer-analysis/value_set.cpp        | 20 +++++++++----------
 src/pointer-analysis/value_set.h          |  2 ++
 src/pointer-analysis/value_set_fi.cpp     | 24 +++++++++++------------
 src/pointer-analysis/value_set_fi.h       |  2 ++
 src/pointer-analysis/value_set_fivr.cpp   | 24 +++++++++++------------
 src/pointer-analysis/value_set_fivr.h     |  2 ++
 src/pointer-analysis/value_set_fivrns.cpp | 24 +++++++++++------------
 src/pointer-analysis/value_set_fivrns.h   |  2 ++
 src/util/std_expr.cpp                     | 10 ++++++++++
 src/util/std_expr.h                       | 10 ++--------
 10 files changed, 62 insertions(+), 58 deletions(-)

diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 629a25509d6..1a6c639ff92 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -799,8 +799,7 @@ void value_sett::get_value_set_rec(
         static_cast(expr.find("#type"));
 
       dynamic_object_exprt dynamic_object(dynamic_type);
-      dynamic_object.instance()=
-        from_integer(location_number, typet(ID_natural));
+      dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -812,8 +811,7 @@ void value_sett::get_value_set_rec(
       assert(expr_type.id()==ID_pointer);
 
       dynamic_object_exprt dynamic_object(expr_type.subtype());
-      dynamic_object.instance()=
-        from_integer(location_number, typet(ID_natural));
+      dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -897,7 +895,7 @@ void value_sett::get_value_set_rec(
 
     const std::string prefix=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     // first try with suffix
     const std::string full_name=prefix+suffix;
@@ -1392,7 +1390,7 @@ void value_sett::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   for(object_map_dt::const_iterator
       it=object_map.begin();
@@ -1407,7 +1405,7 @@ void value_sett::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1433,10 +1431,10 @@ void value_sett::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1507,7 +1505,7 @@ void value_sett::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     entryt &e=get_entry(entryt(name, suffix), lhs.type(), ns);
 
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 486b55e998b..51bf74d48f2 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -115,6 +115,8 @@ class value_sett
 
   typedef std::set expr_sett;
 
+  typedef std::set dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map valuest;
   #else
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 55542296c48..0fbcd7dec00 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -727,9 +727,8 @@ void value_set_fit::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(dynamic_type);
       // let's make up a `unique' number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -742,9 +741,8 @@ void value_set_fit::get_value_set_rec(
       assert(expr.type().id()==ID_pointer);
 
       dynamic_object_exprt dynamic_object(expr.type().subtype());
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -776,7 +774,7 @@ void value_set_fit::get_value_set_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value)+
+      std::to_string(dynamic_object.get_instance())+
       suffix;
 
     // look it up
@@ -1322,7 +1320,7 @@ void value_set_fit::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   forall_objects(it, object_map)
   {
@@ -1334,7 +1332,7 @@ void value_set_fit::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1357,10 +1355,10 @@ void value_set_fit::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1452,7 +1450,7 @@ void value_set_fit::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     if(make_union(get_entry(name, suffix).object_map, values_rhs))
       changed = true;
diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
index 5b76d0f48d9..13defa545ae 100644
--- a/src/pointer-analysis/value_set_fi.h
+++ b/src/pointer-analysis/value_set_fi.h
@@ -155,6 +155,8 @@ class value_set_fit
 
   typedef std::unordered_set expr_sett;
 
+  typedef std::unordered_set dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map valuest;
   typedef std::set flatten_seent;
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
index 582fe015dd3..e06d73b245b 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -857,9 +857,8 @@ void value_set_fivrt::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(dynamic_type);
       // let's make up a `unique' number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -873,9 +872,8 @@ void value_set_fivrt::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(expr.type().subtype());
       // let's make up a unique number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -902,7 +900,7 @@ void value_set_fivrt::get_value_set_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value)+
+      std::to_string(dynamic_object.get_instance())+
       suffix;
 
     // look it up
@@ -1446,7 +1444,7 @@ void value_set_fivrt::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   forall_objects(it, object_map)
   {
@@ -1458,7 +1456,7 @@ void value_set_fivrt::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1481,10 +1479,10 @@ void value_set_fivrt::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1590,7 +1588,7 @@ void value_set_fivrt::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     entryt &temp_entry=get_temporary_entry(name, suffix);
 
diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h
index 5a96e537e77..e12563252ae 100644
--- a/src/pointer-analysis/value_set_fivr.h
+++ b/src/pointer-analysis/value_set_fivr.h
@@ -216,6 +216,8 @@ class value_set_fivrt
 
   typedef std::unordered_set expr_sett;
 
+  typedef std::unordered_set dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map valuest;
   typedef std::unordered_set flatten_seent;
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index 41907d54cfb..4591bdd938d 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -631,9 +631,8 @@ void value_set_fivrnst::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(dynamic_type);
       // let's make up a `unique' number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -647,9 +646,8 @@ void value_set_fivrnst::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(expr.type().subtype());
       // let's make up a unique number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -676,7 +674,7 @@ void value_set_fivrnst::get_value_set_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value)+
+      std::to_string(dynamic_object.get_instance())+
       suffix;
 
     // look it up
@@ -1105,7 +1103,7 @@ void value_set_fivrnst::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   forall_objects(it, object_map)
   {
@@ -1117,7 +1115,7 @@ void value_set_fivrnst::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1140,10 +1138,10 @@ void value_set_fivrnst::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1225,7 +1223,7 @@ void value_set_fivrnst::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     entryt &temp_entry = get_temporary_entry(name, suffix);
 
diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h
index c1d826f2550..f3afc204ef2 100644
--- a/src/pointer-analysis/value_set_fivrns.h
+++ b/src/pointer-analysis/value_set_fivrns.h
@@ -216,6 +216,8 @@ class value_set_fivrnst
 
   typedef std::unordered_set expr_sett;
 
+  typedef std::unordered_set dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map valuest;
   #else
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
index 5efc4d6e70c..4cb9eeff9cc 100644
--- a/src/util/std_expr.cpp
+++ b/src/util/std_expr.cpp
@@ -61,6 +61,16 @@ exprt disjunction(const exprt::operandst &op)
   }
 }
 
+void dynamic_object_exprt::set_instance(unsigned int instance)
+{
+  op0()=from_integer(instance, typet(ID_natural));
+}
+
+unsigned int dynamic_object_exprt::get_instance() const
+{
+  return std::stoul(id2string(to_constant_expr(op0()).get_value()));
+}
+
 /*******************************************************************\
 
 Function: conjunction
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index a2f78ab25e8..8735a8ed333 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -1505,15 +1505,9 @@ class dynamic_object_exprt:public exprt
     op1().id(ID_unknown);
   }
 
-  exprt &instance()
-  {
-    return op0();
-  }
+  void set_instance(unsigned int instance);
 
-  const exprt &instance() const
-  {
-    return op0();
-  }
+  unsigned int get_instance() const;
 
   exprt &valid()
   {

From d811f4d041a6fc6f41374942e40386dd9378ecae Mon Sep 17 00:00:00 2001
From: Daniel Kroening 
Date: Sun, 2 Apr 2017 12:15:25 +0100
Subject: [PATCH 52/58] update compilation instructions

---
 COMPILING | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

diff --git a/COMPILING b/COMPILING
index fded90c50da..7cbdfcaab13 100644
--- a/COMPILING
+++ b/COMPILING
@@ -70,7 +70,7 @@ COMPILATION ON SOLARIS 11
 1) As root, get the necessary development tools:
 
    pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git
-   pkg install --accept developer/gcc-5
+   pkg install --accept developer/gcc/gcc-c++-5
 
 2) As a user, get the CBMC source via
 
@@ -92,9 +92,6 @@ COMPILATION ON SOLARIS 11
 
    export LD_LIBRARY_PATH=/usr/gcc/4.9/lib
 
-   Do not attempt to compile with gcc-45 that comes with Solaris 11.
-   It will mis-optimize MiniSat2.
-
 
 COMPILATION ON FREEBSD 11
 -------------------------
@@ -169,23 +166,21 @@ Follow these instructions:
    The patch removes the dependency on zlib and prevents a problem
    with a header file that is often unavailable on Windows.
 
-2) Adjust src/config.inc for the paths to item 1).
-
-3A) To compile with Cygwin, install the mingw compilers, and adjust
+2A) To compile with Cygwin, install the mingw compilers, and adjust
    the second line of config.inc to say
 
    BUILD_ENV = MinGW
 
-3B) To compile with Visual Studio, make sure you have at least Visual
+2B) To compile with Visual Studio, make sure you have at least Visual
    Studio version 12 (2013), and adjust the second line of config.inc to say
 
    BUILD_ENV = MSVC
 
-   Open the Visual Studio Command prompt, and then run the make.exe
-   from Cygwin from in there.
+   Open the Visual Studio Command prompt, and then bash.exe -login from
+   Cygwin from in there. 
+
+3) Type cd src; make - that should do it.
 
-4) Type cd src; make - that should do it.
-   Note that "nmake" is not expected to work. Use "make".
 
 (Optional) A Visual Studio project file can be generated with the script
 "generate_vcxproj" that is in the subdirectory "scripts".  The project file

From 4fc6633491a7e89b43eda326b2b14681f9c990d4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Wed, 6 Jul 2016 23:30:07 +0200
Subject: [PATCH 53/58] Migrated all message clients to messaget, removing
 deprecated message_streamt

---
 src/util/Makefile           |   2 +-
 src/util/message_stream.cpp | 182 ------------------------------------
 src/util/message_stream.h   | 165 --------------------------------
 3 files changed, 1 insertion(+), 348 deletions(-)
 delete mode 100644 src/util/message_stream.cpp
 delete mode 100644 src/util/message_stream.h

diff --git a/src/util/Makefile b/src/util/Makefile
index fefabaed3af..0cab8cd8a04 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -12,7 +12,7 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \
       rational.cpp options.cpp dstring.cpp \
       find_symbols.cpp rational_tools.cpp ui_message.cpp simplify_utils.cpp \
       time_stopping.cpp symbol.cpp irep_hash_container.cpp cout_message.cpp \
-      type_eq.cpp guard.cpp array_name.cpp message_stream.cpp \
+      type_eq.cpp guard.cpp array_name.cpp \
       substitute.cpp decision_procedure.cpp union_find.cpp \
       xml.cpp xml_irep.cpp xml_expr.cpp std_types.cpp std_code.cpp \
       format_constant.cpp find_macros.cpp ref_expr_set.cpp std_expr.cpp \
diff --git a/src/util/message_stream.cpp b/src/util/message_stream.cpp
deleted file mode 100644
index 347d87915d7..00000000000
--- a/src/util/message_stream.cpp
+++ /dev/null
@@ -1,182 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#include 
-
-#include "prefix.h"
-#include "message_stream.h"
-
-/*******************************************************************\
-
-Function: legacy_message_streamt::error_parse_line
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void legacy_message_streamt::error_parse_line(
-  unsigned level,
-  const std::string &line)
-{
-  std::string error_msg=line;
-
-  if(has_prefix(line, "file "))
-  {
-    const char *tptr=line.c_str();
-    int state=0;
-    std::string file, line_no, column, _error_msg, function;
-
-    tptr+=5;
-
-    char previous=0;
-
-    while(*tptr!=0)
-    {
-      if(strncmp(tptr, " line ", 6)==0 && state!=4)
-      {
-        state=1;
-        tptr+=6;
-        continue;
-      }
-      else if(strncmp(tptr, " column ", 8)==0 && state!=4)
-      {
-        state=2;
-        tptr+=8;
-        continue;
-      }
-      else if(strncmp(tptr, " function ", 10)==0 && state!=4)
-      {
-        state=3;
-        tptr+=10;
-        continue;
-      }
-      else if(*tptr==':' && state!=4)
-      {
-        if(tptr[1]==' ' && previous!=':')
-        {
-          state=4;
-          tptr++;
-          while(*tptr==' ') tptr++;
-          continue;
-        }
-      }
-
-      if(state==0) // file
-        file+=*tptr;
-      else if(state==1) // line number
-        line_no+=*tptr;
-      else if(state==2) // column
-        column+=*tptr;
-      else if(state==3) // function
-        function+=*tptr;
-      else if(state==4) // error message
-        _error_msg+=*tptr;
-
-      previous=*tptr;
-
-      tptr++;
-    }
-
-    if(state==4)
-    {
-      saved_error_location.id(irep_idt());
-      saved_error_location.set_line(line_no);
-      saved_error_location.set_file(file);
-      saved_error_location.set_column(column);
-      error_msg=_error_msg;
-      saved_error_location.set_function(function);
-    }
-  }
-  else if(has_prefix(line, "In file included from "))
-  {
-  }
-  else
-  {
-    const char *tptr=line.c_str();
-    int state=0;
-    std::string file, line_no;
-
-    while(*tptr!=0)
-    {
-      if(state==0)
-      {
-        if(*tptr==':')
-          state++;
-        else
-          file+=*tptr;
-      }
-      else if(state==1)
-      {
-        if(*tptr==':')
-          state++;
-        else if(isdigit(*tptr))
-          line_no+=*tptr;
-        else
-          state=3;
-      }
-
-      tptr++;
-    }
-
-    if(state==2)
-    {
-      saved_error_location.id(irep_idt());
-      saved_error_location.set_line(line_no);
-      saved_error_location.set_file(file);
-      saved_error_location.set_function("");
-      saved_error_location.set_column("");
-    }
-  }
-
-  if(message_handler!=NULL)
-    message_handler->print(
-      level, error_msg, sequence_number++, saved_error_location);
-}
-
-/*******************************************************************\
-
-Function: legacy_message_streamt::error_parse
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void legacy_message_streamt::error_parse(
-  unsigned level,
-  const std::string &error)
-{
-  const char *tptr=error.c_str();
-
-  std::string line;
-
-  while(true)
-  {
-    switch(*tptr)
-    {
-     case 0: return;
-     case '\n':
-      error_parse_line(level, line);
-      line.clear();
-      break;
-
-     case '\r': break;
-     default:
-      line+=*tptr;
-    }
-
-    tptr++;
-  }
-}
diff --git a/src/util/message_stream.h b/src/util/message_stream.h
deleted file mode 100644
index 4b3fc48bb7d..00000000000
--- a/src/util/message_stream.h
+++ /dev/null
@@ -1,165 +0,0 @@
-/*******************************************************************\
-
-Module:
-
-Author: Daniel Kroening, kroening@kroening.com
-
-\*******************************************************************/
-
-#ifndef CPROVER_UTIL_MESSAGE_STREAM_H
-#define CPROVER_UTIL_MESSAGE_STREAM_H
-
-#include 
-
-#include "message.h"
-#include "expr.h"
-
-// deprecated; use warning(), error(), etc. streams in messaget
-
-class legacy_message_streamt:public message_clientt
-{
-public:
-  explicit legacy_message_streamt(message_handlert &_message_handler):
-    message_clientt(_message_handler),
-    error_found(false),
-    saved_error_location(static_cast(get_nil_irep())),
-    sequence_number(1)
-  {
-  }
-
-  virtual ~legacy_message_streamt() { }
-
-  // overload to use language specific syntax
-  virtual std::string to_string(const exprt &expr) { return expr.pretty(); }
-  virtual std::string to_string(const typet &type) { return type.pretty(); }
-
-  void err_location(const exprt &expr)
-  { saved_error_location=expr.find_source_location(); }
-  void err_location(const typet &type)
-  { saved_error_location=type.source_location(); }
-  void err_location(const irept &irep)
-  {
-    saved_error_location=
-      static_cast(irep.find(ID_C_source_location));
-  }
-  void err_location(const source_locationt &_location)
-  { saved_error_location=_location; }
-
-  void error_msg(const std::string &message)
-  {
-    send_msg(1, message);
-  }
-
-  void warning_msg(const std::string &message)
-  {
-    send_msg(2, message);
-  }
-
-  void statistics_msg(const std::string &message)
-  {
-    send_msg(8, message);
-  }
-
-  void debug_msg(const std::string &message)
-  {
-    send_msg(9, message);
-  }
-
-  void error_msg()
-  {
-    send_msg(1, str.str());
-    clear_err();
-    sequence_number++;
-  }
-
-  void warning_msg()
-  {
-    send_msg(2, str.str());
-    clear_err();
-    sequence_number++;
-  }
-
-  void status_msg()
-  {
-    send_msg(6, str.str());
-    clear_err();
-    sequence_number++;
-  }
-
-  void statistics_msg()
-  {
-    send_msg(8, str.str());
-    clear_err();
-    sequence_number++;
-  }
-
-  void debug_msg()
-  {
-    send_msg(9, str.str());
-    clear_err();
-    sequence_number++;
-  }
-
-  std::ostringstream str;
-
-  std::ostream &error()
-  {
-    return str;
-  }
-
-  // API stub, intentional noop
-  static inline std::ostream &eom(std::ostream &m)
-  {
-    return m;
-  }
-
-
-  bool get_error_found() const
-  {
-    return error_found;
-  }
-
-  void error_parse(unsigned level)
-  {
-    error_parse(level, str.str());
-    clear_err();
-  }
-
-  void clear_err()
-  {
-    str.clear();
-    str.str("");
-  }
-
-protected:
-  bool error_found;
-  source_locationt saved_error_location;
-  unsigned sequence_number;
-
-  void send_msg(unsigned level, const std::string &message)
-  {
-    if(message=="")
-      return;
-    if(level<=1)
-      error_found=true;
-
-    if(message_handler!=NULL)
-      message_handler->print(
-        level,
-        message,
-        sequence_number,
-        saved_error_location);
-
-    saved_error_location.make_nil();
-  }
-
-  void error_parse_line(
-    unsigned level,
-    const std::string &line);
-
-  void error_parse(
-    unsigned level,
-    const std::string &error);
-};
-
-#endif // CPROVER_UTIL_MESSAGE_STREAM_H

From ce147fb46f024e6153cddda951cccf786ca8bb99 Mon Sep 17 00:00:00 2001
From: Daniel Kroening 
Date: Mon, 3 Apr 2017 14:16:53 +0100
Subject: [PATCH 54/58] removed legacy_typecheckt

---
 src/util/typecheck.cpp | 39 ---------------------------------------
 src/util/typecheck.h   | 19 ++-----------------
 2 files changed, 2 insertions(+), 56 deletions(-)

diff --git a/src/util/typecheck.cpp b/src/util/typecheck.cpp
index a305fa7ad4c..67b695e53fa 100644
--- a/src/util/typecheck.cpp
+++ b/src/util/typecheck.cpp
@@ -20,45 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-bool legacy_typecheckt::typecheck_main()
-{
-  try
-  {
-    typecheck();
-  }
-
-  catch(int)
-  {
-    error_msg();
-  }
-
-  catch(const char *e)
-  {
-    str << e;
-    error_msg();
-  }
-
-  catch(const std::string &e)
-  {
-    str << e;
-    error_msg();
-  }
-
-  return error_found;
-}
-
-/*******************************************************************\
-
-Function:
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
 bool typecheckt::typecheck_main()
 {
   try
diff --git a/src/util/typecheck.h b/src/util/typecheck.h
index 7de4557de64..ee80f6e42f0 100644
--- a/src/util/typecheck.h
+++ b/src/util/typecheck.h
@@ -9,23 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_TYPECHECK_H
 #define CPROVER_UTIL_TYPECHECK_H
 
-#include "message_stream.h"
-
-class legacy_typecheckt:public legacy_message_streamt
-{
-public:
-  explicit legacy_typecheckt(message_handlert &_message_handler):
-    legacy_message_streamt(_message_handler) { }
-  virtual ~legacy_typecheckt() { }
-
-protected:
-  // main function -- overload this one
-  virtual void typecheck()=0;
-
-public:
-  // call that one
-  virtual bool typecheck_main();
-};
+#include "expr.h"
+#include "message.h"
 
 class typecheckt:public messaget
 {

From b0778bfca9e3dfee1fc032fc9578e8460c2121ed Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Thu, 7 Jul 2016 09:41:02 +0200
Subject: [PATCH 55/58] Consistency: use messaget's error directly instead of
 throwing string/char*

Added error location reporting
---
 src/jsil/jsil_typecheck.cpp | 44 ++++++++++++++++++++++++++++++-------
 src/langapi/language_ui.cpp |  8 ++-----
 2 files changed, 38 insertions(+), 14 deletions(-)

diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
index 38a1b94e6be..07415de550f 100644
--- a/src/jsil/jsil_typecheck.cpp
+++ b/src/jsil/jsil_typecheck.cpp
@@ -87,7 +87,10 @@ void jsil_typecheckt::update_expr_type(exprt &expr, const typet &type)
     const irep_idt &id=to_symbol_expr(expr).get_identifier();
 
     if(!symbol_table.has_symbol(id))
-      throw "unexpected symbol: "+id2string(id);
+    {
+      error() << "unexpected symbol: " << id << eom;
+      throw 0;
+    }
 
     symbolt &s=symbol_table.lookup(id);
     if(s.type.id().empty() || s.type.is_nil())
@@ -924,7 +927,10 @@ void jsil_typecheckt::typecheck_symbol_expr(symbol_exprt &symbol_expr)
       symbol_table.symbols.find(identifier);
 
     if(s_it==symbol_table.symbols.end())
-      throw "unexpected internal symbol: "+id2string(identifier);
+    {
+      error() << "unexpected internal symbol: " << identifier << eom;
+      throw 0;
+    }
     else
     {
       // symbol already exists
@@ -1006,7 +1012,12 @@ void jsil_typecheckt::typecheck_code(codet &code)
   else if(statement==ID_expression)
   {
     if(code.operands().size()!=1)
-      throw "expression statement expected to have one operand";
+    {
+      err_location(code);
+      error() << "expression statement expected to have one operand"
+              << eom;
+      throw 0;
+    }
 
     typecheck_expr(code.op0());
   }
@@ -1090,7 +1101,11 @@ void jsil_typecheckt::typecheck_try_catch(code_try_catcht &code)
 {
   // A special case of try catch with one catch clause
   if(code.operands().size()!=3)
-    throw "try_catch expected to have three operands";
+  {
+    err_location(code);
+    error() << "try_catch expected to have three operands" << eom;
+    throw 0;
+  }
 
   // function call
   typecheck_function_call(to_code_function_call(code.try_code()));
@@ -1116,7 +1131,11 @@ void jsil_typecheckt::typecheck_function_call(
   code_function_callt &call)
 {
   if(call.operands().size()!=3)
-    throw "function call expected to have three operands";
+  {
+    err_location(call);
+    error() << "function call expected to have three operands" << eom;
+    throw 0;
+  }
 
   exprt &lhs=call.lhs();
   typecheck_expr(lhs);
@@ -1194,7 +1213,12 @@ void jsil_typecheckt::typecheck_function_call(
       make_type_compatible(lhs, jsil_any_type(), true);
 
       if(symbol_table.add(new_symbol))
-        throw "failed to add expression symbol to symbol table";
+      {
+        err_location(new_symbol.location);
+        error() << "failed to add expression symbol to symbol table"
+                << eom;
+        throw 0;
+      }
     }
   }
   else
@@ -1287,8 +1311,12 @@ void jsil_typecheckt::typecheck_non_type_symbol(symbolt &symbol)
     // Do nothing
   }
   else
-    throw "non-type symbol value expected code, but got "+
-      symbol.value.pretty();
+  {
+    err_location(symbol.location);
+    error() << "non-type symbol value expected code, but got "
+            << symbol.value.pretty() << eom;
+    throw 0;
+  }
 }
 
 /*******************************************************************\
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index 2c4019a253c..fac4c2f01e9 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -158,9 +158,7 @@ bool language_uit::typecheck()
 
   if(language_files.typecheck(symbol_table))
   {
-    if(get_ui()==ui_message_handlert::PLAIN)
-      std::cerr << "CONVERSION ERROR" << std::endl;
-
+    error() << "CONVERSION ERROR" << eom;
     return true;
   }
 
@@ -185,9 +183,7 @@ bool language_uit::final()
 
   if(language_files.final(symbol_table))
   {
-    if(get_ui()==ui_message_handlert::PLAIN)
-      std::cerr << "CONVERSION ERROR" << std::endl;
-
+    error() << "CONVERSION ERROR" << eom;
     return true;
   }
 

From d13a056d03161fc1eadae1bc0ddf597097de0849 Mon Sep 17 00:00:00 2001
From: Daniel Kroening 
Date: Mon, 3 Apr 2017 14:19:36 +0100
Subject: [PATCH 56/58] use new messaging interface

---
 src/jsil/jsil_typecheck.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
index 07415de550f..a644f1acf99 100644
--- a/src/jsil/jsil_typecheck.cpp
+++ b/src/jsil/jsil_typecheck.cpp
@@ -1214,7 +1214,7 @@ void jsil_typecheckt::typecheck_function_call(
 
       if(symbol_table.add(new_symbol))
       {
-        err_location(new_symbol.location);
+        error().source_location=new_symbol.location;
         error() << "failed to add expression symbol to symbol table"
                 << eom;
         throw 0;
@@ -1312,7 +1312,7 @@ void jsil_typecheckt::typecheck_non_type_symbol(symbolt &symbol)
   }
   else
   {
-    err_location(symbol.location);
+    error().source_location=symbol.location;
     error() << "non-type symbol value expected code, but got "
             << symbol.value.pretty() << eom;
     throw 0;

From 767a373943ca1b2fe8c19924d514424af6d002b3 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Mon, 11 Jul 2016 13:36:10 +0100
Subject: [PATCH 57/58] Added location information to warning messages missing
 it

---
 src/linking/linking.cpp | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index b66c0591b4b..10c5fbd3523 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -1133,17 +1133,20 @@ void linkingt::duplicate_object_symbol(
       }
       else
       {
-        err_location(new_symbol.value);
-        error() << "error: conflicting initializers for variable \""
-                << old_symbol.name
-                << "\"" << '\n';
-        error() << "old value in module " << old_symbol.module
-                << " " << old_symbol.value.find_source_location() << '\n'
-                << expr_to_string(ns, old_symbol.name, tmp_old) << '\n';
-        error() << "new value in module " << new_symbol.module
-                << " " << new_symbol.value.find_source_location() << '\n'
-                << expr_to_string(ns, new_symbol.name, tmp_new) << eom;
-        throw 0;
+        warning().source_location=new_symbol.location;
+
+        warning() << "warning: conflicting initializers for"
+                  << " variable \"" << old_symbol.name << "\"\n";
+        warning() << "using old value in module "
+                  << old_symbol.module << " "
+                  << old_symbol.value.find_source_location() << '\n'
+                  << expr_to_string(ns, old_symbol.name, tmp_old)
+                  << '\n';
+        warning() << "ignoring new value in module "
+                  << new_symbol.module << " "
+                  << new_symbol.value.find_source_location() << '\n'
+                  << expr_to_string(ns, new_symbol.name, tmp_new)
+                  << eom;
       }
     }
   }

From f2f5e36da95c4c29c603b9b666775a2810a9003b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig 
Date: Mon, 11 Jul 2016 13:38:03 +0100
Subject: [PATCH 58/58] Completely remove
 cpp_typecheckt::check_template_restrictions

It was unused and disabled via #if 0; resurrect via git if needed.
---
 src/cpp/cpp_typecheck.h            |  7 ------
 src/cpp/cpp_typecheck_template.cpp | 35 ------------------------------
 2 files changed, 42 deletions(-)

diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
index 9c26ebbe16f..55955cd0334 100644
--- a/src/cpp/cpp_typecheck.h
+++ b/src/cpp/cpp_typecheck.h
@@ -136,13 +136,6 @@ class cpp_typecheckt:public c_typecheck_baset
     const template_typet &old_type,
     template_typet &new_type);
 
-  #if 0
-  void check_template_restrictions(
-    const irept &cpp_name,
-    const irep_idt &final_identifier,
-    const typet &final_type);
-  #endif
-
   void convert_template_declaration(cpp_declarationt &declaration);
 
   void convert_non_template_declaration(cpp_declarationt &declaration);
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
index 002cdb51f69..79c609a0a4b 100644
--- a/src/cpp/cpp_typecheck_template.cpp
+++ b/src/cpp/cpp_typecheck_template.cpp
@@ -48,41 +48,6 @@ void cpp_typecheckt::salvage_default_arguments(
   }
 }
 
-#if 0
-/*******************************************************************\
-
-Function: cpp_typecheckt::check_template_restrictions
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void cpp_typecheckt::check_template_restrictions(
-  const irept &cpp_name,
-  const irep_idt &final_identifier,
-  const typet &final_type)
-{
-  if(final_type.id()==ID_template)
-  {
-    // subtype must be class or function
-
-    if(final_type.subtype().id()!=ID_struct &&
-       final_type.subtype().id()!=ID_code)
-    {
-      error().source_location=cpp_name.location();
-      error() << "template only allowed with classes or functions,"
-              << " but got `" << to_string(final_type.subtype())
-              << "'" << eom;
-      throw 0;
-    }
-  }
-}
-#endif
-
 /*******************************************************************\
 
 Function: cpp_typecheckt::typecheck_class_template