From 486b849f4eade583dd12f7151311375112aa87e4 Mon Sep 17 00:00:00 2001 From: Peter Collingbourne 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(-) 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().ToArray()); } -- cgit v1.2.3