diff options
Diffstat (limited to 'Source/Core/Absy.cs')
| -rw-r--r-- | Source/Core/Absy.cs | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index d6a2a74d..fc28100e 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2747,13 +2747,15 @@ namespace Microsoft.Boogie { CmdSeq newCommands = new CmdSeq();
if (instrumentEntry) {
Expr inv = (Expr)b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/
- PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
+ var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
+ PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv, kv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv, kv);
newCommands.Add(cmd);
}
newCommands.AddRange(b.Cmds);
if (instrumentExit) {
Expr inv = (Expr)b.Lattice.ToPredicate(b.PostInvariant);
- PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv);
+ var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
+ PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv, kv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv, kv);
newCommands.Add(cmd);
}
b.Cmds = newCommands;
@@ -3539,12 +3541,6 @@ namespace Microsoft.Boogie { d.Emit(stream, 0);
}
}
- public void InstrumentWithInvariants() {
- foreach (Declaration/*!*/ d in this) {
- Contract.Assert(d != null);
- d.InstrumentWithInvariants();
- }
- }
}
#endregion
|