Added UNREACHABLE after false INVARIANT to address GCC 12 warnings

Enrico Steffinlongo · Enrico Steffinlongo · commit 4fbde8d62170 · 2023-04-13T00:08:18.000+01:00
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -520,6 +520,7 @@ constant_exprt smt2_convt::parse_literal(
       false,
       "smt2_convt::parse_literal should not be of unsupported type " +
         type.id_string());
+  UNREACHABLE;
 }
 
 exprt smt2_convt::parse_array(
diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp
@@ -233,6 +233,7 @@ add_axioms_for_format_specifier(
   }
 
   INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
+  UNREACHABLE;
 }
 
 /// Deserialize an argument for format from \p string.

Original file line number	Diff line number	Diff line change
`@@ -520,6 +520,7 @@ constant_exprt smt2_convt::parse_literal(`
`520`	`520`	`false,`
`521`	`521`	`"smt2_convt::parse_literal should not be of unsupported type " +`
`522`	`522`	`type.id_string());`
	`523`	`+ UNREACHABLE;`
`523`	`524`	`}`
`524`	`525`
`525`	`526`	`exprt smt2_convt::parse_array(`
Original file line number	Diff line number	Diff line change
`@@ -233,6 +233,7 @@ add_axioms_for_format_specifier(`
`233`	`233`	`}`
`234`	`234`
`235`	`235`	`INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");`
	`236`	`+ UNREACHABLE;`
`236`	`237`	`}`
`237`	`238`
`238`	`239`	`/// Deserialize an argument for format from \p string.`