Use AssertKind::fmt_assert_args now that it's pub

See viperproject#467 and rust-lang/rust#84392 for context.
dario23 · May 3, 2021 · b27f307 · b27f307
1 parent 575c319
commit b27f307
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 16 deletions.
diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs
@@ -2158,14 +2158,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                 };
 
                 // Check or assume the assertion
-                let assert_msg = if let AssertKind::BoundsCheck{ .. } = msg {
-                    // Use the debug impl for BoundsCheck, as it is supposed to be handled before
-                    // calling display() according to the docs
-                    // TODO: use fmt_assert_args once https://github.com/rust-lang/rust/pull/84392 is merged
-                    format!("{:?}", msg)
-                } else {
-                    msg.description().to_string()
-                };
+                let mut assert_msg = String::new();
+                msg.fmt_assert_args(&mut assert_msg).unwrap();
 
                 stmts.push(vir::Stmt::comment(format!("Rust assertion: {}", assert_msg)));
                 if self.check_panics {

diff --git a/prusti-viper/src/encoder/pure_function_encoder.rs b/prusti-viper/src/encoder/pure_function_encoder.rs
@@ -948,14 +948,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
                     vir::Expr::not(cond_val)
                 };
 
-                let assert_msg = if let mir::AssertKind::BoundsCheck{ .. } = msg {
-                    // Use the debug impl for BoundsCheck, as it is supposed to be handled before
-                    // calling display() according to the docs
-                    // TODO: use fmt_assert_args once https://github.com/rust-lang/rust/pull/84392 is merged
-                    format!("{:?}", msg)
-                } else {
-                    msg.description().to_string()
-                };
+                let mut assert_msg = String::new();
+                msg.fmt_assert_args(&mut assert_msg).unwrap();
+
                 let pos = self.encoder.error_manager().register(
                     term.source_info.span,
                     ErrorCtxt::PureFunctionAssertTerminator(assert_msg),