Skip to content

Commit 05d1ec6

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #938 from reuk/pedantic-fix-test-gen-support
Dup of #873 targeting test-gen-support
2 parents f22a696 + f4ba652 commit 05d1ec6

21 files changed

+147
-49
lines changed

‎.travis.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,7 @@ matrix:
143143
install:
144144
- COMMAND="make -C src minisat2-download" &&
145145
eval ${PRE_COMMAND} ${COMMAND}
146-
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare $EXTRA_CXXFLAGS\" -j2" &&
146+
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
147147
eval ${PRE_COMMAND} ${COMMAND}
148148
- COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 cegis.dir clobber.dir memory-models.dir musketeer.dir" &&
149149
eval ${PRE_COMMAND} ${COMMAND}

‎scripts/minisat-2.2.1-patch

+60-41
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
1-
diff -urN minisat-2.2.1/minisat/core/Solver.cc minisat-2.2.1.patched/minisat/core/Solver.cc
2-
--- minisat-2.2.1/minisat/core/Solver.cc 2011-02-21 13:31:17.000000000 +0000
3-
+++ minisat-2.2.1.patched/minisat/core/Solver.cc 2016-03-05 16:21:17.000000000 +0000
4-
@@ -210,7 +210,7 @@
1+
diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc
2+
index 501393d..b450b73 100644
3+
--- a/minisat/core/Solver.cc
4+
+++ b/minisat/core/Solver.cc
5+
@@ -210,7 +210,7 @@ void Solver::cancelUntil(int level) {
56
for (int c = trail.size()-1; c >= trail_lim[level]; c--){
67
Var x = var(trail[c]);
78
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
1011
polarity[x] = sign(trail[c]);
1112
insertVarOrder(x); }
1213
qhead = trail_lim[level];
13-
@@ -666,7 +666,7 @@
14+
@@ -666,7 +666,7 @@ lbool Solver::search(int nof_conflicts)
1415

1516
}else{
1617
// NO CONFLICT
@@ -19,10 +20,11 @@ diff -urN minisat-2.2.1/minisat/core/Solver.cc minisat-2.2.1.patched/minisat/cor
1920
// Reached bound on number of conflicts:
2021
progress_estimate = progressEstimate();
2122
cancelUntil(0);
22-
diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat/core/SolverTypes.h
23-
--- minisat-2.2.1/minisat/core/SolverTypes.h 2011-02-21 13:31:17.000000000 +0000
24-
+++ minisat-2.2.1.patched/minisat/core/SolverTypes.h 2016-03-05 16:29:42.000000000 +0000
25-
@@ -47,7 +47,7 @@
23+
diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h
24+
index 4757b20..c3fae2b 100644
25+
--- a/minisat/core/SolverTypes.h
26+
+++ b/minisat/core/SolverTypes.h
27+
@@ -47,7 +47,7 @@ struct Lit {
2628
int x;
2729

2830
// 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
3133

3234
bool operator == (Lit p) const { return x == p.x; }
3335
bool operator != (Lit p) const { return x != p.x; }
34-
@@ -55,7 +55,7 @@
36+
@@ -55,7 +55,7 @@ struct Lit {
3537
};
3638

3739

@@ -40,7 +42,18 @@ diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat
4042
inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
4143
inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
4244
inline bool sign (Lit p) { return p.x & 1; }
43-
@@ -142,11 +142,12 @@
45+
@@ -127,7 +127,10 @@ class Clause {
46+
unsigned has_extra : 1;
47+
unsigned reloced : 1;
48+
unsigned size : 27; } header;
49+
+#include <util/pragma_push.def>
50+
+#include <util/pragma_wzero_length_array.def>
51+
union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
52+
+#include <util/pragma_pop.def>
53+
54+
friend class ClauseAllocator;
55+
56+
@@ -142,11 +145,12 @@ class Clause {
4457
for (int i = 0; i < ps.size(); i++)
4558
data[i].lit = ps[i];
4659

@@ -54,7 +67,7 @@ diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat
5467
}
5568

5669
// NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
57-
@@ -157,11 +158,12 @@
70+
@@ -157,11 +161,12 @@ class Clause {
5871
for (int i = 0; i < from.size(); i++)
5972
data[i].lit = from[i];
6073

@@ -68,10 +81,11 @@ diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat
6881
}
6982

7083
public:
71-
diff -urN minisat-2.2.1/minisat/mtl/IntTypes.h minisat-2.2.1.patched/minisat/mtl/IntTypes.h
72-
--- minisat-2.2.1/minisat/mtl/IntTypes.h 2011-02-21 13:31:17.000000000 +0000
73-
+++ minisat-2.2.1.patched/minisat/mtl/IntTypes.h 2016-03-05 16:21:17.000000000 +0000
74-
@@ -31,7 +31,9 @@
84+
diff --git a/minisat/mtl/IntTypes.h b/minisat/mtl/IntTypes.h
85+
index c488162..e8e24bd 100644
86+
--- a/minisat/mtl/IntTypes.h
87+
+++ b/minisat/mtl/IntTypes.h
88+
@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
7589
#else
7690

7791
# include <stdint.h>
@@ -81,10 +95,11 @@ diff -urN minisat-2.2.1/minisat/mtl/IntTypes.h minisat-2.2.1.patched/minisat/mtl
8195

8296
#endif
8397

84-
diff -urN minisat-2.2.1/minisat/mtl/Vec.h minisat-2.2.1.patched/minisat/mtl/Vec.h
85-
--- minisat-2.2.1/minisat/mtl/Vec.h 2011-02-21 13:31:17.000000000 +0000
86-
+++ minisat-2.2.1.patched/minisat/mtl/Vec.h 2016-03-05 16:21:17.000000000 +0000
87-
@@ -96,7 +96,7 @@
98+
diff --git a/minisat/mtl/Vec.h b/minisat/mtl/Vec.h
99+
index b225911..d46e169 100644
100+
--- a/minisat/mtl/Vec.h
101+
+++ b/minisat/mtl/Vec.h
102+
@@ -96,7 +96,7 @@ template<class T>
88103
void vec<T>::capacity(int min_cap) {
89104
if (cap >= min_cap) return;
90105
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.
93108
throw OutOfMemoryException();
94109
}
95110

96-
diff -urN minisat-2.2.1/minisat/simp/SimpSolver.cc minisat-2.2.1.patched/minisat/simp/SimpSolver.cc
97-
--- minisat-2.2.1/minisat/simp/SimpSolver.cc 2011-02-21 13:31:17.000000000 +0000
98-
+++ minisat-2.2.1.patched/minisat/simp/SimpSolver.cc 2016-03-05 16:21:17.000000000 +0000
99-
@@ -130,8 +130,6 @@
111+
diff --git a/minisat/simp/SimpSolver.cc b/minisat/simp/SimpSolver.cc
112+
index 1d219a3..5ccdb67 100644
113+
--- a/minisat/simp/SimpSolver.cc
114+
+++ b/minisat/simp/SimpSolver.cc
115+
@@ -130,8 +130,6 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
100116
return result;
101117
}
102118

@@ -105,7 +121,7 @@ diff -urN minisat-2.2.1/minisat/simp/SimpSolver.cc minisat-2.2.1.patched/minisat
105121
bool SimpSolver::addClause_(vec<Lit>& ps)
106122
{
107123
#ifndef NDEBUG
108-
@@ -227,10 +225,12 @@
124+
@@ -227,10 +225,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
109125
if (var(qs[i]) != v){
110126
for (int j = 0; j < ps.size(); j++)
111127
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
118134
out_clause.push(qs[i]);
119135
}
120136
next:;
121-
@@ -261,10 +261,12 @@
137+
@@ -261,10 +261,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
122138
if (var(__qs[i]) != v){
123139
for (int j = 0; j < ps.size(); j++)
124140
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
131147
size++;
132148
}
133149
next:;
134-
diff -urN minisat-2.2.1/minisat/utils/Options.h minisat-2.2.1.patched/minisat/utils/Options.h
135-
--- minisat-2.2.1/minisat/utils/Options.h 2011-02-21 13:31:17.000000000 +0000
136-
+++ minisat-2.2.1.patched/minisat/utils/Options.h 2016-03-05 16:21:17.000000000 +0000
137-
@@ -60,7 +60,7 @@
150+
diff --git a/minisat/utils/Options.h b/minisat/utils/Options.h
151+
index 2dba10f..7d2e83a 100644
152+
--- a/minisat/utils/Options.h
153+
+++ b/minisat/utils/Options.h
154+
@@ -60,7 +60,7 @@ class Option
138155
struct OptionLt {
139156
bool operator()(const Option* x, const Option* y) {
140157
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
143160
}
144161
};
145162

146-
@@ -282,15 +282,15 @@
163+
@@ -282,15 +282,15 @@ class Int64Option : public Option
147164
if (range.begin == INT64_MIN)
148165
fprintf(stderr, "imin");
149166
else
@@ -162,10 +179,11 @@ diff -urN minisat-2.2.1/minisat/utils/Options.h minisat-2.2.1.patched/minisat/ut
162179
if (verbose){
163180
fprintf(stderr, "\n %s\n", description);
164181
fprintf(stderr, "\n");
165-
diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat/utils/ParseUtils.h
166-
--- minisat-2.2.1/minisat/utils/ParseUtils.h 2011-02-21 13:31:17.000000000 +0000
167-
+++ minisat-2.2.1.patched/minisat/utils/ParseUtils.h 2016-03-05 16:21:17.000000000 +0000
168-
@@ -24,7 +24,7 @@
182+
diff --git a/minisat/utils/ParseUtils.h b/minisat/utils/ParseUtils.h
183+
index d307164..7b46f09 100644
184+
--- a/minisat/utils/ParseUtils.h
185+
+++ b/minisat/utils/ParseUtils.h
186+
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
169187
#include <stdlib.h>
170188
#include <stdio.h>
171189

@@ -174,7 +192,7 @@ diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat
174192

175193
namespace Minisat {
176194

177-
@@ -35,7 +35,7 @@
195+
@@ -35,7 +35,7 @@ static const int buffer_size = 1048576;
178196

179197

180198
class StreamBuffer {
@@ -183,7 +201,7 @@ diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat
183201
unsigned char buf[buffer_size];
184202
int pos;
185203
int size;
186-
@@ -43,10 +43,10 @@
204+
@@ -43,10 +43,10 @@ class StreamBuffer {
187205
void assureLookahead() {
188206
if (pos >= size) {
189207
pos = 0;
@@ -196,10 +214,11 @@ diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat
196214

197215
int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
198216
void operator ++ () { pos++; assureLookahead(); }
199-
diff -urN minisat-2.2.1/minisat/utils/System.h minisat-2.2.1.patched/minisat/utils/System.h
200-
--- minisat-2.2.1/minisat/utils/System.h 2017-02-21 18:23:22.727464369 +0000
201-
+++ minisat-2.2.1.patched/minisat/utils/System.h 2017-02-21 18:23:14.451343361 +0000
202-
@@ -21,7 +21,7 @@
217+
diff --git a/minisat/utils/System.h b/minisat/utils/System.h
218+
index 9cbbc51..27b9700 100644
219+
--- a/minisat/utils/System.h
220+
+++ b/minisat/utils/System.h
221+
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
203222
#ifndef Minisat_System_h
204223
#define Minisat_System_h
205224

‎src/ansi-c/expr2c.cpp

-2
Original file line numberDiff line numberDiff line change
@@ -3630,7 +3630,6 @@ std::string expr2ct::convert_code_block(
36303630
const code_blockt &src,
36313631
unsigned indent)
36323632
{
3633-
assert(indent>=0);
36343633
std::string dest=indent_str(indent);
36353634
dest+="{\n";
36363635

@@ -3666,7 +3665,6 @@ std::string expr2ct::convert_code_decl_block(
36663665
const codet &src,
36673666
unsigned indent)
36683667
{
3669-
assert(indent>=0);
36703668
std::string dest;
36713669

36723670
forall_operands(it, src)

‎src/ansi-c/library/jsa.h

+10
Original file line numberDiff line numberDiff line change
@@ -188,6 +188,7 @@ __CPROVER_jsa_inline _Bool __CPROVER_jsa__internal_are_heaps_equal(
188188
const __CPROVER_jsa_abstract_heapt *const rhs)
189189
{
190190
__CPROVER_jsa__internal_index_t i;
191+
#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
191192
for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_NODES; ++i)
192193
{
193194
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(
198199
lhs_node.value_ref!=rhs_node.value_ref)
199200
return false;
200201
}
202+
#endif
203+
#if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES
201204
for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_RANGES; ++i)
202205
{
203206
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(
207210
lhs_range.size!=rhs_range.size)
208211
return false;
209212
}
213+
#endif
210214
for(i=0; i < __CPROVER_JSA_MAX_CONCRETE_NODES; ++i)
211215
{
212216
const __CPROVER_jsa_concrete_nodet lhs_node=lhs->concrete_nodes[i];
@@ -592,6 +596,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
592596
__CPROVER_jsa__internal_assume_linking_correct(h, cnode, prev, nxt);
593597
}
594598
}
599+
#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
595600
for(__CPROVER_jsa__internal_index_t anode=0;
596601
anode<__CPROVER_JSA_MAX_ABSTRACT_NODES;
597602
++anode)
@@ -604,6 +609,8 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
604609
__CPROVER_jsa__internal_get_abstract_node_id(anode);
605610
__CPROVER_jsa__internal_assume_linking_correct(h, nid, prev, nxt);
606611
}
612+
#endif
613+
#if 0 < __CPROVER_JSA_MAX_ABSTRACT_RANGES
607614
for(__CPROVER_jsa__internal_index_t range=0;
608615
range<__CPROVER_JSA_MAX_ABSTRACT_RANGES;
609616
++range)
@@ -612,6 +619,7 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
612619
__CPROVER_jsa_assume(r.size >= 1);
613620
__CPROVER_jsa_assume(r.min <= r.max);
614621
}
622+
#endif
615623
// Iterators point to valid nodes
616624
__CPROVER_jsa_assume(h->iterator_count <= __CPROVER_JSA_MAX_ITERATORS);
617625
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(
653661
++cnodec)
654662
if(h->concrete_nodes[cnodec].list == listc)
655663
++count;
664+
#if 0 < __CPROVER_JSA_MAX_ABSTRACT_NODES
656665
for(__CPROVER_jsa__internal_index_t anodec=0;
657666
anodec<__CPROVER_JSA_MAX_ABSTRACT_NODES;
658667
++anodec)
659668
if(h->abstract_nodes[anodec].list==listc)
660669
++count;
670+
#endif
661671
__CPROVER_jsa_assume(count<=__CPROVER_JSA_MAX_NODES_PER_CE_LIST);
662672
}
663673
}

‎src/ansi-c/scanner.l

+4
Original file line numberDiff line numberDiff line change
@@ -164,6 +164,10 @@ int cpp_operator(int token)
164164
}
165165
}
166166

167+
#include <util/pragma_wsign_compare.def>
168+
#include <util/pragma_wnull_conversion.def>
169+
#include <util/pragma_wdeprecated_register.def>
170+
167171
/*** macros for easier rule definition **********************************/
168172
%}
169173

‎src/assembler/scanner.l

+4
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,10 @@ static int isatty(int) { return 0; }
1515

1616
#include "assembler_parser.h"
1717

18+
#include <util/pragma_wsign_compare.def>
19+
#include <util/pragma_wnull_conversion.def>
20+
#include <util/pragma_wdeprecated_register.def>
21+
1822
/*** macros for easier rule definition **********************************/
1923
%}
2024

