From b0c51b6fdf1960bbee547959eaf9b0985dee10a9 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 30 Oct 2012 17:13:13 -0700
Subject: Rename _reverifyPost to $_reverifyPost, so that it doesn't show up in
 BVD Remove some duplicated hover text in DafnyExtension Enable Code Contracts
 in the build

---
 Source/Dafny/Translator.cs                  | 14 ++++++------
 Source/DafnyExtension/DafnyExtension.csproj | 33 +++++++++++++++++++++++++++++
 Source/DafnyExtension/IdentifierTagger.cs   |  3 +++
 Source/DafnyExtension/ResolverTagger.cs     |  2 +-
 Source/DafnyExtension/TokenTagger.cs        |  1 +
 5 files changed, 45 insertions(+), 8 deletions(-)

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index d2d22851..65fb498b 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1555,8 +1555,8 @@ namespace Microsoft.Dafny {
         }
         // translate the body of the method
         Contract.Assert(m.Body != null);  // follows from method precondition and the if guard
-        // _reverifyPost := false;
-        builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, "_reverifyPost", Bpl.Type.Bool), Bpl.Expr.False));
+        // $_reverifyPost := false;
+        builder.Add(Bpl.Cmd.SimpleAssign(m.tok, new Bpl.IdentifierExpr(m.tok, "$_reverifyPost", Bpl.Type.Bool), Bpl.Expr.False));
         stmts = TrStmt2StmtList(builder, m.Body, localVariables, etran);
       } else {
         // check well-formedness of the preconditions, and then assume each one of them
@@ -3454,8 +3454,8 @@ namespace Microsoft.Dafny {
             foreach (var s in ss) {
               var post = s.E;
               if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) {
-                // this postcondition was inherited into this module, so make it into the form "_reverifyPost ==> s.E"
-                post = Bpl.Expr.Imp(new Bpl.IdentifierExpr(s.E.tok, "_reverifyPost", Bpl.Type.Bool), post);
+                // this postcondition was inherited into this module, so make it into the form "$_reverifyPost ==> s.E"
+                post = Bpl.Expr.Imp(new Bpl.IdentifierExpr(s.E.tok, "$_reverifyPost", Bpl.Type.Bool), post);
               }
               ens.Add(Ensures(s.E.tok, s.IsOnlyFree, post, null, null));
             }
@@ -3790,7 +3790,7 @@ namespace Microsoft.Dafny {
           outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), false));
         }
         if (kind == MethodTranslationKind.Implementation) {
-          outParams.Add(new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "_reverifyPost", Bpl.Type.Bool), false));
+          outParams.Add(new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "$_reverifyPost", Bpl.Type.Bool), false));
         }
       }
     }
@@ -4151,8 +4151,8 @@ namespace Microsoft.Dafny {
         var s = (ReturnStmt)stmt;
         AddComment(builder, stmt, "return statement");
         if (s.ReverifyPost) {
-          // _reverifyPost := true;
-          builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, new Bpl.IdentifierExpr(s.Tok, "_reverifyPost", Bpl.Type.Bool), Bpl.Expr.True));
+          // $_reverifyPost := true;
+          builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, new Bpl.IdentifierExpr(s.Tok, "$_reverifyPost", Bpl.Type.Bool), Bpl.Expr.True));
         }
         if (s.hiddenUpdate != null) {
           TrStmt(s.hiddenUpdate, builder, locals, etran);
diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index b04ecc14..ca15afc8 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -21,6 +21,7 @@
     <UpgradeBackupLocation>
     </UpgradeBackupLocation>
     <OldToolsVersion>4.0</OldToolsVersion>
+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
   </PropertyGroup>
   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
     <DebugSymbols>true</DebugSymbols>
@@ -30,6 +31,38 @@
     <DefineConstants>DEBUG;TRACE</DefineConstants>
     <ErrorReport>prompt</ErrorReport>
     <WarningLevel>4</WarningLevel>
+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+    <CodeContractsInferRequires>False</CodeContractsInferRequires>
+    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
+    <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
+    <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
+    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
+    <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
+    <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+    <CodeContractsCustomRewriterAssembly />
+    <CodeContractsCustomRewriterClass />
+    <CodeContractsLibPaths />
+    <CodeContractsExtraRewriteOptions />
+    <CodeContractsExtraAnalysisOptions />
+    <CodeContractsBaseLineFile />
+    <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
   </PropertyGroup>
   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
     <DebugType>pdbonly</DebugType>
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index ace9ae3f..29e451a6 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -133,6 +133,9 @@ namespace DafnyLanguage
       List<IdRegion> newRegions = new List<IdRegion>();
 
       foreach (var module in program.Modules) {
+        if (module.IsFacade) {
+          continue;
+        }
         foreach (var d in module.TopLevelDecls) {
           if (d is DatatypeDecl) {
             var dt = (DatatypeDecl)d;
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index d1af6878..ca9ed169 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -311,7 +311,7 @@ namespace DafnyLanguage
       Snapshot = snapshot;
     }
     public SnapshotSpan Span() {
-      Contract.Requires(Snapshot != null);  // requires that Snapshot has been filled in
+      Contract.Assume(Snapshot != null);  // requires that Snapshot has been filled in
       var line = Snapshot.GetLineFromLineNumber(Line);
       Contract.Assume(Column <= line.Length);  // this is really a precondition of the constructor + FillInSnapshot
       var length = Math.Min(line.Length - Column, 5);
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 190051ef..a8f63232 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -259,6 +259,7 @@ namespace DafnyLanguage
                 case "invariant":
                 case "iterator":
                 case "label":
+                case "map":
                 case "match":
                 case "method":
                 case "modifies":
-- 
cgit v1.2.3