[TravisCI] Treating some warnings as errors

[delcypher]

Now that we have TravisCI in place we could consider treating certain categories of warnings found by Clang/GCC as errors. This would hopefully prevent certain issues from staying in the master branch for long as they would break the build.

Is there any interest in doing this? If so what warnings should be treated as errors?

This was inspired by #1129.

E.g.

GCC

• -Wodr

Clang

• -Wdelete-non-virtual-dtor
• -Woverloaded-virtual

[NikolajBjorner]

I am fairly anal about getting Z3 to compile without warnings even if they may be benign. They help flag issues even when it comes to code maintainability.
The main issue now becomes that it is a mind-numbing task to nit over some warnings that have no effect especially in the unit tests (I took care of several of these, but many to go).

The warnings you list seem not in the benign category. Are these flagged as warnings at this point? I don't recall seeing them for a while.
Deleting a non-virtual destructor is asking for trouble: we tend to treat these as bugs because they can mask memory leaks. I am not sure what the ramifications of the other warnings are. I was unable to compile a couple of days ago when overloading a virtual, so this was fixed long before pushing.

[delcypher]

@NikolajBjorner

The warnings you list seem not in the benign category. Are these flagged as warnings at this point? I don't recall seeing them for a while.

Yes most of the warnings I gave as examples are not emitted by Z3's current code. These are warnings are remember being in Z3's code at some point which I would be keen to not have re-introduced. It's certainly not exhaustive list, they are just things I thought of just now.

[NikolajBjorner]

OK, sounds good. What should be changed to treat them as errors? The virtual destructor issue is definitely something I would treat as an error unless learning about any compelling evidence to the contrary. The only kind of warnings I feel compelled to punt on are the ones that appear in compiled macros (there are some on potentially uninitialized or unused variables, but these are going to be used properly)

[delcypher]

OK, sounds good. What should be changed to treat them as errors?

There are two places this could be done either as custom flags set in the TravisCI build scripts or as part of the CMake build system itself.

I'd prefer to do it in CMake itself because we can test the compiler at runtime and actually check whether or not it supports the warning we'd like to treat as an error.

This would likely be a modification to https://github.com/Z3Prover/z3/blob/master/cmake/compiler_warnings.cmake . We'd also probably want some sort of CMake option to not treat any warnings as errors just in case there's a bug in the compiler (e.g. certain versions of a compiler might give false positives) but have that off by default so that we treat the same warnings as errors during development as in TravisCI (provided the compiler being used for development supports the same warnings).

Currently compiler_warnings.cmake has an option to treat all warnings as errors but I think that's far too broad. It would probably better to maintain a list of warnings that we know aren't ever false positives.

[NikolajBjorner]

I was assuming it was a cmake change so that breaks are potentially caught in local builds.
Aren't the high quality warnings in a lower level than the "unused variable" warnings? Then one breaks on high quality warnings, for some level of high quality.

[wintersteiger]

Similar here, I fix warnings before pushing from my development platform, and the day after on warnings that show up on our other nightly build platforms. From my point of view we don't really need that enforced by the CI build, but it doesn't hurt to add a sensible subset of them either.

[delcypher]

I was assuming it was a cmake change so that breaks are potentially caught in local builds.
Aren't the high quality warnings in a lower level than the "unused variable" warnings? Then one breaks on high quality warnings, for some level of high quality.

AFAIK for gcc/clang no. It's a bit of a mess really. There's -Wall (that doesn't turn on all warnings. FACEPALM), -Wpedantic, and -Wextra. See https://gcc.gnu.org/onlinedocs/gcc/Warning-Options.html

I think turning the WARNINGS_AS_ERRORS option from a boolean into a three valued option would do the trick

• ON treat all warnings as errors
• OFF all warnings are non-fatal
• ONLY_SERIOUS Treat all warnings that the Z3 developers consider serious as fatal warnings if the compiler supports them.

We'd then make ONLY_SERIOUS be the default so serious warnings are treated as errors by default but the user can set it to OFF to get back the old behaviour.

[NikolajBjorner]

just adding the flags you mention as errors should be very nice.