‎src/jsil/scanner.l

+4
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,10 @@ static int make_identifier()
3636
return TOK_IDENTIFIER;
3737
}
3838

39+
#include <util/pragma_wsign_compare.def>
40+
#include <util/pragma_wnull_conversion.def>
41+
#include <util/pragma_wdeprecated_register.def>
42+
3943
%}
4044

4145
delimiter [ \t\b\r]

‎src/json/scanner.l

+5
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@ static int isatty(int) { return 0; }
1818

1919
#include "json_parser.h"
2020
#include "json_y.tab.h"
21+
22+
#include <util/pragma_wsign_compare.def>
23+
#include <util/pragma_wnull_conversion.def>
24+
#include <util/pragma_wdeprecated_register.def>
25+
2126
%}
2227

2328
string \"\"|\"{chars}\"

‎src/memory-models/scanner.l

+4
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,10 @@ static int isatty(int) { return 0; }
1919

2020
unsigned comment_nesting;
2121

22+
#include <util/pragma_wsign_compare.def>
23+
#include <util/pragma_wnull_conversion.def>
24+
#include <util/pragma_wdeprecated_register.def>
25+
2226
%}
2327

2428
%x GRAMMAR

‎src/path-symex/locs.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -56,13 +56,13 @@ class locst
5656

