prusti_contracts_proc_macros/
lib.rs1#![cfg_attr(not(feature = "prusti"), no_std)]
2use proc_macro::TokenStream;
3
4#[cfg(not(feature = "prusti"))]
8#[proc_macro_attribute]
9pub fn requires(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
10 tokens
11}
12
13#[cfg(not(feature = "prusti"))]
14#[proc_macro_attribute]
15pub fn invariant(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
16 tokens
17}
18
19#[cfg(not(feature = "prusti"))]
20#[proc_macro_attribute]
21pub fn ensures(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
22 tokens
23}
24
25#[cfg(not(feature = "prusti"))]
26#[proc_macro_attribute]
27pub fn after_expiry(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
28 tokens
29}
30
31#[cfg(not(feature = "prusti"))]
32#[proc_macro_attribute]
33pub fn assert_on_expiry(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
34 tokens
35}
36
37#[cfg(not(feature = "prusti"))]
38#[proc_macro_attribute]
39pub fn pure(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
40 tokens
41}
42
43#[cfg(not(feature = "prusti"))]
44#[proc_macro_attribute]
45pub fn trusted(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
46 tokens
47}
48
49#[cfg(not(feature = "prusti"))]
50#[proc_macro_attribute]
51pub fn verified(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
52 tokens
53}
54
55#[cfg(not(feature = "prusti"))]
56#[proc_macro]
57pub fn body_invariant(_tokens: TokenStream) -> TokenStream {
58 TokenStream::new()
59}
60
61#[cfg(not(feature = "prusti"))]
62#[proc_macro]
63pub fn prusti_assert(_tokens: TokenStream) -> TokenStream {
64 TokenStream::new()
65}
66
67#[cfg(not(feature = "prusti"))]
68#[proc_macro]
69pub fn prusti_assume(_tokens: TokenStream) -> TokenStream {
70 TokenStream::new()
71}
72
73#[cfg(not(feature = "prusti"))]
74#[proc_macro]
75pub fn prusti_refute(_tokens: TokenStream) -> TokenStream {
76 TokenStream::new()
77}
78
79#[cfg(not(feature = "prusti"))]
80#[proc_macro_attribute]
81pub fn refine_trait_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
82 tokens
83}
84
85#[cfg(not(feature = "prusti"))]
86#[proc_macro_attribute]
87pub fn extern_spec(_attr: TokenStream, _tokens: TokenStream) -> TokenStream {
88 TokenStream::new()
89}
90
91#[cfg(not(feature = "prusti"))]
92#[proc_macro]
93pub fn predicate(_tokens: TokenStream) -> TokenStream {
94 TokenStream::new()
95}
96
97#[cfg(not(feature = "prusti"))]
98#[proc_macro_attribute]
99pub fn model(_attr: TokenStream, _tokens: TokenStream) -> TokenStream {
100 TokenStream::new()
101}
102
103#[cfg(not(feature = "prusti"))]
104#[proc_macro_attribute]
105pub fn refine_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
106 tokens
107}
108
109#[cfg(not(feature = "prusti"))]
110#[proc_macro]
111pub fn ghost(_tokens: TokenStream) -> TokenStream {
112 TokenStream::new()
113}
114
115#[cfg(not(feature = "prusti"))]
116#[proc_macro_attribute]
117pub fn print_counterexample(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
118 tokens
119}
120
121#[cfg(not(feature = "prusti"))]
122#[proc_macro_attribute]
123pub fn terminates(_attr: TokenStream, _tokens: TokenStream) -> TokenStream {
124 TokenStream::new()
125}
126
127#[cfg(not(feature = "prusti"))]
128#[proc_macro]
129pub fn body_variant(_tokens: TokenStream) -> TokenStream {
130 TokenStream::new()
131}
132
133#[cfg(feature = "prusti")]
137use prusti_specs::{rewrite_prusti_attributes, SpecAttributeKind};
138
139#[cfg(feature = "prusti")]
140#[proc_macro_attribute]
141pub fn requires(attr: TokenStream, tokens: TokenStream) -> TokenStream {
142 rewrite_prusti_attributes(SpecAttributeKind::Requires, attr.into(), tokens.into()).into()
143}
144
145#[cfg(feature = "prusti")]
146#[proc_macro_attribute]
147pub fn ensures(attr: TokenStream, tokens: TokenStream) -> TokenStream {
148 rewrite_prusti_attributes(SpecAttributeKind::Ensures, attr.into(), tokens.into()).into()
149}
150
151#[cfg(feature = "prusti")]
152#[proc_macro_attribute]
153pub fn after_expiry(attr: TokenStream, tokens: TokenStream) -> TokenStream {
154 rewrite_prusti_attributes(SpecAttributeKind::AfterExpiry, attr.into(), tokens.into()).into()
155}
156
157#[cfg(feature = "prusti")]
158#[proc_macro_attribute]
159pub fn assert_on_expiry(attr: TokenStream, tokens: TokenStream) -> TokenStream {
160 rewrite_prusti_attributes(
161 SpecAttributeKind::AssertOnExpiry,
162 attr.into(),
163 tokens.into(),
164 )
165 .into()
166}
167
168#[cfg(feature = "prusti")]
169#[proc_macro_attribute]
170pub fn pure(attr: TokenStream, tokens: TokenStream) -> TokenStream {
171 rewrite_prusti_attributes(SpecAttributeKind::Pure, attr.into(), tokens.into()).into()
172}
173
174#[cfg(feature = "prusti")]
175#[proc_macro_attribute]
176pub fn trusted(attr: TokenStream, tokens: TokenStream) -> TokenStream {
177 prusti_specs::trusted(attr.into(), tokens.into()).into()
178}
179
180#[cfg(feature = "prusti")]
181#[proc_macro_attribute]
182pub fn verified(attr: TokenStream, tokens: TokenStream) -> TokenStream {
183 rewrite_prusti_attributes(SpecAttributeKind::Verified, attr.into(), tokens.into()).into()
184}
185
186#[cfg(feature = "prusti")]
187#[proc_macro]
188pub fn body_invariant(tokens: TokenStream) -> TokenStream {
189 prusti_specs::body_invariant(tokens.into()).into()
190}
191
192#[cfg(feature = "prusti")]
193#[proc_macro]
194pub fn prusti_assert(tokens: TokenStream) -> TokenStream {
195 prusti_specs::prusti_assertion(tokens.into()).into()
196}
197
198#[cfg(feature = "prusti")]
199#[proc_macro]
200pub fn prusti_assume(tokens: TokenStream) -> TokenStream {
201 prusti_specs::prusti_assume(tokens.into()).into()
202}
203
204#[cfg(feature = "prusti")]
205#[proc_macro]
206pub fn prusti_refute(tokens: TokenStream) -> TokenStream {
207 prusti_specs::prusti_refutation(tokens.into()).into()
208}
209
210#[cfg(feature = "prusti")]
211#[proc_macro]
212pub fn closure(tokens: TokenStream) -> TokenStream {
213 prusti_specs::closure(tokens.into()).into()
214}
215
216#[cfg(feature = "prusti")]
217#[proc_macro_attribute]
218pub fn refine_trait_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
219 prusti_specs::refine_trait_spec(attr.into(), tokens.into()).into()
220}
221
222#[cfg(feature = "prusti")]
223#[proc_macro_attribute]
224pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
225 prusti_specs::extern_spec(attr.into(), tokens.into()).into()
226}
227
228#[cfg(feature = "prusti")]
229#[proc_macro_attribute]
230pub fn invariant(attr: TokenStream, tokens: TokenStream) -> TokenStream {
231 prusti_specs::invariant(attr.into(), tokens.into()).into()
232}
233
234#[cfg(feature = "prusti")]
235#[proc_macro]
236pub fn predicate(tokens: TokenStream) -> TokenStream {
237 prusti_specs::predicate(tokens.into()).into()
238}
239
240#[cfg(feature = "prusti")]
241#[proc_macro_attribute]
242pub fn model(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
243 prusti_specs::type_model(_attr.into(), tokens.into()).into()
244}
245
246#[cfg(feature = "prusti")]
247#[proc_macro_attribute]
248pub fn refine_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
249 rewrite_prusti_attributes(SpecAttributeKind::RefineSpec, attr.into(), tokens.into()).into()
250}
251
252#[cfg(feature = "prusti")]
253#[proc_macro]
254pub fn ghost(tokens: TokenStream) -> TokenStream {
255 prusti_specs::ghost(tokens.into()).into()
256}
257
258#[cfg(feature = "prusti")]
259#[proc_macro_attribute]
260pub fn print_counterexample(attr: TokenStream, tokens: TokenStream) -> TokenStream {
261 prusti_specs::print_counterexample(attr.into(), tokens.into()).into()
262}
263
264#[cfg(feature = "prusti")]
265#[proc_macro_attribute]
266pub fn terminates(attr: TokenStream, tokens: TokenStream) -> TokenStream {
267 rewrite_prusti_attributes(SpecAttributeKind::Terminates, attr.into(), tokens.into()).into()
268}
269
270#[cfg(feature = "prusti")]
271#[proc_macro]
272pub fn body_variant(tokens: TokenStream) -> TokenStream {
273 prusti_specs::body_variant(tokens.into()).into()
274}
275
276