Get legalistic about use of virtual with override

[NathanJPhillips]

I recently had a comment on a PR complaining that I used the redundant virtual on a method declaration that I marked override.
I replied that the redundant virtual is useful documentation as it allows developers to see whether a function is virtual in a single place without having to check the beginning and the end of the declaration.
Another reviewer pointed out that our linter was specifically adjusted to allow this format here: a7c24fb#diff-4abdbb2a75f622bb69ca7ae19beee7c6R5647.
An analysis of the code base for CBMC shows that we have 457 uses of override, of which 154 combine it with virtual. Deeptest has a similar proportion with 22 of 64 uses using the combined version.
My hope with this PR is that it will ignite a style war that will get nowhere and result in this PR being closed. This will then be the definitive point of reference for allowing people to do whatever they feel most comfortable with.

[tautschnig]

From my point of view you might as well flip a coin, but I'm a strong proponent of consistency: always use virtual with override or never do so.

[chrisr-diffblue]

I'm going to nail my colours to the mast...

[chrisr-diffblue]

...but I'm not brave enough to merge it, so someone else can do that :-)

[hannes-steffenhagen-diffblue]

My preference would be to not add the redundant virtual. Both the default cpplint and clang-tidy's modernize-use-override warn against this. Although I certainly agree if we're going to do it one way or the other we should be consistent about this.

My argument against the consistency argument would be that if you're only going to check the prefix of the function for the behaviour you could also read an override as introducing a new virtual function instead. Also, you should always check the postfix anyway for constness specifiers.

EDIT
virtual. I meant redundant virtual. The comment previously said override.

[smowton]

Yeah, it's a little clearer. Though an en-masse cleanup should also be submitted in this case.

[peterschrammel]

Technically, neither virtual nor override are required. Using virtual to visually mark overridden functions is a relict from pre-C++11 times.
I agree with @hannes-steffenhagen-diffblue that the fact that clang-tidy offers an option to clean up joint use of virtual and override is a strong argument for getting rid of the remaining redundancies in our code bases.

[kroening]

So, are we doing override without virtual?

[NathanJPhillips]

I think we have three votes for including virtual and two against. Is @kroening against? Then we can have an exact tie and do nothing.

[kroening]

Hm, the Google C++ coding style (which we frequently follow) says use override but no virtual.

[martin-cs]

@NathanJPhillips If you're intent on starting a war over this I can offer to supply one (or both) sides with ammunition at very reasonable prices...

I think I'm with the "does it really matter" faction, or possibly the "add it to the linter and let it change naturally" group,

[kroening]

We'll go for 'no virtual', and it will be a linter recommendation.

[peterschrammel]

#2253 clarifies the rule in the coding standard and enables the corresponding check in cpplint.