diff options
Diffstat (limited to 'Source/ExecutionEngine/ExecutionEngine.cs')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index e7b55dc4..bed9c6c0 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -485,8 +485,7 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.StratifiedInlining == 0)
{
- OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypeChecker, moverTypeChecker);
- ogTransform.Transform();
+ OwickiGriesTransform.Transform(linearTypeChecker, moverTypeChecker);
var eraser = new LinearEraser();
eraser.VisitProgram(program);
if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)
@@ -683,6 +682,14 @@ namespace Microsoft.Boogie CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
}
+ moverTypeChecker = new MoverTypeChecker(program);
+ moverTypeChecker.TypeCheck();
+ if (moverTypeChecker.errorCount != 0)
+ {
+ Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, bplFileName);
+ return PipelineOutcome.TypeCheckingError;
+ }
+
linearTypeChecker = new LinearTypeChecker(program);
linearTypeChecker.TypeCheck();
if (linearTypeChecker.errorCount == 0)
@@ -695,16 +702,6 @@ namespace Microsoft.Boogie return PipelineOutcome.TypeCheckingError;
}
-#if QED
- moverTypeChecker = new MoverTypeChecker(program);
- moverTypeChecker.TypeCheck();
- if (moverTypeChecker.errorCount != 0)
- {
- Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, bplFileName);
- return PipelineOutcome.TypeCheckingError;
- }
-#endif
-
if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)
{
// if PrintDesugaring option is engaged, print the file here, after resolution and type checking
|