Avoid warning about not returning a value

Author: tautschnig

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -496,6 +496,7 @@ static mp_integer max_value(const typet &type)
   else if(type.id() == ID_unsignedbv)
     return to_unsignedbv_type(type).largest();
   UNREACHABLE;
+  return 0;
 }
 
 /// Create code allocating object of size `size` and assigning it to `lhs`

jbmc/src/java_bytecode/java_utils.cpp

@@ -406,6 +406,7 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component(
     }
 
     UNREACHABLE; // Unexpected access modifier
+    return resolve_inherited_componentt::inherited_componentt();
   }
   else
   {

src/cbmc/bmc.cpp

@@ -543,6 +543,9 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv)
 
     return resultt::ERROR;
   }
+
+  UNREACHABLE;
+  return resultt::ERROR;
 }
 
 /// Perform core BMC, using an abstract model to supply GOTO function bodies
@@ -672,6 +675,7 @@ int bmct::do_language_agnostic_bmc(
     UNREACHABLE;
   }
   UNREACHABLE;
+  return CPROVER_EXIT_INTERNAL_ERROR;
 }
 
 void bmct::perform_symbolic_execution(

src/cbmc/fault_localization.cpp

@@ -317,6 +317,9 @@ safety_checkert::resultt fault_localizationt::stop_on_fail()
 
     return safety_checkert::resultt::ERROR;
   }
+
+  UNREACHABLE;
+  return safety_checkert::resultt::ERROR;
 }
 
 void fault_localizationt::goal_covered(

src/cpp/cpp_id.cpp

@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <ostream>
 
+#include <util/invariant.h>
+
 #include "cpp_scope.h"
 
 cpp_idt::cpp_idt():
@@ -119,4 +121,7 @@ std::ostream &operator<<(std::ostream &out, const cpp_idt::id_classt &id_class)
   case cpp_idt::id_classt::NAMESPACE:         return out<<"NAMESPACE";
   case cpp_idt::id_classt::ENUM:              return out<<"ENUM";
   }
+
+  UNREACHABLE;
+  return out;
 }

src/goto-cc/compile.cpp

@@ -217,6 +217,7 @@ bool compilet::add_input_file(const std::string &file_name)
   }
 
   UNREACHABLE;
+  return false;
 }
 
 /// extracts goto binaries from AR archive and add them as input files.

src/goto-instrument/accelerate/polynomial.cpp

@@ -410,6 +410,7 @@ int monomialt::compare(monomialt &other)
   }
 
   UNREACHABLE;
+  return -1;
 }
 
 int polynomialt::max_degree(const exprt &var)

src/goto-instrument/accelerate/util.cpp

@@ -119,4 +119,5 @@ typet join_types(const typet &t1, const typet &t2)
             << '\n';
 
   INVARIANT(false, "failed to join types");
+  return nil_typet();
 }

src/goto-programs/format_strings.cpp

@@ -11,10 +11,10 @@ Author: CM Wintersteiger
 
 #include "format_strings.h"
 
-#include <util/std_types.h>
-#include <util/std_expr.h>
-
 #include <util/c_types.h>
+#include <util/invariant.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
 
 #include <cctype>
 
@@ -309,4 +309,7 @@ typet get_type(const format_tokent &token)
   case format_tokent::token_typet::UNKNOWN:
     return nil_typet();
   }
+
+  UNREACHABLE;
+  return nil_typet();
 }

src/goto-programs/goto_program.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <ostream>
 #include <iomanip>
 
+#include <util/invariant.h>
 #include <util/std_expr.h>
 
 #include <langapi/language_util.h>
@@ -515,6 +516,9 @@ std::string as_string(
   case INCOMPLETE_GOTO:
     return "(INCOMPLETE GOTO)";
   }
+
+  UNREACHABLE;
+  return "";
 }
 
 void goto_programt::compute_loop_numbers()

src/goto-programs/remove_complex.cpp

@@ -27,8 +27,9 @@ static exprt complex_member(const exprt &expr, irep_idt id)
       return expr.op0();
     else if(id==ID_imag)
       return expr.op1();
-    else
-      UNREACHABLE;
+
+    UNREACHABLE;
+    return nil_exprt();
   }
   else
   {

src/goto-programs/safety_checker.h

@@ -91,6 +91,7 @@ operator&=(safety_checkert::resultt &a, safety_checkert::resultt const &b)
     UNREACHABLE;
   }
   UNREACHABLE;
+  return a;
 }
 
 /// \brief The best of two results

src/solvers/flattening/boolbv_bitwise.cpp

@@ -64,4 +64,5 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
   }
 
   UNIMPLEMENTED;
+  return bvt();
 }

src/solvers/flattening/bv_utils.cpp

@@ -385,7 +385,10 @@ literalt bv_utilst::overflow_add(
     return carry_out(op0, op1, const_literal(false));
   }
   else
