diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-10-01 16:04:11 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-10-01 16:04:11 +0100 |
| commit | 591065d4e4388342448351a2a6ae3bdf4fbcd296 (patch) | |
| tree | bbff7f25f19655f3333635a3831d5790dbf1a9bb /Source/VCGeneration/VC.cs | |
| parent | 44095046bd0fd0bc1169ca7a6a19f93b5ac38e9a (diff) | |
support for disabling loop entry invariant assertion checking
Diffstat (limited to 'Source/VCGeneration/VC.cs')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index e02f96d5..f1c01758 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1940,7 +1940,17 @@ namespace VC { {
if (a is AssertCmd) {
Bpl.AssertCmd c = (AssertCmd) a;
- Bpl.AssertCmd b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);
+ Bpl.AssertCmd b = null;
+
+ if (CommandLineOptions.Clo.ConcurrentHoudini) {
+ if (CommandLineOptions.Clo.Cho[taskID].DisableLoopInvEntryAssert)
+ b = new Bpl.LoopInitAssertCmd(c.tok, Expr.True);
+ else
+ b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);
+ } else {
+ b = new Bpl.LoopInitAssertCmd(c.tok, c.Expr);
+ }
+
b.Attributes = c.Attributes;
b.ErrorData = c.ErrorData;
prefixOfPredicateCmdsInit.Add(b);
|