summaryrefslogtreecommitdiff
path: root/src/expr/mkexpr
diff options
context:
space:
mode:
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