Dafny: removed div/mod axioms, since Boogie now interprets div/mod

Dafny: included FloydCycleDetect again (which had been temporarily commented out)
DafnyExtension: adjusted to Boogie's change in abstract-interpretation support

3 files changed, 0 insertions, 27 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 53e8e86a..5530f8a7 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -610,18 +610,3 @@ type TickType;
 var $Tick: TickType;

 

 // ---------------------------------------------------------------

-// -- Arithmetic -------------------------------------------------

-// ---------------------------------------------------------------

-

-// the connection between mod and div

-axiom (forall x:int, y:int :: {x mod y} {x div y}  x mod y == x - x div y * y);

-

-// remainder is always Euclidean Modulus.

-axiom (forall x:int, y:int :: {x mod y}  0 < y  ==>  0 <= x mod y  &&  x mod y < y);

-axiom (forall x:int, y:int :: {x mod y}  y < 0  ==>  0 <= x mod y  &&  x mod y < -y);

-

-// the following axiom has some unfortunate matching, but it does state a property about mod that

-// is sometimes useful

-axiom (forall a: int, b: int, d: int :: { a mod d, b mod d } 2 <= d && a mod d == b mod d && a < b  ==>  a + d <= b);

-

-// ---------------------------------------------------------------

diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
index 3f68ee5d..774008b8 100644
--- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
@@ -205,7 +205,6 @@ class Node {
       invariant forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S);

       decreases S - Visited;

     {

-assume 2<2;  // TEMPORARY HACK

       p, steps, Visited := p.next, steps + 1, Visited + {p};

     }

     if (p == null) {

@@ -219,7 +218,6 @@ assume 2<2;  // TEMPORARY HACK
         invariant forall k :: 0 <= k < A ==> Nexxxt(k, S) != p;

         decreases steps - A;

       {

-assume 2<2;  // TEMPORARY HACK

         A := A + 1;

       }

       B := steps - A;

@@ -228,13 +226,6 @@ assume 2<2;  // TEMPORARY HACK
     }

   }

 

-/**  TEMPORARY

-  ghost method AnalyzeList_Aux(S: set<Node>, steps: int, p: Node) returns (A: int)

-    ensures 0 <= A < steps;

-    ensures forall k :: 0 <= k < A ==> Nexxxt(k, S) != p;

-    ensures Nexxxt(A, S) == p;

-**/

-

   ghost method CrucialLemma(a: int, b: int, S: set<Node>)

     requires IsClosed(S);

     requires 0 <= a && 1 <= b;

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
index 9f22b887..c691d9da 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs
@@ -231,9 +231,6 @@ namespace DafnyLanguage
       if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) {

         if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) {

           Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);

-        } else if (Bpl.CommandLineOptions.Clo.Ai.AnySet) {

-          // run one of the old domains

-          Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

         } else {

           // use /infer:j as the default

           Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true;