diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-01-04 14:42:40 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-01-04 14:42:40 -0800 |
| commit | ab03eafe1c01840e7baab8fd51b4f00f11076d6a (patch) | |
| tree | 2168ea34e56ee333eba992c035df8e8c24f4c6df /Source/Core/Inline.cs | |
| parent | 381e589bd49684b46a00c1bea3514e0d1e84b3fd (diff) | |
bug fix for interaction between inlining and loops
Diffstat (limited to 'Source/Core/Inline.cs')
| -rw-r--r-- | Source/Core/Inline.cs | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 63103399..1f8caff0 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -454,6 +454,21 @@ namespace Microsoft.Boogie { VariableSeq locVars = cce.NonNull(impl.OriginalLocVars);
+ // havoc locals and out parameters in case procedure is invoked in a loop
+ IdentifierExprSeq havocVars = new IdentifierExprSeq();
+ foreach (Variable v in locVars)
+ {
+ havocVars.Add(codeCopier.Subst(v));
+ }
+ foreach (Variable v in impl.OutParams)
+ {
+ havocVars.Add(codeCopier.Subst(v));
+ }
+ if (havocVars.Length > 0)
+ {
+ inCmds.Add(new HavocCmd(Token.NoToken, havocVars));
+ }
+
// add where clauses of local vars as assume
for (int i = 0; i < locVars.Length; ++i) {
Expr whereExpr = (cce.NonNull(locVars[i])).TypedIdent.WhereExpr;
|