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

creusot_contracts_proc/
lib.rs
