Macro mirai_annotations::abstract_value

macro_rules! abstract_value {
    ($value : expr) => { ... };
}

Provides a way to specify a value that should be treated abstractly by the verifier. The concrete argument provides type information to the verifier and a meaning for the expression when compiled by the rust compiler.

The expected use case for this is inside test cases. Principally this would be test cases for the verifier itself, but it can also be used to “fuzz” unit tests in user code.