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

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":