Dafny:

* Added DeclType(f)==C axioms, which for each field f says which class declares it.

Boogie:
* Changed behavior of free loop invariants.  Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures.  The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior.
* NOTE:  I did NOT yet make the corresponding change for loop unrolling, but it is needed.

1 files changed, 7 insertions, 1 deletions

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index 1a25e283..d215de0d 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -112,7 +112,8 @@ namespace Microsoft.Boogie
     public enum SubsumptionOption { Never, NotForQuantifiers, Always }

     public SubsumptionOption UseSubsumption = SubsumptionOption.Always;

 

-    public bool ShowTrace = false;

+    public bool AlwaysAssumeFreeLoopInvariants = false;

+

     public enum ShowEnvironment { Never, DuringPrint, Always }

     public ShowEnvironment ShowEnv = ShowEnvironment.DuringPrint;

     public bool DontShowLogo = false;

@@ -1106,6 +1107,7 @@ namespace Microsoft.Boogie
               ps.CheckBooleanFlag("noRemoveEmptyBlocks", ref RemoveEmptyBlocks, false) ||

               ps.CheckBooleanFlag("traceverify", ref TraceVerify) ||

               ps.CheckBooleanFlag("noConsistencyChecks", ref NoConsistencyChecks, true) ||

+              ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) ||

               ps.CheckBooleanFlag("nologo", ref DontShowLogo) ||

               ps.CheckBooleanFlag("noVerifyByDefault", ref NoVerifyByDefault) ||

               ps.CheckBooleanFlag("useUncheckedContracts", ref UseUncheckedContracts) ||

@@ -1799,6 +1801,10 @@ namespace Microsoft.Boogie
   /traceverify   : print debug output during verification condition generation

   /subsumption:<c> : apply subsumption to asserted conditions:

                     0 - never, 1 - not for quantifiers, 2 (default) - always

+  /alwaysAssumeFreeLoopInvariants : usually, a free loop invariant (or assume

+                   statement in that position) is ignored in checking contexts

+                   (like other free things); this option includes these free

+                   loop invariants as assumes in both contexts

   /bv:<bv>       : bitvector handling

                    n = none

                    z = native Z3 bitvectors (default)