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

kani/
lib.rs
