Merge

3 files changed, 41 insertions, 35 deletions

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 4702d5a0..4af8c9ec 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -211,7 +211,7 @@ namespace BytecodeTranslator {
         }

         module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;

         // The decompiler does not turn calls to Assert/Assume into Code Model nodes

-        module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(module);

+        module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(module);

 

         host.RegisterAsLatest(module);

         modules.Add(module);

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 8542ad01..5a1f8dc5 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -139,37 +139,6 @@ namespace Microsoft.Boogie {
       Dafny

     };

 

-    static void CreateDatatypeSelectors(Program program) {

-      List<Function> constructors = new List<Function>();

-      foreach (Declaration decl in program.TopLevelDeclarations) {

-        if (decl is Function && QKeyValue.FindBoolAttribute(decl.Attributes, "constructor"))

-          constructors.Add((Function)decl);

-      }

-

-      foreach (Function f in constructors) {

-        foreach (Variable v in f.InParams) {

-          Formal inVar = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);

-          Formal outVar = new Formal(Token.NoToken, v.TypedIdent, false);

-          Function selector = new Function(f.tok, v.Name + "#" + f.Name, new VariableSeq(inVar), outVar);

-          selector.AddAttribute("selector");

-          for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {

-            if (kv.Key == "constructor") continue;

-            selector.AddAttribute(kv.Key, kv.Params.ToArray());

-          }

-          program.TopLevelDeclarations.Add(selector);

-        }

-        Formal inv = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);

-        Formal outv = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false);

-        Function isConstructor = new Function(f.tok, "is#" + f.Name, new VariableSeq(inv), outv);

-        for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {

-          if (kv.Key == "constructor") continue;

-          isConstructor.AddAttribute(kv.Key, kv.Params.ToArray());

-        } 

-        isConstructor.AddAttribute("membership");

-        program.TopLevelDeclarations.Add(isConstructor);

-      }

-    }

-

     static void ProcessFiles(List<string> fileNames) {

       Contract.Requires(cce.NonNullElements(fileNames));

       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1])) {

@@ -181,8 +150,6 @@ namespace Microsoft.Boogie {
           PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);

         }

 

-        CreateDatatypeSelectors(program);

-

         PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);

         if (oc != PipelineOutcome.ResolvedAndTypeChecked)

           return;

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index e5e3e549..0c9538d4 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -211,6 +211,44 @@ namespace Microsoft.Boogie {
       stream.SetToken(this);

       Emitter.Declarations(this.TopLevelDeclarations, stream);

     }

+

+    void CreateDatatypeSelectorsAndTesters() {

+      HashSet<string> functions = new HashSet<string>();

+      List<Function> constructors = new List<Function>();

+      foreach (Declaration decl in TopLevelDeclarations) {

+        Function func = decl as Function;

+        if (func == null) continue;

+        functions.Add(func.Name);

+        if (QKeyValue.FindBoolAttribute(func.Attributes, "constructor"))

+          constructors.Add(func);

+      }

+

+      foreach (Function f in constructors) {

+        foreach (Variable v in f.InParams) {

+          Formal inVar = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);

+          Formal outVar = new Formal(Token.NoToken, v.TypedIdent, false);

+          Function selector = new Function(f.tok, v.Name + "#" + f.Name, new VariableSeq(inVar), outVar);

+          selector.AddAttribute("selector");

+          for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {

+            if (kv.Key == "constructor") continue;

+            selector.AddAttribute(kv.Key, kv.Params.ToArray());

+          }

+          if (!functions.Contains(selector.Name))

+            TopLevelDeclarations.Add(selector);

+        }

+        Formal inv = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);

+        Formal outv = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false);

+        Function isConstructor = new Function(f.tok, "is#" + f.Name, new VariableSeq(inv), outv);

+        for (QKeyValue kv = f.Attributes; kv != null; kv = kv.Next) {

+          if (kv.Key == "constructor") continue;

+          isConstructor.AddAttribute(kv.Key, kv.Params.ToArray());

+        }

+        isConstructor.AddAttribute("membership");

+        if (!functions.Contains(isConstructor.Name))

+          TopLevelDeclarations.Add(isConstructor);

+      }

+    }

+

     /// <summary>

     /// Returns the number of name resolution errors.

     /// </summary>

@@ -229,6 +267,8 @@ namespace Microsoft.Boogie {
       //Contract.Requires(rc != null);

       Helpers.ExtraTraceInformation("Starting resolution");

 

+      CreateDatatypeSelectorsAndTesters();

+

       foreach (Declaration d in TopLevelDeclarations) {

         d.Register(rc);

       }

@@ -264,7 +304,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-

     private void ResolveTypes(ResolutionContext rc) {

       Contract.Requires(rc != null);

       // first resolve type constructors