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.

4 files changed, 0 insertions, 17 deletions

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();