search

sambayless / monosat

MonoSAT - An SMT solver for Monotonic Theories
MIT License
106 stars 29 forks source link

Question: Clang compiler warnings #8

Closed seanmcl closed 6 years ago

seanmcl commented 6 years ago

Just curious on this one:

Building monosat on OSX with clang, I get thousands upon thousands of compiler warnings. Most are not so disturbing, but some are a little scary, e.g.

/usr/local/monosat/src/monosat/core/Solver.h:262:142: warning: format specifies type 'long' but the argument has type 'uint64_t' (aka 'unsigned long long') [-Wformat]
                        printf("swapping counter clears/total, max swapping counter value:     %ld/%ld, %ld\n",stats_max_swap_count,stats_swapping_conflict_count,stats_swapping_resets);

Are compiler warnings something that you'd like to eliminate eventually, or will they permanently be there?

sambayless commented 6 years ago

The thousands of warnings were almost exclusively due to two pervasive issues: 1) Missing (but optional) override annotations. 2) Differences between how Linux and OSX deal with 'long' vs fixed-width types (in particular, "%ld" will safely print int64_t on Linux, but is incorrect on OSX).

The missing override annotations were a long standing irritation (but not a correctness problem), and your comments pushed me to finally take the time to deal with it. That should now be fixed.

Issue number 2 was indeed a correctness error for OSX. I've addressed this by standardizing on int64_t everywhere in the codebase (that was already mostly the case), and replacing "%ld" with the portable fixed width format specifiers from C++11's .

There are likely still some subtle portability issues with OSX - but I hope to deal with them as they come up.

Compiling with g++-5, g++-7, and clang-5.0 on 64 bit Linux (Ubuntu 16.04), as well as with clang-700.0.72 on OSX 10.11.6, should come up completely warning free now (modulo some intentionally suppressed warnings about signedness and unused variables).

seanmcl commented 6 years ago

Wow, that has got to be a record turnaround time for fixing compiler warnings. Thanks!