creusot_std_proc/
lib.rs

1#![cfg_attr(
2    feature = "creusot",
3    feature(
4        box_patterns,
5        extend_one,
6        hash_set_entry,
7        if_let_guard,
8        proc_macro_def_site,
9        proc_macro_diagnostic,
10        proc_macro_span,
11    )
12)]
13
14use proc_macro::TokenStream as TS1;
15
16mod common;
17
18/// Macro implementations used by `cargo creusot`.
19#[cfg(feature = "creusot")]
20mod creusot;
21
22#[cfg(creusot)]
23use creusot as c;
24
25/// Macro implementations used by `cargo build`.
26#[cfg(not(creusot))]
27mod dummy;
28
29#[cfg(not(creusot))]
30use dummy as c;
31
32/// For rust-analyzer, we set `cfg(feature = "creusot")` to be able to check
33/// `crate::creusot`, but it is not used (`cfg(creusot)` is still false).
34/// This macro avoids warnings by faking dependencies on the functions from `crate::creusot`.
35macro_rules! allow_unused {
36    ($($name:ident)::+) => {
37        #[cfg(all(not(creusot), feature = "creusot"))]
38        #[allow(unused)]
39        use $($name)::+ as _;
40    };
41}
42
43macro_rules! proc_macro_attributes {
44    ($($name:ident)+) => {
45        $(#[proc_macro_attribute]
46        pub fn $name(attr: TS1, tokens: TS1) -> TS1 {
47            allow_unused!(creusot::$name);
48            c::$name(attr, tokens)
49        })+
50    };
51}
52
53proc_macro_attributes! {
54    requires
55    ensures
56    invariant
57    variant
58    check
59    logic
60    trusted
61    opaque
62    builtin
63    intrinsic
64    open_inv_result
65    bitwise_proof
66    maintains
67    erasure
68}
69
70macro_rules! proc_macros {
71    ($($name:ident)+) => {
72        $(#[proc_macro]
73        pub fn $name(tokens: TS1) -> TS1 {
74            allow_unused!(creusot::$name);
75            c::$name(tokens)
76        })+
77    };
78}
79
80proc_macros! {
81    proof_assert
82    snapshot
83    ghost
84    ghost_let
85    pearlite
86    extern_spec
87    declare_namespace
88}
89
90#[proc_macro_derive(DeepModel, attributes(DeepModelTy))]
91pub fn derive_deep_model(tokens: TS1) -> TS1 {
92    allow_unused!(creusot::derive_deep_model);
93    c::derive_deep_model(tokens)
94}
95
96#[cfg(feature = "creusot")]
97#[proc_macro_derive(Clone)]
98pub fn derive_clone(tokens: TS1) -> TS1 {
99    creusot::derive_clone(tokens)
100}
101
102#[cfg(feature = "creusot")]
103#[proc_macro_derive(Default, attributes(default))]
104pub fn derive_default(tokens: TS1) -> TS1 {
105    creusot::derive_default(tokens)
106}
107
108#[cfg(feature = "creusot")]
109#[proc_macro_derive(PartialEq)]
110pub fn derive_partial_eq(tokens: TS1) -> TS1 {
111    creusot::derive_partial_eq(tokens)
112}
creusot_std_proc/lib.rs

creusot_std_proc/
lib.rs
