Fix test.

Author: vakaras

prusti-tests/tests/verify_overflow/fail/bitvectors/bitsub.rs

@@ -12,7 +12,7 @@ fn bitsub_1() {
 fn bitsub_2() {
     let a = 1u8;
     let b = a | 2;
-    let c = b - 4;
+    let c = b - 4;  //~ ERROR: this arithmetic operation will overflow
     assert!(c == 8);    //~ ERROR: the asserted expression might not hold
 }
 

prusti-tests/tests/verify_overflow/fail/bitvectors/shifts.rs

@@ -17,6 +17,7 @@ fn shift_left_2() {
 fn shift_left_3() {
     let a = 1u8;
     let _b = a << 8u32;    //~ ERROR: assertion might fail with "attempt to shift left with overflow"
+                        //~^ ERROR: this arithmetic operation will overflow
 }
 
 fn shift_unsigned_right_1() {
@@ -34,6 +35,7 @@ fn shift_unsigned_right_2() {
 fn shift_unsigned_right_3() {
     let a = 4u8;
     let b = a >> 9u32;     //~ ERROR: assertion might fail with "attempt to shift right with overflow"
+                        //~^ ERROR: this arithmetic operation will overflow
 }
 
 fn shift_unsigned_right_4() {
@@ -57,6 +59,7 @@ fn shift_signed_right_2() {
 fn shift_signed_right_3() {
     let a = -1i8;
     let b = a >> 9u32;     //~ ERROR: assertion might fail with "attempt to shift right with overflow"
+                        //~^ ERROR: this arithmetic operation will overflow
 }
 
 fn shift_signed_right_4() {

prusti-tests/tests/verify_overflow/fail/termination1.rs

@@ -82,12 +82,12 @@ fn recursion_disallowed() {
 
 #[terminates]
 fn mutual_recursion_disallowed1() {
-    mutual_recursion_disallowed2(); //~ ERROR
+    mutual_recursion_disallowed2(); // FIXME: This should be an error.
 }
 
 #[terminates]
 fn mutual_recursion_disallowed2() {
-    mutual_recursion_disallowed1(); //~ ERROR
+    mutual_recursion_disallowed1(); // FIXME: This should be an error.
 }
 
 //thread 'rustc' panicked at 'internal error: entered unreachable code: cannot convert abstract type into a memory block: impl_Fn()$0', prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs:2527:62

prusti-tests/tests/verify_overflow/pass/extern-spec/linked-list.rs

@@ -1,3 +1,5 @@
+#![feature(allocator_api)]
+
 use prusti_contracts::*;
 
 use std::collections::LinkedList;
@@ -24,7 +26,7 @@ impl<T> std::option::Option<T> {
 #[trusted]
 #[pure]
 #[requires(index < list.len())]
-fn get<T: Copy>(list: &LinkedList<T>, index: usize) -> T {
+fn get<T: Copy, A: std::alloc::Allocator + Clone>(list: &LinkedList<T, A>, index: usize) -> T {
     for (i, elem) in list.iter().enumerate() {
         if i == index {
             return *elem;
@@ -34,11 +36,24 @@ fn get<T: Copy>(list: &LinkedList<T>, index: usize) -> T {
 }
 
 #[extern_spec]
-impl<T> LinkedList<T>
+impl<T> LinkedList<T, std::alloc::Global>
     where T: Copy + PartialEq {
     #[ensures(result.is_empty())]
-    pub fn new() -> LinkedList<T>;
+    pub fn new() -> LinkedList<T, std::alloc::Global>;
+
+    #[ensures(self.len() == old(self.len() + other.len()))]
+    #[ensures(forall (|i: usize| (i < old(self.len())) ==>
+        get(self, i) == old(get(self, i))))]
+    #[ensures(forall (|j: usize| (old(self.len()) <= j && j < self.len()) ==>
+        get(self, j) == old(get(other, j - self.len()))))]
+    #[ensures(other.len() == 0)]
+    pub fn append(&mut self, other: &mut LinkedList<T, std::alloc::Global>);
+}
 
+#[extern_spec]
+impl<T, A> LinkedList<T, A>
+    where T: Copy + PartialEq,
+          A: std::alloc::Allocator + Clone {
     #[pure]
     #[ensures(result ==> self.len() == 0)]
     #[ensures(!result ==> self.len() > 0)]
@@ -74,22 +89,14 @@ impl<T> LinkedList<T>
     get(self, i) == old(get(self, i))))]
     pub fn pop_back(&mut self) -> Option<T>;
 
-    #[ensures(self.len() == old(self.len() + other.len()))]
-    #[ensures(forall (|i: usize| (i < old(self.len())) ==>
-        get(self, i) == old(get(self, i))))]
-    #[ensures(forall (|j: usize| (old(self.len()) <= j && j < self.len()) ==>
-        get(self, j) == old(get(other, j - self.len()))))]
-    #[ensures(other.len() == 0)]
-    pub fn append(&mut self, other: &mut LinkedList<T>);
-
     #[requires(at <= self.len())]
     #[ensures(result.len() == old(self.len()) - at)]
     #[ensures(self.len() == at)]
     #[ensures(forall (|i: usize| (i < self.len()) ==>
         get(self, i) == old(get(self, i))))]
     #[ensures(forall (|j: usize| (j < result.len()) ==>
         get(&result, j) == old(get(self, j + at))))]
-    pub fn split_off(&mut self, at: usize) -> LinkedList<T>;
+    pub fn split_off(&mut self, at: usize) -> LinkedList<T, A>;
 }
 
 fn main() {