summaryrefslogtreecommitdiff
path: root/Test/dafny0/JustWarnings.dfy
blob: 86523f5b74017c7df28efb97a4aa2caa5c4adc0d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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<T> {
  var u: T
  method P<T>(t: T)  // warning: this shadows the type parameter 'T'
}