diff options
| author |  Mike Barnett <mbarnett@microsoft.com> | 2011-10-23 14:02:05 -0700 |
|---|---|---|
| committer | Mike Barnett <mbarnett@microsoft.com> | 2011-10-23 14:02:05 -0700 |
| commit | 6452dd68ea7078ad8bfd4c5be32f21b21d20060a (patch) | |
| tree | 7a66d39473f08ba32aef2e0c8ebbf82c5b744343 /BCT/BytecodeTranslator/Program.cs | |
| parent | a1665f0b3fbe164c5eefee06ce89e1ba4adb66a8 (diff) | |
Don't let /s be specified for stub files. (But keep the old code in case we
go back to it.)
Diffstat (limited to 'BCT/BytecodeTranslator/Program.cs')
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index f08d8536..d3994a6c 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -95,6 +95,10 @@ namespace BytecodeTranslator { Console.WriteLine("Specified exemption file '{0}' not found.", fileName);
}
}
+ if (options.stub != null) {
+ Console.WriteLine("/s is no longer used to specify stub assemblies");
+ return errorReturnValue;
+ }
if (options.breakIntoDebugger) {
System.Diagnostics.Debugger.Break();
@@ -338,6 +342,32 @@ namespace BytecodeTranslator { finalizeNavigationAnalysisAndBoogieCode(phoneControlsConfigFile, sink, outputFileName);
}
+ //sink.CreateIdentifierCorrespondenceTable(primaryModule.Name.Value);
+
+ //var rc = new Bpl.ResolutionContext((Bpl.IErrorSink)null);
+ //foreach (var decl in sink.TranslatedProgram.TopLevelDeclarations) {
+ // decl.Register(rc);
+ //}
+ //sink.TranslatedProgram.Resolve(rc);
+ //var goodDecls = new List<Bpl.Declaration>();
+ //var tc = new Bpl.TypecheckingContext(null);
+ //foreach (var decl in sink.TranslatedProgram.TopLevelDeclarations) {
+ // var impl = decl as Bpl.Implementation;
+ // if (impl == null) {
+ // goodDecls.Add(decl);
+ // continue;
+ // }
+ // try {
+ // //var tc = new Bpl.TypecheckingContext(null);
+ // impl.Typecheck(tc);
+ // goodDecls.Add(impl);
+ // } catch {
+ // Console.WriteLine("Deleting implementation for: " + impl.Name);
+ // // nothing to do, just continue
+ // }
+ //}
+ //sink.TranslatedProgram.TopLevelDeclarations = goodDecls;
+
Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);
Prelude.Emit(writer);
sink.TranslatedProgram.Emit(writer);
|