summaryrefslogtreecommitdiff
path: root/src/expr/mkexpr
diff options
context:
space:
mode:
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>2020-09-02 22:15:30 +0200
committerGitHub <noreply@github.com>2020-09-02 15:15:30 -0500
commitf845c04a147021937f1b0a942ee2080df950cda3 (patch)
tree4b88acf9730f489904cade66cb3f9fec8969dab7 /src/expr/mkexpr
parentf9a4549c3dab3cd91f0d9973b24b7891048ed1d9 (diff)
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.
Diffstat (limited to 'src/expr/mkexpr')
-rwxr-xr-xsrc/expr/mkexpr15
1 files changed, 0 insertions, 15 deletions
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 \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback