Merge pull request #2905 from NlightNFotis/2814_takeover

Cleanup of throws and asserts of goto_convert.cpp

Author: tautschnig

regression/ansi-c/goto_convert_break/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  break;
+  return 0;
+}

regression/ansi-c/goto_convert_break/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=1$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+^warning: ignoring

regression/ansi-c/goto_convert_continue/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  continue;
+  return 0;
+}

regression/ansi-c/goto_convert_continue/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=1$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+^warning: ignoring

regression/ansi-c/goto_convert_invalid_goto_label/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  goto x;
+
+  // x:
+
+  return 0;
+}

regression/ansi-c/goto_convert_invalid_goto_label/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^CONVERSION ERROR$
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ansi-c/goto_convert_switch_range_bounds/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+  int x;
+  int n = 5;
+  switch(x)
+  {
+  case 0 ... n:
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/ansi-c/goto_convert_switch_range_bounds/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^CONVERSION ERROR$
+^EXIT=1$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ansi-c/goto_convert_switch_range_case_valid/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+#define false 0
+
+int main(void)
+{
+  int x = 5;
+  switch (x)
+  {
+    case 0 ... 10:
+      break;
+    default:
+      assert(false);
+      break;
+  }
+}

regression/ansi-c/goto_convert_switch_range_case_valid/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed

regression/ansi-c/goto_convert_switch_range_empty/main.c

@@ -0,0 +1,12 @@
+int main()
+{
+  int x;
+  switch(x)
+  {
+  case 10 ... 0:
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/ansi-c/goto_convert_switch_range_empty/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Invariant check failed

regression/ansi-c/goto_convert_switch_range_operands_count/main.c

@@ -0,0 +1,12 @@
+int main()
+{
+  int x;
+  switch(x)
+  {
+  case 0 ... 10 20:
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/ansi-c/goto_convert_switch_range_operands_count/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=1$
+^SIGNAL=0$
+^PARSING ERROR$
+--
+^warning: ignoring

src/cbmc/cbmc_parse_options.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 
 #include <util/config.h>
+#include <util/exception_utils.h>
 #include <util/exit_codes.h>
 #include <util/invariant.h>
 #include <util/unicode.h>
@@ -611,6 +612,12 @@ int cbmc_parse_optionst::get_goto_program(
     log.status() << config.object_bits_info() << log.eom;
   }
 
+  catch(incorrect_goto_program_exceptiont &e)
+  {
+    log.error() << e.what() << log.eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
+
   catch(const char *e)
   {
     log.error() << e << log.eom;