diff options
| -rw-r--r-- | Source/Dafny/Makefile | 2 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 2 | ||||
| -rw-r--r-- | Source/DafnyExtension/ResolverTagger.cs | 4 |
3 files changed, 4 insertions, 4 deletions
diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile index e1f1f19f..95cd7748 100644 --- a/Source/Dafny/Makefile +++ b/Source/Dafny/Makefile @@ -6,7 +6,7 @@ # ###############################################################################
COCO_EXE_DIR = ..\..\..\boogiepartners\CocoRdownload
FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified
-COCO = Coco.exe
+COCO = COCO = $(COCO_EXE_DIR)\Coco.exe
# "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they
# are both generated in one go and I don't know a better way to tell
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index eadf24e3..3d4e7916 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -248,7 +248,7 @@ namespace DafnyLanguage translator.UniqueIdPrefix = uniqueIdPrefix;
Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
- resolver.ReInitializeVerificationErrors(requestId, boogieProgram.TopLevelDeclarations);
+ resolver.ReInitializeVerificationErrors(requestId, boogieProgram.Implementations);
// TODO(wuestholz): Maybe we should use a fixed program ID to limit the memory overhead due to the program cache in Boogie.
PipelineOutcome oc = BoogiePipeline(boogieProgram, 1 < Dafny.DafnyOptions.Clo.VerifySnapshots ? uniqueIdPrefix : null, requestId, er);
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs index 3adb37a4..f0acc279 100644 --- a/Source/DafnyExtension/ResolverTagger.cs +++ b/Source/DafnyExtension/ResolverTagger.cs @@ -154,9 +154,9 @@ namespace DafnyLanguage string MostRecentRequestId;
- internal void ReInitializeVerificationErrors(string mostRecentRequestId, IEnumerable<Microsoft.Boogie.Declaration> units)
+ internal void ReInitializeVerificationErrors(string mostRecentRequestId, IEnumerable<Microsoft.Boogie.Implementation> implementations)
{
- var implNames = units.OfType<Microsoft.Boogie.Implementation>().Select(impl => impl.Name);
+ var implNames = implementations.Select(impl => impl.Name);
lock (this)
{
MostRecentRequestId = mostRecentRequestId;
|