summaryrefslogtreecommitdiff
path: root/Source/GPUVerify
diff options
context:
space:
mode:
Diffstat (limited to 'Source/GPUVerify')
-rw-r--r--Source/GPUVerify/BlockPredicator.cs7
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());
}