Remove #line directives from generated files. (#5005)

This PR removes any usage of the #line directive.
We no longer consider it particularly useful, and it obstructs reproducible builds (see #4980).
Fixes #4980.

16 files changed, 11 insertions, 107 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 0d22a3c41..bac9e3b43 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -26,12 +26,6 @@
 
 ${includes}
 
-// This is a hack, but an important one: if there's an error, the
-// compiler directs the user to the template file instead of the
-// generated one.  We don't want the user to modify the generated one,
-// since it'll get overwritten on a later build.
-#line 34 "${template}"
-
 #ifdef CVC4_STATISTICS_ON
   #define INC_STAT(kind) \
   { \
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index a6fce56a2..145f64bd3 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -28,12 +28,6 @@
 
 ${includes}
 
-// This is a hack, but an important one: if there's an error, the
-// compiler directs the user to the template file instead of the
-// generated one.  We don't want the user to modify the generated one,
-// since it'll get overwritten on a later build.
-#line 36 "${template}"
-
 namespace CVC4 {
 
 namespace api {
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 226736e8f..a92081fe8 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -29,12 +29,6 @@
 
 ${includes}
 
-// This is a hack, but an important one: if there's an error, the
-// compiler directs the user to the template file instead of the
-// generated one.  We don't want the user to modify the generated one,
-// since it'll get overwritten on a later build.
-#line 37 "${template}"
-
 using namespace CVC4::kind;
 using namespace std;
 
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 34374d354..0acce2cb0 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -39,12 +39,6 @@ ${includes}
 #include "options/language.h"
 #include "util/hash.h"
 
-// This is a hack, but an important one: if there's an error, the
-// compiler directs the user to the template file instead of the
-// generated one.  We don't want the user to modify the generated one,
-// since it'll get overwritten on a later build.
-#line 47 "${template}"
-
 namespace CVC4 {
 
 // The internal expression representation
@@ -621,8 +615,6 @@ private:
 
 ${getConst_instantiations}
 
-#line 625 "${template}"
-
 inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
   return (size_t) e.getId();
 }
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index 0d7f5f4e4..b2e165558 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -69,7 +69,6 @@ std::string kindToString(::CVC4::Kind k) {
 std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
   switch(typeConstant) {
 ${type_constant_descriptions}
-#line 73 "${template}"
   default:
     out << "UNKNOWN_TYPE_CONSTANT";
     break;
@@ -85,7 +84,6 @@ TheoryId kindToTheoryId(::CVC4::Kind k) {
   case kind::NULL_EXPR:
     break;
 ${kind_to_theory_id}
-#line 89 "${template}"
   case kind::LAST_KIND:
     break;
   }
@@ -97,7 +95,6 @@ TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
   switch (typeConstant)
   {
 ${type_constant_to_theory_id}
-#line 101 "${template}"
     case LAST_TYPE: break;
   }
   throw IllegalArgumentException(
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index d34179252..8ae7018b3 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -63,8 +63,6 @@ const char* toString(CVC4::Kind k);
  */
 std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
 
-#line 67 "${template}"
-
 /** Returns true if the given kind is associative. This is used by ExprManager to
  * decide whether it's safe to modify big expressions by changing the grouping of
  * the arguments. */
@@ -86,7 +84,6 @@ struct KindHashFunction {
 enum CVC4_PUBLIC TypeConstant
 {
   ${type_constant_list}
-#line 90 "${template}"
   LAST_TYPE
 }; /* enum TypeConstant */
 
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 5fa10c90a..e1668836b 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -201,8 +201,6 @@ Kind operatorToKind(::CVC4::expr::NodeValue* nv);
 
 }/* CVC4::kind namespace */
 
-#line 205 "${template}"
-
 }/* CVC4 namespace */
 
 #endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index c5f12f487..58531cba4 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -150,9 +150,7 @@ function typerule {
   lineno=${BASH_LINENO[0]}
   check_theory_seen
   typerules="${typerules}
-#line $lineno \"$kf\"
   case kind::$1:
-#line $lineno \"$kf\"
     typeNode = $2::computeType(nodeManager, n, check);
     break;
 "
@@ -163,9 +161,7 @@ function construle {
   lineno=${BASH_LINENO[0]}
   check_theory_seen
   construles="${construles}
-#line $lineno \"$kf\"
   case kind::$1:
-#line $lineno \"$kf\"
     return $2::computeIsConst(nodeManager, n);
 "
 }
@@ -218,26 +214,19 @@ function constant {
   fi
 
   mkConst_instantiations="${mkConst_instantiations}
-#line $lineno \"$kf\"
 template <> Expr ExprManager::mkConst($2 const& val);
 "
   mkConst_implementations="${mkConst_implementations}
-#line $lineno \"$kf\"
 template <> Expr ExprManager::mkConst($2 const& val) {
-#line $lineno \"$kf\"
   return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val)));
 }
 "
   getConst_instantiations="${getConst_instantiations}
-#line $lineno \"$kf\"
 template <> $2 const & Expr::getConst< $2 >() const;
 "
   getConst_implementations="${getConst_implementations}
-#line $lineno \"$kf\"
 template <> $2 const & Expr::getConst() const {
-#line $lineno \"$kf\"
   PrettyCheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\");
-#line $lineno \"$kf\"
   return d_node->getConst< $2 >();
 }
 "
@@ -288,10 +277,6 @@ check_builtin_theory_seen
 
 ## output
 
-# generate warnings about incorrect #line annotations in templates
-nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
-  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
-
 text=$(cat "$template")
 for var in \
     includes \
diff --git a/src/expr/mkkind b/src/expr/mkkind
index fbf37eff4..55276549a 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -257,23 +257,23 @@ function register_sort {
 "
   type_constant_to_theory_id="${type_constant_to_theory_id}  case $id: return $theory_id;
 "
-  type_constant_cardinalities="${type_constant_cardinalities}#line $lineno \"$kf\"
+  type_constant_cardinalities="${type_constant_cardinalities}
   case $id: return Cardinality($cardinality);
 "
-  type_constant_wellfoundednesses="${type_constant_wellfoundednesses}#line $lineno \"$kf\"
+  type_constant_wellfoundednesses="${type_constant_wellfoundednesses}
   case $id: return $wellfoundedness;
 "
   if [ -n "$groundterm" ]; then
-    type_constant_groundterms="${type_constant_groundterms}#line $lineno \"$kf\"
+    type_constant_groundterms="${type_constant_groundterms}
   case $id: return $groundterm;
 "
     if [ -n "$header" ]; then
-      type_properties_includes="${type_properties_includes}#line $lineno \"$kf\"
+      type_properties_includes="${type_properties_includes}
 #include \"$header\"
 "
     fi
   else
-    type_constant_groundterms="${type_constant_groundterms}#line $lineno \"$kf\"
+    type_constant_groundterms="${type_constant_groundterms}
   case $id: Unhandled() << tc;
 "
   fi
@@ -284,11 +284,11 @@ function register_cardinality {
   cardinality_computer=$(sed 's,%TYPE%,typeNode,g' <<<"$2")
   header=$3
 
-  type_cardinalities="${type_cardinalities}#line $lineno \"$kf\"
+  type_cardinalities="${type_cardinalities}
   case $id: return $cardinality_computer;
 "
   if [ -n "$header" ]; then
-    type_properties_includes="${type_properties_includes}#line $lineno \"$kf\"
+    type_properties_includes="${type_properties_includes}
 #include \"$header\"
 "
   fi
@@ -314,20 +314,20 @@ function register_wellfoundedness {
     fi
   fi
 
-  type_wellfoundednesses="${type_wellfoundednesses}#line $lineno \"$kf\"
+  type_wellfoundednesses="${type_wellfoundednesses}
   case $id: return $wellfoundedness_computer;
 "
   if [ -n "$groundterm_computer" ]; then
-    type_groundterms="${type_groundterms}#line $lineno \"$kf\"
+    type_groundterms="${type_groundterms}
   case $id: return $groundterm_computer;
 "
   else
-    type_groundterms="${type_groundterms}#line $lineno \"$kf\"
+    type_groundterms="${type_groundterms}
   case $id: Unhandled() << typeNode;
 "
   fi
   if [ -n "$header" ]; then
-    type_properties_includes="${type_properties_includes}#line $lineno \"$kf\"
+    type_properties_includes="${type_properties_includes}
 #include \"$header\"
 "
   fi
@@ -390,10 +390,6 @@ check_builtin_theory_seen
 
 ## output
 
-# generate warnings about incorrect #line annotations in templates
-nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
-  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
-
 text=$(cat "$template")
 for var in \
     kind_decls \
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index e2a733ec8..9d2f0a475 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -270,19 +270,16 @@ $2 const& NodeValue::getConst< $2 >() const {
 "
   metakind_constHashes="${metakind_constHashes}
   case kind::$1:
-#line $lineno \"$kf\"
     return $3()(nv->getConst< $2 >());
 "
   metakind_constPrinters="${metakind_constPrinters}
   case kind::$1:
-#line $lineno \"$kf\"
     out << nv->getConst< $2 >();
     break;
 "
   cname=`echo "$2" | awk 'BEGIN {FS="::"} {print$NF}'`
   metakind_constDeleters="${metakind_constDeleters}
   case kind::$1:
-#line $lineno \"$kf\"
     std::allocator< $2 >().destroy(reinterpret_cast< $2* >(nv->d_children));
     break;
 "
@@ -301,7 +298,6 @@ function registerOperatorToKind {
   operatorKind=$1
   applyKind=$2
   metakind_operatorKinds="${metakind_operatorKinds}
-#line $lineno \"$kf\"
     case kind::$applyKind: return kind::$operatorKind;";
 }
 
@@ -396,10 +392,6 @@ check_builtin_theory_seen
 
 ## output
 
-# generate warnings about incorrect #line annotations in templates
-nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
-  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
-
 text=$(cat "$template")
 for var in \
     metakind_includes \
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 3dedd856a..8e4dd9236 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -14,8 +14,6 @@
  ** TypeChecker implementation.
  **/
 
-#line 18 "${template}"
-
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/type_checker.h"
@@ -23,8 +21,6 @@
 
 ${typechecker_includes}
 
-#line 27 "${template}"
-
 namespace CVC4 {
 namespace expr {
 
@@ -44,8 +40,6 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
 
 ${typerules}
 
-#line 48 "${template}"
-
   default:
     Debug("getType") << "FAILURE" << std::endl;
     Unhandled() << n.getKind();
@@ -68,8 +62,6 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
   switch(n.getKind()) {
 ${construles}
 
-#line 72 "${template}"
-
     default:;
   }
 
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index a8adadf6e..9bccd5892 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__TYPE_PROPERTIES_H
 #define CVC4__TYPE_PROPERTIES_H
 
-#line 23 "${template}"
-
 #include <sstream>
 
 #include "base/check.h"
@@ -31,8 +29,6 @@
 
 ${type_properties_includes}
 
-#line 35 "${template}"
-
 namespace CVC4 {
 namespace kind {
 
@@ -47,7 +43,6 @@ inline Cardinality getCardinality(TypeConstant tc)
   switch (tc)
   {
 ${type_constant_cardinalities}
-#line 51 "${template}"
     default: InternalError() << "No cardinality known for type constant " << tc;
   }
 } /* getCardinality(TypeConstant) */
@@ -64,7 +59,6 @@ inline Cardinality getCardinality(TypeNode typeNode) {
   case TYPE_CONSTANT:
     return getCardinality(typeNode.getConst<TypeConstant>());
 ${type_cardinalities}
-#line 68 "${template}"
   default:
     InternalError() << "A theory kinds file did not provide a cardinality "
                     << "or cardinality computer for type:\n"
@@ -75,7 +69,6 @@ ${type_cardinalities}
 inline bool isWellFounded(TypeConstant tc) {
   switch(tc) {
 ${type_constant_wellfoundednesses}
-#line 79 "${template}"
 default:
   InternalError() << "No well-foundedness status known for type constant: "
                   << tc;
@@ -88,7 +81,6 @@ inline bool isWellFounded(TypeNode typeNode) {
   case TYPE_CONSTANT:
     return isWellFounded(typeNode.getConst<TypeConstant>());
 ${type_wellfoundednesses}
-#line 92 "${template}"
   default:
     InternalError() << "A theory kinds file did not provide a well-foundedness "
                     << "or well-foundedness computer for type:\n"
@@ -101,7 +93,6 @@ inline Node mkGroundTerm(TypeConstant tc)
   switch (tc)
   {
 ${type_constant_groundterms}
-#line 105 "${template}"
     default:
       InternalError() << "No ground term known for type constant: " << tc;
   }
@@ -115,7 +106,6 @@ inline Node mkGroundTerm(TypeNode typeNode)
     case TYPE_CONSTANT:
       return mkGroundTerm(typeNode.getConst<TypeConstant>());
 ${type_groundterms}
-#line 119 "${template}"
     default:
       InternalError() << "A theory kinds file did not provide a ground term "
                       << "or ground term computer for type:\n"
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 3c27f1b53..871927760 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -243,10 +243,6 @@ check_builtin_theory_seen
 
 ## output
 
-# generate warnings about incorrect #line annotations in templates
-nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
-  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
-
 text=$(cat "$template")
 for var in \
     rewriter_includes \
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index a87203015..1b1350abe 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -214,20 +214,15 @@ function enumerator {
   lineno=${BASH_LINENO[0]}
   check_theory_seen
   type_enumerator_includes="${type_enumerator_includes}
-#line $lineno \"$kf\"
 #include \"$3\""
   if expr "$type_constants" : '.* '"$1"' ' &>/dev/null; then
     mk_type_enumerator_type_constant_cases="${mk_type_enumerator_type_constant_cases}
-#line $lineno \"$kf\"
     case $1:
-#line $lineno \"$kf\"
       return new $2(type, tep);
 "
   elif expr "$type_kinds" : '.* '"$1"' ' &>/dev/null; then
     mk_type_enumerator_cases="${mk_type_enumerator_cases}
-#line $lineno \"$kf\"
   case kind::$1:
-#line $lineno \"$kf\"
     return new $2(type, tep);
 "
   else
@@ -395,10 +390,6 @@ check_builtin_theory_seen
 
 eval "theory_constructors=\"$theory_constructors\""
 
-# generate warnings about incorrect #line annotations in templates
-nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
-  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
-
 text=$(cat "$template")
 for var in \
     theory_traits \
diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h
index 775f42a46..d591affba 100644
--- a/src/theory/theory_traits_template.h
+++ b/src/theory/theory_traits_template.h
@@ -34,8 +34,6 @@ struct TheoryTraits;
 
 ${theory_traits}
 
-#line 38 "${template}"
-
 struct TheoryConstructor {
   static void addTheory(TheoryEngine* engine, TheoryId id) {
     switch(id) {
diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp
index e9fdc6a86..47405f74e 100644
--- a/src/theory/type_enumerator_template.cpp
+++ b/src/theory/type_enumerator_template.cpp
@@ -22,7 +22,6 @@
 
 
 ${type_enumerator_includes}
-#line 26 "${template}"
 
 using namespace std;
 
@@ -42,7 +41,6 @@ TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(
       }
       Unreachable();
       ${mk_type_enumerator_cases}
-#line 46 "${template}"
     default: Unhandled() << "No type enumerator for type `" << type << "'";
   }
   Unreachable();