Dup of #873 targeting test-gen-support

.travis.yml

@@ -143,7 +143,7 @@ matrix:
 install:
   - 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 $EXTRA_CXXFLAGS\" -j2" &&
+  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
     eval ${PRE_COMMAND} ${COMMAND}
   - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
     eval ${PRE_COMMAND} ${COMMAND}

scripts/minisat-2.2.1-patch

@@ -1,7 +1,8 @@
-diff -urN minisat-2.2.1/minisat/core/Solver.cc minisat-2.2.1.patched/minisat/core/Solver.cc
---- minisat-2.2.1/minisat/core/Solver.cc	2011-02-21 13:31:17.000000000 +0000
-+++ minisat-2.2.1.patched/minisat/core/Solver.cc	2016-03-05 16:21:17.000000000 +0000
-@@ -210,7 +210,7 @@
+diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc
+index 501393d..b450b73 100644
+--- a/minisat/core/Solver.cc
++++ b/minisat/core/Solver.cc
+@@ -210,7 +210,7 @@ void Solver::cancelUntil(int level) {
          for (int c = trail.size()-1; c >= trail_lim[level]; c--){
              Var      x  = var(trail[c]);
              assigns [x] = l_Undef;
@@ -10,7 +11,7 @@ diff -urN minisat-2.2.1/minisat/core/Solver.cc minisat-2.2.1.patched/minisat/cor
                  polarity[x] = sign(trail[c]);
              insertVarOrder(x); }
          qhead = trail_lim[level];
-@@ -666,7 +666,7 @@
+@@ -666,7 +666,7 @@ lbool Solver::search(int nof_conflicts)
 
          }else{
              // NO CONFLICT
@@ -19,10 +20,11 @@ diff -urN minisat-2.2.1/minisat/core/Solver.cc minisat-2.2.1.patched/minisat/cor
                  // Reached bound on number of conflicts:
                  progress_estimate = progressEstimate();
                  cancelUntil(0);
-diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat/core/SolverTypes.h
---- minisat-2.2.1/minisat/core/SolverTypes.h	2011-02-21 13:31:17.000000000 +0000
-+++ minisat-2.2.1.patched/minisat/core/SolverTypes.h	2016-03-05 16:29:42.000000000 +0000
-@@ -47,7 +47,7 @@
+diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h
+index 4757b20..c3fae2b 100644
+--- a/minisat/core/SolverTypes.h
++++ b/minisat/core/SolverTypes.h
+@@ -47,7 +47,7 @@ struct Lit {
      int     x;
 
      // Use this as a constructor:
@@ -31,7 +33,7 @@ diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat
 
      bool operator == (Lit p) const { return x == p.x; }
      bool operator != (Lit p) const { return x != p.x; }
-@@ -55,7 +55,7 @@
+@@ -55,7 +55,7 @@ struct Lit {
  };
 
 
@@ -40,7 +42,18 @@ diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat
  inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
  inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
  inline  bool sign      (Lit p)              { return p.x & 1; }
-@@ -142,11 +142,12 @@
+@@ -127,7 +127,10 @@ class Clause {
+         unsigned has_extra : 1;
+         unsigned reloced   : 1;
+         unsigned size      : 27; }                        header;
++#include <util/pragma_push.def>
++#include <util/pragma_wzero_length_array.def>
+     union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
++#include <util/pragma_pop.def>
+
+     friend class ClauseAllocator;
+
+@@ -142,11 +145,12 @@ class Clause {
          for (int i = 0; i < ps.size(); i++) 
              data[i].lit = ps[i];
 
@@ -54,7 +67,7 @@ diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat
      }
 
      // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
-@@ -157,11 +158,12 @@
+@@ -157,11 +161,12 @@ class Clause {
          for (int i = 0; i < from.size(); i++)
              data[i].lit = from[i];
 
@@ -68,10 +81,11 @@ diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat
      }
 
  public:
-diff -urN minisat-2.2.1/minisat/mtl/IntTypes.h minisat-2.2.1.patched/minisat/mtl/IntTypes.h
---- minisat-2.2.1/minisat/mtl/IntTypes.h	2011-02-21 13:31:17.000000000 +0000
-+++ minisat-2.2.1.patched/minisat/mtl/IntTypes.h	2016-03-05 16:21:17.000000000 +0000
-@@ -31,7 +31,9 @@
+diff --git a/minisat/mtl/IntTypes.h b/minisat/mtl/IntTypes.h
+index c488162..e8e24bd 100644
+--- a/minisat/mtl/IntTypes.h
++++ b/minisat/mtl/IntTypes.h
+@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
  #else
 
  #   include <stdint.h>
@@ -81,10 +95,11 @@ diff -urN minisat-2.2.1/minisat/mtl/IntTypes.h minisat-2.2.1.patched/minisat/mtl
 
  #endif
 
-diff -urN minisat-2.2.1/minisat/mtl/Vec.h minisat-2.2.1.patched/minisat/mtl/Vec.h
---- minisat-2.2.1/minisat/mtl/Vec.h	2011-02-21 13:31:17.000000000 +0000
-+++ minisat-2.2.1.patched/minisat/mtl/Vec.h	2016-03-05 16:21:17.000000000 +0000
-@@ -96,7 +96,7 @@
+diff --git a/minisat/mtl/Vec.h b/minisat/mtl/Vec.h
+index b225911..d46e169 100644
+--- a/minisat/mtl/Vec.h
++++ b/minisat/mtl/Vec.h
+@@ -96,7 +96,7 @@ template<class T>
  void vec<T>::capacity(int min_cap) {
      if (cap >= min_cap) return;
      int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);   // NOTE: grow by approximately 3/2
@@ -93,10 +108,11 @@ diff -urN minisat-2.2.1/minisat/mtl/Vec.h minisat-2.2.1.patched/minisat/mtl/Vec.
          throw OutOfMemoryException();
   }
 
-diff -urN minisat-2.2.1/minisat/simp/SimpSolver.cc minisat-2.2.1.patched/minisat/simp/SimpSolver.cc
---- minisat-2.2.1/minisat/simp/SimpSolver.cc	2011-02-21 13:31:17.000000000 +0000
-+++ minisat-2.2.1.patched/minisat/simp/SimpSolver.cc	2016-03-05 16:21:17.000000000 +0000
-@@ -130,8 +130,6 @@
+diff --git a/minisat/simp/SimpSolver.cc b/minisat/simp/SimpSolver.cc
+index 1d219a3..5ccdb67 100644
+--- a/minisat/simp/SimpSolver.cc
++++ b/minisat/simp/SimpSolver.cc
+@@ -130,8 +130,6 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
      return result;
  }
 
