chore(*): add LCOV_EXCL_LINE to lean_unreachable statements

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/operator_info.cpp

@@ -119,7 +119,7 @@ char const * to_string(fixity f) {
     case fixity::Mixfixc: return "Mixfixc";
     case fixity::Mixfixo: return "Mixfixo";
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 format pp(operator_info const & o) {
@@ -169,10 +169,10 @@ format pp(operator_info const & o) {
                 r += format{space(), format("_"), space(), format(p)};
             r += format{space(), format("_")};
             return r;
-        default: lean_unreachable();
+        default: lean_unreachable(); // LCOV_EXCL_LINE
         }
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 char const * notation_declaration::keyword() const {

src/frontends/lean/parser.cpp

@@ -604,7 +604,7 @@ class parser::imp {
                 case fixity::Prefix:  return parse_prefix(op);
                 case fixity::Mixfixl: return parse_mixfixl(op);
                 case fixity::Mixfixc: return parse_mixfixc(op);
-                default: lean_unreachable();
+                default: lean_unreachable(); // LCOV_EXCL_LINE
                 }
             } else {
                 return save(get_name_ref(id, p), p);
@@ -639,7 +639,7 @@ class parser::imp {
                 case fixity::Mixfixr: return parse_mixfixr(left, op);
                 case fixity::Mixfixo: return parse_mixfixo(left, op);
                 case fixity::Postfix: return parse_postfix(left, op);
-                default: lean_unreachable();
+                default: lean_unreachable(); // LCOV_EXCL_LINE
                 }
             } else {
                 return save(mk_app(left, save(get_name_ref(id, p), p)), p2);
@@ -1255,7 +1255,7 @@ class parser::imp {
         case fixity::Infix:   m_frontend.add_infix(op_id, prec, d); break;
         case fixity::Infixl:  m_frontend.add_infixl(op_id, prec, d); break;
         case fixity::Infixr:  m_frontend.add_infixr(op_id, prec, d); break;
-        default: lean_unreachable();
+        default: lean_unreachable(); // LCOV_EXCL_LINE
         }
     }
 
@@ -1302,7 +1302,7 @@ class parser::imp {
                             // prefix: ID _
                             m_frontend.add_prefix(parts[0], prec, d);
                         } else {
-                            lean_unreachable();
+                            lean_unreachable(); // LCOV_EXCL_LINE
                         }
                     } else {
                         if (first_placeholder && prev_placeholder) {

src/frontends/lean/pp.cpp

@@ -586,7 +586,7 @@ class pp_fn {
                         --i;
                     }
                 }
-                lean_unreachable();
+                lean_unreachable(); // LCOV_EXCL_LINE
             } else {
                 return arg(m_app, i + 1);
             }
@@ -615,7 +615,7 @@ class pp_fn {
         case fixity::Mixfixo:
             return app.get_num_args() == length(op.get_op_name_parts()) + 1;
         }
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     }
 
     /**
@@ -688,7 +688,7 @@ class pp_fn {
                 }
                 return mk_result(group(r_format), r_weight);
             }}
-            lean_unreachable();
+            lean_unreachable(); // LCOV_EXCL_LINE
         } else if (m_notation && is_forall_expr(e)) {
             return pp_forall(e, depth);
         } else if (m_notation && is_exists_expr(e)) {
@@ -1380,7 +1380,7 @@ public:
                 return format("Unknown neutral object");
             }
         }
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     }
 
     virtual format operator()(environment const & env, options const & opts) {

src/frontends/lean/scanner.cpp

@@ -426,7 +426,7 @@ scanner::token scanner::scan() {
         case '0':  return read_number();
         case '\"': return read_string();
         case -1:   return token::Eof;
-        default:   lean_unreachable();
+        default:   lean_unreachable(); // LCOV_EXCL_LINE
         }
     }
 }

src/kernel/environment.cpp

@@ -182,7 +182,7 @@ struct environment::imp {
         case level_kind::Lift: return is_ge(l1, lift_of(l2), safe_add(k, lift_offset(l2)));
         case level_kind::Max:  return std::all_of(max_begin_levels(l2), max_end_levels(l2), [&](level const & l) { return is_ge(l1, l, k); });
         }
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     }
 
     /** \brief Return true iff l1 >= l2 is implied by asserted universe constraints. */