+  {
     UNREACHABLE;
+    return literalt();
+  }
 }
 
 literalt bv_utilst::overflow_sub(
@@ -410,7 +413,10 @@ literalt bv_utilst::overflow_sub(
     return !carry_out(op0, inverted(op1), const_literal(true));
   }
   else
+  {
     UNREACHABLE;
+    return literalt();
+  }
 }
 
 void bv_utilst::adder_no_overflow(
@@ -816,8 +822,10 @@ bvt bv_utilst::multiplier(
   {
   case representationt::SIGNED: return signed_multiplier(op0, op1);
   case representationt::UNSIGNED: return unsigned_multiplier(op0, op1);
-  default: UNREACHABLE;
   }
+
+  UNREACHABLE;
+  return bvt();
 }
 
 bvt bv_utilst::multiplier_no_overflow(
@@ -831,8 +839,10 @@ bvt bv_utilst::multiplier_no_overflow(
     return signed_multiplier_no_overflow(op0, op1);
   case representationt::UNSIGNED:
     return unsigned_multiplier_no_overflow(op0, op1);
-  default: UNREACHABLE;
   }
+
+  UNREACHABLE;
+  return bvt();
 }
 
 void bv_utilst::signed_divider(
@@ -885,7 +895,6 @@ void bv_utilst::divider(
     signed_divider(op0, op1, result, remainer); break;
   case representationt::UNSIGNED:
     unsigned_divider(op0, op1, result, remainer); break;
-  default: assert(false);
   }
 }
 
@@ -1297,7 +1306,10 @@ literalt bv_utilst::rel(
   else if(id==ID_gt)
     return lt_or_le(false, bv1, bv0, rep); // swapped
   else
+  {
     UNREACHABLE;
+    return literalt();
+  }
 }
 
 bool bv_utilst::is_constant(const bvt &bv)

src/solvers/prop/prop_conv.cpp

@@ -480,6 +480,9 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
     case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
     case propt::resultt::P_ERROR: return resultt::D_ERROR;
   }
+
+  UNREACHABLE;
+  return resultt::D_ERROR;
 }
 
 exprt prop_conv_solvert::get(const exprt &expr) const

src/solvers/refinement/bv_refinement_loop.cpp

@@ -110,6 +110,9 @@ decision_proceduret::resultt bv_refinementt::prop_solve()
     case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE;
     case propt::resultt::P_ERROR: return resultt::D_ERROR;
   }
+
+  UNREACHABLE;
+  return resultt::D_ERROR;
 }
 
 void bv_refinementt::check_SAT()

src/solvers/refinement/string_builtin_function.h

@@ -190,6 +190,7 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
     if(args.size() == 3)
       UNIMPLEMENTED;
     UNREACHABLE;
+    return nil_exprt();
   };
 
   exprt length_constraint() const override
@@ -199,6 +200,7 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
     if(args.size() == 3)
       UNIMPLEMENTED;
     UNREACHABLE;
+    return nil_exprt();
   };
 
   bool maybe_testing_function() const override
@@ -246,6 +248,7 @@ class string_concatenation_builtin_functiont final
       return generator.add_axioms_for_concat_substr(
         result, input1, input2, args[0], args[1]);
     UNREACHABLE;
+    return nil_exprt();
   };
 
   exprt length_constraint() const override
@@ -256,6 +259,7 @@ class string_concatenation_builtin_functiont final
       return length_constraint_for_concat_substr(
         result, input1, input2, args[0], args[1]);
     UNREACHABLE;
+    return nil_exprt();
   }
 };
 
@@ -337,6 +341,7 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
     // For now, there is no need for implementing that as `add_constraints`
     // should always be called on these functions
     UNIMPLEMENTED;
+    return nil_exprt();
   }
 };
 

src/solvers/smt2/smt2_parser.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "smt2_parser.h"
 
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 
 void smt2_parsert::command_sequence()
 {
@@ -873,6 +874,9 @@ exprt smt2_parsert::function_application()
 
     return tmp;
   }
+
+  UNREACHABLE;
+  return nil_exprt();
 }
 
 exprt smt2_parsert::expression()
@@ -939,6 +943,9 @@ exprt smt2_parsert::expression()
     error() << "unexpected token in an expression" << eom;
     return nil_exprt();
   }
+
+  UNREACHABLE;
+  return nil_exprt();
 }
 
 typet smt2_parsert::sort()
@@ -1014,6 +1021,9 @@ typet smt2_parsert::sort()
     error() << "unexpected token in a sort " << buffer << eom;
     return nil_typet();
   }
+
+  UNREACHABLE;
+  return nil_typet();
 }
 
 typet smt2_parsert::function_signature_definition()

src/util/byte_operators.cpp

@@ -24,8 +24,11 @@ irep_idt byte_extract_id()
     return ID_byte_extract_big_endian;
 
   case configt::ansi_ct::endiannesst::NO_ENDIANNESS:
-    UNREACHABLE;
+    break;
   }
+
+  UNREACHABLE;
+  return ID_nil;
 }
 
 irep_idt byte_update_id()
@@ -39,6 +42,9 @@ irep_idt byte_update_id()
     return ID_byte_update_big_endian;
 
   case configt::ansi_ct::endiannesst::NO_ENDIANNESS:
-    UNREACHABLE;
+    break;
   }
+
+  UNREACHABLE;
+  return ID_nil;
 }

src/util/c_types.cpp

@@ -68,7 +68,10 @@ unsignedbv_typet size_type()
   else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
     return unsigned_long_long_int_type();
   else
+  {
     INVARIANT(false, "width of size type"); // aaah!
+    return unsignedbv_typet(0);
+  }
 }
 
 signedbv_typet signed_size_type()
@@ -237,7 +240,10 @@ signedbv_typet pointer_diff_type()
   else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
     return signed_long_long_int_type();
   else
+  {
     INVARIANT(false, "width of pointer difference");
+    return signedbv_typet(0);
+  }
 }
 
 pointer_typet pointer_type(const typet &subtype)

src/util/config.cpp

@@ -1047,6 +1047,8 @@ std::string configt::ansi_ct::os_to_string(ost os)
   case ost::OS_WIN: return "win";
   case ost::NO_OS: return "none";
   }
+  UNREACHABLE;
+  return "";
 }
 
 configt::ansi_ct::ost configt::ansi_ct::string_to_os(const std::string &os)