@@ -105,7 +121,7 @@ diff -urN minisat-2.2.1/minisat/simp/SimpSolver.cc minisat-2.2.1.patched/minisat
  bool SimpSolver::addClause_(vec<Lit>& ps)
  {
  #ifndef NDEBUG
-@@ -227,10 +225,12 @@
+@@ -227,10 +225,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
          if (var(qs[i]) != v){
              for (int j = 0; j < ps.size(); j++)
                  if (var(ps[j]) == var(qs[i]))
@@ -118,7 +134,7 @@ diff -urN minisat-2.2.1/minisat/simp/SimpSolver.cc minisat-2.2.1.patched/minisat
              out_clause.push(qs[i]);
          }
          next:;
-@@ -261,10 +261,12 @@
+@@ -261,10 +261,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
          if (var(__qs[i]) != v){
              for (int j = 0; j < ps.size(); j++)
                  if (var(__ps[j]) == var(__qs[i]))
@@ -131,10 +147,11 @@ diff -urN minisat-2.2.1/minisat/simp/SimpSolver.cc minisat-2.2.1.patched/minisat
              size++;
          }
          next:;
-diff -urN minisat-2.2.1/minisat/utils/Options.h minisat-2.2.1.patched/minisat/utils/Options.h
---- minisat-2.2.1/minisat/utils/Options.h	2011-02-21 13:31:17.000000000 +0000
-+++ minisat-2.2.1.patched/minisat/utils/Options.h	2016-03-05 16:21:17.000000000 +0000
-@@ -60,7 +60,7 @@
+diff --git a/minisat/utils/Options.h b/minisat/utils/Options.h
+index 2dba10f..7d2e83a 100644
+--- a/minisat/utils/Options.h
++++ b/minisat/utils/Options.h
+@@ -60,7 +60,7 @@ class Option
      struct OptionLt {
          bool operator()(const Option* x, const Option* y) {
              int test1 = strcmp(x->category, y->category);
@@ -143,7 +160,7 @@ diff -urN minisat-2.2.1/minisat/utils/Options.h minisat-2.2.1.patched/minisat/ut
          }
      };
 
-@@ -282,15 +282,15 @@
+@@ -282,15 +282,15 @@ class Int64Option : public Option
          if (range.begin == INT64_MIN)
              fprintf(stderr, "imin");
          else
@@ -162,10 +179,11 @@ diff -urN minisat-2.2.1/minisat/utils/Options.h minisat-2.2.1.patched/minisat/ut
          if (verbose){
              fprintf(stderr, "\n        %s\n", description);
              fprintf(stderr, "\n");
-diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat/utils/ParseUtils.h
---- minisat-2.2.1/minisat/utils/ParseUtils.h	2011-02-21 13:31:17.000000000 +0000
-+++ minisat-2.2.1.patched/minisat/utils/ParseUtils.h	2016-03-05 16:21:17.000000000 +0000
-@@ -24,7 +24,7 @@
+diff --git a/minisat/utils/ParseUtils.h b/minisat/utils/ParseUtils.h
+index d307164..7b46f09 100644
+--- a/minisat/utils/ParseUtils.h
++++ b/minisat/utils/ParseUtils.h
+@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
  #include <stdlib.h>
  #include <stdio.h>
 
@@ -174,7 +192,7 @@ diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat
 
  namespace Minisat {
 
-@@ -35,7 +35,7 @@
+@@ -35,7 +35,7 @@ static const int buffer_size = 1048576;
 
 
  class StreamBuffer {
@@ -183,7 +201,7 @@ diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat
      unsigned char buf[buffer_size];
      int           pos;
      int           size;
-@@ -43,10 +43,10 @@
+@@ -43,10 +43,10 @@ class StreamBuffer {
      void assureLookahead() {
          if (pos >= size) {
              pos  = 0;
@@ -196,10 +214,11 @@ diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat
 
      int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }
      void operator ++ ()       { pos++; assureLookahead(); }
-diff -urN minisat-2.2.1/minisat/utils/System.h minisat-2.2.1.patched/minisat/utils/System.h
---- minisat-2.2.1/minisat/utils/System.h	2017-02-21 18:23:22.727464369 +0000
-+++ minisat-2.2.1.patched/minisat/utils/System.h	2017-02-21 18:23:14.451343361 +0000
-@@ -21,7 +21,7 @@
+diff --git a/minisat/utils/System.h b/minisat/utils/System.h
+index 9cbbc51..27b9700 100644
+--- a/minisat/utils/System.h
++++ b/minisat/utils/System.h
+@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
  #ifndef Minisat_System_h
  #define Minisat_System_h
 

src/ansi-c/expr2c.cpp

@@ -3630,7 +3630,6 @@ std::string expr2ct::convert_code_block(
   const code_blockt &src,
   unsigned indent)
 {
-  assert(indent>=0);
   std::string dest=indent_str(indent);
   dest+="{\n";
 
@@ -3666,7 +3665,6 @@ std::string expr2ct::convert_code_decl_block(
   const codet &src,
   unsigned indent)
 {
-  assert(indent>=0);
   std::string dest;
 
   forall_operands(it, src)

src/ansi-c/library/jsa.h

@@ -188,6 +188,7 @@ __CPROVER_jsa_inline _Bool __CPROVER_jsa__internal_are_heaps_equal(
   const __CPROVER_jsa_abstract_heapt *const rhs)
 {
   __CPROVER_jsa__internal_index_t i;
+#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
   for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_NODES; ++i)
   {
     const __CPROVER_jsa_abstract_nodet lhs_node=lhs->abstract_nodes[i];
@@ -198,6 +199,8 @@ __CPROVER_jsa_inline _Bool __CPROVER_jsa__internal_are_heaps_equal(
        lhs_node.value_ref!=rhs_node.value_ref)
       return false;
   }
+#endif
+#if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES
   for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_RANGES; ++i)
   {
     const __CPROVER_jsa_abstract_ranget lhs_range=lhs->abstract_ranges[i];
@@ -207,6 +210,7 @@ __CPROVER_jsa_inline _Bool __CPROVER_jsa__internal_are_heaps_equal(
        lhs_range.size!=rhs_range.size)
       return false;
   }
+#endif
   for(i=0; i < __CPROVER_JSA_MAX_CONCRETE_NODES; ++i)
   {
     const __CPROVER_jsa_concrete_nodet lhs_node=lhs->concrete_nodes[i];
@@ -592,6 +596,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
       __CPROVER_jsa__internal_assume_linking_correct(h, cnode, prev, nxt);
     }
   }
+#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
   for(__CPROVER_jsa__internal_index_t anode=0;
       anode<__CPROVER_JSA_MAX_ABSTRACT_NODES;
       ++anode)
@@ -604,6 +609,8 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
       __CPROVER_jsa__internal_get_abstract_node_id(anode);
     __CPROVER_jsa__internal_assume_linking_correct(h, nid, prev, nxt);
   }
+#endif
+#if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES
   for(__CPROVER_jsa__internal_index_t range=0;
       range<__CPROVER_JSA_MAX_ABSTRACT_RANGES;
       ++range)
@@ -612,6 +619,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
     __CPROVER_jsa_assume(r.size >= 1);
     __CPROVER_jsa_assume(r.min <= r.max);
   }
+#endif
   // Iterators point to valid nodes
   __CPROVER_jsa_assume(h->iterator_count <= __CPROVER_JSA_MAX_ITERATORS);
   for(__CPROVER_jsa_iterator_id_t it=0; it < __CPROVER_JSA_MAX_ITERATORS; ++it)
@@ -653,11 +661,13 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
         ++cnodec)
       if(h->concrete_nodes[cnodec].list == listc)
         ++count;
+#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
     for(__CPROVER_jsa__internal_index_t anodec=0;
         anodec<__CPROVER_JSA_MAX_ABSTRACT_NODES;
         ++anodec)
       if(h->abstract_nodes[anodec].list==listc)
         ++count;
+#endif
     __CPROVER_jsa_assume(count<=__CPROVER_JSA_MAX_NODES_PER_CE_LIST);
   }
 }

src/ansi-c/scanner.l

@@ -164,6 +164,10 @@ int cpp_operator(int token)
   }
 }
 
