diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-04 11:24:35 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-04 11:24:35 -0700 |
| commit | 47d88acd5e49ea9f68dd93bc2eb8dca85036b7ca (patch) | |
| tree | ae9fe1fd8987d740c38c4989aa91957257d60d3b /Source/BoogieDriver/BoogieDriver.cs | |
| parent | 4024e730fe78f4f210b497041ca083b1464426b5 (diff) | |
fixed bug reported by Akash
Diffstat (limited to 'Source/BoogieDriver/BoogieDriver.cs')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 125 |
1 files changed, 70 insertions, 55 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index c12ba47d..1f4edf87 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -157,71 +157,86 @@ namespace Microsoft.Boogie { static void ProcessFiles(List<string> fileNames) {
Contract.Requires(cce.NonNullElements(fileNames));
- using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1])) {
- //BoogiePL.Errors.count = 0;
- Program program = ParseBoogieProgram(fileNames, false);
- if (program == null)
- return;
- if (CommandLineOptions.Clo.PrintFile != null) {
- PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);
- }
+ using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1]))
+ {
+ //BoogiePL.Errors.count = 0;
+ Program program = ParseBoogieProgram(fileNames, false);
+ if (program == null)
+ return;
+ if (CommandLineOptions.Clo.PrintFile != null)
+ {
+ PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);
+ }
- PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);
- if (oc != PipelineOutcome.ResolvedAndTypeChecked)
- return;
- //BoogiePL.Errors.count = 0;
+ PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);
+ if (oc != PipelineOutcome.ResolvedAndTypeChecked)
+ return;
+ //BoogiePL.Errors.count = 0;
- // Do bitvector analysis
- if (CommandLineOptions.Clo.DoBitVectorAnalysis) {
- Microsoft.Boogie.BitVectorAnalysis.DoBitVectorAnalysis(program);
- PrintBplFile(CommandLineOptions.Clo.BitVectorAnalysisOutputBplFile, program, false);
- return;
- }
+ // Do bitvector analysis
+ if (CommandLineOptions.Clo.DoBitVectorAnalysis)
+ {
+ Microsoft.Boogie.BitVectorAnalysis.DoBitVectorAnalysis(program);
+ PrintBplFile(CommandLineOptions.Clo.BitVectorAnalysisOutputBplFile, program, false);
+ return;
+ }
- if (CommandLineOptions.Clo.PrintCFGPrefix != null) {
- foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>()) {
- using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot")) {
- sw.Write(program.ProcessLoops(impl).ToDot());
- }
+ if (CommandLineOptions.Clo.PrintCFGPrefix != null)
+ {
+ foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+ {
+ using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot"))
+ {
+ sw.Write(program.ProcessLoops(impl).ToDot());
+ }
+ }
}
- }
- if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)
- {
- OwickiGriesTransform ogTransform = new OwickiGriesTransform(program);
- ogTransform.Transform();
- int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
- CommandLineOptions.Clo.PrintUnstructured = 1;
- PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false);
- CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
- }
+ if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)
+ {
+ OwickiGriesTransform ogTransform = new OwickiGriesTransform(program);
+ ogTransform.Transform();
+ int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+ CommandLineOptions.Clo.PrintUnstructured = 1;
+ PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false);
+ CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+ }
- LinearSetTransform linearTransform = new LinearSetTransform(program);
- linearTransform.Transform();
+ {
+ LinearSetTransform linearTransform = new LinearSetTransform(program);
+ linearTransform.Transform();
+ //int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;
+ //CommandLineOptions.Clo.PrintUnstructured = 1;
+ //PrintBplFile("lsd.bpl", program, false, false);
+ //CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;
+ }
- EliminateDeadVariablesAndInline(program);
+ EliminateDeadVariablesAndInline(program);
- if (CommandLineOptions.Clo.StagedHoudini > 0) {
- var candidateDependenceAnalyser = new CandidateDependenceAnalyser(program);
- candidateDependenceAnalyser.Analyse();
- candidateDependenceAnalyser.ApplyStages();
- if (CommandLineOptions.Clo.Trace) {
- candidateDependenceAnalyser.dump();
+ if (CommandLineOptions.Clo.StagedHoudini > 0)
+ {
+ var candidateDependenceAnalyser = new CandidateDependenceAnalyser(program);
+ candidateDependenceAnalyser.Analyse();
+ candidateDependenceAnalyser.ApplyStages();
+ if (CommandLineOptions.Clo.Trace)
+ {
+ candidateDependenceAnalyser.dump();
+ }
+ PrintBplFile("staged.bpl", program, false, false);
+ Environment.Exit(0);
}
- PrintBplFile("staged.bpl", program, false, false);
- Environment.Exit(0);
- }
- int errorCount, verified, inconclusives, timeOuts, outOfMemories;
- oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
- switch (oc) {
- case PipelineOutcome.Done:
- case PipelineOutcome.VerificationCompleted:
- WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
- break;
- default:
- break;
- }
+ int errorCount, verified, inconclusives, timeOuts, outOfMemories;
+ oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
+ switch (oc)
+ {
+ case PipelineOutcome.Done:
+ case PipelineOutcome.VerificationCompleted:
+ WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ break;
+ default:
+ break;
+ }
}
}
|