Provide messages via expect, instead of unwrap

Author: parno

verify/rust_verify/tests/recursion.rs

@@ -92,13 +92,13 @@ test_verify_with_pervasive! {
         fn count_down_b_stmt(i:nat) {
             decreases(i);
 
-            if i != 0 { 
+            if i != 0 {
                 count_down_a_stmt(i - 1);
             }
         }
     } => Ok(())
 }
-    
+
 test_verify_with_pervasive! {
     // Expression that fails to decrease
     #[test] expr_decrease_fail_1 code! {
@@ -185,7 +185,6 @@ test_verify_with_pervasive! {
     } => Err(err) => assert_one_fails(err)
 }
 
-
 test_verify_with_pervasive! {
     // Mutually recursive expressions fail to decrease
     #[test] mutual_expr_decrease_fail code! {
@@ -221,15 +220,15 @@ test_verify_with_pervasive! {
         fn count_down_b_stmt(i:nat) {
             decreases(i);
 
-            if i != 0 { 
+            if i != 0 {
                 count_down_a_stmt(i + 1);   // FAILS
             }
         }
     } => Err(err) => assert_two_fails(err)
 }
-    
-    // TODO: Expression that fails to decrease in a function returning unit
-    /*
+
+// TODO: Expression that fails to decrease in a function returning unit
+/*
 test_verify_with_pervasive! {
     #[test] unit_expr_decrease_fail code! {
         #[spec]
@@ -243,4 +242,3 @@ test_verify_with_pervasive! {
     } => Err(err) => assert_one_fails(err)
 }
 */
-

verify/vir/src/recursion.rs

@@ -63,13 +63,15 @@ fn check_decrease_rename(ctxt: &Ctxt, span: &Span, args: &Exps) -> Exp {
 }
 
 fn update_decreases_exp<'a>(ctxt: &'a Ctxt, name: &Ident) -> Result<Ctxt<'a>, VirErr> {
-    let function = ctxt.ctx.func_map.get(name).unwrap();
-    let (new_decreases_expr, _) = function.x.decrease.as_ref().unwrap().clone();
+    let function = ctxt.ctx.func_map.get(name).expect("func_map should hold all functions");
+    let (new_decreases_expr, _) = function
+        .x
+        .decrease
+        .as_ref()
+        .expect("shouldn't call update_decreases_exp on a function without a decreases clause")
+        .clone();
     let new_decreases_exp = crate::ast_to_sst::expr_to_exp(ctxt.ctx, &new_decreases_expr)?;
-    Ok(Ctxt {
-        decreases_exp: new_decreases_exp,
-        ..ctxt.clone()
-    })
+    Ok(Ctxt { decreases_exp: new_decreases_exp, ..ctxt.clone() })
 }
 
 // Check that exp terminates

verify/vir/src/scc.rs

@@ -78,7 +78,7 @@ impl<T: std::cmp::Eq + std::hash::Hash + Clone> Graph<T> {
             Some(v) => *v,
             None => {
                 self.add_node(value.clone());
-                *self.h.get(&value).unwrap()
+                *self.h.get(&value).expect("Just added this node, so get should always succeed")
             }
         }
     }
@@ -159,7 +159,7 @@ impl<T: std::cmp::Eq + std::hash::Hash + Clone> Graph<T> {
     pub fn get_scc_rep(&self, t: &T) -> T {
         assert!(self.has_run);
         assert!(self.mapping.contains_key(&t));
-        let id = self.mapping.get(&t).unwrap();
+        let id = self.mapping.get(&t).expect("key was present in the line above");
         self.nodes[self.sccs[*id].rep()].t.clone()
     }
 }