@@ -239,7 +239,7 @@ struct environment::imp {
         case level_kind::Lift: add_constraints(n, lift_of(l), safe_add(k, lift_offset(l))); return;
         case level_kind::Max:  std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { add_constraints(n, l1, k); }); return;
         }
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     }
 
     /** \brief Add a new universe variable with constraint n >= l */

src/kernel/expr.cpp

@@ -183,6 +183,6 @@ expr copy(expr const & a) {
     case expr_kind::Let:      return mk_let(let_name(a), let_type(a), let_value(a), let_body(a));
     case expr_kind::MetaVar:  return mk_metavar(metavar_name(a), metavar_lctx(a));
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 }

src/kernel/expr_eq.h

@@ -45,7 +45,7 @@ class expr_eq_fn {
             m_eq_visited->insert(p);
         }
         switch (a.kind()) {
-        case expr_kind::Var:      lean_unreachable();
+        case expr_kind::Var:      lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::Constant: return const_name(a) == const_name(b);
         case expr_kind::App:
             if (num_args(a) != num_args(b))
@@ -72,7 +72,7 @@ class expr_eq_fn {
                             return e1.n() == e2.n();
                     });
         }
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     }
 public:
     expr_eq_fn(N const & norm = N()):m_norm(norm) {

src/kernel/free_vars.cpp

@@ -60,7 +60,7 @@ protected:
         switch (e.kind()) {
         case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
             // easy cases were already handled
-            lean_unreachable();
+            lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::App:
             result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
             break;
@@ -135,7 +135,7 @@ protected:
         switch (e.kind()) {
         case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
             // easy cases were already handled
-            lean_unreachable();
+            lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::App:
             result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); });
             break;
@@ -182,7 +182,7 @@ expr lower_free_vars(expr const & e, unsigned s, unsigned d) {
             lean_assert(var_idx(e) >= offset + d);
             return mk_var(var_idx(e) - d);
         } else if (is_metavar(e)) {
-            lean_unreachable();
+            lean_unreachable(); // LCOV_EXCL_LINE
         } else {
             return e;
         }

src/kernel/level.cpp