+#include <util/pragma_wsign_compare.def>
+#include <util/pragma_wnull_conversion.def>
+#include <util/pragma_wdeprecated_register.def>
+
 /*** macros for easier rule definition **********************************/
 %}
 

src/assembler/scanner.l

@@ -15,6 +15,10 @@ static int isatty(int) { return 0; }
 
 #include "assembler_parser.h"
 
+#include <util/pragma_wsign_compare.def>
+#include <util/pragma_wnull_conversion.def>
+#include <util/pragma_wdeprecated_register.def>
+
 /*** macros for easier rule definition **********************************/
 %}
 

src/jsil/scanner.l

@@ -36,6 +36,10 @@ static int make_identifier()
   return TOK_IDENTIFIER;
 }
 
+#include <util/pragma_wsign_compare.def>
+#include <util/pragma_wnull_conversion.def>
+#include <util/pragma_wdeprecated_register.def>
+
 %}
 
 delimiter       [ \t\b\r]

src/json/scanner.l

@@ -18,6 +18,11 @@ static int isatty(int) { return 0; }
 
 #include "json_parser.h"
 #include "json_y.tab.h"
+
+#include <util/pragma_wsign_compare.def>
+#include <util/pragma_wnull_conversion.def>
+#include <util/pragma_wdeprecated_register.def>
+
 %}
 
 string  \"\"|\"{chars}\"

