charon_lib/transform/add_missing_info/
link_specs.rs

1use crate::ast::*;
2use crate::transform::{TransformCtx, ctx::TransformPass};
3
4pub struct Transform;
5impl TransformPass for Transform {
6    fn transform_ctx(&self, ctx: &mut TransformCtx) {
7        let mut specs = Vec::new();
8        for (spec_id, item) in ctx.translated.all_items_with_ids() {
9            let ItemId::Fun(spec_id) = spec_id else {
10                continue;
11            };
12            for attr in &item.item_meta().attr_info.attributes {
13                match attr {
14                    Attribute::IsPrecondition(parent_id) => {
15                        specs.push((spec_id, *parent_id, SpecKind::Precondition));
16                    }
17                    Attribute::IsPostcondition(parent_id) => {
18                        specs.push((spec_id, *parent_id, SpecKind::Postcondition));
19                    }
20                    _ => {}
21                }
22            }
23        }
24
25        for (spec_id, parent_id, kind) in specs {
26            if ctx.translated.get_item(parent_id).is_none() {
27                continue;
28            }
29            let Some(ItemRefMut::Fun(spec)) = ctx.translated.get_item_mut(spec_id.into()) else {
30                continue;
31            };
32            spec.src = ItemSource::Spec {
33                kind,
34                item: parent_id,
35            };
36
37            let mut parent = ctx.translated.get_item_mut(parent_id).unwrap();
38            let attr = match kind {
39                SpecKind::Precondition => Attribute::HasPrecondition(spec_id),
40                SpecKind::Postcondition => Attribute::HasPostcondition(spec_id),
41            };
42            parent.item_meta().attr_info.attributes.push(attr);
43        }
44    }
45}
charon_lib/transform/add_missing_info/link_specs.rs

charon_lib/transform/add_missing_info/
link_specs.rs
