Update Viper toolchain and broken tests.

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

@@ -10,7 +10,7 @@ pub mod m {
         let mut i: usize = 0;
         while i < 14 {
             body_invariant!(i < 14);
-            let t1 = a[i + 1] + (a[i] >> 2);
+            let t1 = a[i + 1] + (a[i] >> 2u32);
             a[i + 1] = t1;
             let t2 = a[i] & 0x3f;
             a[i] = t2;
@@ -22,7 +22,7 @@ pub mod m {
         let mut i: usize = 0;
         while i < 14 {
             body_invariant!(i < 14);
-            let t1 = a[i + 1] + (a[i] >> 2);
+            let t1 = a[i + 1] + (a[i] >> 2u32);
             a[i + 1] = t1;
             let t2 = a[i] & 0x3f;
             a[i] = t2;
@@ -37,7 +37,7 @@ pub mod m {
         let mut i: usize = 0;
         while i < 14 {
             body_invariant!(i < 14);
-            let t1 = a[i + 1] + (a[i] >> 2);
+            let t1 = a[i + 1] + (a[i] >> 2u32);
             a[i + 1] = t1;
             let t2 = a[i] & 0x3f;
             a[i] = t2;
@@ -49,7 +49,7 @@ pub mod m {
         let mut i: usize = 0;
         while i < 14 {
             body_invariant!(i < 14);
-            let t1 = a[i + 1] + (a[i] >> 2);
+            let t1 = a[i + 1] + (a[i] >> 2u32);
             a[i + 1] = t1;
             let t2 = a[i] & 0x3f;
             a[i] = t2;

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

@@ -4,64 +4,64 @@ use prusti_contracts::*;
 
 fn shift_left_1() {
     let a = 1u8;
-    let b = a << 2;
+    let b = a << 2u32;
     assert!(b == 4);
 }
 
 fn shift_left_2() {
     let a = 1u8;
-    let b = a << 2;
+    let b = a << 2u32;
     assert!(b == 8);    //~ ERROR: the asserted expression might not hold
 }
 
 fn shift_left_3() {
     let a = 1u8;
-    let _b = a << 8;    //~ ERROR: assertion might fail with "attempt to shift left with overflow"
+    let _b = a << 8u32;    //~ ERROR: assertion might fail with "attempt to shift left with overflow"
 }
 
 fn shift_unsigned_right_1() {
     let a = 4u8;
-    let b = a >> 2;
+    let b = a >> 2u32;
     assert!(b == 1);
 }
 
 fn shift_unsigned_right_2() {
     let a = 4u8;
-    let b = a >> 2;
+    let b = a >> 2u32;
     assert!(b == 2);    //~ ERROR: the asserted expression might not hold
 }
 
 fn shift_unsigned_right_3() {
     let a = 4u8;
-    let b = a >> 9;     //~ ERROR: assertion might fail with "attempt to shift right with overflow"
+    let b = a >> 9u32;     //~ ERROR: assertion might fail with "attempt to shift right with overflow"
 }
 
 fn shift_unsigned_right_4() {
     let a = 255u8;
-    let b = a >> 2;
+    let b = a >> 2u32;
     assert!(b == 63);
 }
 
 fn shift_signed_right_1() {
     let a = -1i8;
-    let b = a >> 2;
+    let b = a >> 2u32;
     assert!(b == -1);
 }
 
 fn shift_signed_right_2() {
     let a = -1i8;
-    let b = a >> 2;
+    let b = a >> 2u32;
     assert!(b == -2);   //~ ERROR: the asserted expression might not hold
 }
 
 fn shift_signed_right_3() {
     let a = -1i8;
-    let b = a >> 9;     //~ ERROR: assertion might fail with "attempt to shift right with overflow"
+    let b = a >> 9u32;     //~ ERROR: assertion might fail with "attempt to shift right with overflow"
 }
 
 fn shift_signed_right_4() {
     let a = 4i8;
-    let b = a >> 2;
+    let b = a >> 2u32;
     assert!(b == 1);
 }
 

viper-sys/build.rs

@@ -196,6 +196,9 @@ fn main() {
             java_class!("viper.silver.ast.AndOp$", vec![
                 object_getter!(),
             ]),
+            java_class!("viper.silver.ast.AnnotationInfo", vec![
+                constructor!(),
+            ]),
             java_class!("viper.silver.ast.AnySetContains", vec![
                 constructor!(),
             ]),

viper-toolchain

@@ -1 +1 @@
-v-2023-03-29-1448
+v-2023-05-17-0733

viper/src/ast_factory/program.rs

@@ -74,6 +74,42 @@ impl<'a> AstFactory<'a> {
         )
     }
 
+    pub fn annotations(&self, annotations: &BTreeMap<String, Vec<String>>) -> JObject {
+        let mut map = Vec::new();
+        for (key, values) in annotations {
+            let mut sequence = Vec::new();
+            for value in values {
+                sequence.push(self.jni.new_string(value));
+            }
+            map.push((self.jni.new_string(key), self.jni.new_seq(&sequence)));
+        }
+        self.jni.new_map(&map)
+    }
+
+    pub fn predicate_with_annotations(
+        &self,
+        name: &str,
+        formal_args: &[LocalVarDecl],
+        body: Option<Expr>,
+        annotations: &BTreeMap<String, Vec<String>>,
+    ) -> Predicate<'a> {
+        let info = self
+            .jni
+            .unwrap_result(ast::AnnotationInfo::with(self.env).new(self.annotations(annotations)));
+        let obj = self.jni.unwrap_result(ast::Predicate::with(self.env).new(
+            self.jni.new_string(name),
+            self.jni.new_seq(&map_to_jobjects!(formal_args)),
+            match body {
+                None => self.jni.new_option(None),
+                Some(x) => self.jni.new_option(Some(x.to_jobject())),
+            },
+            self.no_position().to_jobject(),
+            info,
+            self.no_trafos(),
+        ));
+        Predicate::new(obj)
+    }
+
     #[allow(clippy::too_many_arguments)]
     pub fn function(
         &self,