kani/
lib.rs

1// Copyright Kani Contributors
2// SPDX-License-Identifier: Apache-2.0 OR MIT
3
4// Required so we can use kani_macros attributes.
5#![feature(register_tool)]
6#![register_tool(kanitool)]
7// Used for rustc_diagnostic_item.
8// Note: We could use a kanitool attribute instead.
9#![feature(rustc_attrs)]
10// Used to model simd.
11#![feature(repr_simd)]
12#![feature(generic_const_exprs)]
13#![allow(incomplete_features)]
14// Features used for tests only.
15#![cfg_attr(test, feature(core_intrinsics, portable_simd))]
16// Required for `rustc_diagnostic_item` and `core_intrinsics`
17#![allow(internal_features)]
18// Required for implementing memory predicates.
19#![feature(layout_for_ptr)]
20#![feature(ptr_metadata)]
21#![feature(f16)]
22#![feature(f128)]
23#![feature(convert_float_to_int)]
24#![feature(sized_hierarchy)]
25
26// Allow us to use `kani::` to access crate features.
27extern crate self as kani;
28
29pub mod arbitrary;
30pub mod bounded_arbitrary;
31#[cfg(feature = "concrete_playback")]
32mod concrete_playback;
33pub mod futures;
34pub mod invariant;
35pub mod shadow;
36pub mod vec;
37
38mod models;
39
40#[cfg(feature = "concrete_playback")]
41pub use concrete_playback::concrete_playback_run;
42pub use invariant::Invariant;
43
44#[cfg(not(feature = "concrete_playback"))]
45/// NOP `concrete_playback` for type checking during verification mode.
46pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
47    unreachable!("Concrete playback does not work during verification")
48}
49
50pub use futures::{RoundRobin, block_on, block_on_with_spawn, spawn, yield_now};
51
52// Kani proc macros must be in a separate crate
53pub use kani_macros::*;
54
55// Declare common Kani API such as assume, assert
56kani_core::kani_lib!(kani);
57
58// Used to bind `core::assert` to a different name to avoid possible name conflicts if a
59// crate uses `extern crate std as core`. See
60// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187
61#[doc(hidden)]
62#[cfg(not(feature = "concrete_playback"))]
63pub use core::assert as __kani__workaround_core_assert;
64
65#[macro_export]
66macro_rules! cover {
67    () => {
68        kani::cover(true, "cover location");
69    };
70    ($cond:expr $(,)?) => {
71        kani::cover($cond, concat!("cover condition: ", stringify!($cond)));
72    };
73    ($cond:expr, $msg:literal) => {
74        kani::cover($cond, $msg);
75    };
76}
77
78/// `implies!(premise => conclusion)` means that if the `premise` is true, so
79/// must be the `conclusion`.
80///
81/// This simply expands to `!premise || conclusion` and is intended to make checks more readable,
82/// as the concept of an implication is more natural to think about than its expansion.
83#[macro_export]
84macro_rules! implies {
85    ($premise:expr => $conclusion:expr) => {
86        !($premise) || ($conclusion)
87    };
88}
89
90pub(crate) use kani_macros::unstable_feature as unstable;
91
92pub mod contracts;
kani/lib.rs

kani/
lib.rs
