Build cleanly without globally disabling warnings #873

reuk · 2017-04-26T12:02:21Z

Disabling warnings globally by setting 'Wno-deprecated-register' and 'Wno-sign-compare' in CXXFLAGS will silence these errors in all files, 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.

The goal is to create a clean build using the flags -Wall -Wpedantic -Werror on all platforms, without having to disable any errors.

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.

reuk · 2017-04-26T16:13:31Z

This is ready for review now (@tautschnig?)

tautschnig · 2017-04-26T16:18:54Z

Looking.

tautschnig

Thank you very much for this work. What I'd like to see a rationale for is the file-names-without-suffix choice. Furthermore I'm of course asking you to do even more work as those warnings have turned up actual bugs/useless checks.

tautschnig · 2017-04-26T16:21:37Z

scripts/minisat-2.2.1-patch

+index 501393d..b450b73 100644
+--- a/minisat/core/Solver.cc
+++ b/minisat/core/Solver.cc
+@@ -210,7 +210,7 @@ void Solver::cancelUntil(int level) {


I'd prefer for those changes to not be included (and similarly below), but also I'm not going to embark on bike shedding here.

tautschnig · 2017-04-26T16:22:19Z

scripts/minisat-2.2.1-patch

+         unsigned has_extra : 1;
+         unsigned reloced   : 1;
+         unsigned size      : 27; }                        header;
+#include <util/pragma_push>


I disagree with the choice of not using a suffix in the file name.

tautschnig · 2017-04-26T16:23:10Z

src/ansi-c/expr2c.cpp

  assert(indent>=0);
+#include <util/pragma_pop>


That assert should just be removed.

tautschnig · 2017-04-26T16:23:39Z

src/ansi-c/expr2c.cpp

  assert(indent>=0);
+#include <util/pragma_pop> // NOLINT(build/include)


Remove the assert instead.

tautschnig · 2017-04-26T16:25:54Z

src/ansi-c/library/jsa.h

  for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_NODES; ++i)
+#include <util/pragma_pop>


Any idea why we're getting a tautological-comparison warning here?

tautschnig · 2017-04-26T16:26:46Z

src/path-symex/locs.h

    assert(l.loc_number>=0 && l.loc_number<loc_vector.size());
+#include <util/pragma_pop>


The first condition in the assertion should be removed.

tautschnig · 2017-04-26T16:26:55Z

src/path-symex/locs.h

    assert(l.loc_number>=0 && l.loc_number<loc_vector.size());
+#include <util/pragma_pop> // NOLINT(build/include)


tautschnig · 2017-04-26T16:27:49Z

src/util/pragma_pop

@@ -0,0 +1,7 @@
+#if defined __clang__


What is the reason to use file names without suffix here?

reuk · 2017-04-26T17:18:45Z

Firstly, I agree that the asserts should be changed/removed.

The patch file changed because I recreated it with git (I had to add some stuff around the zero length array), but if there's another way that results in fewer changes then I'll do that instead.

The no-suffix thing is to differentiate the includes from normal headers or source files - where they don't include any declarations or definitions, it's a bit misleading to call them headers. I could give them some other extension though (.macro, .def or similar?)

tautschnig · 2017-04-26T17:42:28Z

Firstly, I agree that the asserts should be changed/removed.

Thanks in advance!

The patch file changed because I recreated it with git (I had to add some stuff around the zero length array), but if there's another way that results in fewer changes then I'll do that instead.

I had figured that you had re-generated the patch using git; what I would have done is largely the same, except I'd then only selectively add the resulting changes to the commit using git add -p. Yet only embark on this if it's quick.

The no-suffix thing is to differentiate the includes from normal headers or source files - where they don't include any declarations or definitions, it's a bit misleading to call them headers. I could give them some other extension though (.macro, .def or similar?)

I think using .inc or .def might align well with other parts of the code base. I'd reserve the suffix-less ones for the system library.

tautschnig · 2017-04-26T20:26:14Z

src/ansi-c/library/jsa.h

  for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_NODES; ++i)
+#include <util/pragma_pop.def>


