diff options
Diffstat (limited to 'src/expr/mkexpr')
-rwxr-xr-x | src/expr/mkexpr | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/src/expr/mkexpr b/src/expr/mkexpr index da2847d84..a7302da26 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -104,10 +104,17 @@ function endtheory { # endtheory lineno=${BASH_LINENO[0]} check_theory_seen + seen_endtheory=true } function sort { - # sort TYPE ["comment"] + # sort TYPE cardinality ["comment"] + lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function cardinality { + # cardinality TYPE cardinality-computer [header] lineno=${BASH_LINENO[0]} check_theory_seen } @@ -164,6 +171,10 @@ template <> $2 const & Expr::getConst() const { } function check_theory_seen { + if $seen_endtheory; then + echo "$kf:$lineno: error: command after \"endtheory\" declaration (endtheory has to be last)" >&2 + exit 1 + fi if ! $seen_theory; then echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2 exit 1 @@ -179,15 +190,27 @@ function check_builtin_theory_seen { while [ $# -gt 0 ]; do kf=$1 seen_theory=false + seen_endtheory=false b=$(basename $(dirname "$kf")) source "$kf" - check_theory_seen + if ! $seen_theory; then + echo "$kf: error: no theory content found in file!" >&2 + exit 1 + fi + if ! $seen_endtheory; then + echo "$kf:$lineno: error: no \"endtheory\" declaration found (it is required at the end)" >&2 + exit 1 + fi shift done 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 \ @@ -195,7 +218,8 @@ for var in \ getConst_instantiations \ getConst_implementations \ mkConst_instantiations \ - mkConst_implementations; do + mkConst_implementations \ + ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` |