flux_rs/
lib.rs

1#![no_std]
2pub mod bitvec;
3
4pub use attrs::*;
5pub use flux_attrs as attrs;
6
7#[sig(fn(bool[true]) )]
8pub fn assert(_: bool) {}
9
10#[sig (fn() -> _ requires false)]
11pub fn unreachable() -> ! {
12    unreachable!("impossible case")
13}
14
15/// Macro for creating detached specifications.
16///
17/// # Example
18/// ```
19/// flux_rs::macros::detached_spec! {
20///     fn inc(n:i32) -> i32[n+1];
21///     fn watermelon(n:usize) -> usize[n+2];
22/// }
23/// ```
24#[macro_export]
25#[doc(hidden)]
26macro_rules! __private_detached_spec {
27    ($($e:tt)*) => {
28        #[flux_rs::specs {
29            $($e)*
30        }]
31        const _: () = ();
32    };
33}
34
35/// Macro for creating `invariant qualifier`s
36/// # Example
37/// ```
38/// invariant!(res: int, i: int, n: int ; res + i == n);
39/// ```
40#[macro_export]
41#[doc(hidden)]
42macro_rules! __private_invariant {
43    ($($param:ident : $ty:ty),* ; $expr:expr) => {
44        #[flux::defs{
45            invariant qualifier Auto($($param: $ty),*) { $expr }
46        }]
47        const _: () = ();
48        flux_rs::assert($expr);
49    };
50}
51
52pub mod macros {
53    /// Macro for creating detached specifications.
54    ///
55    /// # Example
56    /// ```
57    /// flux_rs::macros::detached_spec! {
58    ///     fn inc(n:i32) -> i32[n+1];
59    ///     fn watermelon(n:usize) -> usize[n+2];
60    /// }
61    /// ```
62    pub use crate::__private_detached_spec as detached_spec;
63    /// Macro for creating `invariant qualifier`s
64    /// # Example
65    /// ```
66    /// flux_rs::macros::invariant!(res: int, i: int, n: int ; res + i == n);
67    /// ```
68    pub use crate::__private_invariant as invariant;
69}
flux_rs/lib.rs

flux_rs/
lib.rs
