Handle all enum values in switch/case [blocks: #2310] by tautschnig · Pull Request #2548 · diffblue/cbmc

tautschnig · 2018-07-07T09:24:56Z

No description provided.

smowton · 2018-07-07T09:42:32Z

What crazy compiler won't let you use default:?

tautschnig · 2018-07-08T19:23:22Z

What crazy compiler won't let you use default:?

I'd say that's a perfectly sane compiler as far as enums are concerned: it helps you not forget about values that were added to the enum type later on, but aren't handled in switch statements. But I do accept that I might be the only one thinking this is a better approach.

allredj

Passed Diffblue compatibility checks (cbmc commit: ca1ceb9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78386231

smowton · 2018-07-09T08:38:57Z

your branch name has a vs- prefix though, does that imply MSVC was complaining?

tautschnig · 2018-07-09T08:46:30Z

[...] does that imply MSVC was complaining?

Yes, Visual Studio does complain about cases not being handled (despite the default).

smowton

Fair point, in that case I support the change. If you do this, consider enabling -Wswitch-enum in our GCC configs so any mistake is detected early, rather than presenting developers with an annoying stumbling block when the shorthand is only flagged on Windows.

smowton · 2018-07-09T08:55:38Z

src/ansi-c/c_typecast.cpp

+  case FIXEDBV:
+  case LARGE_UNSIGNED_INT:
+  case LARGE_SIGNED_INT:
+                   return; // do nothing


Weird indent

chrisr-diffblue

Generally approve of the change. A minor nit being a possible independent commit being included in this PR, but given the PR is one of a series of nice clean ups related to compiler warnings, I'm not going to block this PR :-)

chrisr-diffblue · 2018-07-10T10:05:38Z

jbmc/src/java_bytecode/java_object_factory.cpp

  else if(type.id() == ID_unsignedbv)
    return to_unsignedbv_type(type).largest();
  UNREACHABLE;
+  return 0;


It seems like this change (and the others in this commit) are somewhat independent of the stated purpose of this PR or are these warnings triggered by the change in switch/case statements?

I'm afraid they are: making Visual Studio happy that all cases are covered implies that the default can be removed. Doing so makes GCC unhappy as it thinks code becomes reachable. The specific code that you highlighted above, though, is not linked to one of those default-is-gone cases, but did fit the same topic. Let me know if you'd want me to dissect it.

Thanks for the clarification - I'm fine with this PR as it is :-)

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 04f3ac3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/78602309
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

martin-cs

I wish I could say I was surprised by this. See also #4323 for a discussion of what to do about this.

tautschnig · 2019-03-04T16:12:29Z

@kroening @peterschrammel Please review commit-by-commit, where you may wish to skip the clang-format-only commit.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 7b51b0c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103086699
Status will be re-evaluated on next push.
Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).
the compatibility was already broken by an earlier merge.

src/analyses/uncaught_exceptions_analysis.cpp

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 0727459).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103501248

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: bf2df04).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104505124
Status will be re-evaluated on next push.
Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).
the compatibility was already broken by an earlier merge.

This is now consistent with the warnings that Visual Studio would generate, which warns about missing enum cases in switch/case even when a default: is present.

We should not re-indent a large number of lines of code just because some case statements were added. Silence clang-format for these instead.

There are a number of reasons why instruction types were left out of these case statements : 1. Ignoring this instruction is generally a valid overapproximation. 2. Ignoring this instruction is a valid overapproximation for this domain. 3. The instruction is assumed to not be present due to preceding passes. 4. The instruction should never appear in any valid goto program. 5. The instruction is newer than the analysis code and was forgotten. This patch tries to correctly document which of these apply.

This takes us back to the behaviour prior to this series of commits, and effectively is a to-do list to be addressed. We should either handle the cases, or get rid of the instruction type.

tautschnig requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, romainbrenguier, smowton and thk123 as code owners July 7, 2018 09:24

tautschnig force-pushed the vs-switch-case branch from 42e2381 to ca1ceb9 Compare July 8, 2018 19:23

