From 2f65735d93a06206fcfa1cf48a519677067b1948 Mon Sep 17 00:00:00 2001 From: leino Date: Thu, 13 Nov 2014 08:41:44 -0800 Subject: Use arbitrary lookahead to determine if the next expression is a lambda expression. --- Test/hofs/Apply.dfy.expect | 4 ++-- Test/hofs/FnRef.dfy.expect | 4 ++-- Test/hofs/Frame.dfy.expect | 6 +++--- Test/hofs/Lambda.dfy.expect | 12 ++++++------ Test/hofs/LambdaParsefail.dfy.expect | 10 +++++----- Test/hofs/LambdaParsefail2.dfy.expect | 2 +- Test/hofs/OneShot.dfy.expect | 6 +++--- Test/hofs/ReadsReads.dfy.expect | 4 ++-- Test/hofs/Simple.dfy.expect | 2 +- 9 files changed, 25 insertions(+), 25 deletions(-) (limited to 'Test/hofs') diff --git a/Test/hofs/Apply.dfy.expect b/Test/hofs/Apply.dfy.expect index fad1fe33..77d34c4c 100644 --- a/Test/hofs/Apply.dfy.expect +++ b/Test/hofs/Apply.dfy.expect @@ -1,7 +1,7 @@ Apply.dfy(27,16): Error: assertion violation Execution trace: (0,0): anon0 - Apply.dfy(26,35): anon15_Else - Apply.dfy(27,27): anon17_Else + Apply.dfy(26,27): anon15_Else + Apply.dfy(27,19): anon17_Else Dafny program verifier finished with 6 verified, 1 error diff --git a/Test/hofs/FnRef.dfy.expect b/Test/hofs/FnRef.dfy.expect index 016ee494..0f6f2aa9 100644 --- a/Test/hofs/FnRef.dfy.expect +++ b/Test/hofs/FnRef.dfy.expect @@ -11,12 +11,12 @@ Execution trace: FnRef.dfy(46,12): Error: assertion violation Execution trace: (0,0): anon0 - FnRef.dfy(43,13): anon7_Else + FnRef.dfy(43,12): anon7_Else (0,0): anon9_Then FnRef.dfy(65,14): Error: assertion violation Execution trace: (0,0): anon0 - FnRef.dfy(56,13): anon8_Else + FnRef.dfy(56,12): anon8_Else (0,0): anon10_Then Dafny program verifier finished with 4 verified, 4 errors diff --git a/Test/hofs/Frame.dfy.expect b/Test/hofs/Frame.dfy.expect index a4d10c47..0ee2eadb 100644 --- a/Test/hofs/Frame.dfy.expect +++ b/Test/hofs/Frame.dfy.expect @@ -1,17 +1,17 @@ Frame.dfy(23,16): Error: assertion violation Execution trace: (0,0): anon0 - Frame.dfy(19,13): anon5_Else + Frame.dfy(19,12): anon5_Else (0,0): anon6_Then Frame.dfy(37,14): Error: assertion violation Execution trace: (0,0): anon0 - Frame.dfy(33,13): anon3_Else + Frame.dfy(33,12): anon3_Else Frame.dfy(63,23): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon13_Then - Frame.dfy(55,13): anon14_Else + Frame.dfy(55,12): anon14_Else (0,0): anon15_Then (0,0): anon5 Frame.dfy(66,19): Error: insufficient reads clause to read array element diff --git a/Test/hofs/Lambda.dfy.expect b/Test/hofs/Lambda.dfy.expect index a32c27ff..4fe8275f 100644 --- a/Test/hofs/Lambda.dfy.expect +++ b/Test/hofs/Lambda.dfy.expect @@ -2,13 +2,13 @@ Lambda.dfy(24,12): Error: assertion violation Execution trace: (0,0): anon0 Lambda.dfy(6,24): anon31_Else - Lambda.dfy(7,26): anon32_Else - Lambda.dfy(8,27): anon33_Else - Lambda.dfy(10,39): anon34_Else - Lambda.dfy(11,23): anon35_Else + Lambda.dfy(7,24): anon32_Else + Lambda.dfy(8,26): anon33_Else + Lambda.dfy(10,34): anon34_Else + Lambda.dfy(11,15): anon35_Else Lambda.dfy(13,15): anon36_Else Lambda.dfy(14,15): anon39_Else - Lambda.dfy(18,16): anon42_Else - Lambda.dfy(23,16): anon44_Else + Lambda.dfy(18,15): anon42_Else + Lambda.dfy(23,15): anon44_Else Dafny program verifier finished with 7 verified, 1 error diff --git a/Test/hofs/LambdaParsefail.dfy.expect b/Test/hofs/LambdaParsefail.dfy.expect index d7ee9510..11deb9b0 100644 --- a/Test/hofs/LambdaParsefail.dfy.expect +++ b/Test/hofs/LambdaParsefail.dfy.expect @@ -1,6 +1,6 @@ -LambdaParsefail.dfy(5,17): error: Invalid variable binding in lambda. -LambdaParsefail.dfy(6,16): error: Expected variable binding. -LambdaParsefail.dfy(7,16): error: Expected variable binding. -LambdaParsefail.dfy(8,21): error: cannot declare identifier beginning with underscore -LambdaParsefail.dfy(9,17): error: semi expected +LambdaParsefail.dfy(5,19): error: this symbol not expected in VarDeclStatement +LambdaParsefail.dfy(6,19): error: this symbol not expected in VarDeclStatement +LambdaParsefail.dfy(7,21): error: this symbol not expected in VarDeclStatement +LambdaParsefail.dfy(8,15): error: cannot declare identifier beginning with underscore +LambdaParsefail.dfy(9,17): error: this symbol not expected in VarDeclStatement 5 parse errors detected in LambdaParsefail.dfy diff --git a/Test/hofs/LambdaParsefail2.dfy.expect b/Test/hofs/LambdaParsefail2.dfy.expect index 8bbf643c..0c9ecb83 100644 --- a/Test/hofs/LambdaParsefail2.dfy.expect +++ b/Test/hofs/LambdaParsefail2.dfy.expect @@ -1,2 +1,2 @@ -LambdaParsefail2.dfy(6,33): error: Type specification not allowed here, comma separator was expected. +LambdaParsefail2.dfy(6,39): error: invalid LambdaArrow 1 parse errors detected in LambdaParsefail2.dfy diff --git a/Test/hofs/OneShot.dfy.expect b/Test/hofs/OneShot.dfy.expect index 78a9864b..91b931b8 100644 --- a/Test/hofs/OneShot.dfy.expect +++ b/Test/hofs/OneShot.dfy.expect @@ -2,19 +2,19 @@ OneShot.dfy(20,12): Error: possible violation of function precondition Execution trace: (0,0): anon0 (0,0): anon5_Then - OneShot.dfy(13,9): anon5_Else + OneShot.dfy(13,8): anon5_Else (0,0): anon6_Then OneShot.dfy(22,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon5_Then - OneShot.dfy(13,9): anon5_Else + OneShot.dfy(13,8): anon5_Else (0,0): anon6_Else OneShot.dfy(22,13): Error: possible violation of function precondition Execution trace: (0,0): anon0 (0,0): anon5_Then - OneShot.dfy(13,9): anon5_Else + OneShot.dfy(13,8): anon5_Else (0,0): anon6_Else Dafny program verifier finished with 1 verified, 3 errors diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect index f1da2003..44a95b6d 100644 --- a/Test/hofs/ReadsReads.dfy.expect +++ b/Test/hofs/ReadsReads.dfy.expect @@ -28,12 +28,12 @@ Execution trace: ReadsReads.dfy(98,37): Error: assertion violation Execution trace: (0,0): anon0 - ReadsReads.dfy(95,16): anon15_Else + ReadsReads.dfy(95,14): anon15_Else (0,0): anon19_Then ReadsReads.dfy(100,29): Error: assertion violation Execution trace: (0,0): anon0 - ReadsReads.dfy(95,16): anon15_Else + ReadsReads.dfy(95,14): anon15_Else (0,0): anon21_Then Dafny program verifier finished with 17 verified, 9 errors diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect index 55fe50e0..b3c126d5 100644 --- a/Test/hofs/Simple.dfy.expect +++ b/Test/hofs/Simple.dfy.expect @@ -11,7 +11,7 @@ Execution trace: Simple.dfy(37,9): Error: possible violation of function precondition Execution trace: (0,0): anon0 - Simple.dfy(35,15): anon5_Else + Simple.dfy(35,13): anon5_Else Simple.dfy(49,9): Error: possible violation of function precondition Execution trace: (0,0): anon0 -- cgit v1.2.3