diff options
| -rw-r--r-- | Source/Core/LinearSets.cs | 12 | ||||
| -rw-r--r-- | Test/linear/Answer | 1 | ||||
| -rw-r--r-- | Test/linear/runtest.bat | 8 | ||||
| -rw-r--r-- | Test/linear/typecheck.bpl | 9 |
4 files changed, 27 insertions, 3 deletions
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 7230d0a3..f30336e5 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -41,9 +41,15 @@ namespace Microsoft.Boogie errorCount++;
}
private Dictionary<Variable, string> scope;
+ private HashSet<Variable> frame;
public override Implementation VisitImplementation(Implementation node)
{
scope = new Dictionary<Variable, string>();
+ frame = new HashSet<Variable>();
+ foreach (IdentifierExpr ie in node.Proc.Modifies)
+ {
+ frame.Add(ie.Decl);
+ }
for (int i = 0; i < node.OutParams.Length; i++)
{
string domainName = QKeyValue.FindStringAttribute(node.Proc.OutParams[i].Attributes, "linear");
@@ -113,7 +119,7 @@ namespace Microsoft.Boogie if (rhs == null)
{
Error(node, "Only variable can be assigned to a linear variable");
- continue;
+ continue;
}
string rhsDomainName = FindDomainName(rhs.Decl);
if (rhsDomainName == null)
@@ -132,6 +138,10 @@ namespace Microsoft.Boogie continue;
}
rhsVars.Add(rhs.Decl);
+ if (!CommandLineOptions.Clo.DoModSetAnalysis && rhs.Decl is GlobalVariable && !frame.Contains(rhs.Decl))
+ {
+ Error(node, "A linear variable on the right hand side of an assignment must be in the modifies set");
+ }
}
return base.VisitAssignCmd(node);
}
diff --git a/Test/linear/Answer b/Test/linear/Answer index 69caec25..680f9895 100644 --- a/Test/linear/Answer +++ b/Test/linear/Answer @@ -14,6 +14,7 @@ typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be typecheck.bpl(57,4): Error: Only a linear argument can be passed to a linear parameter
typecheck.bpl(61,4): Error: A linear set can occur only once as an in parameter
typecheck.bpl(66,6): Error: Only linear variable can be assigned to another linear variable
+typecheck.bpl(75,4): Error: A linear variable on the right hand side of an assignment must be in the modifies set
0 type checking errors detected in typecheck.bpl
-------------------- list.bpl --------------------
diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat index d054b097..5681784a 100644 --- a/Test/linear/runtest.bat +++ b/Test/linear/runtest.bat @@ -3,7 +3,13 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (typecheck.bpl list.bpl allocator.bpl) do (
+for %%f in (typecheck.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f
+)
+
+for %%f in (list.bpl allocator.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index c188d5b5..ff2d7da4 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -66,4 +66,11 @@ procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, c := a;
}
-procedure F({:linear "D"} a: X) returns ({:linear "D"} c: X);
\ No newline at end of file +procedure F({:linear "D"} a: X) returns ({:linear "D"} c: X);
+
+var{:linear "x"} g:int;
+
+procedure G(i:int) returns({:linear "x"} r:int)
+{
+ r := g;
+}
|