dafny/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy at master · prosyslab/dafny · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s"


module AutoInitRegressions {
  trait Y { }

  datatype Datatype = Make
  {
    static const Static: Y  // error: Y is not auto-init
    const Instance: Y  // error: Y is not auto-init
  }

  method Main() {
    print Datatype.Static, "\n";
    var c := Make;
    print c.Instance, "\n";
  }

  const Global: Y  // error: Y is not auto-init

  class Class {  // error: InstanceField is of type Y, which is not auto-init, so class must have a constructor
    static const StaticField: Y  // error: Y is not auto-init
    const InstanceField: Y
  }

  trait Trait extends object {
    static const StaticField: Y  // error: Y is not auto-init
    const InstanceField: Y
  }

  class TraitImpl extends Trait {  // error: inherited InstanceField is of type Y, which is not auto-init, so class must have a constructor
  }

  newtype Newtype = int
  {
    static const Static: Y  // error: Y is not auto-init
    const Instance: Y  // error: Y is not auto-init
  }

  type Opaque
  {
    static const Static: Y  // error: Y is not auto-init
    const Instance: Y  // error: Y is not auto-init
  }
}

module NonemptyRegressions {
  type Y { }

  datatype Datatype = Make
  {
    ghost static const Static: Y  // error: Y is not nonempty
    ghost const Instance: Y  // error: Y is not nonempty
  }

  ghost const Global: Y  // error: Y is not nonempty

  class Class {  // error: InstanceField is of type Y, which is not nonempty, so class must have a constructor
    ghost static const StaticField: Y  // error: Y is not nonempty
    ghost const InstanceField: Y
  }

  trait Trait extends object {
    ghost static const StaticField: Y  // error: Y is not nonempty
    ghost const InstanceField: Y
  }

  class TraitImpl extends Trait {  // error: inherited InstanceField is of type Y, which is not auto-init, so class must have a constructor
  }

  newtype Newtype = int
  {
    ghost static const Static: Y  // error: Y is not nonempty
    ghost const Instance: Y  // error: Y is not nonempty
  }

  type Opaque
  {
    ghost static const Static: Y  // error: Y is not nonempty
    ghost const Instance: Y  // error: Y is not nonempty
  }
}