path: root/Test/dafny0/Answer

-------------------- Simple.dfy --------------------
// Simple.dfy

class MyClass<T, U> {
  var x: int;

  method M(s: bool, lotsaObjects: set<object>)
      returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)
    requires s;
    modifies this, lotsaObjects;
    ensures t == t;
    ensures old(null) != this;
  {
    x := 12;
    while (x < 100)
      invariant x <= 100;
    {
      x := x + 17;
      if (x % 20 == 3) {
        x := this.x + 1;
      } else {
        this.x := x + 0;
      }
      call t, u, v := M(true, lotsaObjects);
      var to: MyClass<T,U>;
      call to, u, v := M(true, lotsaObjects);
      call to, u, v := to.M(true, lotsaObjects);
      assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
    }
  }

  function F(x: int, y: int, h: WildData, k: WildData): WildData
  {
    if x < 0 then
      h
    else if x == 0 then
      if if h == k then true else false then
        h
      else if y == 0 then
        k
      else
        h
    else
      k
  }
}

datatype List<T> {
  Nil;
  Cons(T, List<T>);
}

datatype WildData {
  Something;
  JustAboutAnything<G, H>(G, myName: set<H>, int, WildData);
  More(List<int>);
}

class C {
  var w: WildData;
  var list: List<bool>;
}

Dafny program verifier finished with 0 verified, 0 errors

-------------------- TypeTests.dfy --------------------
TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)
TypeTests.dfy(11,4): Error: incorrect type of method in-parameter 0 (expected int, got bool)
TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected int, got C)
TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int)
TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed
TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
TypeTests.dfy(64,6): Error: Duplicate local-variable name: z
TypeTests.dfy(66,6): Error: Duplicate local-variable name: x
TypeTests.dfy(69,8): Error: Duplicate local-variable name: x
TypeTests.dfy(72,6): Error: Duplicate local-variable name: y
14 resolution/type errors detected in TypeTests.dfy

-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
Execution trace:
    (0,0): anon0
SmallTests.dfy(61,36): Error: possible division by zero
Execution trace:
    (0,0): anon12_Then
SmallTests.dfy(62,51): Error: possible division by zero
Execution trace:
    (0,0): anon12_Else
    (0,0): anon3
    (0,0): anon13_Else
SmallTests.dfy(63,22): Error: target object may be null
Execution trace:
    (0,0): anon12_Then
    (0,0): anon3
    (0,0): anon13_Then
    (0,0): anon6
SmallTests.dfy(82,24): Error: target object may be null
Execution trace:
    (0,0): anon0
    SmallTests.dfy(81,5): anon9_LoopHead
    (0,0): anon9_LoopBody
    (0,0): anon10_Then
SmallTests.dfy(116,5): Error: call may violate caller's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
    (0,0): anon3
