GPUVerify: factor out CreateCandidateInvariant from AddCandidateInvariant

This allows us to build candidate invariants in situations where we
don't have a Region, such as the block predicator.

1 files changed, 7 insertions, 2 deletions

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index d43bda9a..fbf27669 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -2156,14 +2156,19 @@ namespace GPUVerify
 

         internal void AddCandidateInvariant(IRegion region, Expr e, string tag)

         {

+            region.AddInvariant(CreateCandidateInvariant(e, tag));

+        }

+

+        internal PredicateCmd CreateCandidateInvariant(Expr e, string tag)

+        {

             Constant ExistentialBooleanConstant = MakeExistentialBoolean(Token.NoToken);

             IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);

             PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));

             invariant.Attributes = new QKeyValue(Token.NoToken, "tag", new List<object>(new object[] { tag }), null);

-            region.AddInvariant(invariant);

             Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);

+            return invariant;

         }

-

+            

         internal Implementation GetImplementation(string procedureName)

         {

             foreach (Declaration D in Program.TopLevelDeclarations)