Having had another look at the code I do now seem to understand. For all cases in this file, could you please wrap the for loop (and also the preceding declaration by #if __CPROVER_JSA_MAX_ABSTRACT_NODES > 0 - this will resolve the need for the pragma in those loops. (This is all due to cegis/jsa/value/jsa_genetic_synthesis.h.)

reuk · 2017-04-27T09:41:49Z

I've made the suggested changes.

tautschnig

Thanks a lot for all the fixes!

martin-cs · 2017-04-27T13:02:36Z

On Wed, 2017-04-26 at 09:29 -0700, Michael Tautschnig wrote: <snip>

> @@ -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) { I'd prefer for those changes to not be included (and similarly below), but also I'm not going to embark on bike shedding here.

I would strongly recommend not changing MiniSAT code.

tautschnig · 2017-04-28T05:35:47Z

I would strongly recommend not changing MiniSAT code.

While I do agree in general, our patches primarily reduce the number of warnings. (And this particular additional change just adds pragmas.) Is that something to be concerned about?

Dup of #873 targeting test-gen-support

reuk force-pushed the pedantic-fix branch 7 times, most recently from 08feae5 to db93002 Compare April 26, 2017 15:10

reuk added 2 commits April 26, 2017 16:29

Remove unnecessary flags from travis.yml

130287f

reuk force-pushed the pedantic-fix branch from db93002 to 130287f Compare April 26, 2017 15:30

tautschnig requested changes Apr 26, 2017

View reviewed changes

tautschnig reviewed Apr 26, 2017

View reviewed changes

reuk added 2 commits April 26, 2017 22:53

Remove unnecessary asserts

16ff24b

Give pragma files a '.def' suffix

24fd67b

reuk force-pushed the pedantic-fix branch from 5bb5d5a to 24fd67b Compare April 26, 2017 21:55

tautschnig approved these changes Apr 27, 2017

View reviewed changes

tautschnig assigned kroening Apr 27, 2017

kroening merged commit 448853c into diffblue:master May 9, 2017

peterschrammel added a commit that referenced this pull request May 18, 2017

Merge pull request #938 from reuk/pedantic-fix-test-gen-support

05d1ec6

Dup of #873 targeting test-gen-support

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Build cleanly without globally disabling warnings #873

Build cleanly without globally disabling warnings #873

reuk commented Apr 26, 2017 •

edited

Loading

reuk commented Apr 26, 2017

tautschnig commented Apr 26, 2017

tautschnig left a comment

tautschnig Apr 26, 2017

tautschnig Apr 26, 2017

tautschnig Apr 26, 2017

tautschnig Apr 26, 2017

tautschnig Apr 26, 2017

tautschnig Apr 26, 2017

tautschnig Apr 26, 2017

tautschnig Apr 26, 2017

reuk commented Apr 26, 2017

tautschnig commented Apr 26, 2017

tautschnig Apr 26, 2017

reuk commented Apr 27, 2017

tautschnig left a comment

martin-cs commented Apr 27, 2017 via email

tautschnig commented Apr 28, 2017

		assert(indent>=0);
		#include <util/pragma_pop> // NOLINT(build/include)

		for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_NODES; ++i)
		#include <util/pragma_pop>

		assert(l.loc_number>=0 && l.loc_number<loc_vector.size());
		#include <util/pragma_pop>

		for(i=0; i < __CPROVER_JSA_MAX_ABSTRACT_NODES; ++i)
		#include <util/pragma_pop.def>

Build cleanly without globally disabling warnings #873

Build cleanly without globally disabling warnings #873

Conversation

reuk commented Apr 26, 2017 • edited Loading

reuk commented Apr 26, 2017

tautschnig commented Apr 26, 2017

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

reuk commented Apr 26, 2017

tautschnig commented Apr 26, 2017

Choose a reason for hiding this comment

reuk commented Apr 27, 2017

tautschnig left a comment

Choose a reason for hiding this comment

martin-cs commented Apr 27, 2017 via email

tautschnig commented Apr 28, 2017

reuk commented Apr 26, 2017 •

edited

Loading