Skip to main content

charon_driver/translate/
translate_functions.rs

1//! Translate functions from the rust compiler MIR to our internal representation.
2//! Our internal representation is very close to MIR, but is more convenient for
3//! us to handle, and easier to maintain - rustc's representation can evolve
4//! independently.
5
6use crate::hax;
7
8use super::translate_ctx::*;
9use charon_lib::ast::*;
10
11impl<'tcx> ItemTransCtx<'tcx, '_> {
12    /// Translate the names of the arguments of this definition, if they are available,
13    /// otherwise naming arguments `arg0`, `arg1`, etc.
14    /// Note that the names of the arguments are not always available, even when
15    /// we can retrieve the MIR body, in which case we also fall back to `argN`.
16    pub fn translate_argument_names(
17        &mut self,
18        span: Span,
19        def: &hax::FullDef<'tcx>,
20        n_args: usize,
21    ) -> Vec<Option<String>> {
22        let Ok(Some(body)) = self.get_mir(def.this(), span) else {
23            return vec![None; n_args];
24        };
25        body.local_decls
26            .iter_enumerated()
27            .skip(1)
28            .take(body.arg_count)
29            .map(|(index, _)| hax::name_of_local(index, &body.var_debug_info))
30            .collect()
31    }
32}