Merge branch 'issue_203' into 'master'

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

See merge request !42

bench/bench

@@ -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 ""
 

src/parser/typing.ml

@@ -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) ->