Reenable some passing tests from tests_old

prusti-tests/tests_old/verify/fail/pure-fn/wrong-quantifiers.rs → prusti-tests/tests/verify/fail/pure-fn/wrong-quantifiers.rs

@@ -12,7 +12,7 @@ struct List {
 }
 
 #[pure]
-fn lookup(head: &List, index: isize) -> u32 {
+fn lookup(head: &List, index: usize) -> u32 {
     if index == 0 {
         head.value
     } else {
@@ -24,7 +24,7 @@ fn lookup(head: &List, index: isize) -> u32 {
 }
 
 #[pure]
-fn len(head: &List) -> isize {
+fn len(head: &List) -> usize {
     match head.next {
         None => 1,
         Some(box ref tail) => 1 + len(tail)

prusti-tests/tests_old/verify/pass/equality/pure-chain-1.rs → prusti-tests/tests/verify/pass/equality/pure-chain-1.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -19,6 +17,4 @@ fn first(_x: A, _y: A) -> A {
     _x
 }
 
-fn main() {
-}
-
+fn main() {}

prusti-tests/tests_old/verify/pass/equality/pure-chain-2.rs → prusti-tests/tests/verify/pass/equality/pure-chain-2.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -19,6 +17,4 @@ fn first(_x: A, _y: A) -> A {
     _x
 }
 
-fn main() {
-}
-
+fn main() {}

prusti-tests/tests_old/verify/pass/equality/pure-chain-3.rs → prusti-tests/tests/verify/pass/equality/pure-chain-3.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -19,6 +17,4 @@ fn first(_x: A, _y: A) -> A {
     _x
 }
 
-fn main() {
-}
-
+fn main() {}

prusti-tests/tests_old/verify/pass/equality/pure-chain-4.rs → prusti-tests/tests/verify/pass/equality/pure-chain-4.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -19,6 +17,4 @@ fn first(_x: A, _y: A) -> A {
     _x
 }
 
-fn main() {
-}
-
+fn main() {}

prusti-tests/tests_old/verify/pass/equality/pure-chain-5.rs → prusti-tests/tests/verify/pass/equality/pure-chain-5.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -19,7 +17,4 @@ fn foo(x: A) -> A {
     x
 }
 
-
-fn main() {
-}
-
+fn main() {}

prusti-tests/tests_old/verify/pass/equality/pure-chain-6.rs → prusti-tests/tests/verify/pass/equality/pure-chain-6.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -19,6 +17,4 @@ fn first(_x: A, _y: A) -> A {
     _x
 }
 
-fn main() {
-}
-
+fn main() {}

prusti-tests/tests_old/verify/pass/equality/pure-chain-7.rs → prusti-tests/tests/verify/pass/equality/pure-chain-7.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -18,6 +16,4 @@ fn first(_x: A, _y: A) -> A {
     _x
 }
 
-fn main() {
-}
-
+fn main() {}

prusti-tests/tests_old/verify/pass/equality/pure-impure-1.rs → prusti-tests/tests/verify/pass/equality/pure-impure-1.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -18,6 +16,4 @@ fn first(_x: A, _y: A) -> A {
     _x
 }
 
-fn main() {
-}
-
+fn main() {}

prusti-tests/tests_old/verify/pass/equality/pure-impure-2.rs → prusti-tests/tests/verify/pass/equality/pure-impure-2.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -18,6 +16,4 @@ fn first(_x: A, _y: A) -> A {
     _x
 }
 
-fn main() {
-}
-
+fn main() {}

prusti-tests/tests_old/verify/pass/erdinm/traits-basic-norm-prov-defi-pre.rs → prusti-tests/tests/verify/pass/erdinm/traits-basic-norm-prov-defi-pre.rs

@@ -1,4 +1,4 @@
-extern crate prusti_contracts;
+use prusti_contracts::*;
 
 trait Percentage {
     #[requires(arg <= 100)]

prusti-tests/tests/verify/pass/extern-spec/traits-3.rs

@@ -1,10 +1,7 @@
 extern crate prusti_contracts;
 use prusti_contracts::*;
 
-// ignore-test This fails when encoding the postcondition of the trait method.
-
 pub trait Trait {
-    #[ensures(result == 3)]
     fn foo(&mut self) -> i32 { 3 }
 }
 

prusti-tests/tests/verify/pass/extern-spec/traits-5.rs

@@ -14,4 +14,4 @@ impl PrustiStructstdcloneClone12e4123 {
     }
 }
 
-fn main() {}
+fn main() {}

prusti-tests/tests_old/verify/pass/no-annotations/timeout.rs → prusti-tests/tests/verify/pass/no-annotations/timeout.rs

@@ -1,3 +1,5 @@
+use prusti_contracts::*;
+
 #[derive(Eq, PartialEq)]
 pub struct T {
     val: u32,

prusti-tests/tests_old/verify/pass/pure-fn/Dijkstras_algorithm-simpl.rs → prusti-tests/tests/verify/pass/pure-fn/Dijkstras_algorithm-simpl.rs

@@ -7,8 +7,7 @@ use std::cmp::Ordering;
 use std::collections::BinaryHeap;
 use std::usize;
 
-
-struct VecWrapperNode{}
+struct VecWrapperNode {}
 
 impl VecWrapperNode {
     #[pure]
@@ -23,7 +22,7 @@ struct Grid {
 }
 
 impl Grid {
-    fn find_path(&mut self){
+    fn find_path(&mut self) {
         while true {
             body_invariant!(self.nodes.len() >= 0);
         }

prusti-tests/tests_old/verify/ui/collect.stdout → prusti-tests/tests/verify/ui/collect.stdout

@@ -10,10 +10,11 @@
 #![feature(register_tool)]
 #![register_tool(prusti)]
 #[prelude_import]
-use std::prelude::v1::*;
+use std::prelude::rust_2018::*;
 #[macro_use]
 extern crate std;
 use prusti_contracts::*;
+#[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 #[prusti::assertion =
@@ -26,6 +27,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() {
 }
 #[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
 fn test1() { }
+#[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 #[prusti::assertion =
@@ -41,25 +43,32 @@ fn test2() { }
 fn test3() {
     let mut curr = 0;
     while curr < 2 {
+
+        #[allow(unused_must_use, unused_variables)]
         if false {
 
-            #[prusti::spec_only]
-            #[prusti::loop_body_invariant_spec]
-            #[prusti::spec_id = "$(NUM_UUID)"]
-            #[prusti::assertion =
-              "{/"kind/":{/"Expr/":{/"spec_id/":/"$(UUID)/",/"expr_id/":101}}}"]
-            ||
-                {
-
-                    #[prusti::spec_only]
-                    #[prusti::expr_id =
-                      "$(NUM_UUID)_101"]
-                    || -> bool { true };
-                };
+            #[allow(unused_must_use, unused_variables)]
+            {
+
+                #[prusti::spec_only]
+                #[prusti::loop_body_invariant_spec]
+                #[prusti::spec_id = "$(NUM_UUID)"]
+                #[prusti::assertion =
+                  "{/"kind/":{/"Expr/":{/"spec_id/":/"$(UUID)/",/"expr_id/":101}}}"]
+                ||
+                    {
+
+                        #[prusti::spec_only]
+                        #[prusti::expr_id =
+                          "$(NUM_UUID)_101"]
+                        || -> bool { true };
+                    };
+            }
         };
         curr += 1;
     }
 }
+#[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 #[prusti::assertion =
@@ -70,6 +79,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() {
     #[prusti::expr_id = "$(NUM_UUID)_101"]
     || -> bool { true };
 }
+#[allow(unused_must_use, unused_variables, dead_code)]
 #[prusti::spec_only]
 #[prusti::spec_id = "$(NUM_UUID)"]
 #[prusti::assertion =
@@ -85,28 +95,35 @@ fn prusti_post_item_test4_$(NUM_UUID)(result: ()) {
 fn test4() {
     let mut curr = 0;
     while curr < 2 {
+
+        #[allow(unused_must_use, unused_variables)]
         if false {
 
-            #[prusti::spec_only]
-            #[prusti::loop_body_invariant_spec]
-            #[prusti::spec_id = "$(NUM_UUID)"]
-            #[prusti::assertion =
-              "{/"kind/":{/"Expr/":{/"spec_id/":/"$(UUID)/",/"expr_id/":101}}}"]
-                {
-
-                    #[prusti::spec_only]
-                    #[prusti::expr_id =
-                      "$(NUM_UUID)_101"]
-                    || -> bool { true };
-                };
+            #[allow(unused_must_use, unused_variables)]
+            {
+
+                #[prusti::spec_only]
+                #[prusti::loop_body_invariant_spec]
+                #[prusti::spec_id = "$(NUM_UUID)"]
+                #[prusti::assertion =
+                  "{/"kind/":{/"Expr/":{/"spec_id/":/"$(UUID)/",/"expr_id/":101}}}"]
+                ||
+                    {
+
+                        #[prusti::spec_only]
+                        #[prusti::expr_id =
+                          "$(NUM_UUID)_101"]
+                        || -> bool { true };
+                    };
+            }
         };
         curr += 1;
     }
 }
 fn main() { }
 Collected verification items 5:
-procedure: collect::test3[0] at $DIR/collect.rs:13:1: 13:11 (#0)
-procedure: collect::main[0] at $DIR/collect.rs:31:1: 31:10 (#0)
-procedure: collect::test1[0] at $DIR/collect.rs:8:1: 8:11 (#0)
-procedure: collect::test2[0] at $DIR/collect.rs:11:1: 11:11 (#0)
-procedure: collect::test4[0] at $DIR/collect.rs:23:1: 23:11 (#0)
+procedure: collect::test3 at $DIR/collect.rs:13:1: 13:11 (#0)
+procedure: collect::main at $DIR/collect.rs:31:1: 31:10 (#0)
+procedure: collect::test1 at $DIR/collect.rs:8:1: 8:11 (#0)
+procedure: collect::test2 at $DIR/collect.rs:11:1: 11:11 (#0)
+procedure: collect::test4 at $DIR/collect.rs:23:1: 23:11 (#0)

prusti-tests/tests_old/verify/ui/failures.stderr → prusti-tests/tests/verify/ui/failures.stderr

@@ -16,16 +16,16 @@ note: the error originates here
    | |_^
 
 error: [Prusti: verification error] loop invariant might not hold in the first loop iteration.
-  --> $DIR/failures.rs:22:17
+  --> $DIR/failures.rs:23:25
    |
-22 |     #[invariant(false)]
-   |                 ^^^^^
+23 |         body_invariant!(false);
+   |                         ^^^^^
    |
 note: the error originates here
-  --> $DIR/failures.rs:22:17
+  --> $DIR/failures.rs:23:25
    |
-22 |     #[invariant(false)]
-   |                 ^^^^^
+23 |         body_invariant!(false);
+   |                         ^^^^^
 
 error: [Prusti: verification error] precondition might not hold.
   --> $DIR/failures.rs:29:5

prusti-tests/tests_old/verify/fail/marker-traits/basic.rs

@@ -1,12 +1,12 @@
 use prusti_contracts::*;
 
 #[invariant(self.d1 > 5)] //~ ERROR mismatched types
-trait Foo { }
+trait Foo {}
 
 struct Dummy {
     d1: bool
 }
 
 impl Foo for Dummy {}
 
-fn main() { }
+fn main() {}

prusti-tests/tests_old/verify/pass/equality/pure-first-arg.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -13,11 +11,8 @@ fn get_value(_x: A, _y: A) -> A {
 }
 
 fn main() {
-
     let _a = A { i: 17 };
     let _b = A { i: 19 };
     let _x = get_value(_a, _b);
-
     assert!(_x == _a);
 }
-

prusti-tests/tests_old/verify/pass/equality/pure-identity-main.rs

@@ -1,5 +1,3 @@
-
-
 use prusti_contracts::*;
 
 #[derive(Clone,Copy,PartialEq,Eq)]
@@ -18,4 +16,3 @@ fn main() {
     let _z = get_value(_x);
     assert!(_y == _z);
 }
-