Skip to content

Commit cd3b29b

Browse files
committed
make it work
1 parent 135c66a commit cd3b29b

6 files changed

Lines changed: 14 additions & 12 deletions

File tree

crates/anodized-core/src/instrument/impls.rs

Lines changed: 9 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,9 @@
22
#[path = "impls_tests.rs"]
33
mod impls_tests;
44

5-
use syn::{Attribute, ImplItem, ImplItemFn, ReturnType, Visibility, parse_quote};
5+
use syn::{
6+
Attribute, Error, ImplItem, ImplItemFn, ItemImpl, Result, ReturnType, Visibility, parse_quote,
7+
};
68

79
use crate::{
810
DataSpec, Spec,
@@ -11,11 +13,7 @@ use crate::{
1113

1214
impl Mode {
1315
/// Expand impl items.
14-
pub fn instrument_impl(
15-
&self,
16-
spec: DataSpec,
17-
mut the_impl: syn::ItemImpl,
18-
) -> syn::Result<syn::ItemImpl> {
16+
pub fn instrument_impl(&self, spec: DataSpec, mut the_impl: ItemImpl) -> Result<ItemImpl> {
1917
if the_impl.trait_.is_some() {
2018
return Err(make_item_error(&the_impl, "trait impl"));
2119
};
@@ -33,7 +31,7 @@ impl Mode {
3331
item_fn.attrs = func_attrs;
3432

3533
if item_fn.sig.ident.to_string().starts_with("__anodized_") {
36-
return Err(syn::Error::new_spanned(
34+
return Err(Error::new_spanned(
3735
item_fn.sig.ident,
3836
r#"An item with the `__anodized_` prefix is internal. Do not implement it directly.
3937
Instead, ensure that both the impl block and the fn have a `#[spec]` annotation."#,
@@ -102,7 +100,7 @@ Instead, ensure that both the impl block and the fn have a `#[spec]` annotation.
102100
// Build a wrapper that forwards to the "split" function.
103101
let mut wrapper_fn = item_fn.clone();
104102
let mangled_ident =
105-
Self::build_split_fn(false, &mut wrapper_fn.sig, &mut wrapper_fn.block);
103+
Self::build_split_fn(true, &mut wrapper_fn.sig, &mut wrapper_fn.block);
106104
new_items.push(ImplItem::Fn(wrapper_fn));
107105

108106
// "Split" the original function by mangling its return type.
@@ -122,23 +120,23 @@ Instead, ensure that both the impl block and the fn have a `#[spec]` annotation.
122120
ImplItem::Const(mut const_item) => {
123121
let (spec, attrs) = find_spec_attr(const_item.attrs)?;
124122
if let Some(ref spec_attr) = spec {
125-
return Err(make_item_error(&spec_attr, "trait impl const"));
123+
return Err(make_item_error(&spec_attr, "impl const"));
126124
}
127125
const_item.attrs = attrs;
128126
new_items.push(ImplItem::Const(const_item));
129127
}
130128
ImplItem::Type(mut type_item) => {
131129
let (spec, attrs) = find_spec_attr(type_item.attrs)?;
132130
if let Some(ref spec_attr) = spec {
133-
return Err(make_item_error(&spec_attr, "trait impl type"));
131+
return Err(make_item_error(&spec_attr, "impl type"));
134132
}
135133
type_item.attrs = attrs;
136134
new_items.push(ImplItem::Type(type_item));
137135
}
138136
ImplItem::Macro(mut macro_item) => {
139137
let (spec, attrs) = find_spec_attr(macro_item.attrs)?;
140138
if let Some(ref spec_attr) = spec {
141-
return Err(make_item_error(&spec_attr, "trait impl macro"));
139+
return Err(make_item_error(&spec_attr, "impl macro"));
142140
}
143141
macro_item.attrs = attrs;
144142
new_items.push(ImplItem::Macro(macro_item));

crates/anodized-core/src/instrument/impls_tests.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -123,7 +123,7 @@ fn split_panic_instrument_item_impl() {
123123
let expected: TokenStream = parse_quote! {
124124
impl IMPL_TYPE {
125125
fn FUNC(&self, input_1: TYPE_1, input_2: TYPE_2) -> RET_TYPE {
126-
match __anodized_split_FUNC(self, input_1, input_2) {
126+
match Self::__anodized_split_FUNC(self, input_1, input_2) {
127127
Ok(output) => output,
128128
Err((false, errors)) => panic!("precondition failed:{errors}"),
129129
Err((true, errors)) => panic!("postcondition failed:{errors}"),

crates/anodized/tests/captures_feature.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,7 @@ fn precondition_runs_before_captures() {
143143
counter: u32,
144144
}
145145

146+
#[spec]
146147
impl TestStruct {
147148
#[spec(
148149
requires: self.counter < 100,

crates/anodized/tests/method_call_invariant.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ struct Validator {
66
valid: bool,
77
}
88

9+
#[spec]
910
impl Validator {
1011
fn is_valid(&self) -> bool {
1112
self.valid

crates/anodized/tests/method_with_invariant.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ struct Counter {
66
capacity: u32,
77
}
88

9+
#[spec]
910
impl Counter {
1011
#[spec(
1112
maintains: self.count <= self.capacity,

crates/anodized/tests/multiple_conditions.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ struct SafeBuffer<T> {
77
locked: bool,
88
}
99

10+
#[spec]
1011
impl<T> SafeBuffer<T> {
1112
#[spec(
1213
requires: [

0 commit comments

Comments
 (0)