summaryrefslogtreecommitdiff
path: root/Source/GPUVerify/GPUVerifier.cs
diff options
context:
space:
mode:
authorGravatar Unknown <afd@insolent.win.doc.ic.ac.uk>2011-11-15 16:56:43 +0000
committerGravatar Unknown <afd@insolent.win.doc.ic.ac.uk>2011-11-15 16:56:43 +0000
commit8e1a19a4fc73dcde12f0d20d3f40fc5fb0146425 (patch)
tree6b86ca1c6cc9b027252bf9097264f902874ec090 /Source/GPUVerify/GPUVerifier.cs
parente1d66ac9026c503d3723895faacdcb5bc68ed520 (diff)
Some fixes for race checking contracts
Diffstat (limited to 'Source/GPUVerify/GPUVerifier.cs')
-rw-r--r--Source/GPUVerify/GPUVerifier.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 25974225..36881f88 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -597,7 +597,7 @@ namespace GPUVerify
- private void AddCandidateRequires(Procedure Proc, Expr e)
+ internal void AddCandidateRequires(Procedure Proc, Expr e)
{
Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);
@@ -605,7 +605,7 @@ namespace GPUVerify
Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
}
- private void AddCandidateEnsures(Procedure Proc, Expr e)
+ internal void AddCandidateEnsures(Procedure Proc, Expr e)
{
Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);
IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);