diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-03-07 13:13:22 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-03-07 13:13:22 -0800 |
| commit | 49e3076cd0fa9a11f8df94f1e40e28045125b8de (patch) | |
| tree | 7db1b21f68d09cae8d9ffe54a1309786344a5a01 /Source/Dafny/RefinementTransformer.cs | |
| parent | 4bd03ca62ba3a97ec0d8dca33ce1993b577b153e (diff) | |
Dafny: added ghost modules (the meaning is simply that such a module will not be compiled)
Dafny: improved :autocontracts heuristic for detecting "simple query method"
Dafny: fixed some bugs
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index c37ba18f..36ae8f22 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -494,7 +494,11 @@ namespace Microsoft.Dafny { void AddStmtLabels(Statement s, LabelNode node) {
if (node != null) {
AddStmtLabels(s, node.Next);
- s.Labels = new LabelNode(Tok(node.Tok), node.Label, s.Labels);
+ if (node.Label == null) {
+ // this indicates an implicit-target break statement that has been resolved; don't add it
+ } else {
+ s.Labels = new LabelNode(Tok(node.Tok), node.Label, s.Labels);
+ }
}
}
|