diff options
author | qadeer <unknown> | 2013-12-11 14:01:40 -0800 |
---|---|---|
committer | qadeer <unknown> | 2013-12-11 14:01:40 -0800 |
commit | 42b80a61e83e8d569700340ee9ad8f8aa3a270a8 (patch) | |
tree | c1d45493a0e3c645a7d30060a5c6053ca2141714 /Source | |
parent | 614648876bd81d6683a9d94207bb514a615202fb (diff) |
fixes to type checking code
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Concurrency/TypeCheck.cs | 30 | ||||
-rw-r--r-- | Source/Core/Absy.cs | 8 |
2 files changed, 26 insertions, 12 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 8f8638d6..b3b3b34a 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -19,7 +19,8 @@ namespace Microsoft.Boogie CheckingContext checkingContext;
public int errorCount;
HashSet<Variable> globalVariables;
- bool insideYield;
+ bool globalVarAccessAllowed;
+ bool visitingProcedure;
int phaseNumEnclosingProc;
public Dictionary<Procedure, ActionInfo> procToActionInfo;
public Program program;
@@ -57,25 +58,27 @@ namespace Microsoft.Boogie public MoverTypeChecker(Program program)
{
- globalVariables = new HashSet<Variable>(program.GlobalVariables());
- procToActionInfo = new Dictionary<Procedure, ActionInfo>();
+ this.globalVariables = new HashSet<Variable>(program.GlobalVariables());
+ this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
this.errorCount = 0;
this.checkingContext = new CheckingContext(null);
this.program = program;
+ this.visitingProcedure = false;
+ this.phaseNumEnclosingProc = int.MaxValue;
}
public override Block VisitBlock(Block node)
{
- insideYield = false;
+ globalVarAccessAllowed = false;
return base.VisitBlock(node);
}
public override Cmd VisitHavocCmd(HavocCmd node)
{
- insideYield = false;
+ globalVarAccessAllowed = false;
return base.VisitHavocCmd(node);
}
public override Cmd VisitAssignCmd(AssignCmd node)
{
- insideYield = false;
+ globalVarAccessAllowed = false;
return base.VisitAssignCmd(node);
}
public override Implementation VisitImplementation(Implementation node)
@@ -85,12 +88,15 @@ namespace Microsoft.Boogie }
public override Procedure VisitProcedure(Procedure node)
{
+ visitingProcedure = true;
phaseNumEnclosingProc = FindPhaseNumber(node);
- return base.VisitProcedure(node);
+ Procedure ret = base.VisitProcedure(node);
+ visitingProcedure = false;
+ return ret;
}
public override Cmd VisitCallCmd(CallCmd node)
{
- insideYield = false;
+ globalVarAccessAllowed = false;
if (!node.IsAsync && node.InParallelWith == null) {
int calleePhaseNum = FindPhaseNumber(node.Proc);
@@ -103,16 +109,16 @@ namespace Microsoft.Boogie }
public override YieldCmd VisitYieldCmd(YieldCmd node)
{
- insideYield = true;
+ globalVarAccessAllowed = true;
return base.VisitYieldCmd(node);
}
- public override Variable VisitVariable(Variable node)
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
{
- if (!insideYield && globalVariables.Contains(node))
+ if (!visitingProcedure && !globalVarAccessAllowed && globalVariables.Contains(node.Decl))
{
Error(node, "Cannot access global variable");
}
- return base.VisitVariable(node);
+ return base.VisitIdentifierExpr(node);
}
public override Ensures VisitEnsures(Ensures ensures)
{
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 1776f64e..d1651ff4 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2358,6 +2358,11 @@ namespace Microsoft.Boogie { QKeyValue.FindIntAttribute(this.Attributes, "right", int.MaxValue) != int.MaxValue ||
QKeyValue.FindIntAttribute(this.Attributes, "left", int.MaxValue) != int.MaxValue ||
QKeyValue.FindIntAttribute(this.Attributes, "both", int.MaxValue) != int.MaxValue;
+ if (isAtomicSpecification && !tc.Yields)
+ {
+ tc.Error(this, "atomic specification allowed only in a yielding procedure");
+ return;
+ }
bool oldYields = tc.Yields;
tc.Yields = isAtomicSpecification;
this.Condition.Typecheck(tc);
@@ -2520,10 +2525,13 @@ namespace Microsoft.Boogie { Contract.Assert(e != null);
e.Typecheck(tc);
}
+ bool oldYields = tc.Yields;
+ tc.Yields = QKeyValue.FindBoolAttribute(Attributes, "yields");
foreach (Ensures/*!*/ e in Ensures) {
Contract.Assert(e != null);
e.Typecheck(tc);
}
+ tc.Yields = oldYields;
}
public override Absy StdDispatch(StandardVisitor visitor) {
|