cvlr 0.6.1

Certora Verification Language for Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

#![no_std]

pub mod u128_arith;

pub mod asserts {
    pub use cvlr_asserts::*;
}

pub mod mathint {
    pub use cvlr_mathint::*;
}

pub mod nondet {
    pub use cvlr_nondet::*;
}

pub mod log {
    pub use cvlr_log::*;
}

pub mod macros {
    pub use cvlr_macros::*;
}

pub mod derive {
    pub use cvlr_derive::*;
}

pub mod spec {
    pub use cvlr_spec::*;
}

pub mod fixed {
    pub use cvlr_fixed::*;
}

pub mod decimal {
    pub use cvlr_decimal::*;
}

pub mod prelude {
    pub use super::asserts::*;

    pub use super::log::cvlr_log as clog;
    pub use super::nondet::nondet;
    pub use super::nondet::nondet as cvlr_nondet;

    pub use __macro_support::rule as cvlr_rule;
    pub use cvlr_early_panic::early_panic as cvlr_early_panic;
    pub use cvlr_hook::cvlr_hook_on_entry;
    pub use cvlr_hook::cvlr_hook_on_exit;

    pub use __macro_support::mock_fn;
    pub use __macro_support::rule;
    pub use cvlr_early_panic::early_panic;
    pub use cvlr_hook::cvlr_hook_on_entry as hook_on_entry;
    pub use cvlr_hook::cvlr_hook_on_exit as hook_on_exit;

    pub use super::macros::{
        cvlr_assert_all, cvlr_assert_that, cvlr_assume_all, cvlr_assume_that, cvlr_eval_all,
        cvlr_eval_that,
    };

    pub use super::derive::{CvlrLog, Nondet};

    pub use super::spec::*;
}

pub use prelude::*;

pub use crate::mathint::{is_u128, is_u16, is_u32, is_u64, is_u8};
pub use macros::cvlr_pif as pif;
pub use macros::cvlr_predicate as predicate;