berkus
/
topola
mirror of https://codeberg.org/topola/topola.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

contracts: Tell whether invariant was violation was pre or post

This commit is contained in:
Mikolaj Wielgus 2023-09-19 18:04:08 +02:00
parent f36f80537f
commit 12e37e0e91
1 changed files with 16 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
vendor/contracts/src/implementation/codegen.rs vendored
View File

@ -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(