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 iter;
36pub mod shadow;
37pub mod vec;
38
39mod models;
40
41#[cfg(feature = "concrete_playback")]
42pub use concrete_playback::concrete_playback_run;
43pub use invariant::Invariant;
44
45#[cfg(not(feature = "concrete_playback"))]
46/// NOP `concrete_playback` for type checking during verification mode.
47pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
48    unreachable!("Concrete playback does not work during verification")
49}
50
51pub use futures::{RoundRobin, block_on, block_on_with_spawn, spawn, yield_now};
52
53// Kani proc macros must be in a separate crate
54pub use kani_macros::*;
55
56// Declare common Kani API such as assume, assert
57kani_core::kani_lib!(kani);
58
59// Used to bind `core::assert` to a different name to avoid possible name conflicts if a
60// crate uses `extern crate std as core`. See
61// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187
62#[doc(hidden)]
63#[cfg(not(feature = "concrete_playback"))]
64pub use core::assert as __kani__workaround_core_assert;
65
66#[macro_export]
67macro_rules! cover {
68    () => {
69        kani::cover(true, "cover location");
70    };
71    ($cond:expr $(,)?) => {
72        kani::cover($cond, concat!("cover condition: ", stringify!($cond)));
73    };
74    ($cond:expr, $msg:literal) => {
75        kani::cover($cond, $msg);
76    };
77}
78
79/// `implies!(premise => conclusion)` means that if the `premise` is true, so
80/// must be the `conclusion`.
81///
82/// This simply expands to `!premise || conclusion` and is intended to make checks more readable,
83/// as the concept of an implication is more natural to think about than its expansion.
84#[macro_export]
85macro_rules! implies {
86    ($premise:expr => $conclusion:expr) => {
87        !($premise) || ($conclusion)
88    };
89}
90
91pub(crate) use kani_macros::unstable_feature as unstable;
92
93pub mod contracts;
kani/lib.rs

kani/
lib.rs
