1mod rt_decls {
2 extern "C" {
3 pub fn CVT_assume(_c: bool);
4 pub fn CVT_assert(_c: bool);
5 pub fn CVT_satisfy(_c: bool);
6 pub fn CVT_sanity(_c: bool);
7 }
8}
9
10#[cfg(feature = "rt")]
11mod rt_impls {
12 #[no_mangle]
13 pub extern "C" fn CVT_assume(c: bool) {
14 if !c {
15 panic!()
16 }
17 }
18
19 #[no_mangle]
20 pub extern "C" fn CVT_assert(c: bool) {
21 assert!(c);
22 }
23
24 #[no_mangle]
25 pub extern "C" fn CVT_satisfy(c: bool) {
26 assert!(c);
27 }
28
29 #[no_mangle]
30 pub extern "C" fn CVT_sanity(c: bool) {
31 CVT_satisfy(c)
32 }
33}
34
35use rt_decls::*;
36
37#[inline(always)]
38pub fn cvlr_assert_checked(c: bool) {
39 unsafe {
40 CVT_assert(c);
41 }
42}
43
44#[inline(always)]
45pub fn cvlr_assume_checked(c: bool) {
46 unsafe {
47 CVT_assume(c);
48 }
49}
50
51#[inline(always)]
52pub fn cvlr_satisfy_checked(c: bool) {
53 unsafe {
54 CVT_satisfy(c);
55 }
56}
57
58#[inline(always)]
59pub fn cvlr_sanity_checked(c: bool) {
60 unsafe {
61 CVT_sanity(c);
62 }
63}
64
65#[macro_export]
66macro_rules! cvlr_assert {
67 ($cond: expr $(, $desc: literal)?) => {{
68 let c_ = $cond;
69 $crate::add_loc!();
70 $crate::cvlr_assert_checked(c_);
71 }};
72}
73
74#[macro_export]
75macro_rules! cvlr_assume {
76 ($cond: expr $(, $desc: literal)?) => {
77 $crate::cvlr_assume_checked($cond)
78 };
79}
80
81#[macro_export]
82macro_rules! cvlr_satisfy {
83 ($cond: expr $(, $desc: literal)?) => {{
84 let c_ = $cond;
85 $crate::add_loc!();
86 $crate::cvlr_satisfy_checked(c_);
87 }};
88}
89
90#[cfg(feature = "vacuity")]
91#[macro_export]
92macro_rules! cvlr_vacuity_check {
93 () => {
94 $crate::cvlr_assert!(false)
95 };
96}
97
98#[cfg(not(feature = "vacuity"))]
99#[macro_export]
100macro_rules! cvlr_vacuity_check {
101 () => {
102 $crate::cvlr_sanity_checked(true)
103 };
104}