tautschnig requested review from NathanJPhillips, cesaro, cristina-david and mgudemann as code owners July 8, 2018 19:23

allredj reviewed Jul 8, 2018

View reviewed changes

smowton approved these changes Jul 9, 2018

View reviewed changes

tautschnig force-pushed the vs-switch-case branch from ca1ceb9 to b5b3ff3 Compare July 9, 2018 16:01

tautschnig assigned kroening, peterschrammel and chrisr-diffblue Jul 9, 2018

chrisr-diffblue approved these changes Jul 10, 2018

View reviewed changes

tautschnig force-pushed the vs-switch-case branch from b5b3ff3 to b08eabb Compare July 10, 2018 11:32

tautschnig unassigned chrisr-diffblue Jul 10, 2018

tautschnig force-pushed the vs-switch-case branch 3 times, most recently from e31bd35 to 04f3ac3 Compare July 10, 2018 17:04

allredj reviewed Jul 10, 2018

View reviewed changes

martin-cs mentioned this pull request Mar 4, 2019

What is a safe overapproximation of an OTHER instruction #4323

Open

tautschnig assigned kroening and peterschrammel and unassigned martin-cs Mar 4, 2019

martin-cs approved these changes Mar 4, 2019

View reviewed changes

allredj reviewed Mar 4, 2019

View reviewed changes

peterschrammel approved these changes Mar 6, 2019

View reviewed changes

src/analyses/uncaught_exceptions_analysis.cpp Outdated Show resolved Hide resolved

peterschrammel removed their assignment Mar 6, 2019

tautschnig force-pushed the vs-switch-case branch 2 times, most recently from 16f41ce to 0727459 Compare March 7, 2019 07:54

allredj reviewed Mar 7, 2019

View reviewed changes

tautschnig force-pushed the vs-switch-case branch from 0727459 to bf2df04 Compare March 14, 2019 20:57

allredj reviewed Mar 15, 2019

View reviewed changes

tautschnig mentioned this pull request Mar 29, 2019

Do not generate nil_exprt in bv_get #4197

Merged

3 tasks

kroening added the Needs rebase label Apr 30, 2019

kroening approved these changes Apr 30, 2019

View reviewed changes

tautschnig assigned tautschnig and unassigned kroening Apr 30, 2019

tautschnig force-pushed the vs-switch-case branch from bf2df04 to 09b2fe0 Compare April 30, 2019 23:25

tautschnig removed the Needs rebase label Apr 30, 2019

tautschnig and others added 5 commits April 30, 2019 23:55

Handle all enum values in switch/case

81cd230

Add -Wswitch-enum to default GCC/Clang build options

5e1c7bf

This is now consistent with the warnings that Visual Studio would generate, which warns about missing enum cases in switch/case even when a default: is present.

Disable clang-format for recently touched switch statements

87e86bb

We should not re-indent a large number of lines of code just because some case statements were added. Silence clang-format for these instead.

clang-format switch statements touched in this PR

81fb35f

tautschnig force-pushed the vs-switch-case branch from 09b2fe0 to 3a333a2 Compare April 30, 2019 23:57

Disable a number of invariants that currently fail

93b2371

This takes us back to the behaviour prior to this series of commits, and effectively is a to-do list to be addressed. We should either handle the cases, or get rid of the instruction type.

tautschnig force-pushed the vs-switch-case branch from 3a333a2 to 93b2371 Compare May 1, 2019 07:36

tautschnig merged commit 07c5e1d into diffblue:develop May 1, 2019

Conversation

tautschnig commented Jul 7, 2018

Uh oh!

smowton commented Jul 7, 2018

Uh oh!

tautschnig commented Jul 8, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Jul 9, 2018

Uh oh!

tautschnig commented Jul 9, 2018

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

smowton Jul 9, 2018

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue Jul 10, 2018

Choose a reason for hiding this comment

Uh oh!

tautschnig Jul 10, 2018

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue Jul 10, 2018

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 4, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants