From f177d7dc96b27f5ca3b777d31fcd9bad26be6ce5 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 6 Jul 2015 14:46:51 -0700 Subject: Report warnings only once. (This is the last step in fixing Issue #86.) --- Test/dafny0/JustWarnings.dfy | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 Test/dafny0/JustWarnings.dfy (limited to 'Test/dafny0/JustWarnings.dfy') diff --git a/Test/dafny0/JustWarnings.dfy b/Test/dafny0/JustWarnings.dfy new file mode 100644 index 00000000..86523f5b --- /dev/null +++ b/Test/dafny0/JustWarnings.dfy @@ -0,0 +1,19 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /warnShadowing "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This file tests the behavior where the Resolver reports some warnings +// but no errors. In the case of errors, resolution does not continue +// to clone modules and resolve them, but the cloning does proceed if there +// are only warnings. Dafny should report only one copy of these warnings, +// and warnings are therefore turned off when processing the clones. This +// test file makes sure the warnings don't appear twice. + +method M(x: int) +{ + var x := 10; // warning: this shadows the parameter 'x' +} + +class C { + var u: T + method P(t: T) // warning: this shadows the type parameter 'T' +} -- cgit v1.2.3