SmallTests.dfy(129,7): Error: call may violate caller's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
SmallTests.dfy(131,7): Error: call may violate caller's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Else
SmallTests.dfy(171,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
    (0,0): anon3
SmallTests.dfy(199,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon12_Then
SmallTests.dfy(206,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon12_Else
    (0,0): anon3
    (0,0): anon13_Then
SmallTests.dfy(226,12): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon12_Else
    (0,0): anon3
    (0,0): anon13_Else
    (0,0): anon6
    (0,0): anon14_Then
    (0,0): anon11

Dafny program verifier finished with 29 verified, 12 errors

-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
Execution trace:
    (0,0): anon3_Else
Definedness.dfy(15,16): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(24,16): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(25,21): Error: target object may be null
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
Definedness.dfy(26,17): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(33,16): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(50,18): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(55,18): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(77,7): Error: target object may be null
Execution trace:
    (0,0): anon0
Definedness.dfy(78,5): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
Definedness.dfy(79,10): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
Definedness.dfy(84,14): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(84,23): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(85,15): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(90,12): Error: possible division by zero
Execution trace:
    (0,0): anon0
Definedness.dfy(97,15): Error: possible division by zero
Execution trace:
    (0,0): anon0
    Definedness.dfy(97,5): anon8_LoopHead
    (0,0): anon8_LoopBody
    Definedness.dfy(97,5): anon9_Else
    (0,0): anon3
Definedness.dfy(106,23): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    Definedness.dfy(105,5): anon13_LoopHead
    (0,0): anon13_LoopBody
    (0,0): anon14_Then
Definedness.dfy(112,17): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    Definedness.dfy(105,5): anon13_LoopHead
    (0,0): anon13_LoopBody
    Definedness.dfy(105,5): anon14_Else
    (0,0): anon3
    (0,0): anon15_Then
    (0,0): anon6
    Definedness.dfy(111,5): anon16_LoopHead
    (0,0): anon16_LoopBody
    (0,0): anon17_Then
Definedness.dfy(122,17): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    Definedness.dfy(121,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    (0,0): anon8_Then
Definedness.dfy(122,22): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
    (0,0): anon0
Definedness.dfy(123,17): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    Definedness.dfy(121,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    (0,0): anon8_Then
Definedness.dfy(132,15): Error: possible division by zero
Execution trace:
    (0,0): anon0
    Definedness.dfy(132,5): anon9_LoopHead
    (0,0): anon9_LoopBody
    Definedness.dfy(132,5): anon10_Else
    (0,0): anon3
Definedness.dfy(151,15): Error: possible division by zero
Execution trace:
    (0,0): anon0
    Definedness.dfy(145,5): anon17_LoopHead
    (0,0): anon17_LoopBody
    Definedness.dfy(145,5): anon18_Else
    (0,0): anon3
    (0,0): anon19_Then
    (0,0): anon5
    (0,0): anon20_Then
    (0,0): anon8
    Definedness.dfy(151,5): anon21_LoopHead
    (0,0): anon21_LoopBody
    Definedness.dfy(151,5): anon22_Else
    (0,0): anon11
Definedness.dfy(170,17): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    Definedness.dfy(162,5): anon19_LoopHead
    (0,0): anon19_LoopBody
    Definedness.dfy(162,5): anon20_Else
    (0,0): anon3
    (0,0): anon21_Then
    (0,0): anon6
    Definedness.dfy(169,5): anon22_LoopHead
    (0,0): anon22_LoopBody
    (0,0): anon23_Then
    (0,0): anon24_Then
    (0,0): anon11
Definedness.dfy(191,24): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
Definedness.dfy(193,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
Execution trace:
    (0,0): anon0
Definedness.dfy(195,33): Error: range expression must be well defined
Execution trace:
    (0,0): anon0
Definedness.dfy(201,18): Error: RHS of assignment must be well defined
Execution trace:
    (0,0): anon0
Definedness.dfy(210,19): Error: possible division by zero
Execution trace:
    (0,0): anon0
    Definedness.dfy(208,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    (0,0): anon8_Then
Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
    (0,0): anon0
Definedness.dfy(210,28): Error: possible division by zero
Execution trace:
    (0,0): anon0
    Definedness.dfy(208,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    (0,0): anon8_Then
Definedness.dfy(231,30): Error: possible violation of function postcondition
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
Definedness.dfy(238,22): Error: target object may be null
Execution trace:
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then
Definedness.dfy(254,24): Error: possible violation of function postcondition
Execution trace:
    (0,0): anon7_Then
    (0,0): anon2
    (0,0): anon8_Else

Dafny program verifier finished with 23 verified, 34 errors

-------------------- FunctionSpecifications.dfy --------------------
FunctionSpecifications.dfy(31,13): Error: possible violation of function postcondition
Execution trace:
    (0,0): anon10_Else
    (0,0): anon11_Else
    (0,0): anon12_Then
    (0,0): anon13_Else
    (0,0): anon7
    (0,0): anon9
FunctionSpecifications.dfy(40,18): Error: possible violation of function postcondition
Execution trace:
    (0,0): anon12_Else
    (0,0): anon15_Else
    (0,0): anon16_Then
    (0,0): anon11
FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon9_Then
    (0,0): anon3

Dafny program verifier finished with 3 verified, 3 errors

-------------------- Array.dfy --------------------
Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then
Array.dfy(17,16): Error: target object may be null
Execution trace:
    (0,0): anon0
Array.dfy(24,6): Error: index out of range
Execution trace:
    (0,0): anon0
Array.dfy(48,20): Error: assertion violation
Execution trace:
    (0,0): anon0
Array.dfy(56,12): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then
Array.dfy(63,12): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon2
    (0,0): anon6_Then
Array.dfy(95,18): Error: assertion violation
Execution trace:
    (0,0): anon0
Array.dfy(107,6): Error: insufficient reads clause to read array element
Execution trace:
    (0,0): anon7_Else
    (0,0): anon8_Then
    (0,0): anon9_Then
Array.dfy(115,6): Error: insufficient reads clause to read array element
Execution trace:
    (0,0): anon7_Else
    (0,0): anon8_Then
    (0,0): anon9_Then
Array.dfy(131,10): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
    (0,0): anon0
Array.dfy(138,10): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 22 verified, 11 errors

-------------------- MultiDimArray.dfy --------------------
MultiDimArray.dfy(53,21): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon11_Then
    (0,0): anon12_Then
MultiDimArray.dfy(80,25): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon6_Then

Dafny program verifier finished with 8 verified, 2 errors

-------------------- Modules0.dfy --------------------
Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
Modules0.dfy(13,7): Error: module T named among imports does not exist
Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G
Modules0.dfy(51,6): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)
Modules0.dfy(62,6): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)
Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts
8 resolution/type errors detected in Modules0.dfy

-------------------- Modules1.dfy --------------------
Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0
Execution trace:
    (0,0): anon0
Modules1.dfy(61,3): Error: failure to decrease termination measure
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 16 verified, 2 errors

-------------------- BadFunction.dfy --------------------
BadFunction.dfy(6,3): Error: failure to decrease termination measure
Execution trace:
    (0,0): anon3_Else

Dafny program verifier finished with 2 verified, 1 error

-------------------- Termination.dfy --------------------
Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
    (0,0): anon0
    Termination.dfy(102,3): anon7_LoopHead
    (0,0): anon7_LoopBody
    Termination.dfy(102,3): anon8_Else
    (0,0): anon3
    Termination.dfy(102,3): anon9_Else
    (0,0): anon5
Termination.dfy(110,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
    (0,0): anon0
    Termination.dfy(110,3): anon9_LoopHead
    (0,0): anon9_LoopBody
    Termination.dfy(110,3): anon10_Else
    (0,0): anon11_Then
    (0,0): anon5
    Termination.dfy(110,3): anon12_Else
    (0,0): anon7
Termination.dfy(119,3): Error: decreases expression might not decrease
Execution trace:
    (0,0): anon0
    Termination.dfy(119,3): anon9_LoopHead
    (0,0): anon9_LoopBody
    Termination.dfy(119,3): anon10_Else
    (0,0): anon11_Then
    (0,0): anon5
    Termination.dfy(119,3): anon12_Else
    (0,0): anon7
Termination.dfy(120,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
    (0,0): anon0
    Termination.dfy(119,3): anon9_LoopHead
    (0,0): anon9_LoopBody
    Termination.dfy(119,3): anon10_Else
    (0,0): anon11_Then
    (0,0): anon5
    Termination.dfy(119,3): anon12_Else
    (0,0): anon7
Termination.dfy(248,36): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon6_Else
    (0,0): anon7_Else
    (0,0): anon8_Then
Termination.dfy(288,3): Error: decreases expression might not decrease
Execution trace:
    (0,0): anon0
    Termination.dfy(288,3): anon10_LoopHead
    (0,0): anon10_LoopBody
    Termination.dfy(288,3): anon11_Else
    Termination.dfy(288,3): anon12_Else
    (0,0): anon13_Else
    (0,0): anon8

Dafny program verifier finished with 41 verified, 6 errors

-------------------- Use.dfy --------------------
Use.dfy(16,18): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(26,18): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(35,18): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(54,12): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(84,17): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(126,23): Error: assertion violation
Execution trace:
    (0,0): anon0
Use.dfy(151,12): Error: assertion violation
Use.dfy(143,5): Related location: Related location
Execution trace:
    (0,0): anon0
Use.dfy(160,12): Error: assertion violation
Use.dfy(143,5): Related location: Related location
Execution trace:
    (0,0): anon0
Use.dfy(169,12): Error: assertion violation
Use.dfy(143,5): Related location: Related location
Execution trace:
    (0,0): anon0
Use.dfy(213,19): Error: assertion violation
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 39 verified, 10 errors

-------------------- DTypes.dfy --------------------
DTypes.dfy(15,14): Error: assertion violation
Execution trace:
    (0,0): anon0
DTypes.dfy(53,18): Error: assertion violation
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 15 verified, 2 errors

-------------------- TypeParameters.dfy --------------------
TypeParameters.dfy(41,22): Error: assertion violation
Execution trace:
    (0,0): anon0
TypeParameters.dfy(63,27): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
    (0,0): anon2
TypeParameters.dfy(130,12): Error: assertion violation
TypeParameters.dfy(130,28): Related location: Related location
Execution trace:
    (0,0): anon0
    (0,0): anon14_Then
    TypeParameters.dfy(130,32): anon15_Else
    (0,0): anon5
TypeParameters.dfy(132,12): Error: assertion violation
TypeParameters.dfy(132,33): Related location: Related location
Execution trace:
    (0,0): anon0
    (0,0): anon17_Then
    TypeParameters.dfy(132,37): anon18_Else
    (0,0): anon11
TypeParameters.dfy(146,15): Error BP5005: This loop invariant might not be maintained by the loop.
TypeParameters.dfy(146,38): Related location: Related location
Execution trace:
    (0,0): anon0
    TypeParameters.dfy(139,3): anon17_LoopHead
    (0,0): anon17_LoopBody
    TypeParameters.dfy(139,3): anon18_Else
    (0,0): anon5
    (0,0): anon20_Then
    (0,0): anon8
    TypeParameters.dfy(145,3): anon21_LoopHead
    (0,0): anon21_LoopBody
    TypeParameters.dfy(145,3): anon22_Else
    (0,0): anon13
    TypeParameters.dfy(145,3): anon24_Else
    (0,0): anon15

Dafny program verifier finished with 33 verified, 5 errors

-------------------- Datatypes.dfy --------------------
Datatypes.dfy(82,20): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon20_Else
    (0,0): anon21_Then
    (0,0): anon4
    (0,0): anon22_Else
    (0,0): anon23_Then
    (0,0): anon24_Else
    (0,0): anon25_Then

Dafny program verifier finished with 11 verified, 1 error

-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(34,13): Error: assertion violation
Execution trace:
    (0,0): anon0
TypeAntecedents.dfy(60,1): Error BP5003: A postcondition might not hold on this return path.
TypeAntecedents.dfy(59,15): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon15_Then
    (0,0): anon6
    (0,0): anon18_Then
    (0,0): anon8
    (0,0): anon19_Then
    (0,0): anon10
    (0,0): anon20_Then
    (0,0): anon21_Then
    (0,0): anon14
TypeAntecedents.dfy(68,16): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon15_Else
    (0,0): anon16_Then
    (0,0): anon17_Else

Dafny program verifier finished with 12 verified, 3 errors

-------------------- SplitExpr.dfy --------------------

Dafny program verifier finished with 5 verified, 0 errors

-------------------- Refinement.dfy --------------------

Dafny program verifier finished with 53 verified, 0 errors

-------------------- RefinementErrors.dfy --------------------
RefinementErrors.dfy(1,6): Error: Detected a cyclic refinement declaration: C -> B -> A
RefinementErrors.dfy(27,11): Error: Coupling invariants can only be declared in refinement classes
RefinementErrors.dfy(40,6): Error: Refined class has a member with the same name as in the refinement class: x
RefinementErrors.dfy(42,9): Error: Refined class has a member with the same name as in the refinement class: M
RefinementErrors.dfy(12,10): Error: Refinement methods can only be declared in refinement classes: M
RefinementErrors.dfy(34,10): Error: Different number of output variables
6 resolution/type errors detected in RefinementErrors.dfy