Skip to content

Commit 1dc27ae

Browse files
reukreuk
committed
Build cleanly without globally disabling warnings
Disabling warnings globally by setting 'Wno-deprecated-register' and 'Wno-sign-compare' in CXXFLAGS will silence these errors, even in new code. It's better to use `pragma`-based warning suppression, so that warnings are only disabled in locations that won't or can't be fixed. Likewise, rather than filtering 'Wpedantic' from CXXFLAGS when building some of the solvers, it's better to disable warnings just on the problematic headers.
1 parent 340a5ff commit 1dc27ae

19 files changed

+160
-43
lines changed

‎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>
50+
+#include <util/pragma_wzero_length_array>
51+
union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
52+
+#include <util/pragma_pop>
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

+6
Original file line numberDiff line numberDiff line change
@@ -3618,7 +3618,10 @@ std::string expr2ct::convert_code_block(
36183618
const code_blockt &src,
36193619
unsigned indent)
36203620
{
3621+
#include <util/pragma_push>
3622+
#include <util/pragma_wtautological_compare>
36213623
assert(indent>=0);
3624+
#include <util/pragma_pop>
36223625
std::string dest=indent_str(indent);
36233626
dest+="{\n";
36243627

@@ -3654,7 +3657,10 @@ std::string expr2ct::convert_code_decl_block(
36543657
const codet &src,
36553658
unsigned indent)
36563659
{
3660+
#include <util/pragma_push> // NOLINT(build/include)
3661+
#include <util/pragma_wtautological_compare> // NOLINT(build/include)
36573662
assert(indent>=0);
3663+
#include <util/pragma_pop> // NOLINT(build/include)
36583664
std::string dest;
36593665

36603666
forall_operands(it, src)

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

+15
Original file line numberDiff line numberDiff line change
@@ -188,7 +188,10 @@ __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+
#include <util/pragma_push>
192+
#include <util/pragma_wtautological_compare>
191193
for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_NODES; ++i)
194+
#include <util/pragma_pop>
192195
{
193196
const __CPROVER_jsa_abstract_nodet lhs_node=lhs->abstract_nodes[i];
194197
const __CPROVER_jsa_abstract_nodet rhs_node=rhs->abstract_nodes[i];
@@ -198,7 +201,10 @@ __CPROVER_jsa_inline _Bool __CPROVER_jsa__internal_are_heaps_equal(
198201
lhs_node.value_ref!=rhs_node.value_ref)
199202
return false;
200203
}
204+
#include <util/pragma_push> // NOLINT(build/include)
205+
#include <util/pragma_wtautological_compare> // NOLINT(build/include)
201206
for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_RANGES; ++i)
207+
#include <util/pragma_pop> // NOLINT(build/include)
202208
{
203209
const __CPROVER_jsa_abstract_ranget lhs_range=lhs->abstract_ranges[i];
204210
const __CPROVER_jsa_abstract_ranget rhs_range=rhs->abstract_ranges[i];
@@ -592,9 +598,12 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
592598
__CPROVER_jsa__internal_assume_linking_correct(h, cnode, prev, nxt);
593599
}
594600
}
601+
#include <util/pragma_push> // NOLINT(build/include)
602+
#include <util/pragma_wtautological_compare> // NOLINT(build/include)
595603
for(__CPROVER_jsa__internal_index_t anode=0;
596604
anode<__CPROVER_JSA_MAX_ABSTRACT_NODES;
597605
++anode)
606+
#include <util/pragma_pop> // NOLINT(build/include)
598607
{
599608
const __CPROVER_jsa_id_t nxt=h->abstract_nodes[anode].next;
600609
__CPROVER_jsa_assume(__CPROVER_jsa__internal_is_valid_node_id(nxt));
@@ -604,9 +613,12 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
604613
__CPROVER_jsa__internal_get_abstract_node_id(anode);
605614
__CPROVER_jsa__internal_assume_linking_correct(h, nid, prev, nxt);
606615
}
616+
#include <util/pragma_push> // NOLINT(build/include)
617+
#include <util/pragma_wtautological_compare> // NOLINT(build/include)
607618
for(__CPROVER_jsa__internal_index_t range=0;
608619
range<__CPROVER_JSA_MAX_ABSTRACT_RANGES;
609620
++range)
621+
#include <util/pragma_pop> // NOLINT(build/include)
610622
{
611623
const __CPROVER_jsa_abstract_ranget r=h->abstract_ranges[range];
612624
__CPROVER_jsa_assume(r.size >= 1);
@@ -653,9 +665,12 @@ __CPROVER_jsa_inline void __CPROVER_jsa_assume_valid_heap(
653665
++cnodec)
654666
if(h->concrete_nodes[cnodec].list == listc)
655667
++count;
668+
#include <util/pragma_push> // NOLINT(build/include)
669+
#include <util/pragma_wtautological_compare> // NOLINT(build/include)
656670
for(__CPROVER_jsa__internal_index_t anodec=0;
657671
anodec<__CPROVER_JSA_MAX_ABSTRACT_NODES;
658672
++anodec)
673+
#include <util/pragma_pop> // NOLINT(build/include)
659674
if(h->abstract_nodes[anodec].list==listc)
660675
++count;
661676
__CPROVER_jsa_assume(count<=__CPROVER_JSA_MAX_NODES_PER_CE_LIST);

‎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>
168+
#include <util/pragma_wnull_conversion>
169+
#include <util/pragma_wdeprecated_register>
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>
19+
#include <util/pragma_wnull_conversion>
20+
#include <util/pragma_wdeprecated_register>
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>
40+
#include <util/pragma_wnull_conversion>
41+
#include <util/pragma_wdeprecated_register>
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>
23+
#include <util/pragma_wnull_conversion>
24+
#include <util/pragma_wdeprecated_register>
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>
23+
#include <util/pragma_wnull_conversion>
24+
#include <util/pragma_wdeprecated_register>
25+
2226
%}
2327

2428
%x GRAMMAR

‎src/path-symex/locs.h

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

5757
loct &operator[] (loc_reft l)
5858
{
59+
#include <util/pragma_push>
60+
#include <util/pragma_wtautological_compare>
5961
assert(l.loc_number>=0 && l.loc_number<loc_vector.size());
62+
#include <util/pragma_pop>
6063
return loc_vector[l.loc_number];
6164
}
6265

6366
const loct &operator[] (loc_reft l) const
6467
{
68+
#include <util/pragma_push> // NOLINT(build/include)
69+
#include <util/pragma_wtautological_compare> // NOLINT(build/include)
6570
assert(l.loc_number>=0 && l.loc_number<loc_vector.size());
71+
#include <util/pragma_pop> // NOLINT(build/include)
6672
return loc_vector[l.loc_number];
6773
}
6874

‎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),)

‎src/util/pragma_pop

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#if defined __clang__
2+
#pragma clang diagnostic pop
3+
#elif defined __GNUC__
4+
#pragma GCC diagnostic pop
5+
#elif defined _MSC_VER
6+
#pragma warning(pop)
7+
#endif

0 commit comments

Comments
 (0)