From 8baf2f4bdba4cb7a4ef3bb52cb6491b815069175 Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Sat, 25 Feb 2023 19:15:20 +0100 Subject: [PATCH] Ugly commit. --- prusti-viper/src/encoder/errors/error_manager.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index c282dd5e08c..ac2f0e873d3 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -737,6 +737,8 @@ impl<'tcx> ErrorManager<'tcx> { ) } + ("exhale.failed:insufficient.permission", ErrorCtxt::CopyPlace) | + ("exhale.failed:insufficient.permission", ErrorCtxt::MovePlace) | ("call.precondition:insufficient.permission", ErrorCtxt::CopyPlace) | ("call.precondition:insufficient.permission", ErrorCtxt::MovePlace) => { PrustiError::verification(