From 486b849f4eade583dd12f7151311375112aa87e4 Mon Sep 17 00:00:00 2001
From: Peter Collingbourne <peter@pcc.me.uk>
Date: Thu, 31 May 2012 20:18:29 +0100
Subject: GPUVerify: use a Formal for procedure predicates

---
 Source/GPUVerify/BlockPredicator.cs | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'Source/GPUVerify')

diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs
index 80d97ebc..99c36af7 100644
--- a/Source/GPUVerify/BlockPredicator.cs
+++ b/Source/GPUVerify/BlockPredicator.cs
@@ -195,9 +195,10 @@ class BlockPredicator {
     foreach (var decl in p.TopLevelDeclarations) {
       if (decl is DeclWithFormals && !(decl is Function)) {
         var dwf = (DeclWithFormals)decl;
-        var fpVar = new LocalVariable(Token.NoToken,
-                                    new TypedIdent(Token.NoToken, "fp",
-                                                   Microsoft.Boogie.Type.Bool));
+        var fpVar = new Formal(Token.NoToken,
+                               new TypedIdent(Token.NoToken, "fp",
+                                              Microsoft.Boogie.Type.Bool),
+                               /*incoming=*/true);
         dwf.InParams = new VariableSeq((dwf.InParams + new VariableSeq(fpVar))
                        .Cast<Variable>().ToArray());
       }
-- 
cgit v1.2.3