From 544da1e8cfb5d60a9803cc263383181e9fe3c25f Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 4 Jan 2012 15:10:03 -0800 Subject: Dafny: disengaged old refinement test files --- Test/dafny0/Answer | 13 ------------- Test/dafny0/runtest.bat | 2 +- 2 files changed, 1 insertion(+), 14 deletions(-) (limited to 'Test') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index adc49908..20e96185 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1200,19 +1200,6 @@ Dafny program verifier finished with 12 verified, 3 errors 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 - -------------------- LoopModifies.dfy -------------------- LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause Execution trace: diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 7761b47d..c4bc5d82 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -18,7 +18,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy Comprehensions.dfy Basics.dfy ControlStructures.dfy Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy - Refinement.dfy RefinementErrors.dfy LoopModifies.dfy + LoopModifies.dfy ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy) do ( echo. -- cgit v1.2.3