5757
loct &operator[] (loc_reft l)
5858
{
59-
assert(l.loc_number>=0 && l.loc_number<loc_vector.size());
59+
assert(l.loc_number<loc_vector.size());
6060
return loc_vector[l.loc_number];
6161
}
6262

6363
const loct &operator[] (loc_reft l) const
6464
{
65-
assert(l.loc_number>=0 && l.loc_number<loc_vector.size());
65+
assert(l.loc_number<loc_vector.size());
6666
return loc_vector[l.loc_number];
6767
}
6868

‎src/solvers/Makefile

-2
Original file line numberDiff line numberDiff line change
@@ -19,15 +19,13 @@ ifneq ($(MINISAT2),)
1919
MINISAT2_INCLUDE=-I $(MINISAT2)
2020
MINISAT2_LIB=$(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT) $(MINISAT2)/minisat/core/Solver$(OBJEXT)
2121
CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
22-
override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
2322
endif
2423

2524
ifneq ($(GLUCOSE),)
2625
GLUCOSE_SRC=sat/satcheck_glucose.cpp
2726
GLUCOSE_INCLUDE=-I $(GLUCOSE)
2827
GLUCOSE_LIB=$(GLUCOSE)/simp/SimpSolver$(OBJEXT) $(GLUCOSE)/core/Solver$(OBJEXT)
2928
CP_CXXFLAGS += -DHAVE_GLUCOSE -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
30-
override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
3129
endif
3230

3331
ifneq ($(SMVSAT),)

0 commit comments

Comments
 (0)