charon_lib/transform/
prettify_cfg.rs

1use crate::llbc_ast::*;
2use crate::transform::TransformCtx;
3
4use super::ctx::LlbcPass;
5
6pub struct Transform;
7
8impl Transform {
9    fn update_statements(locals: &Locals, seq: &mut [Statement]) -> Vec<Statement> {
10        // Remove double aborts. This can happen when a function call is turned into an `Abort` by
11        // `inline_local_panic_functions`.
12        if let [
13            Statement {
14                content: RawStatement::Abort(_),
15                ..
16            },
17            Statement {
18                content: second_abort @ RawStatement::Abort(_),
19                ..
20            },
21            ..,
22        ] = seq
23        {
24            *second_abort = RawStatement::Nop;
25            return Vec::new();
26        }
27        if let [
28            Statement {
29                content: RawStatement::Call(call),
30                ..
31            },
32            Statement {
33                content: second_abort @ RawStatement::Abort(_),
34                ..
35            },
36            ..,
37        ] = seq
38            && let Some(local_id) = call.dest.as_local()
39            && locals[local_id].ty.kind().is_never()
40        {
41            *second_abort = RawStatement::Nop;
42            return Vec::new();
43        }
44
45        Vec::new()
46    }
47}
48
49impl LlbcPass for Transform {
50    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
51        b.body
52            .transform_sequences(|seq| Transform::update_statements(&b.locals, seq))
53    }
54}
charon_lib/transform/prettify_cfg.rs

charon_lib/transform/
prettify_cfg.rs
