diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-05 18:17:54 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-05 18:17:54 -0700 |
| commit | bbfefea4f221c0be1b295ba1c5ee622fda9ec0d0 (patch) | |
| tree | dcee0caa1cfffa222a146ab8906edd29c1103547 | |
| parent | a1a041f3549cb1665964d30b666c825767d59afb (diff) | |
Longer output lines to indicate failures in regression test suite
| -rw-r--r-- | Source/Dafny/Resolver.cs | 2 | ||||
| -rw-r--r-- | Test/runtest.bat | 2 |
2 files changed, 1 insertions, 3 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 11acfb2d..945bf5c2 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -2468,11 +2468,9 @@ namespace Microsoft.Dafny Error(e.E, "Precondition must be a boolean (got {0})", e.E.Type);
}
}
-
foreach (FrameExpression fe in m.Mod.Expressions) {
ResolveFrameExpression(fe, "modifies");
}
-
foreach (Expression e in m.Decreases.Expressions) {
ResolveExpression(e, false);
// any type is fine
diff --git a/Test/runtest.bat b/Test/runtest.bat index 667ca579..dfc3ae00 100644 --- a/Test/runtest.bat +++ b/Test/runtest.bat @@ -11,7 +11,7 @@ rem Calling fc twice seems to fix (or at least alleviate) the problem. fc /W Answer Output > nul
fc /W Answer Output > nul
if not errorlevel 1 goto passTest
-echo ============ %1 FAILED ============
+echo ============ %1 FAILED ====================================
goto errorEnd
:passTest
|