feat: show different message if invariant was violated before or after

taken from https://gitlab.com/karroffel/contracts/-/merge_requests/8/diffs

Author: robjtede

CHANGELOG.md

@@ -6,6 +6,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 
 ## Unreleased
 
+- Add effective contract type to invariant violation messages.
+
 ## [0.6.3] - 2022-03-13
 
 ### Fixed

src/implementation/codegen.rs

@@ -213,13 +213,14 @@ pub(crate) fn generate(
         .iter()
         .filter(|c| 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 {
+                c.ty.message_name().to_string()
+            };
+
             let desc = if let Some(desc) = c.desc.as_ref() {
-                format!(
-                    "{} of {} violated: {}",
-                    c.ty.message_name(),
-                    func_name,
-                    desc
-                )
+                format!("{} of {} violated: {}", contract_type_name, func_name, desc)
             } else {
                 format!("{} of {} violated", c.ty.message_name(), func_name)
             };
@@ -250,13 +251,14 @@ pub(crate) fn generate(
         .iter()
         .filter(|c| 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 {
+                c.ty.message_name().to_string()
+            };
+
             let desc = if let Some(desc) = c.desc.as_ref() {
-                format!(
-                    "{} of {} violated: {}",
-                    c.ty.message_name(),
-                    func_name,
-                    desc
-                )
+                format!("{} of {} violated: {}", contract_type_name, func_name, desc)
             } else {
                 format!("{} of {} violated", c.ty.message_name(), func_name)
             };