diff options
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 16 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenter.cs | 2 |
2 files changed, 18 insertions, 0 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 31b7c776..87eac73f 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -1725,6 +1725,22 @@ namespace GPUVerify }
+ internal GlobalVariable FindOrCreateSourceVariable(Variable v, string accessType) {
+ string name = MakeSourceVariableName(v.Name, accessType) + "$1";
+ foreach (Declaration D in Program.TopLevelDeclarations) {
+ if (D is GlobalVariable && ((GlobalVariable)D).Name.Equals(name)) {
+ return D as GlobalVariable;
+ }
+ }
+
+ GlobalVariable result = new VariableDualiser(1, null, null).VisitVariable(
+ MakeSourceVariable(v, accessType)) as GlobalVariable;
+
+ Program.TopLevelDeclarations.Add(result);
+ return result;
+
+ }
+
internal static GlobalVariable MakeAccessHasOccurredVariable(string varName, string accessType)
{
return new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, MakeAccessHasOccurredVariableName(varName, accessType), Microsoft.Boogie.Type.Bool));
diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs index cc13fb00..fbc3356a 100644 --- a/Source/GPUVerify/RaceInstrumenter.cs +++ b/Source/GPUVerify/RaceInstrumenter.cs @@ -389,6 +389,7 @@ namespace GPUVerify { result.Add(checkAccessCallCmd);
string fname = QKeyValue.FindStringAttribute(SourceLocationAttributes, "fname");
+
if (fname != null)
{
writeSourceLocToFile(SourceLocationAttributes, Path.GetFileNameWithoutExtension(CommandLineOptions.inputFiles[0]) + ".loc");
@@ -788,6 +789,7 @@ namespace GPUVerify { Debug.Assert(mt.Arguments.Length == 1);
verifier.FindOrCreateOffsetVariable(v, ReadOrWrite);
+ verifier.FindOrCreateSourceVariable(v, ReadOrWrite);
}
|