Commit 431ed6ca authored by Sylvain Dailler's avatar Sylvain Dailler

"at/old operator unused" is now a warning not an error.

The warning can be disabled by a debug flag.
The bench was changed so as to accept examples that **should** output
warning but not fail (this category did not exist, it does now) and
label_scope has been switched to it.
parent 584f9fe5
......@@ -59,6 +59,26 @@ bads () {
done
}
warns () {
pgm="bin/why3prove$suffix"
test -d $1 || exit 1
rm -f bench_errors
for f in $1/*.[wm][hl][yw] ; do
printf " $f... "
if ! $pgm $2 $f > /dev/null 2>bench_errors; then
echo "FAILED!"
echo "invocation: $pgm $2 $f"
exit 1
fi
if ! test -s bench_errors; then
echo "SHOULD HAVE A WARNING !"
echo "invocation: $pgm $2 $f"
exit 1
fi
echo "ok"
done
}
drivers () {
pgm="bin/why3prove$suffix"
test -d $1 || exit 1
......@@ -250,8 +270,10 @@ echo ""
echo "=== Checking bad files ==="
goods bench/typing/bad --parse-only
goods bench/programs/bad-typing --parse-only
goods bench/programs/warn-typing --parse-only
bads bench/typing/bad --type-only
bads bench/programs/bad-typing --type-only
warns bench/programs/warn-typing --type-only
goods bench/typing/x-bad --type-only
echo ""
......
......@@ -30,6 +30,9 @@ let debug_parse_only = Debug.register_flag "parse_only"
let debug_type_only = Debug.register_flag "type_only"
~desc:"Stop@ after@ type-checking."
let debug_useless_at = Debug.register_flag "ignore_useless_at"
~desc:"Remove@ warning@ for@ useless@ at/old."
(** symbol lookup *)
let rec qloc = function
......@@ -365,8 +368,8 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
(* check if the label has actually been defined *)
ignore (Loc.try2 ~loc gvars (Some l) (Qident id));
let e1 = dterm ns km crcmap gvars (Some l) denv e1 in
if not (Hstr.find at_uses l) then Loc.errorm ~loc
"this `at'/`old' operator is never used";
if not (Hstr.find at_uses l) && Debug.test_noflag debug_useless_at then
Warning.emit ~loc "this `at'/`old' operator is never used";
Hstr.remove at_uses l;
DTattr (e1, Sattr.empty)
| Ptree.Tscope (q, e1) ->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment