diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-04 18:29:39 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-05-04 18:29:39 -0700 |
| commit | b35c3daef15cdaea422bf408c4cff62242a9fb04 (patch) | |
| tree | 46061fb5e806a4a44cec22d23ee8076c5ba3467f | |
| parent | 0b2caab971a9ba7dc0949aa0556d8e092ba368e2 (diff) | |
In the typecheck method of HavocCmd, added calls to typecheck the havoced vars
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index b37ed400..3005aaa6 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2632,10 +2632,13 @@ namespace Microsoft.Boogie { }
public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
+ foreach (IdentifierExpr ie in Vars)
+ {
+ ie.Typecheck(tc);
+ }
this.CheckAssignments(tc);
}
-
public override Absy StdDispatch(StandardVisitor visitor) {
//Contract.Requires(visitor != null);
Contract.Ensures(Contract.Result<Absy>() != null);
|