fixed crash reported by Dan.

DoModSetAnalysis needs to run before the linear and mover type checking.

3 files changed, 7 insertions, 8 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index ab1e185c..7756973d 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -505,12 +505,6 @@ namespace Microsoft.Boogie
           }

         }

 

-        EliminateDeadVariables(program);

-

-        CollectModSets(program);

-

-        CoalesceBlocks(program);

-

         if (CommandLineOptions.Clo.StratifiedInlining == 0)

         {

           Concurrency.Transform(linearTypeChecker, moverTypeChecker);

@@ -524,6 +518,10 @@ namespace Microsoft.Boogie
           }

         }

 

+        EliminateDeadVariables(program);

+

+        CoalesceBlocks(program);

+

         Inline(program);

 

         var stats = new PipelineStatistics();

@@ -742,6 +740,8 @@ namespace Microsoft.Boogie
           CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;

       }

 

+      CollectModSets(program);

+

       moverTypeChecker = new MoverTypeChecker(program);

       moverTypeChecker.TypeCheck();

       if (moverTypeChecker.errorCount != 0)

diff --git a/Test/og/parallel4.bpl.expect b/Test/og/parallel4.bpl.expect
index eaead450..25ad398c 100644
--- a/Test/og/parallel4.bpl.expect
+++ b/Test/og/parallel4.bpl.expect
@@ -1,6 +1,6 @@
 parallel4.bpl(31,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    (0,0): og_init

+    parallel4.bpl(29,5): anon0

     (0,0): anon01

 

 Boogie program verifier finished with 3 verified, 1 error

diff --git a/Test/og/t1.bpl.expect b/Test/og/t1.bpl.expect
index f0195727..0b0c936e 100644
--- a/Test/og/t1.bpl.expect
+++ b/Test/og/t1.bpl.expect
@@ -1,6 +1,5 @@
 t1.bpl(65,5): Error: Non-interference check failed

 Execution trace:

-    (0,0): og_init

     t1.bpl(84,13): anon0

     (0,0): anon05

     (0,0): inline$SetG_1$0$Entry