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            && locals[call.dest.local_id()].ty.kind().is_never()
39        {
40            *second_abort = RawStatement::Nop;
41            return Vec::new();
42        }
43
44        Vec::new()
45    }
46}
47
48impl LlbcPass for Transform {
49    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
50        b.body
51            .transform_sequences(|seq| Transform::update_statements(&b.locals, seq))
52    }
53}
charon_lib/transform/prettify_cfg.rs

charon_lib/transform/
prettify_cfg.rs
