diff options
Diffstat (limited to 'Test/dafny0/snapshots/Inputs')
18 files changed, 330 insertions, 0 deletions
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy new file mode 100644 index 00000000..73db9f9c --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy @@ -0,0 +1,8 @@ +method foo()
+{
+ bar();
+ assert false;
+}
+
+method bar()
+ ensures false;
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy new file mode 100644 index 00000000..db9fc01a --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy @@ -0,0 +1,8 @@ +method foo()
+{
+ bar();
+ assert false; // error
+}
+
+method bar()
+ ensures true;
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy new file mode 100644 index 00000000..34d066c3 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy @@ -0,0 +1,13 @@ +method M()
+{
+ N();
+ assert false;
+}
+
+method N()
+ ensures P();
+
+predicate P()
+{
+ false
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy new file mode 100644 index 00000000..184ac65d --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy @@ -0,0 +1,13 @@ +method M()
+{
+ N();
+ assert false; // error
+}
+
+method N()
+ ensures P();
+
+predicate P()
+{
+ true
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy new file mode 100644 index 00000000..727e177d --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy @@ -0,0 +1,19 @@ +method M()
+{
+ N();
+ assert false;
+}
+
+method N()
+ ensures P();
+
+predicate P()
+ ensures P() == Q();
+
+predicate Q()
+ ensures Q() == R();
+
+predicate R()
+{
+ false
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy new file mode 100644 index 00000000..02a91b52 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy @@ -0,0 +1,19 @@ +method M()
+{
+ N();
+ assert false; // error
+}
+
+method N()
+ ensures P();
+
+predicate P()
+ ensures P() == Q();
+
+predicate Q()
+ ensures Q() == R();
+
+predicate R()
+{
+ true
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy new file mode 100644 index 00000000..72607412 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy @@ -0,0 +1,11 @@ +method M()
+{
+ if (*)
+ {
+
+ }
+ else
+ {
+ assert 0 != 0; // error
+ }
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy new file mode 100644 index 00000000..3b186318 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy @@ -0,0 +1,11 @@ +method M()
+{
+ if (*)
+ {
+ assert true;
+ }
+ else
+ {
+ assert 0 != 0; // error
+ }
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy new file mode 100644 index 00000000..beaadfeb --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy @@ -0,0 +1,11 @@ +method M()
+{
+ if (*)
+ {
+
+ }
+ else
+ {
+ assert 0 == 0;
+ }
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy new file mode 100644 index 00000000..cf9ae753 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy @@ -0,0 +1,12 @@ +method M()
+{
+ if (*)
+ {
+ assert 1 != 1; // error
+ }
+ else
+ {
+ assert 0 == 0;
+ assert 2 != 2; // error
+ }
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy new file mode 100644 index 00000000..b81c1a2b --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy @@ -0,0 +1,26 @@ +method M()
+{
+ N();
+ if (*)
+ {
+
+ }
+ else
+ {
+ assert (forall b: bool :: b || !b) || 0 != 0;
+ }
+ N();
+ assert (forall b: bool :: b || !b) || 3 != 3;
+ if (*)
+ {
+
+ }
+ else
+ {
+ assert (forall b: bool :: b || !b) || 1 != 1;
+ }
+}
+
+
+method N()
+ ensures (forall b: bool :: b || !b) || 2 != 2;
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy new file mode 100644 index 00000000..7b207d74 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy @@ -0,0 +1,27 @@ +method M()
+{
+ N();
+ if (*)
+ {
+
+ }
+ else
+ {
+ assert (forall b: bool :: b || !b) || 0 != 0;
+ }
+ N();
+ assert (forall b: bool :: b || !b) || 3 != 3;
+ if (*)
+ {
+
+ }
+ else
+ {
+ assert (exists b: bool :: true) || 4 != 4;
+ }
+ assert (exists b: bool :: true) || 5 != 5;
+}
+
+
+method N()
+ ensures (forall b: bool :: b || !b) || 2 != 2;
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy new file mode 100644 index 00000000..c3742f4b --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy @@ -0,0 +1,23 @@ +module M0
+{
+ class C
+ {
+ method Foo()
+ {
+ assume false;
+ }
+ }
+}
+
+
+module M1 refines M0
+{
+ class C
+ {
+ method Foo()
+ {
+ ...;
+ assert false;
+ }
+ }
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy new file mode 100644 index 00000000..aeb520cb --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy @@ -0,0 +1,23 @@ +module M0
+{
+ class C
+ {
+ method Foo()
+ {
+ assume true;
+ }
+ }
+}
+
+
+module M1 refines M0
+{
+ class C
+ {
+ method Foo()
+ {
+ ...;
+ assert false;
+ }
+ }
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy new file mode 100644 index 00000000..27c7da5f --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy @@ -0,0 +1,22 @@ +module M0
+{
+ class C
+ {
+ method Foo()
+ requires false;
+ {
+ }
+ }
+}
+
+
+module M1 refines M0
+{
+ class C
+ {
+ method Foo...
+ {
+ assert false;
+ }
+ }
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy new file mode 100644 index 00000000..b45dfe78 --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy @@ -0,0 +1,22 @@ +module M0
+{
+ class C
+ {
+ method Foo()
+ requires true;
+ {
+ }
+ }
+}
+
+
+module M1 refines M0
+{
+ class C
+ {
+ method Foo...
+ {
+ assert false;
+ }
+ }
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy new file mode 100644 index 00000000..97fcfccb --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots8.v0.dfy @@ -0,0 +1,29 @@ +method M(x: int)
+{ assert x < 20 || 10 <= x; // always true
+ assert x < 10; // error
+ Other(x); // error: precondition violation
+}
+
+method Other(y: int)
+ requires 0 <= y
+{
+}
+
+method Posty() returns (z: int)
+ ensures 2 <= z // error: postcondition violation
+{
+ var t := 20;
+ if t < z {
+ } else { // the postcondition violation occurs on this 'else' branch
+ }
+}
+
+method NoChangeWhazzoeva(u: int)
+{
+ assert u != 53; // error
+}
+
+method NoChangeAndCorrect()
+{
+ assert true;
+}
diff --git a/Test/dafny0/snapshots/Inputs/Snapshots8.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots8.v1.dfy new file mode 100644 index 00000000..8d8b215b --- /dev/null +++ b/Test/dafny0/snapshots/Inputs/Snapshots8.v1.dfy @@ -0,0 +1,33 @@ +method M(x: int)
+{
+assert x < 20 || 10 <= x; // always true
+
+ assert x < 10; // error
+ Other(x); // error: precondition violation
+ assert x == 7; // error: this is a new error in v1
+}
+
+
+ method Other(y: int)
+ requires 0 <= y
+ {
+ }
+
+
+
+method Posty() returns (z: int)
+ ensures 2 <= z // error: postcondition violation
+{
+ var t := 20;
+ if t < z {
+ assert true; // this is a new assert
+ } else { // the postcondition violation occurs on this 'else' branch
+ }
+}
+
+ method NoChangeWhazzoeva(u: int)
+ {
+ assert u != 53; // error
+ }
+
+method NoChangeAndCorrect() { assert true; }
|