charon_lib/ast/
builtins.rs

1//! This file contains information about the builtin functions/types/traits definitions
2//!
3//! **IMPORTANT**:
4//! When checking whether names are equal to one of the reference names below,
5//! we ignore the disambiguators (see [crate::names] and [crate::ast::names_utils]).
6// TODO: rename to "primitive"
7
8use crate::names::*;
9use crate::types::*;
10
11// Built-in functions
12// We treat this one specially in the `inline_local_panic_functions` pass. See there for details.
13pub static EXPLICIT_PANIC_NAME: &[&str] = &["core", "panicking", "panic_explicit"];
14
15pub static BOX_ASSUME_INIT_INTO_VEC_UNSAFE: &str = "box_assume_init_into_vec_unsafe";
16
17pub static BOX_WRITE: &str = "alloc::boxed::Box::write";
18
19// The translated Charon name contains an inherent impl path element where the Rust path contains
20// `Box`. `NamePattern` does not yet inspect inherent impl receiver types, so passes that match the
21// translated name need this wildcarded pattern.
22pub static BOX_WRITE_PATTERN: &str = "alloc::boxed::_::write";
23
24impl BuiltinTy {
25    pub fn get_name(self) -> Name {
26        let name: &[_] = match self {
27            BuiltinTy::Box => &["alloc", "boxed", "Box"],
28            BuiltinTy::Str => &["str"],
29        };
30        Name::from_path(name)
31    }
32}
charon_lib/ast/builtins.rs

charon_lib/ast/
builtins.rs
