Add error messages to invariants/static asserts

Some static asserts/invariants just had "" as an error message.

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -414,7 +414,7 @@ class method_handle_infot : public structured_pool_entryt
     }
     case method_handle_kindt::REF_invokeInterface:
     {
-      INVARIANT(ref_entry.get_tag() == CONSTANT_InterfaceMethodref, "");
+      INVARIANT(ref_entry.get_tag() == CONSTANT_InterfaceMethodref, "4.4.8");
       break;
     }
     }

src/solvers/floatbv/float_bv.cpp

@@ -893,7 +893,9 @@ void float_bvt::normalization_shift(
       if_exprt(prefix_is_zero, shifted, fraction);
 
     // add corresponding weight to exponent
-    INVARIANT(d < (signed int)exponent_bits, "");
+    INVARIANT(
+      d < (signed int)exponent_bits,
+      "depth must be smaller than exponent bits");
 
     exponent_delta=
       bitor_exprt(exponent_delta,

src/solvers/floatbv/float_utils.cpp

@@ -578,7 +578,7 @@ literalt float_utilst::relation(
   else if(rel==relt::GE)
     return relation(src2, relt::LE, src1); // swapped
 
-  INVARIANT(rel == relt::EQ || rel == relt::LT || rel == relt::LE, "");
+  PRECONDITION(rel == relt::EQ || rel == relt::LT || rel == relt::LE);
 
   // special cases: -0 and 0 are equal
   literalt is_zero1=is_zero(src1);
@@ -797,7 +797,8 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent)
   for(int d=depth-1; d>=0; d--)
   {
     std::size_t distance=(1<<d);
-    INVARIANT(fraction.size() > distance, "");
+    INVARIANT(
+      fraction.size() > distance, "fraction must be larger than distance");
 
     // check if first 'distance'-many bits are zeros
     const bvt prefix=bv_utils.extract_msb(fraction, distance);
@@ -812,7 +813,9 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent)
       bv_utils.select(prefix_is_zero, shifted, fraction);
 
     // add corresponding weight to exponent
-    INVARIANT(d < (signed)exponent_delta.size(), "");
+    INVARIANT(
+      d < (signed)exponent_delta.size(),
+      "depth must be smaller than exponent size");
     exponent_delta[d]=prefix_is_zero;
   }
 
@@ -1209,7 +1212,7 @@ float_utilst::unbiased_floatt float_utilst::unpack(const bvt &src)
   result.fraction.push_back(is_normal(src)); // add hidden bit
 
   result.exponent=get_exponent(src);
-  INVARIANT(result.exponent.size() == spec.e, "");
+  CHECK_RETURN(result.exponent.size() == spec.e);
 
   // unbias the exponent
   literalt denormal=bv_utils.is_zero(result.exponent);

src/util/small_map.h

@@ -73,7 +73,7 @@ class small_mapt
   }
 
 private:
-  static_assert(std::is_unsigned<Ind>::value, "");
+  static_assert(std::is_unsigned<Ind>::value, "Ind should be an unsigned type");
 
   typedef Ind index_fieldt;
 
@@ -167,7 +167,7 @@ class small_mapt
 
   static const std::size_t NUM = Num;
 
-  static_assert(NUM >= 2, "");
+  static_assert(NUM >= 2, "NUM should be at least 2");
 
   static constexpr std::size_t num_bits(const std::size_t n)
   {
@@ -187,9 +187,11 @@ class small_mapt
 
   static const index_fieldt MASK = ((index_fieldt)1 << BITS) - 1;
 
-  static_assert(S_BITS <= N_BITS, "");
+  static_assert(S_BITS <= N_BITS, "S_BITS should be no larger than N_BITS");
 
-  static_assert(std::numeric_limits<unsigned>::digits >= BITS, "");
+  static_assert(
+    std::numeric_limits<unsigned>::digits >= BITS,
+    "BITS must fit into an unsigned");
 
   // Internal
 

src/util/small_shared_two_way_ptr.h

@@ -38,8 +38,12 @@ class small_shared_two_way_ptrt final
 
   typedef small_shared_two_way_pointeet<use_countt> pointeet;
 
-  static_assert(std::is_base_of<pointeet, U>::value, "");
-  static_assert(std::is_base_of<pointeet, V>::value, "");
+  static_assert(
+    std::is_base_of<pointeet, U>::value,
+    "pointeet must be a base of U");
+  static_assert(
+    std::is_base_of<pointeet, V>::value,
+    "pointeet must be a base of V");
 
   small_shared_two_way_ptrt() = default;
 
@@ -217,7 +221,7 @@ template <typename Num>
 class small_shared_two_way_pointeet
 {
 public:
-  static_assert(std::is_unsigned<Num>::value, "");
+  static_assert(std::is_unsigned<Num>::value, "Num must be an unsigned type");
 
   static const int bit_idx = std::numeric_limits<Num>::digits - 1;
   static const Num mask = ~((Num)1 << bit_idx);

src/util/validate_helpers.h

@@ -17,7 +17,9 @@ enum class validation_modet;
 template <typename Base, typename T>
 struct call_checkt
 {
-  static_assert(std::is_base_of<Base, T>::value, "");
+  static_assert(
+    std::is_base_of<Base, T>::value,
+    "T should be derived from Base");
 
   void operator()(const Base &base, const validation_modet vm)
   {
@@ -28,7 +30,9 @@ struct call_checkt
 template <typename Base, typename T>
 struct call_validatet
 {
-  static_assert(std::is_base_of<Base, T>::value, "");
+  static_assert(
+    std::is_base_of<Base, T>::value,
+    "T should be derived from Base");
 
   void
   operator()(const Base &base, const namespacet &ns, const validation_modet vm)
@@ -40,7 +44,9 @@ struct call_validatet
 template <typename Base, typename T>
 struct call_validate_fullt
 {
-  static_assert(std::is_base_of<Base, T>::value, "");
+  static_assert(
+    std::is_base_of<Base, T>::value,
+    "T should be derived from Base");
 
   void
   operator()(const Base &base, const namespacet &ns, const validation_modet vm)