diff options
| author |  Unknown <afd@afd-THINK.hsd1.or.comcast.net.> | 2012-03-16 23:40:39 -0700 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.hsd1.or.comcast.net.> | 2012-03-16 23:40:39 -0700 |
| commit | a753b076ebf93a687cbed1049534b6cfe7074c81 (patch) | |
| tree | b3589983ab69f235c1731a9bcc2b94135c73c067 | |
| parent | 6ad022644a490a0019993325324782ccd58cff01 (diff) | |
Added support for further annotations
| -rw-r--r-- | Source/GPUVerify/AccessInvariantProcessor.cs | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/Source/GPUVerify/AccessInvariantProcessor.cs b/Source/GPUVerify/AccessInvariantProcessor.cs index 4a5c34e8..71d3e482 100644 --- a/Source/GPUVerify/AccessInvariantProcessor.cs +++ b/Source/GPUVerify/AccessInvariantProcessor.cs @@ -26,20 +26,6 @@ namespace GPUVerify {
FunctionCall call = node.Fun as FunctionCall;
- if (MatchesIntrinsic(call.Func, NO_READ))
- {
- return Expr.Not(
- MakeReadHasOccurred(node, call, NO_READ)
- );
- }
-
- if (MatchesIntrinsic(call.Func, NO_WRITE))
- {
- return Expr.Not(
- MakeWriteHasOccurred(node, call, NO_WRITE)
- );
- }
-
if (MatchesIntrinsic(call.Func, READ_OFFSET))
{
return new IdentifierExpr(node.tok, new GlobalVariable(
@@ -56,24 +42,38 @@ namespace GPUVerify );
}
- if (MatchesIntrinsic(call.Func, READ))
+ if (MatchesIntrinsic(call.Func, READ_IMPLIES))
{
- return MakeReadHasOccurred(node, call, READ);
+ return Expr.Imp(MakeReadHasOccurred(node, call, READ_IMPLIES), VisitExpr(node.Args[0]));
}
- if (MatchesIntrinsic(call.Func, WRITE))
+ if (MatchesIntrinsic(call.Func, WRITE_IMPLIES))
{
- return MakeWriteHasOccurred(node, call, WRITE);
+ return Expr.Imp(MakeWriteHasOccurred(node, call, WRITE_IMPLIES), VisitExpr(node.Args[0]));
}
- if (MatchesIntrinsic(call.Func, READ_IMPLIES))
+ if (MatchesIntrinsic(call.Func, NO_READ))
{
- return Expr.Imp(MakeReadHasOccurred(node, call, READ_IMPLIES), node.Args[0]);
+ return Expr.Not(
+ MakeReadHasOccurred(node, call, NO_READ)
+ );
}
- if (MatchesIntrinsic(call.Func, WRITE_IMPLIES))
+ if (MatchesIntrinsic(call.Func, NO_WRITE))
+ {
+ return Expr.Not(
+ MakeWriteHasOccurred(node, call, NO_WRITE)
+ );
+ }
+
+ if (MatchesIntrinsic(call.Func, READ))
+ {
+ return MakeReadHasOccurred(node, call, READ);
+ }
+
+ if (MatchesIntrinsic(call.Func, WRITE))
{
- return Expr.Imp(MakeWriteHasOccurred(node, call, WRITE_IMPLIES), node.Args[0]);
+ return MakeWriteHasOccurred(node, call, WRITE);
}
}
|