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::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
15impl BuiltinTy {
16    pub fn get_name(self) -> Name {
17        let name: &[_] = match self {
18            BuiltinTy::Box => &["alloc", "boxed", "Box"],
19            BuiltinTy::Str => &["Str"],
20            BuiltinTy::Array => &["Array"],
21            BuiltinTy::Slice => &["Slice"],
22        };
23        Name::from_path(name)
24    }
25}
26
27/// When translating from MIR to ULLBC, we ignore some type parameters for some builtin types.
28/// For instance, many types like box or vec are parameterized (in MIR) by an allocator
29/// (`std::alloc::Allocator`): we ignore it.
30pub fn type_to_used_params(id: BuiltinTy) -> Vec<bool> {
31    match id {
32        BuiltinTy::Box => {
33            vec![true, false]
34        }
35        BuiltinTy::Str => {
36            vec![]
37        }
38        BuiltinTy::Array | BuiltinTy::Slice => vec![true],
39    }
40}
charon_lib/ast/builtins.rs

charon_lib/ast/
builtins.rs
