From 12e37e0e91afb2adbe23c5d8955697697f634f12 Mon Sep 17 00:00:00 2001 From: Mikolaj Wielgus Date: Tue, 19 Sep 2023 18:04:08 +0200 Subject: [PATCH] contracts: Tell whether invariant was violation was pre or post --- .../contracts/src/implementation/codegen.rs | 24 ++++++++++++------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/vendor/contracts/src/implementation/codegen.rs b/vendor/contracts/src/implementation/codegen.rs index c3a59f9..fc23feb 100644 --- a/vendor/contracts/src/implementation/codegen.rs +++ b/vendor/contracts/src/implementation/codegen.rs @@ -226,15 +226,19 @@ pub(crate) fn generate( c.ty == ContractType::Requires || c.ty == ContractType::Invariant }) .flat_map(|c| { + let contract_type_name = if c.ty == ContractType::Invariant { + format!("{} (as pre-condition)", c.ty.message_name()) + } else { + format!("{}", c.ty.message_name()) + }; + let desc = if let Some(desc) = c.desc.as_ref() { format!( "{} of {} violated: {}", - c.ty.message_name(), - func_name, - desc + contract_type_name, func_name, desc ) } else { - format!("{} of {} violated", c.ty.message_name(), func_name) + format!("{} of {} violated", contract_type_name, func_name) }; c.assertions.iter().zip(c.streams.iter()).map( @@ -264,15 +268,19 @@ pub(crate) fn generate( c.ty == ContractType::Ensures || c.ty == ContractType::Invariant }) .flat_map(|c| { + let contract_type_name = if c.ty == ContractType::Invariant { + format!("{} (as post-condition)", c.ty.message_name()) + } else { + format!("{}", c.ty.message_name()) + }; + let desc = if let Some(desc) = c.desc.as_ref() { format!( "{} of {} violated: {}", - c.ty.message_name(), - func_name, - desc + contract_type_name, func_name, desc ) } else { - format!("{} of {} violated", c.ty.message_name(), func_name) + format!("{} of {} violated", contract_type_name, func_name) }; c.assertions.iter().zip(c.streams.iter()).map(