@@ -148,7 +148,7 @@ level operator+(level const & l, unsigned k)  {
             new_lvls.push_back(max_level(l, i) + k);
         return max_core(new_lvls.size(), new_lvls.data());
     }}
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 level_kind    kind       (level const & l) { lean_assert(l.m_ptr); return l.m_ptr->m_kind; }
@@ -176,7 +176,7 @@ bool operator==(level const & l1, level const & l2) {
             return false;
         }
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 bool operator<(level const & l1, level const & l2) {
@@ -196,7 +196,7 @@ bool operator<(level const & l1, level const & l2) {
                 return max_level(l1, i) < max_level(l2, i);
         return false;
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 std::ostream & operator<<(std::ostream & out, level const & l) {
@@ -245,7 +245,7 @@ format pp(level const & l, bool unicode) {
             return paren(r);
         }
     }}
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 format pp(level const & l, options const & opts) {

src/kernel/normalizer.cpp

@@ -138,7 +138,7 @@ class normalizer::imp {
         case svalue_kind::BoundedVar: return mk_var(k - to_bvar(v) - 1);
         case svalue_kind::Closure:    return reify_closure(to_expr(v), stack_of(v), k);
         }
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     }
 
     /** \brief Return true iff the value_stack does affect the context of a metavariable */

src/kernel/object.h

@@ -36,24 +36,24 @@ public:
     /** \brief Return true iff object has a name. */
     virtual bool has_name() const { return false; }
     /** \brief Return object name. \pre has_name() */
-    virtual name get_name() const { lean_unreachable(); }
+    virtual name get_name() const { lean_unreachable(); } // LCOV_EXCL_LINE
 
     /** \brief Has constraint level associated with it (for universal variables). */
     virtual bool has_cnstr_level() const { return false; }
     /** \brief Return the constraint level associated with the object. */
-    virtual level get_cnstr_level() const { lean_unreachable(); }
+    virtual level get_cnstr_level() const { lean_unreachable(); } // LCOV_EXCL_LINE
 
     /** \brief Return true iff object has a type. */
     virtual bool has_type() const { return false; }
     /** \brief Return object type. \pre has_type() */
-    virtual expr get_type() const { lean_unreachable(); }
+    virtual expr get_type() const { lean_unreachable(); } // LCOV_EXCL_LINE
 
     /** \brief Return true iff object is a definition */
     virtual bool is_definition() const { return false; }
     /** \brief Return true iff the definition is opaque. \pre is_definition() */
-    virtual bool is_opaque() const { lean_unreachable(); }
+    virtual bool is_opaque() const { lean_unreachable(); } // LCOV_EXCL_LINE
     /** \brief Return object value. \pre is_definition() */
-    virtual expr get_value() const { lean_unreachable(); }
+    virtual expr get_value() const { lean_unreachable(); } // LCOV_EXCL_LINE
 
     virtual bool is_axiom() const { return false; }
     virtual bool is_builtin() const { return false; }

src/kernel/type_checker.cpp

@@ -302,7 +302,9 @@ public:
     bool is_convertible(expr const & t1, expr const & t2, context const & ctx) {
         set_ctx(ctx);
         set_menv(nullptr);
-        auto mk_justification = [](){ lean_unreachable(); return justification(); };
+        auto mk_justification = [](){
+            lean_unreachable(); return justification(); // LCOV_EXCL_LINE
+        };
         return is_convertible(t1, t2, ctx, mk_justification);
     }
 

src/library/elaborator/elaborator.cpp

@@ -368,7 +368,7 @@ class elaborator::imp {
         case unification_constraint_kind::Max:         return process_max(c);
         case unification_constraint_kind::Choice:      return process_choice(c);
         }
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
         return true;
     }
 
@@ -1168,7 +1168,7 @@ class elaborator::imp {
                 }
                 break;
             case expr_kind::Let:
-                lean_unreachable();
+                lean_unreachable(); // LCOV_EXCL_LINE
                 return true;
             default:
                 break;

src/library/expr_lt.cpp

@@ -17,7 +17,7 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) {
     if (is_var(a))                       return var_idx(a) < var_idx(b);
     switch (a.kind()) {
     case expr_kind::Var:
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     case expr_kind::Constant:
         return const_name(a) < const_name(b);
     case expr_kind::App:
@@ -27,7 +27,7 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) {
             if (arg(a, i) != arg(b, i))
                 return is_lt(arg(a, i), arg(b, i), use_hash);
         }
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     case expr_kind::Eq:
         if (eq_lhs(a) != eq_lhs(b))
             return is_lt(eq_lhs(a), eq_lhs(b), use_hash);
@@ -75,6 +75,6 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) {
             return it1 == end1 && it2 != end2;
         }
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 }

src/library/max_sharing.cpp

@@ -73,7 +73,7 @@ struct max_sharing_fn::imp {
             cache(r);
             return r;
         }}
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     }
     expr operator()(expr const & a) { return apply(a); }
 };

src/library/type_inferer.cpp

@@ -153,7 +153,7 @@ class type_inferer::imp {
         case expr_kind::Constant: case expr_kind::Eq:
         case expr_kind::Value:    case expr_kind::Type:
         case expr_kind::MetaVar:
-            lean_unreachable();
+            lean_unreachable(); // LCOV_EXCL_LINE
         case expr_kind::Var: {
             auto p = lookup_ext(ctx, var_idx(e));
             context_entry const & ce = p.first;

src/util/interval/interval.cpp

@@ -942,7 +942,7 @@ void interval<T>::inv(interval_deps & deps) {
             deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
         }
     } else {
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     }
     lean_assert(check_invariant());
 }