src/memory-models/scanner.l

@@ -19,6 +19,10 @@ static int isatty(int) { return 0; }
 
 unsigned comment_nesting;
 
+#include <util/pragma_wsign_compare.def>
+#include <util/pragma_wnull_conversion.def>
+#include <util/pragma_wdeprecated_register.def>
+
 %}
 
 %x GRAMMAR

src/path-symex/locs.h

@@ -56,13 +56,13 @@ class locst
 
   loct &operator[] (loc_reft l)
   {
-    assert(l.loc_number>=0 && l.loc_number<loc_vector.size());
+    assert(l.loc_number<loc_vector.size());
     return loc_vector[l.loc_number];
   }
 
   const loct &operator[] (loc_reft l) const
   {
-    assert(l.loc_number>=0 && l.loc_number<loc_vector.size());
+    assert(l.loc_number<loc_vector.size());
     return loc_vector[l.loc_number];
   }
 

src/solvers/Makefile

@@ -19,15 +19,13 @@ ifneq ($(MINISAT2),)
   MINISAT2_INCLUDE=-I $(MINISAT2)
   MINISAT2_LIB=$(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT) $(MINISAT2)/minisat/core/Solver$(OBJEXT)
   CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
-  override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
 endif
 
 ifneq ($(GLUCOSE),)
   GLUCOSE_SRC=sat/satcheck_glucose.cpp
   GLUCOSE_INCLUDE=-I $(GLUCOSE)
   GLUCOSE_LIB=$(GLUCOSE)/simp/SimpSolver$(OBJEXT) $(GLUCOSE)/core/Solver$(OBJEXT)
   CP_CXXFLAGS += -DHAVE_GLUCOSE -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
-  override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
 endif
 
 ifneq ($(SMVSAT),)