From bcc2de7ff9390509b1087c47d8b5e825ca9df3c1 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 30 May 2011 22:01:35 -0700 Subject: Dafny: Translate general LHSs for var and := (not yet for call, no compilation yet) --- Test/dafny0/Answer | 123 +++++++++++++++++++++++++++++++---------------------- 1 file changed, 73 insertions(+), 50 deletions(-) (limited to 'Test/dafny0/Answer') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c82d3803..75025b2f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -85,7 +85,7 @@ TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subran NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 -NatTypes.dfy(31,5): Error: value assigned to a nat must be non-negative +NatTypes.dfy(31,10): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 NatTypes.dfy(19,3): anon10_LoopHead @@ -111,7 +111,7 @@ Execution trace: (0,0): anon0 (0,0): anon5_Else (0,0): anon6_Then -NatTypes.dfy(86,16): Error: value assigned to a nat must be non-negative +NatTypes.dfy(86,19): Error: value assigned to a nat must be non-negative Execution trace: (0,0): anon0 (0,0): anon3_Then @@ -450,7 +450,7 @@ ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator 9 parse errors detected in ParseErrors.dfy -------------------- Array.dfy -------------------- -Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause +Array.dfy(10,8): Error: assignment may update an array element not in the enclosing method's modifies clause Execution trace: (0,0): anon0 (0,0): anon5_Then @@ -465,13 +465,13 @@ Execution trace: 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 +Array.dfy(56,8): 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 +Array.dfy(63,8): Error: assignment may update an array element not in the enclosing method's modifies clause Execution trace: (0,0): anon0 (0,0): anon5_Then @@ -490,10 +490,10 @@ 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 +Array.dfy(131,6): 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 +Array.dfy(138,6): Error: assignment may update an array element not in the enclosing method's modifies clause Execution trace: (0,0): anon0 @@ -598,8 +598,31 @@ Execution trace: (0,0): anon10 Basics.dfy(66,95): anon18_Else (0,0): anon12 +Basics.dfy(86,16): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon10_Then +Basics.dfy(99,12): Error: left-hand sides 0 and 1 may refer to the same location +Execution trace: + (0,0): anon0 + (0,0): anon3 + (0,0): anon11_Else + (0,0): anon6 + (0,0): anon12_Then +Basics.dfy(105,10): Error: left-hand sides 0 and 1 may refer to the same location +Execution trace: + (0,0): anon0 + (0,0): anon10_Then + (0,0): anon3 + (0,0): anon11_Then + (0,0): anon6 + (0,0): anon12_Then + (0,0): anon9 +Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location +Execution trace: + (0,0): anon0 -Dafny program verifier finished with 7 verified, 2 errors +Dafny program verifier finished with 9 verified, 6 errors -------------------- ControlStructures.dfy -------------------- ControlStructures.dfy(5,3): Error: missing case in case statement: Blue @@ -638,112 +661,112 @@ ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibil Execution trace: (0,0): anon0 (0,0): anon5_Else -ControlStructures.dfy(218,18): Error: assertion violation +ControlStructures.dfy(215,18): Error: assertion violation Execution trace: (0,0): anon0 - ControlStructures.dfy(197,3): anon62_LoopHead + ControlStructures.dfy(194,3): anon62_LoopHead (0,0): anon62_LoopBody - ControlStructures.dfy(197,3): anon63_Else + ControlStructures.dfy(194,3): anon63_Else (0,0): anon3 - ControlStructures.dfy(197,3): anon64_Else + ControlStructures.dfy(194,3): anon64_Else (0,0): anon5 - ControlStructures.dfy(201,5): anon65_LoopHead + ControlStructures.dfy(198,5): anon65_LoopHead (0,0): anon65_LoopBody - ControlStructures.dfy(201,5): anon66_Else + ControlStructures.dfy(198,5): anon66_Else (0,0): anon8 - ControlStructures.dfy(201,5): anon67_Else + ControlStructures.dfy(198,5): anon67_Else (0,0): anon10 (0,0): anon71_Then - ControlStructures.dfy(213,9): anon72_LoopHead + ControlStructures.dfy(210,9): anon72_LoopHead (0,0): anon72_LoopBody - ControlStructures.dfy(213,9): anon73_Else + ControlStructures.dfy(210,9): anon73_Else (0,0): anon20 (0,0): anon74_Then (0,0): anon29 -ControlStructures.dfy(235,21): Error: assertion violation +ControlStructures.dfy(232,21): Error: assertion violation Execution trace: (0,0): anon0 - ControlStructures.dfy(197,3): anon62_LoopHead + ControlStructures.dfy(194,3): anon62_LoopHead (0,0): anon62_LoopBody - ControlStructures.dfy(197,3): anon63_Else + ControlStructures.dfy(194,3): anon63_Else (0,0): anon3 - ControlStructures.dfy(197,3): anon64_Else + ControlStructures.dfy(194,3): anon64_Else (0,0): anon5 - ControlStructures.dfy(201,5): anon65_LoopHead + ControlStructures.dfy(198,5): anon65_LoopHead (0,0): anon65_LoopBody - ControlStructures.dfy(201,5): anon66_Else + ControlStructures.dfy(198,5): anon66_Else (0,0): anon8 - ControlStructures.dfy(201,5): anon67_Else + ControlStructures.dfy(198,5): anon67_Else (0,0): anon10 (0,0): anon71_Then - ControlStructures.dfy(213,9): anon72_LoopHead + ControlStructures.dfy(210,9): anon72_LoopHead (0,0): anon72_LoopBody - ControlStructures.dfy(213,9): anon73_Else + ControlStructures.dfy(210,9): anon73_Else (0,0): anon20 - ControlStructures.dfy(213,9): anon74_Else + ControlStructures.dfy(210,9): anon74_Else (0,0): anon22 (0,0): anon75_Then (0,0): after_4 - ControlStructures.dfy(224,7): anon77_LoopHead + ControlStructures.dfy(221,7): anon77_LoopHead (0,0): anon77_LoopBody - ControlStructures.dfy(224,7): anon78_Else + ControlStructures.dfy(221,7): anon78_Else (0,0): anon33 - ControlStructures.dfy(224,7): anon79_Else + ControlStructures.dfy(221,7): anon79_Else (0,0): anon35 (0,0): anon81_Then (0,0): anon38 (0,0): after_9 (0,0): anon86_Then (0,0): anon53 -ControlStructures.dfy(238,30): Error: assertion violation +ControlStructures.dfy(235,30): Error: assertion violation Execution trace: (0,0): anon0 - ControlStructures.dfy(197,3): anon62_LoopHead + ControlStructures.dfy(194,3): anon62_LoopHead (0,0): anon62_LoopBody - ControlStructures.dfy(197,3): anon63_Else + ControlStructures.dfy(194,3): anon63_Else (0,0): anon3 - ControlStructures.dfy(197,3): anon64_Else + ControlStructures.dfy(194,3): anon64_Else (0,0): anon5 - ControlStructures.dfy(201,5): anon65_LoopHead + ControlStructures.dfy(198,5): anon65_LoopHead (0,0): anon65_LoopBody - ControlStructures.dfy(201,5): anon66_Else + ControlStructures.dfy(198,5): anon66_Else (0,0): anon8 - ControlStructures.dfy(201,5): anon67_Else + ControlStructures.dfy(198,5): anon67_Else (0,0): anon10 (0,0): anon68_Then (0,0): after_5 (0,0): anon87_Then (0,0): anon88_Then (0,0): anon58 -ControlStructures.dfy(241,17): Error: assertion violation +ControlStructures.dfy(238,17): Error: assertion violation Execution trace: (0,0): anon0 - ControlStructures.dfy(197,3): anon62_LoopHead + ControlStructures.dfy(194,3): anon62_LoopHead (0,0): anon62_LoopBody - ControlStructures.dfy(197,3): anon63_Else + ControlStructures.dfy(194,3): anon63_Else (0,0): anon3 - ControlStructures.dfy(197,3): anon64_Else + ControlStructures.dfy(194,3): anon64_Else (0,0): anon5 - ControlStructures.dfy(201,5): anon65_LoopHead + ControlStructures.dfy(198,5): anon65_LoopHead (0,0): anon65_LoopBody - ControlStructures.dfy(201,5): anon66_Else + ControlStructures.dfy(198,5): anon66_Else (0,0): anon8 - ControlStructures.dfy(201,5): anon67_Else + ControlStructures.dfy(198,5): anon67_Else (0,0): anon10 (0,0): anon71_Then - ControlStructures.dfy(213,9): anon72_LoopHead + ControlStructures.dfy(210,9): anon72_LoopHead (0,0): anon72_LoopBody - ControlStructures.dfy(213,9): anon73_Else + ControlStructures.dfy(210,9): anon73_Else (0,0): anon20 - ControlStructures.dfy(213,9): anon74_Else + ControlStructures.dfy(210,9): anon74_Else (0,0): anon22 (0,0): anon75_Then (0,0): after_4 - ControlStructures.dfy(224,7): anon77_LoopHead + ControlStructures.dfy(221,7): anon77_LoopHead (0,0): anon77_LoopBody - ControlStructures.dfy(224,7): anon78_Else + ControlStructures.dfy(221,7): anon78_Else (0,0): anon33 - ControlStructures.dfy(224,7): anon79_Else + ControlStructures.dfy(221,7): anon79_Else (0,0): anon35 (0,0): anon82_Then (0,0): anon85_Then -- cgit v1.2.3