summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-05 15:42:12 -0800
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-05 15:42:12 -0800
commit47ac92a139c1cc11ff7f68b726960fcd902e41d2 (patch)
tree2cf5bbb30998c8f3987020196c82d94573f1a870 /Source/Core
parentf82dab21f1240fb3f8d67a880f4f93017d85c345 (diff)
fixed datatype bug reported by Chris
fixed function body referring to globals bug
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/Absy.cs6
1 files changed, 5 insertions, 1 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 967ac4e3..616a0e21 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2009,7 +2009,11 @@ namespace Microsoft.Boogie {
RegisterFormals(OutParams, rc);
ResolveAttributes(rc);
if (Body != null)
- Body.Resolve(rc);
+ {
+ rc.StateMode = ResolutionContext.State.StateLess;
+ Body.Resolve(rc);
+ rc.StateMode = ResolutionContext.State.Single;
+ }
rc.PopVarContext();
Type.CheckBoundVariableOccurrences(TypeParameters,
InParams.ToTypeSeq, OutParams.ToTypeSeq,