diff options
-rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 2 | ||||
-rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 33 | ||||
-rw-r--r-- | Source/Core/Absy.cs | 41 |
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
|