diff options
| author |  Unknown <shuvendu@SHUVENDU-Z400.redmond.corp.microsoft.com> | 2012-06-01 01:36:11 -0700 |
|---|---|---|
| committer | Unknown <shuvendu@SHUVENDU-Z400.redmond.corp.microsoft.com> | 2012-06-01 01:36:11 -0700 |
| commit | 7552293514e40a6dcd9749d3668519d7d32049d5 (patch) | |
| tree | 2ae7fec112e8228b808d652e07b6bd19d4722a4a /Source | |
| parent | 622c64cbbba5d3619eaf4de03458111ff6589027 (diff) | |
1. Fix for free ensures in inlined procedures. Becomes a skip instead of an assume.
2. Fix for deterministic loop extraction, and a new regression.
3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Absy.cs | 35 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 3 | ||||
| -rw-r--r-- | Source/Core/Inline.cs | 3 |
3 files changed, 23 insertions, 18 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index d7fcca7a..148a739d 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -590,7 +590,25 @@ namespace Microsoft.Boogie { if (!found) {
Block auxNewBlock = new Block();
auxNewBlock.Label = ((Block)bl).Label;
- auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)block).Cmds);
+ auxNewBlock.Cmds = codeCopier.CopyCmdSeq(((Block)bl).Cmds);
+ //add restoration code for such blocks
+ if (loopHeaderToAssignCmd.ContainsKey(header))
+ {
+ AssignCmd assignCmd = loopHeaderToAssignCmd[header];
+ auxNewBlock.Cmds.Add(assignCmd);
+ }
+ List<AssignLhs> lhsg = new List<AssignLhs>();
+ IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;
+ foreach (IdentifierExpr gl in globalsMods)
+ lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));
+ List<Expr> rhsg = new List<Expr>();
+ foreach (IdentifierExpr gl in globalsMods)
+ rhsg.Add(new OldExpr(Token.NoToken, gl));
+ if (lhsg.Count != 0)
+ {
+ AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg);
+ auxNewBlock.Cmds.Add(globalAssignCmd);
+ }
blockMap[(Block)bl] = auxNewBlock;
}
}
@@ -666,21 +684,6 @@ namespace Microsoft.Boogie { if (newTargets.Length == 0) {
if (!detLoopExtract)
newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
- else {
- if (loopHeaderToAssignCmd.ContainsKey(header)) {
- AssignCmd assignCmd = loopHeaderToAssignCmd[header];
- newBlock.Cmds.Add(assignCmd);
- }
- List<AssignLhs> lhsg = new List<AssignLhs>();
- IdentifierExprSeq/*!*/ globalsMods = loopHeaderToLoopProc[header].Modifies;
- foreach (IdentifierExpr gl in globalsMods)
- lhsg.Add(new SimpleAssignLhs(Token.NoToken, gl));
- List<Expr> rhsg = new List<Expr>();
- foreach (IdentifierExpr gl in globalsMods)
- rhsg.Add(new OldExpr(Token.NoToken, gl));
- AssignCmd globalAssignCmd = new AssignCmd(Token.NoToken, lhsg, rhsg);
- newBlock.Cmds.Add(globalAssignCmd);
- }
newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
} else {
newBlock.TransferCmd = new GotoCmd(Token.NoToken, newLabels, newTargets);
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 5baf8667..c28d8c8a 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1222,7 +1222,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||
ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||
ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
- ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding)
+ ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||
+ ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)
) {
// one of the boolean flags matched
return true;
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 71f7bbb4..88512025 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -402,7 +402,8 @@ namespace Microsoft.Boogie { return new AssertEnsuresCmd(ensCopy);
}
else {
- return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));
+ //return new AssumeCmd(ens.tok, codeCopier.CopyExpr(ens.Condition));
+ return new AssumeCmd(ens.tok, Expr.True);
}
}
|