Added /trustAtomicityTypes option

2 files changed, 7 insertions, 3 deletions

diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs
index 45d538df..a3a621ac 100644
--- a/Source/Concurrency/Program.cs
+++ b/Source/Concurrency/Program.cs
@@ -32,8 +32,10 @@ namespace Microsoft.Boogie
 

             List<Declaration> decls = new List<Declaration>();

             OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls);

-            MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);

-

+            if (!CommandLineOptions.Clo.TrustAtomicityTypes)

+            {

+                MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls);

+            }

             foreach (Declaration decl in decls)

             {

                 Procedure proc = decl as Procedure;

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index a4374623..88d78fa9 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -488,6 +488,7 @@ namespace Microsoft.Boogie {
     public int  /*0..9*/StepsBeforeWidening = 0;           // The number of steps that must be done before applying a widen operator

 

     public string OwickiGriesDesugaredOutputFile = null;

+    public bool TrustAtomicityTypes = false;

 

     public enum VCVariety {

       Structured,

@@ -1371,7 +1372,8 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||

               ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||

               ps.CheckBooleanFlag("verifySnapshots", ref VerifySnapshots) ||

-              ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately)

+              ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately) ||

+              ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes)

               ) {

             // one of the boolean flags matched

             return true;