@@ -1869,7 +1869,7 @@ void interval<T>::csc  (interval_deps & deps) {
             }
             return;
         }
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     }
 
     if (m_lower <= pi && m_upper <= pi) {

src/util/numerics/mpbq.h

@@ -282,27 +282,27 @@ public:
     static void power(mpbq & v, unsigned k) { _power(v, v, k); }
 
     // Transcendental functions
-    static void exp(mpbq & )   { lean_unreachable(); }
-    static void exp2(mpbq & )  { lean_unreachable(); }
-    static void exp10(mpbq & ) { lean_unreachable(); }
-    static void log(mpbq & )   { lean_unreachable(); }
-    static void log2(mpbq & )  { lean_unreachable(); }
-    static void log10(mpbq & ) { lean_unreachable(); }
-    static void sin(mpbq & )   { lean_unreachable(); }
-    static void cos(mpbq & )   { lean_unreachable(); }
-    static void tan(mpbq & )   { lean_unreachable(); }
-    static void sec(mpbq & )   { lean_unreachable(); }
-    static void csc(mpbq & )   { lean_unreachable(); }
-    static void cot(mpbq & )   { lean_unreachable(); }
-    static void asin(mpbq & )  { lean_unreachable(); }
-    static void acos(mpbq & )  { lean_unreachable(); }
-    static void atan(mpbq & )  { lean_unreachable(); }
-    static void sinh(mpbq & )  { lean_unreachable(); }
-    static void cosh(mpbq & )  { lean_unreachable(); }
-    static void tanh(mpbq & )  { lean_unreachable(); }
-    static void asinh(mpbq & ) { lean_unreachable(); }
-    static void acosh(mpbq & ) { lean_unreachable(); }
-    static void atanh(mpbq & ) { lean_unreachable(); }
+    static void exp(mpbq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void exp2(mpbq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void exp10(mpbq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void log(mpbq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void log2(mpbq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void log10(mpbq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void sin(mpbq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void cos(mpbq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void tan(mpbq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void sec(mpbq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void csc(mpbq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void cot(mpbq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void asin(mpbq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void acos(mpbq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void atan(mpbq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void sinh(mpbq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void cosh(mpbq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void tanh(mpbq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void asinh(mpbq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void acosh(mpbq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void atanh(mpbq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
 };
 
 }

src/util/numerics/mpq.h

@@ -253,27 +253,27 @@ public:
     static inline mpq pi_twice_upper() { return pi_u * 2; }
 
     // Transcendental functions
-    static void exp(mpq & )   { lean_unreachable(); }
-    static void exp2(mpq & )  { lean_unreachable(); }
-    static void exp10(mpq & ) { lean_unreachable(); }
-    static void log(mpq & )   { lean_unreachable(); }
-    static void log2(mpq & )  { lean_unreachable(); }
-    static void log10(mpq & ) { lean_unreachable(); }
-    static void sin(mpq & )   { lean_unreachable(); }
-    static void cos(mpq & )   { lean_unreachable(); }
-    static void tan(mpq & )   { lean_unreachable(); }
-    static void sec(mpq & )   { lean_unreachable(); }
-    static void csc(mpq & )   { lean_unreachable(); }
-    static void cot(mpq & )   { lean_unreachable(); }
-    static void asin(mpq & )  { lean_unreachable(); }
-    static void acos(mpq & )  { lean_unreachable(); }
-    static void atan(mpq & )  { lean_unreachable(); }
-    static void sinh(mpq & )  { lean_unreachable(); }
-    static void cosh(mpq & )  { lean_unreachable(); }
-    static void tanh(mpq & )  { lean_unreachable(); }
-    static void asinh(mpq & ) { lean_unreachable(); }
-    static void acosh(mpq & ) { lean_unreachable(); }
-    static void atanh(mpq & ) { lean_unreachable(); }
+    static void exp(mpq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void exp2(mpq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void exp10(mpq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void log(mpq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void log2(mpq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void log10(mpq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void sin(mpq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void cos(mpq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void tan(mpq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void sec(mpq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void csc(mpq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void cot(mpq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void asin(mpq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void acos(mpq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void atan(mpq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void sinh(mpq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void cosh(mpq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void tanh(mpq & )  { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void asinh(mpq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void acosh(mpq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
+    static void atanh(mpq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
 };
 
 }

src/util/pdeque.h

@@ -226,7 +226,7 @@ class pdeque {
                     case cell_kind::PopBack:   update_cell(new pop_back_cell(to_pop_back(m_ptr))); break;
                     case cell_kind::PopFront:  update_cell(new pop_front_cell(to_pop_front(m_ptr))); break;
                     case cell_kind::Set:       update_cell(new set_cell(to_set(m_ptr))); break;
-                    case cell_kind::Root:      lean_unreachable();
+                    case cell_kind::Root:      lean_unreachable(); // LCOV_EXCL_LINE
                     }
                 }
                 lean_assert(!is_shared());

src/util/pvector.h

@@ -191,7 +191,7 @@ class pvector {
                     case cell_kind::PushBack: update_cell(new push_cell(to_push(m_ptr))); break;
                     case cell_kind::PopBack:  update_cell(new pop_cell(to_pop(m_ptr))); break;
                     case cell_kind::Set:      update_cell(new set_cell(to_set(m_ptr))); break;
-                    case cell_kind::Root:     lean_unreachable();
+                    case cell_kind::Root:     lean_unreachable(); // LCOV_EXCL_LINE
                     }
                 }
                 lean_assert(!is_shared());
@@ -396,7 +396,7 @@ unsigned pvector<T>::cell::size() const {
     case cell_kind::Root:
         return static_cast<root_cell const *>(this)->m_vector.size();
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 template<typename T>
@@ -412,7 +412,7 @@ unsigned pvector<T>::cell::quota() const {
             return sz;
     }
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 /** \brief Non-destructive push_back. It is simulated using O(1) copy. */

src/util/sexpr/format.cpp

@@ -75,7 +75,7 @@ std::ostream & layout(std::ostream & out, bool colors, sexpr const & s) {
     case format::format_kind::CHOICE:
     case format::format_kind::COMPOSE:
     case format::format_kind::FLAT_COMPOSE:
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
 
     case format::format_kind::NIL:
         out << "";
@@ -194,7 +194,7 @@ sexpr format::flatten(sexpr const & s) {
     case format_kind::COLOR_END:
         return s;
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 format format::flatten(format const & f){
     return format(flatten(f.m_value));
@@ -302,7 +302,7 @@ int format::space_upto_line_break(sexpr const & s, int available, bool & found_n
         return space_upto_line_break(x, available, found_newline);
     }
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 sexpr format::be(unsigned w, unsigned k, sexpr const & s) {
@@ -357,7 +357,7 @@ sexpr format::be(unsigned w, unsigned k, sexpr const & s) {
         }
     }
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 sexpr format::best(unsigned w, unsigned k, sexpr const & s) {
@@ -427,7 +427,7 @@ struct sexpr_pp_fn {
                 }
             }
         }}
-        lean_unreachable();
+        lean_unreachable(); // LCOV_EXCL_LINE
     }
 
     format operator()(sexpr const & s) {

src/util/sexpr/sexpr.cpp

@@ -96,7 +96,7 @@ struct sexpr_cons : public sexpr_cell {
 
 void sexpr_cell::dealloc() {
     switch (m_kind) {
-    case sexpr_kind::NIL:         lean_unreachable();
+    case sexpr_kind::NIL:         lean_unreachable(); // LCOV_EXCL_LINE
     case sexpr_kind::STRING:      delete static_cast<sexpr_string*>(this); break;
     case sexpr_kind::BOOL:        delete static_cast<sexpr_bool*>(this);   break;
     case sexpr_kind::INT:         delete static_cast<sexpr_int*>(this);    break;
@@ -193,7 +193,7 @@ bool operator==(sexpr const & a, sexpr const & b) {
     case sexpr_kind::MPQ:         return to_mpq(a) == to_mpq(b);
     case sexpr_kind::CONS:        return head(a) == head(b) && tail(a) == tail(b);
     }
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 int cmp(sexpr const & a, sexpr const & b) {
@@ -222,7 +222,7 @@ int cmp(sexpr const & a, sexpr const & b) {
             return r;
         return cmp(tail(a), tail(b));
     }}
-    lean_unreachable();
+    lean_unreachable(); // LCOV_EXCL_LINE
 }
 
 std::ostream & operator<<(std::ostream & out, sexpr const & s) {