From 76854766a7685b69a865e52c0bdc585f57ab5747 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 27 Sep 2018 16:52:41 +0100 Subject: [PATCH 1/2] Fix handling of case range statement in special case In the case where a gcc case range switch statement has a case that reduces to an empty expression, both gcc and clang reluctantly accept it, producing warnings. CBMC up until now was asserting against that case, and this divergence in behaviour was unwanted. --- regression/ansi-c/goto_convert_switch_range_empty/test.desc | 2 +- src/goto-programs/goto_convert.cpp | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/regression/ansi-c/goto_convert_switch_range_empty/test.desc b/regression/ansi-c/goto_convert_switch_range_empty/test.desc index 2718746733c..936c704a3e2 100644 --- a/regression/ansi-c/goto_convert_switch_range_empty/test.desc +++ b/regression/ansi-c/goto_convert_switch_range_empty/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=0$ diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 12837784077..7fce24e1d24 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1249,7 +1249,8 @@ void goto_convertt::convert_switch( { const caset &case_ops=case_pair.second; - assert(!case_ops.empty()); + if (case_ops.empty()) + continue; exprt guard_expr=case_guard(argument, case_ops); From 5da7d4f48463466035ddb22ca097f917aaee3402 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 28 Sep 2018 14:34:22 +0100 Subject: [PATCH 2/2] Add extra test for switch case range with no default and empty case --- .../goto_convert_switch_range_empty_nodefault/main.c | 10 ++++++++++ .../test.desc | 8 ++++++++ 2 files changed, 18 insertions(+) create mode 100644 regression/ansi-c/goto_convert_switch_range_empty_nodefault/main.c create mode 100644 regression/ansi-c/goto_convert_switch_range_empty_nodefault/test.desc diff --git a/regression/ansi-c/goto_convert_switch_range_empty_nodefault/main.c b/regression/ansi-c/goto_convert_switch_range_empty_nodefault/main.c new file mode 100644 index 00000000000..af7b57486c3 --- /dev/null +++ b/regression/ansi-c/goto_convert_switch_range_empty_nodefault/main.c @@ -0,0 +1,10 @@ +int main() +{ + int x; + switch(x) + { + case 10 ... 0: + break; + } + return 0; +} diff --git a/regression/ansi-c/goto_convert_switch_range_empty_nodefault/test.desc b/regression/ansi-c/goto_convert_switch_range_empty_nodefault/test.desc new file mode 100644 index 00000000000..936c704a3e2 --- /dev/null +++ b/regression/ansi-c/goto_convert_switch_range_empty_nodefault/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^Invariant check failed