#[macro_export]
macro_rules! abstract_value {
($value:expr) => {
if cfg!(mirai) {
mirai_annotations::mirai_abstract_value($value)
} else {
$value
}
};
}
pub type TagPropagationSet = u128;
#[derive(Ord, PartialOrd, Eq, PartialEq, Debug, Copy, Clone)]
pub enum TagPropagation {
Add,
AddOverflows,
And,
BitAnd,
BitNot,
BitOr,
BitXor,
Cast,
Div,
Equals,
GreaterOrEqual,
GreaterThan,
IntrinsicBinary,
IntrinsicBitVectorUnary,
IntrinsicFloatingPointUnary,
LessOrEqual,
LessThan,
LogicalNot,
Mul,
MulOverflows,
Ne,
Neg,
Or,
Offset,
Rem,
Shl,
ShlOverflows,
Shr,
ShrOverflows,
Sub,
SubComponent,
SubOverflows,
UninterpretedCall,
}
#[macro_export]
macro_rules! tag_propagation_set {
($($x:expr),*) => {
0 $(| (1 << ($x as u8)))*
};
}
pub const TAG_PROPAGATION_ALL: TagPropagationSet = tag_propagation_set!(
TagPropagation::Add,
TagPropagation::AddOverflows,
TagPropagation::And,
TagPropagation::BitAnd,
TagPropagation::BitNot,
TagPropagation::BitOr,
TagPropagation::BitXor,
TagPropagation::Cast,
TagPropagation::Div,
TagPropagation::Equals,
TagPropagation::GreaterOrEqual,
TagPropagation::GreaterThan,
TagPropagation::IntrinsicBinary,
TagPropagation::IntrinsicBitVectorUnary,
TagPropagation::IntrinsicFloatingPointUnary,
TagPropagation::LessOrEqual,
TagPropagation::LessThan,
TagPropagation::LogicalNot,
TagPropagation::Mul,
TagPropagation::MulOverflows,
TagPropagation::Ne,
TagPropagation::Neg,
TagPropagation::Or,
TagPropagation::Offset,
TagPropagation::Rem,
TagPropagation::Shl,
TagPropagation::ShlOverflows,
TagPropagation::Shr,
TagPropagation::ShrOverflows,
TagPropagation::Sub,
TagPropagation::SubComponent,
TagPropagation::SubOverflows,
TagPropagation::UninterpretedCall
);
#[macro_export]
macro_rules! add_tag {
($value:expr, $tag:ty) => {
if cfg!(mirai) {
mirai_annotations::mirai_add_tag::<_, $tag>($value)
}
};
}
#[macro_export]
macro_rules! has_tag {
($value:expr, $tag:ty) => {
if cfg!(mirai) {
mirai_annotations::mirai_has_tag::<_, $tag>($value)
} else {
true
}
};
}
#[macro_export]
macro_rules! does_not_have_tag {
($value:expr, $tag:ty) => {
if cfg!(mirai) {
mirai_annotations::mirai_does_not_have_tag::<_, $tag>($value)
} else {
true
}
};
}
#[macro_export]
macro_rules! assume {
($condition:expr) => {
if cfg!(mirai) {
mirai_annotations::mirai_assume($condition)
}
};
}
#[macro_export]
macro_rules! assume_preconditions {
() => {
if cfg!(mirai) {
mirai_annotations::mirai_assume_preconditions()
}
};
}
#[macro_export]
macro_rules! checked_assume {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($condition)
} else {
assert!($condition);
}
);
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($condition);
} else {
assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_assume_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left == $right)
} else {
assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left == $right);
} else {
assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_assume_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left != $right)
} else {
assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left != $right);
} else {
assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_assume {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($condition)
} else {
debug_assert!($condition);
}
);
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($condition);
} else {
debug_assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_assume_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left == $right)
} else {
debug_assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left == $right);
} else {
debug_assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_assume_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left != $right)
} else {
debug_assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_assume($left != $right);
} else {
debug_assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! postcondition {
($condition:expr) => {
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($condition, false, "unsatisfied postcondition");
}
};
($condition:expr, $message:literal) => {
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($condition, false, concat!("unsatisfied postcondition: ", $message));
}
};
($condition:expr, $($arg:tt)*) => {
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($condition, false, concat!("unsatisfied postcondition: ", stringify!($($arg)*)));
}
};
}
#[macro_export]
macro_rules! assumed_postcondition {
($condition:expr) => {
#[cfg(mirai)]
{
mirai_annotations::mirai_postcondition($condition, true, "")
}
#[cfg(not(mirai))]
{
debug_assert!($condition);
}
};
}
#[macro_export]
macro_rules! checked_postcondition {
($condition:expr) => (
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($condition, false, "unsatisfied postcondition")
}
#[cfg(not(mirai))] {
assert!($condition);
}
);
($condition:expr, $message:literal) => {
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($condition, false, concat!("unsatisfied postcondition: ", $message))
}
#[cfg(not(mirai))] {
assert!($condition, $message);
}
};
($condition:expr, $($arg:tt)*) => {
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($condition, false, concat!("unsatisfied postcondition: ", stringify!($($arg)*)));
}
#[cfg(not(mirai))] {
assert!($condition, $($arg)*);
}
};
}
#[macro_export]
macro_rules! checked_postcondition_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_postcondition($left == $right, false, concat!("unsatisfied postcondition: ", stringify!($left == $right)))
} else {
assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_postcondition($left == $right, false, concat!("unsatisfied postcondition: ", stringify!($left == $right), ", ", $message))
} else {
assert_eq!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_postcondition($left == $right, false, concat!("unsatisfied postcondition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
} else {
assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_postcondition_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_postcondition($left != $right, false, concat!("unsatisfied postcondition: ", stringify!($left != $right)))
} else {
assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_postcondition($left != $right, false, concat!("unsatisfied postcondition: ", stringify!($left != $right), ", ", $message))
} else {
assert_ne!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_postcondition($left != $right, false, concat!("unsatisfied postcondition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
} else {
assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_postcondition {
($condition:expr) => (
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($condition, false, "unsatisfied postcondition")
}
#[cfg(not(mirai))] {
debug_assert!($condition);
}
);
($condition:expr, $message:literal) => (
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($condition, false, concat!("unsatisfied postcondition: ", $message))
}
#[cfg(not(mirai))] {
debug_assert!($condition, $message);
}
);
($condition:expr, $($arg:tt)*) => (
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($condition, false, concat!("unsatisfied postcondition: ", stringify!($($arg)*)));
}
#[cfg(not(mirai))] {
debug_assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_postcondition_eq {
($left:expr, $right:expr) => (
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($left == $right, false, concat!("unsatisfied postcondition: ", stringify!($left == $right)))
}
#[cfg(not(mirai))] {
debug_assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($left == $right, false, concat!("unsatisfied postcondition: ", stringify!($left == $right), ", ", $message))
}
#[cfg(not(mirai))] {
debug_assert_eq!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($left == $right, false, concat!("unsatisfied postcondition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
}
#[cfg(not(mirai))] {
debug_assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_postcondition_ne {
($left:expr, $right:expr) => (
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($left != $right, false, concat!("unsatisfied postcondition: ", stringify!($left != $right)))
}
#[cfg(not(mirai))] {
debug_assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($left != $right, false, concat!("unsatisfied postcondition: ", stringify!($left != $right), ", ", $message))
}
#[cfg(not(mirai))] {
debug_assert_ne!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
#[cfg(mirai)] {
mirai_annotations::mirai_postcondition($left != $right, false, concat!("unsatisfied postcondition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
}
#[cfg(not(mirai))] {
debug_assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! precondition {
($condition:expr) => {
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($condition, "unsatisfied precondition")
}
};
($condition:expr, $message:literal) => {
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", $message))
}
};
($condition:expr, $($arg:tt)*) => {
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", stringify!($($arg)*)));
}
};
}
#[macro_export]
macro_rules! checked_precondition {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($condition, "unsatisfied precondition")
} else {
assert!($condition);
}
);
($condition:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", $message))
} else {
assert!($condition, $message);
}
);
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", stringify!($($arg)*)));
} else {
assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_precondition_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right)))
} else {
assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", $message))
} else {
assert_eq!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
} else {
assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_precondition_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right)))
} else {
assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", $message))
} else {
assert_ne!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
} else {
assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_precondition {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($condition, "unsatisfied precondition")
} else {
debug_assert!($condition);
}
);
($condition:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", $message))
} else {
debug_assert!($condition, $message);
}
);
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($condition, concat!("unsatisfied precondition: ", stringify!($($arg)*)));
} else {
debug_assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_precondition_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right)))
} else {
debug_assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", $message))
} else {
debug_assert_eq!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left == $right, concat!("unsatisfied precondition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
} else {
debug_assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_precondition_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right)))
} else {
debug_assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", $message))
} else {
debug_assert_ne!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_precondition_start();
mirai_annotations::mirai_precondition($left != $right, concat!("unsatisfied precondition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
} else {
debug_assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! unrecoverable {
($fmt:expr) => (
panic!(concat!("unrecoverable: ", stringify!($fmt)));
);
($fmt:expr, $($arg:tt)+) => (
panic!(concat!("unrecoverable: ", stringify!($fmt)), $($arg)+);
);
}
#[macro_export]
macro_rules! verify {
($condition:expr) => {
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, "false verification condition")
}
};
}
#[macro_export]
macro_rules! checked_verify {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, "false verification condition")
} else {
assert!($condition);
}
);
($condition:expr, $message:literal) => {
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, concat!("false verification condition: ", $message))
} else {
assert!($condition, $message);
}
};
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, concat!("false verification condition: ", stringify!($($arg)*)));
} else {
assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_verify_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right)))
} else {
assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", $message))
} else {
assert_eq!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
} else {
assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! checked_verify_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right)))
} else {
assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", $message))
} else {
assert_ne!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
} else {
assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_verify {
($condition:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, "false verification condition")
} else {
debug_assert!($condition);
}
);
($condition:expr, $message:literal) => {
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, concat!("false verification condition: ", $message))
} else {
debug_assert!($condition, $message);
}
};
($condition:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($condition, concat!("false verification condition: ", stringify!($($arg)*)));
} else {
debug_assert!($condition, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_verify_eq {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right)))
} else {
debug_assert_eq!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", $message))
} else {
debug_assert_eq!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left == $right, concat!("false verification condition: ", stringify!($left == $right), ", ", stringify!($($arg)*)));
} else {
debug_assert_eq!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! debug_checked_verify_ne {
($left:expr, $right:expr) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right)))
} else {
debug_assert_ne!($left, $right);
}
);
($left:expr, $right:expr, $message:literal) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", $message))
} else {
debug_assert_ne!($left, $right, $message);
}
);
($left:expr, $right:expr, $($arg:tt)*) => (
if cfg!(mirai) {
mirai_annotations::mirai_verify($left != $right, concat!("false verification condition: ", stringify!($left != $right), ", ", stringify!($($arg)*)));
} else {
debug_assert_ne!($left, $right, $($arg)*);
}
);
}
#[macro_export]
macro_rules! get_model_field {
($target:expr, $field_name:ident, $default_value:expr) => {
mirai_annotations::mirai_get_model_field($target, stringify!($field_name), $default_value)
};
}
#[macro_export]
macro_rules! result {
() => {
if cfg!(mirai) {
mirai_annotations::mirai_result()
} else {
unimplemented!()
}
};
}
#[macro_export]
macro_rules! set_model_field {
($target:expr, $field_name:ident, $value:expr) => {
if cfg!(mirai) {
mirai_annotations::mirai_set_model_field($target, stringify!($field_name), $value);
}
};
}
#[macro_export]
macro_rules! assume_unreachable {
() => {
if cfg!(mirai) {
unreachable!()
} else {
unreachable!()
}
};
($message:literal) => {
if cfg!(mirai) {
unreachable!()
} else {
unreachable!($message)
}
};
($msg:expr,) => ({
if cfg!(mirai) {
unreachable!()
} else {
unreachable!($msg)
}
});
($fmt:expr, $($arg:tt)*) => {
if cfg!(mirai) {
unreachable!()
} else {
unreachable!($fmt, $($arg)*)
}
};
}
#[macro_export]
macro_rules! verify_unreachable {
() => {
if cfg!(mirai) {
panic!("statement is reachable");
} else {
unreachable!()
}
};
($message:literal) => {
if cfg!(mirai) {
panic!($message);
} else {
unreachable!($message)
}
};
($msg:expr,) => ({
if cfg!(mirai) {
panic!($message)
} else {
unreachable!($msg)
}
});
($fmt:expr, $($arg:tt)*) => {
if cfg!(mirai) {
panic!($fmt, $($arg)*);
} else {
unreachable!($fmt, $($arg)*)
}
};
}
#[doc(hidden)]
pub fn mirai_abstract_value<T>(x: T) -> T {
x
}
#[doc(hidden)]
pub fn mirai_add_tag<V: ?Sized, T>(_v: &V) {}
#[doc(hidden)]
pub fn mirai_has_tag<V: ?Sized, T>(_v: &V) -> bool {
false
}
#[doc(hidden)]
pub fn mirai_does_not_have_tag<V: ?Sized, T>(_v: &V) -> bool {
false
}
#[doc(hidden)]
pub fn mirai_assume(_condition: bool) {}
#[doc(hidden)]
pub fn mirai_assume_preconditions() {}
#[doc(hidden)]
pub fn mirai_postcondition(_condition: bool, _assumed: bool, _message: &str) {}
#[doc(hidden)]
pub fn mirai_precondition_start() {}
#[doc(hidden)]
pub fn mirai_precondition(_condition: bool, _message: &str) {}
#[doc(hidden)]
pub fn mirai_verify(_condition: bool, _message: &str) {}
#[doc(hidden)]
pub fn mirai_get_model_field<T, V>(_target: T, _field_name: &str, default_value: V) -> V {
default_value
}
#[doc(hidden)]
pub fn mirai_result<T>() -> T {
unreachable!()
}
#[doc(hidden)]
pub fn mirai_set_model_field<T, V>(_target: T, _field_name: &str, _value: V) {}