Build using C++17

[tautschnig]

This raises the minimum GCC version supported to 7 (see https://gcc.gnu.org/projects/cxx-status.html#cxx17).

Add -Wno-register to silence warnings about the use of the register storage class by older flex versions (as present on macOS).

CMake doesn't know about C++ 17 until version 3.8, so we need to hard-code the necessary command-line options.

This is now the single commit from #6749 that actually switches over to C++17. All other commits in #6749 are improvements enabled by this commit, but some of them require large changes that may take a lot of time to get reviewed. The aim of this PR is to unblock use of C++17, without necessarily reaping all benefit right away.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Base: 78.02% // Head: 78.01% // Decreases project coverage by -0.00% ⚠️

Coverage data is based on head (0a3b0ef) compared to base (b19b412).
Patch coverage: 90.14% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7172      +/-   ##
===========================================
- Coverage    78.02%   78.01%   -0.01%     
===========================================
  Files         1625     1622       -3     
  Lines       187427   187412      -15     
===========================================
- Hits        146231   146211      -20     
- Misses       41196    41201       +5     

Impacted Files	Coverage Δ
src/cprover/cprover_parse_options.cpp	56.58% <ø> (ø)
src/cprover/generalization.cpp	84.21% <ø> (ø)
src/cprover/inductiveness.cpp	78.35% <ø> (ø)
src/cprover/propagate.cpp	74.28% <ø> (ø)
src/cprover/report_properties.cpp	88.46% <ø> (ø)
src/cprover/report_traces.cpp	89.74% <ø> (ø)
src/cprover/solver.cpp	92.00% <ø> (ø)
src/cprover/solver_progress.cpp	60.00% <ø> (ø)
src/goto-symex/field_sensitivity.h	100.00% <ø> (ø)
src/util/console.cpp	29.76% <ø> (ø)
... and 41 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[martin-cs]

General "dependencies are barriers to users, especially new ones" feelings but #6749 (comment) seems sufficiently reassuring and motivating for why this is useful.

[thomasspriggs]

Could we bump the cmake version to avoid "hard coding" the compiler flags? #7184

[kroening]

I would probably wait for 6.0 with this.

[thomasspriggs]

I would probably wait for 6.0 with this.

For bumping the cmake version or for moving to C++17 or both?

[kroening]

Apologies for being unclear; I meant "moving to C++17". I'd say that bumping cmake is ok, since users who have difficulties getting a new cmake can fall back onto the Makefile build system.

So I'd merge #7184, but wait with #7172.

[thomasspriggs]

@tautschnig I have now merged the cmake version bump PR. Therefore it should no longer be necessary to "hard-code the necessary command-line options."

[tautschnig]

@tautschnig I have now merged the cmake version bump PR. Therefore it should no longer be necessary to "hard-code the necessary command-line options."

Done.

[esteffin]

Another PR has been created for this #7989.
We agreed that that PR will be part of version 6.

Closing as duplicate