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 [Statement {
13            content: RawStatement::Abort(_),
14            ..
15        }, Statement {
16            content: second_abort @ RawStatement::Abort(_),
17            ..
18        }, ..] = seq
19        {
20            *second_abort = RawStatement::Nop;
21            return Vec::new();
22        }
23        if let [Statement {
24            content: RawStatement::Call(call),
25            ..
26        }, Statement {
27            content: second_abort @ RawStatement::Abort(_),
28            ..
29        }, ..] = seq
30            && locals[call.dest.local_id()].ty.kind().is_never()
31        {
32            *second_abort = RawStatement::Nop;
33            return Vec::new();
34        }
35
36        Vec::new()
37    }
38}
39
40impl LlbcPass for Transform {
41    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
42        b.body
43            .transform_sequences(|seq| Transform::update_statements(&b.locals, seq))
44    }
45}
charon_lib/transform/prettify_cfg.rs

charon_lib/transform/
prettify_cfg.rs
