diff options
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 5 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 25 | ||||
| -rw-r--r-- | Source/Core/ResolutionContext.cs | 58 |
3 files changed, 88 insertions, 0 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 0bf55b17..f7a6d9d6 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1483,6 +1483,10 @@ namespace Microsoft.Boogie { }
public void ResolveWhere(ResolutionContext rc) {
Contract.Requires(rc != null);
+ if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && this.TypedIdent.WhereExpr != null)
+ {
+ rc.Error(tok, "assumption variable may not be declared with a where clause");
+ }
if (this.TypedIdent.WhereExpr != null) {
this.TypedIdent.WhereExpr.Resolve(rc);
}
@@ -2805,6 +2809,7 @@ namespace Microsoft.Boogie { // already resolved
return;
}
+
DeclWithFormals dwf = rc.LookUpProcedure(cce.NonNull(this.Name));
Proc = dwf as Procedure;
if (dwf == null) {
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index c7a813d3..e4451807 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1210,6 +1210,31 @@ namespace Microsoft.Boogie { Lhss[j].DeepAssignedVariable);
}
}
+
+ for (int i = 0; i < Lhss.Count; i++)
+ {
+ var lhs = Lhss[i].AsExpr as IdentifierExpr;
+ if (lhs != null && QKeyValue.FindBoolAttribute(lhs.Decl.Attributes, "assumption"))
+ {
+ var rhs = Rhss[i] as NAryExpr;
+ if (rhs == null
+ || !(rhs.Fun is BinaryOperator)
+ || ((BinaryOperator)(rhs.Fun)).Op != BinaryOperator.Opcode.And
+ || !(rhs.Args[0] is IdentifierExpr)
+ || ((IdentifierExpr)(rhs.Args[0])).Name != lhs.Name)
+ {
+ rc.Error(tok, string.Format("RHS of assignment to assumption variable {0} must match expression \"{0} && <boolean expression>\"", lhs.Name));
+ }
+ else if (rc.HasVariableBeenAssigned(lhs.Decl.Name))
+ {
+ rc.Error(tok, "assumption variable may not be assigned to more than once");
+ }
+ else
+ {
+ rc.MarkVariableAsAssigned(lhs.Decl.Name);
+ }
+ }
+ }
}
public override void Typecheck(TypecheckingContext tc) {
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 403803a3..eb27c82a 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -265,6 +265,48 @@ namespace Microsoft.Boogie { public readonly Hashtable /*string->Variable*//*!*/ VarSymbols = new Hashtable /*string->Variable*/();
public /*maybe null*/ VarContextNode ParentContext;
public readonly bool Opaque;
+ readonly ISet<string> assignedAssumptionVariables = new HashSet<string>();
+
+ public bool HasVariableBeenAssigned(string name)
+ {
+ Contract.Requires(name != null);
+
+ if (assignedAssumptionVariables.Contains(name))
+ {
+ return true;
+ }
+ else if (ParentContext != null)
+ {
+ return ParentContext.HasVariableBeenAssigned(name);
+ }
+ else
+ {
+ return false;
+ }
+ }
+
+ public bool MarkVariableAsAssigned(string name)
+ {
+ Contract.Requires(name != null);
+
+ if (VarSymbols.Contains(name))
+ {
+ if (assignedAssumptionVariables.Contains(name))
+ {
+ return false;
+ }
+ assignedAssumptionVariables.Add(name);
+ return true;
+ }
+ else if (ParentContext != null)
+ {
+ return ParentContext.MarkVariableAsAssigned(name);
+ }
+ else
+ {
+ return false;
+ }
+ }
public VarContextNode(/*maybe null*/ VarContextNode parentContext, bool opaque) {
ParentContext = parentContext;
@@ -349,6 +391,22 @@ namespace Microsoft.Boogie { // not present in the relevant levels
return null;
}
+
+ public bool HasVariableBeenAssigned(string name)
+ {
+ Contract.Requires(name != null);
+
+ return varContext.HasVariableBeenAssigned(name);
+ }
+
+ public void MarkVariableAsAssigned(string name)
+ {
+ Contract.Requires(name != null);
+
+ var success = varContext.MarkVariableAsAssigned(name);
+ Contract.Assume(success);
+ }
+
Hashtable axioms = new Hashtable();
public void AddAxiom(Axiom axiom) {
|