diff options
| -rw-r--r-- | Source/GPUVerify/BlockPredicator.cs | 7 |
1 files 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<Variable>().ToArray()); } |