charon_lib/ast/
from_rustc.rs

1// This file is automatically generated by `cargo run --bin generate-asts`.
2// Do not edit it by hand.
3
4#![allow(
5    clippy::doc_lazy_continuation,
6    clippy::enum_variant_names,
7    clippy::large_enum_variant
8)]
9
10use crate::ast::meta::Span;
11use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
12use serde::{Deserialize, Serialize};
13use ustr::Ustr;
14
15#[derive(Debug, Copy, Clone, PartialEq, Eq)]
16pub struct FromRustcError;
17
18/// Represents parsed *built-in* inert attributes.
19///
20/// ## Overview
21/// These attributes are markers that guide the compilation process and are never expanded into other code.
22/// They persist throughout the compilation phases, from AST to HIR and beyond.
23///
24/// ## Attribute Processing
25/// While attributes are initially parsed by [`rustc_parse`] into [`ast::Attribute`], they still contain raw token streams
26/// because different attributes have different internal structures. This enum represents the final,
27/// fully parsed form of these attributes, where each variant contains all the information and
28/// structure relevant for the specific attribute.
29///
30/// Some attributes can be applied multiple times to the same item, and they are "collapsed" into a single
31/// semantic attribute. For example:
32/// ```rust
33/// #[repr(C)]
34/// #[repr(packed)]
35/// struct S { }
36/// ```
37/// This is equivalent to `#[repr(C, packed)]` and results in a single [`AttributeKind::Repr`] containing
38/// both `C` and `packed` annotations. This collapsing happens during parsing and is reflected in the
39/// data structures defined in this enum.
40///
41/// ## Usage
42/// These parsed attributes are used throughout the compiler to:
43/// - Control code generation (e.g., `#[repr]`)
44/// - Mark API stability (`#[stable]`, `#[unstable]`)
45/// - Provide documentation (`#[doc]`)
46/// - Guide compiler behavior (e.g., `#[allow_internal_unstable]`)
47///
48/// ## Note on Attribute Organization
49/// Some attributes like `InlineAttr`, `OptimizeAttr`, and `InstructionSetAttr` are defined separately
50/// from this enum because they are used in specific compiler phases (like code generation) and don't
51/// need to persist throughout the entire compilation process. They are typically processed and
52/// converted into their final form earlier in the compilation pipeline.
53///
54/// For example:
55/// - `InlineAttr` is used during code generation to control function inlining
56/// - `OptimizeAttr` is used to control optimization levels
57/// - `InstructionSetAttr` is used for target-specific code generation
58///
59/// These attributes are handled by their respective compiler passes in the [`rustc_codegen_ssa`] crate
60/// and don't need to be preserved in the same way as the attributes in this enum.
61///
62/// For more details on attribute parsing, see the [`rustc_attr_parsing`] crate.
63///
64/// [`rustc_parse`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_parse/index.html
65/// [`rustc_codegen_ssa`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_codegen_ssa/index.html
66/// [`rustc_attr_parsing`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_attr_parsing/index.html
67#[derive(Debug, Clone, PartialEq, Eq)]
68#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
69#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcAttributeKind"))]
70#[cfg_attr(
71    feature = "charon_on_charon",
72    charon::variants_prefix("RustcAttributeKind")
73)]
74pub enum AttributeKind {
75    /// Represents `#[automatically_derived]`
76    AutomaticallyDerived,
77    /// Represents `#[cold]`.
78    Cold,
79    /// Represents [`#[deprecated]`](https://doc.rust-lang.org/stable/reference/attributes/diagnostics.html#the-deprecated-attribute).
80    Deprecated {
81        deprecation: Deprecation,
82        span: Span,
83    },
84    /// Represents [`#[export_name]`](https://doc.rust-lang.org/reference/abi.html#the-export_name-attribute).
85    ExportName {
86        /// The name to export this item with.
87        /// It may not contain \0 bytes as it will be converted to a null-terminated string.
88        name: Ustr,
89        span: Span,
90    },
91    /// Represents `#[fundamental]`.
92    Fundamental,
93    /// Represents `#[ignore]`
94    Ignore {
95        span: Span,
96        /// ignore can optionally have a reason: `#[ignore = "reason this is ignored"]`
97        reason: Option<Ustr>,
98    },
99    /// Represents `#[inline]` and `#[rustc_force_inline]`.
100    Inline(InlineAttr, Span),
101    /// Represents [`#[link_section]`](https://doc.rust-lang.org/reference/abi.html#the-link_section-attribute)
102    LinkSection { name: Ustr },
103    /// Represents `#[linkage]`.
104    Linkage(Linkage, Span),
105    /// Represents [`#[may_dangle]`](https://std-dev-guide.rust-lang.org/tricky/may-dangle.html).
106    MayDangle(Span),
107    /// Represents `#[naked]`
108    Naked(Span),
109    /// Represents `#[no_link]`
110    NoLink,
111    /// Represents `#[no_mangle]`
112    NoMangle(Span),
113    /// Represents `#[non_exhaustive]`
114    NonExhaustive(Span),
115    /// Represents `#[optimize(size|speed)]`
116    Optimize(OptimizeAttr, Span),
117    /// Represents `#[align(N)]`.
118    RustcAlign { align: u64, span: Span },
119    /// Represents `#[rustc_intrinsic]`
120    RustcIntrinsic,
121    /// Represents `#[should_panic]`
122    ShouldPanic { reason: Option<Ustr> },
123    /// Represents `#[target_feature(enable = "...")]` and
124    /// `#[unsafe(force_target_feature(enable = "...")]`.
125    TargetFeature {
126        features: Vec<(Ustr, Span)>,
127        attr_span: Span,
128        was_forced: bool,
129    },
130    /// Represents `#[track_caller]`
131    TrackCaller(Span),
132}
133
134/// A representation of all the valid lang items in Rust.
135#[derive(Debug, Clone, PartialEq, Eq)]
136#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
137#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcLangItem"))]
138#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("RustcLangItem"))]
139pub enum LangItem {
140    ///The `sized` lang item.
141    Sized,
142    ///The `meta_sized` lang item.
143    MetaSized,
144    ///The `pointee_sized` lang item.
145    PointeeSized,
146    ///The `unsize` lang item.
147    Unsize,
148    ///The `mem_align_const` lang item.
149    AlignOf,
150    ///The `mem_size_const` lang item.
151    SizeOf,
152    ///The `offset_of` lang item.
153    OffsetOf,
154    ///The `structural_peq` lang item.
155    /// Trait injected by `#[derive(PartialEq)]`, (i.e. "Partial EQ").
156    StructuralPeq,
157    ///The `copy` lang item.
158    Copy,
159    ///The `clone` lang item.
160    Clone,
161    ///The `clone_fn` lang item.
162    CloneFn,
163    ///The `use_cloned` lang item.
164    UseCloned,
165    ///The `trivial_clone` lang item.
166    TrivialClone,
167    ///The `sync` lang item.
168    Sync,
169    ///The `discriminant_kind` lang item.
170    DiscriminantKind,
171    ///The `discriminant_type` lang item.
172    /// The associated item of the `DiscriminantKind` trait.
173    Discriminant,
174    ///The `pointee_trait` lang item.
175    PointeeTrait,
176    ///The `metadata_type` lang item.
177    Metadata,
178    ///The `dyn_metadata` lang item.
179    DynMetadata,
180    ///The `non_null` lang item.
181    NonNull,
182    ///The `freeze` lang item.
183    Freeze,
184    ///The `unsafe_unpin` lang item.
185    UnsafeUnpin,
186    ///The `fn_ptr_trait` lang item.
187    FnPtrTrait,
188    ///The `fn_ptr_as_ptr` lang item.
189    FnPtrAsPtr,
190    ///The `fn_ptr_from_ptr` lang item.
191    FnPtrFromPtr,
192    ///The `code` lang item.
193    Code,
194    ///The `drop` lang item.
195    Drop,
196    ///The `destruct` lang item.
197    Destruct,
198    ///The `async_drop` lang item.
199    AsyncDrop,
200    ///The `async_drop_in_place` lang item.
201    AsyncDropInPlace,
202    ///The `coerce_unsized` lang item.
203    CoerceUnsized,
204    ///The `dispatch_from_dyn` lang item.
205    DispatchFromDyn,
206    ///The `try_as_dyn` lang item.
207    TryAsDyn,
208    ///The `transmute_opts` lang item.
209    TransmuteOpts,
210    ///The `transmute_trait` lang item.
211    TransmuteTrait,
212    ///The `add` lang item.
213    Add,
214    ///The `sub` lang item.
215    Sub,
216    ///The `mul` lang item.
217    Mul,
218    ///The `div` lang item.
219    Div,
220    ///The `rem` lang item.
221    Rem,
222    ///The `neg` lang item.
223    Neg,
224    ///The `not` lang item.
225    Not,
226    ///The `bitxor` lang item.
227    BitXor,
228    ///The `bitand` lang item.
229    BitAnd,
230    ///The `bitor` lang item.
231    BitOr,
232    ///The `shl` lang item.
233    Shl,
234    ///The `shr` lang item.
235    Shr,
236    ///The `add_assign` lang item.
237    AddAssign,
238    ///The `sub_assign` lang item.
239    SubAssign,
240    ///The `mul_assign` lang item.
241    MulAssign,
242    ///The `div_assign` lang item.
243    DivAssign,
244    ///The `rem_assign` lang item.
245    RemAssign,
246    ///The `bitxor_assign` lang item.
247    BitXorAssign,
248    ///The `bitand_assign` lang item.
249    BitAndAssign,
250    ///The `bitor_assign` lang item.
251    BitOrAssign,
252    ///The `shl_assign` lang item.
253    ShlAssign,
254    ///The `shr_assign` lang item.
255    ShrAssign,
256    ///The `index` lang item.
257    Index,
258    ///The `index_mut` lang item.
259    IndexMut,
260    ///The `unsafe_cell` lang item.
261    UnsafeCell,
262    ///The `covariant_unsafe_cell` lang item.
263    CovariantUnsafeCell,
264    ///The `unsafe_pinned` lang item.
265    UnsafePinned,
266    ///The `va_arg_safe` lang item.
267    VaArgSafe,
268    ///The `va_list` lang item.
269    VaList,
270    ///The `complex` lang item.
271    Complex,
272    ///The `deref` lang item.
273    Deref,
274    ///The `deref_mut` lang item.
275    DerefMut,
276    ///The `deref_pure` lang item.
277    DerefPure,
278    ///The `deref_target` lang item.
279    DerefTarget,
280    ///The `receiver` lang item.
281    Receiver,
282    ///The `receiver_target` lang item.
283    ReceiverTarget,
284    ///The `legacy_receiver` lang item.
285    LegacyReceiver,
286    ///The `Fn` lang item.
287    Fn,
288    ///The `fn_mut` lang item.
289    FnMut,
290    ///The `fn_once` lang item.
291    FnOnce,
292    ///The `fn_static` lang item.
293    FnStatic,
294    ///The `async_fn` lang item.
295    AsyncFn,
296    ///The `async_fn_mut` lang item.
297    AsyncFnMut,
298    ///The `async_fn_once` lang item.
299    AsyncFnOnce,
300    ///The `async_fn_once_output` lang item.
301    AsyncFnOnceOutput,
302    ///The `call_once_future` lang item.
303    CallOnceFuture,
304    ///The `call_ref_future` lang item.
305    CallRefFuture,
306    ///The `async_fn_kind_helper` lang item.
307    AsyncFnKindHelper,
308    ///The `async_fn_kind_upvars` lang item.
309    AsyncFnKindUpvars,
310    ///The `fn_once_output` lang item.
311    FnOnceOutput,
312    ///The `iterator` lang item.
313    Iterator,
314    ///The `fused_iterator` lang item.
315    FusedIterator,
316    ///The `future_trait` lang item.
317    Future,
318    ///The `future_output` lang item.
319    FutureOutput,
320    ///The `async_iterator` lang item.
321    AsyncIterator,
322    ///The `coroutine_state` lang item.
323    CoroutineState,
324    ///The `coroutine` lang item.
325    Coroutine,
326    ///The `coroutine_return` lang item.
327    CoroutineReturn,
328    ///The `coroutine_yield` lang item.
329    CoroutineYield,
330    ///The `coroutine_resume` lang item.
331    CoroutineResume,
332    ///The `unpin` lang item.
333    Unpin,
334    ///The `Pin` lang item.
335    Pin,
336    ///The `Ordering` lang item.
337    OrderingEnum,
338    ///The `eq` lang item.
339    PartialEq,
340    ///The `partial_ord` lang item.
341    PartialOrd,
342    ///The `c_void` lang item.
343    CVoid,
344    ///The `type_info` lang item.
345    Type,
346    ///The `type_info_generic` lang item.
347    TypeGeneric,
348    ///The `type_id` lang item.
349    TypeId,
350    ///The `panic` lang item.
351    Panic,
352    ///The `panic_nounwind` lang item.
353    PanicNounwind,
354    ///The `panic_fmt` lang item.
355    PanicFmt,
356    ///The `panic_display` lang item.
357    PanicDisplay,
358    ///The `const_panic_fmt` lang item.
359    ConstPanicFmt,
360    ///The `panic_bounds_check` lang item.
361    PanicBoundsCheck,
362    ///The `panic_misaligned_pointer_dereference` lang item.
363    PanicMisalignedPointerDereference,
364    ///The `panic_info` lang item.
365    PanicInfo,
366    ///The `panic_location` lang item.
367    PanicLocation,
368    ///The `panic_impl` lang item.
369    PanicImpl,
370    ///The `panic_cannot_unwind` lang item.
371    PanicCannotUnwind,
372    ///The `panic_in_cleanup` lang item.
373    PanicInCleanup,
374    ///The `panic_const_add_overflow` lang item.
375    /// Constant panic messages, used for codegen of MIR asserts.
376    PanicAddOverflow,
377    ///The `panic_const_sub_overflow` lang item.
378    PanicSubOverflow,
379    ///The `panic_const_mul_overflow` lang item.
380    PanicMulOverflow,
381    ///The `panic_const_div_overflow` lang item.
382    PanicDivOverflow,
383    ///The `panic_const_rem_overflow` lang item.
384    PanicRemOverflow,
385    ///The `panic_const_neg_overflow` lang item.
386    PanicNegOverflow,
387    ///The `panic_const_shr_overflow` lang item.
388    PanicShrOverflow,
389    ///The `panic_const_shl_overflow` lang item.
390    PanicShlOverflow,
391    ///The `panic_const_div_by_zero` lang item.
392    PanicDivZero,
393    ///The `panic_const_rem_by_zero` lang item.
394    PanicRemZero,
395    ///The `panic_const_coroutine_resumed` lang item.
396    PanicCoroutineResumed,
397    ///The `panic_const_async_fn_resumed` lang item.
398    PanicAsyncFnResumed,
399    ///The `panic_const_async_gen_fn_resumed` lang item.
400    PanicAsyncGenFnResumed,
401    ///The `panic_const_gen_fn_none` lang item.
402    PanicGenFnNone,
403    ///The `panic_const_coroutine_resumed_panic` lang item.
404    PanicCoroutineResumedPanic,
405    ///The `panic_const_async_fn_resumed_panic` lang item.
406    PanicAsyncFnResumedPanic,
407    ///The `panic_const_async_gen_fn_resumed_panic` lang item.
408    PanicAsyncGenFnResumedPanic,
409    ///The `panic_const_gen_fn_none_panic` lang item.
410    PanicGenFnNonePanic,
411    ///The `panic_null_pointer_dereference` lang item.
412    PanicNullPointerDereference,
413    ///The `panic_null_reference_constructed` lang item.
414    PanicNullReferenceConstructed,
415    ///The `panic_invalid_enum_construction` lang item.
416    PanicInvalidEnumConstruction,
417    ///The `panic_const_coroutine_resumed_drop` lang item.
418    PanicCoroutineResumedDrop,
419    ///The `panic_const_async_fn_resumed_drop` lang item.
420    PanicAsyncFnResumedDrop,
421    ///The `panic_const_async_gen_fn_resumed_drop` lang item.
422    PanicAsyncGenFnResumedDrop,
423    ///The `panic_const_gen_fn_none_drop` lang item.
424    PanicGenFnNoneDrop,
425    ///The `begin_panic` lang item.
426    /// libstd panic entry point. Necessary for const eval to be able to catch it
427    BeginPanic,
428    ///The `format_argument` lang item.
429    FormatArgument,
430    ///The `format_arguments` lang item.
431    FormatArguments,
432    ///The `drop_glue` lang item.
433    DropGlue,
434    ///The `alloc_layout` lang item.
435    AllocLayout,
436    ///The `start` lang item.
437    /// For all binary crates without `#![no_main]`, Rust will generate a "main" function.
438    /// The exact name and signature are target-dependent. The "main" function will invoke
439    /// this lang item, passing it the `argc` and `argv` (or null, if those don't exist
440    /// on the current target) as well as the user-defined `fn main` from the binary crate.
441    Start,
442    ///The `eh_personality` lang item.
443    EhPersonality,
444    ///The `compiler_move` lang item.
445    CompilerMove,
446    ///The `compiler_copy` lang item.
447    CompilerCopy,
448    ///The `owned_box` lang item.
449    OwnedBox,
450    ///The `global_alloc_ty` lang item.
451    GlobalAlloc,
452    ///The `phantom_data` lang item.
453    PhantomData,
454    ///The `manually_drop` lang item.
455    ManuallyDrop,
456    ///The `maybe_dangling` lang item.
457    MaybeDangling,
458    ///The `bikeshed_guaranteed_no_drop` lang item.
459    BikeshedGuaranteedNoDrop,
460    ///The `maybe_uninit` lang item.
461    MaybeUninit,
462    ///The `termination` lang item.
463    Termination,
464    ///The `Try` lang item.
465    Try,
466    ///The `tuple_trait` lang item.
467    Tuple,
468    ///The `slice_len_fn` lang item.
469    SliceLen,
470    ///The `from_residual` lang item.
471    TryTraitFromResidual,
472    ///The `from_output` lang item.
473    TryTraitFromOutput,
474    ///The `branch` lang item.
475    TryTraitBranch,
476    ///The `from_yeet` lang item.
477    TryTraitFromYeet,
478    ///The `into_try_type` lang item.
479    ResidualIntoTryType,
480    ///The `coerce_pointee_validated` lang item.
481    CoercePointeeValidated,
482    ///The `const_param_ty` lang item.
483    ConstParamTy,
484    ///The `Poll` lang item.
485    Poll,
486    ///The `Ready` lang item.
487    PollReady,
488    ///The `Pending` lang item.
489    PollPending,
490    ///The `AsyncGenReady` lang item.
491    AsyncGenReady,
492    ///The `AsyncGenPending` lang item.
493    AsyncGenPending,
494    ///The `AsyncGenFinished` lang item.
495    AsyncGenFinished,
496    ///The `ResumeTy` lang item.
497    ResumeTy,
498    ///The `get_context` lang item.
499    GetContext,
500    ///The `Context` lang item.
501    Context,
502    ///The `poll` lang item.
503    FuturePoll,
504    ///The `async_iterator_poll_next` lang item.
505    AsyncIteratorPollNext,
506    ///The `into_async_iter_into_iter` lang item.
507    IntoAsyncIterIntoIter,
508    ///The `Option` lang item.
509    Option,
510    ///The `Some` lang item.
511    OptionSome,
512    ///The `None` lang item.
513    OptionNone,
514    ///The `Ok` lang item.
515    ResultOk,
516    ///The `Err` lang item.
517    ResultErr,
518    ///The `Continue` lang item.
519    ControlFlowContinue,
520    ///The `Break` lang item.
521    ControlFlowBreak,
522    ///The `into_future` lang item.
523    IntoFutureIntoFuture,
524    ///The `into_iter` lang item.
525    IntoIterIntoIter,
526    ///The `next` lang item.
527    IteratorNext,
528    ///The `new_unchecked` lang item.
529    PinNewUnchecked,
530    ///The `RangeFrom` lang item.
531    RangeFrom,
532    ///The `RangeFull` lang item.
533    RangeFull,
534    ///The `RangeInclusive` lang item.
535    RangeInclusiveStruct,
536    ///The `range_inclusive_new` lang item.
537    RangeInclusiveNew,
538    ///The `Range` lang item.
539    Range,
540    ///The `RangeToInclusive` lang item.
541    RangeToInclusive,
542    ///The `RangeTo` lang item.
543    RangeTo,
544    ///The `RangeMax` lang item.
545    RangeMax,
546    ///The `RangeMin` lang item.
547    RangeMin,
548    ///The `RangeSub` lang item.
549    RangeSub,
550    ///The `RangeFromCopy` lang item.
551    RangeFromCopy,
552    ///The `RangeCopy` lang item.
553    RangeCopy,
554    ///The `RangeInclusiveCopy` lang item.
555    RangeInclusiveCopy,
556    ///The `RangeToInclusiveCopy` lang item.
557    RangeToInclusiveCopy,
558    ///The `String` lang item.
559    String,
560    ///The `CStr` lang item.
561    CStr,
562    ///The `contract_build_check_ensures` lang item.
563    ContractBuildCheckEnsures,
564    ///The `contract_check_requires` lang item.
565    ContractCheckRequires,
566    ///The `default_trait4` lang item.
567    DefaultTrait4,
568    ///The `default_trait3` lang item.
569    DefaultTrait3,
570    ///The `default_trait2` lang item.
571    DefaultTrait2,
572    ///The `default_trait1` lang item.
573    DefaultTrait1,
574    ///The `contract_check_ensures` lang item.
575    ContractCheckEnsures,
576    ///The `reborrow` lang item.
577    Reborrow,
578    ///The `coerce_shared` lang item.
579    CoerceShared,
580    ///The `field_representing_type` lang item.
581    FieldRepresentingType,
582    ///The `field` lang item.
583    Field,
584    ///The `field_base` lang item.
585    FieldBase,
586    ///The `field_type` lang item.
587    FieldType,
588    ///The `field_offset` lang item.
589    FieldOffset,
590    ///The `From` lang item.
591    From,
592    ///The `from` lang item.
593    FromFn,
594    ///The `FnPtr` lang item.
595    FnPtr,
596}
597
598#[derive(Debug, Clone, PartialEq, Eq)]
599#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
600#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcArch"))]
601#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("RustcArch"))]
602pub enum Arch {
603    AArch64,
604    AmdGpu,
605    Arm,
606    Arm64EC,
607    Avr,
608    Bpf,
609    CSky,
610    Hexagon,
611    LoongArch32,
612    LoongArch64,
613    M68k,
614    Mips,
615    Mips32r6,
616    Mips64,
617    Mips64r6,
618    Msp430,
619    Nvptx64,
620    PowerPC,
621    PowerPC64,
622    RiscV32,
623    RiscV64,
624    S390x,
625    Sparc,
626    Sparc64,
627    SpirV,
628    Wasm32,
629    Wasm64,
630    X86,
631    X86_64,
632    Xtensa,
633    /// The vast majority of the time, the compiler deals with a fixed
634    /// set of values, so it is convenient for them to be represented in
635    /// an enum. However, it is possible to have arbitrary values in a
636    /// target JSON file (which can be parsed when `--target` is
637    /// specified). This might occur, for example, for an out-of-tree
638    /// codegen backend that supports a value (e.g. architecture or OS)
639    /// that rustc currently doesn't know about. This variant exists as
640    /// an escape hatch for such cases.
641    Other(Ustr),
642}
643
644#[derive(Debug, Clone, PartialEq, Eq)]
645#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
646#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcOs"))]
647#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("RustcOs"))]
648pub enum Os {
649    Aix,
650    AmdHsa,
651    Android,
652    Cuda,
653    Cygwin,
654    Dragonfly,
655    Emscripten,
656    EspIdf,
657    FreeBsd,
658    Fuchsia,
659    Haiku,
660    HelenOs,
661    Hermit,
662    Horizon,
663    Hurd,
664    Illumos,
665    IOs,
666    L4Re,
667    Linux,
668    LynxOs178,
669    MacOs,
670    Managarm,
671    Motor,
672    NetBsd,
673    None,
674    Nto,
675    NuttX,
676    OpenBsd,
677    Ps3,
678    Psp,
679    Psx,
680    Qnx,
681    Qurt,
682    Redox,
683    Rtems,
684    Solaris,
685    SolidAsp3,
686    TeeOs,
687    Trusty,
688    TvOs,
689    Uefi,
690    VexOs,
691    VisionOs,
692    Vita,
693    VxWorks,
694    Wasi,
695    WatchOs,
696    Windows,
697    Xous,
698    Zkvm,
699    Unknown,
700    /// The vast majority of the time, the compiler deals with a fixed
701    /// set of values, so it is convenient for them to be represented in
702    /// an enum. However, it is possible to have arbitrary values in a
703    /// target JSON file (which can be parsed when `--target` is
704    /// specified). This might occur, for example, for an out-of-tree
705    /// codegen backend that supports a value (e.g. architecture or OS)
706    /// that rustc currently doesn't know about. This variant exists as
707    /// an escape hatch for such cases.
708    Other(Ustr),
709}
710
711#[derive(Debug, Clone, PartialEq, Eq)]
712#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
713#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcEnv"))]
714#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("RustcEnv"))]
715pub enum Env {
716    Gnu,
717    MacAbi,
718    Mlibc,
719    Msvc,
720    Musl,
721    Newlib,
722    Nto70,
723    Nto71,
724    Nto71IoSock,
725    Ohos,
726    Relibc,
727    Sgx,
728    Sim,
729    P1,
730    P2,
731    P3,
732    Uclibc,
733    V5,
734    Unspecified,
735    /// The vast majority of the time, the compiler deals with a fixed
736    /// set of values, so it is convenient for them to be represented in
737    /// an enum. However, it is possible to have arbitrary values in a
738    /// target JSON file (which can be parsed when `--target` is
739    /// specified). This might occur, for example, for an out-of-tree
740    /// codegen backend that supports a value (e.g. architecture or OS)
741    /// that rustc currently doesn't know about. This variant exists as
742    /// an escape hatch for such cases.
743    Other(Ustr),
744}
745
746/// An enum representing possible values for `cfg(target_abi)`.
747/// This field is not forwarded to LLVM so it does not by itself affect codegen.
748/// See the `cfg_abi` field of [`TargetOptions`] for more details.
749#[derive(Debug, Clone, PartialEq, Eq)]
750#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
751#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcCfgAbi"))]
752#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("RustcCfgAbi"))]
753pub enum CfgAbi {
754    Abi64,
755    AbiV2,
756    AbiV2Hf,
757    Eabi,
758    EabiHf,
759    ElfV1,
760    ElfV2,
761    Fortanix,
762    Ilp32,
763    Ilp32e,
764    Llvm,
765    MacAbi,
766    Pauthtest,
767    Sim,
768    SoftFloat,
769    Spe,
770    Uwp,
771    VecDefault,
772    VecExtAbi,
773    X32,
774    V8Plus,
775    Unspecified,
776    /// The vast majority of the time, the compiler deals with a fixed
777    /// set of values, so it is convenient for them to be represented in
778    /// an enum. However, it is possible to have arbitrary values in a
779    /// target JSON file (which can be parsed when `--target` is
780    /// specified). This might occur, for example, for an out-of-tree
781    /// codegen backend that supports a value (e.g. architecture or OS)
782    /// that rustc currently doesn't know about. This variant exists as
783    /// an escape hatch for such cases.
784    Other(Ustr),
785}
786
787#[derive(Debug, Clone, PartialEq, Eq)]
788#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
789#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcDeprecation"))]
790pub struct Deprecation {
791    pub since: DeprecatedSince,
792    /// The note to issue a reason.
793    pub note: Option<Ident>,
794    /// A text snippet used to completely replace any use of the deprecated item in an expression.
795    ///
796    /// This is currently unstable.
797    pub suggestion: Option<Ustr>,
798}
799
800#[derive(Debug, Clone, PartialEq, Eq)]
801#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
802#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcInlineAttr"))]
803#[cfg_attr(
804    feature = "charon_on_charon",
805    charon::variants_prefix("RustcInlineAttr")
806)]
807pub enum InlineAttr {
808    None,
809    Hint,
810    Always,
811    Never,
812    /// `#[rustc_force_inline]` forces inlining to happen in the MIR inliner - it reports an error
813    /// if the inlining cannot happen. It is limited to only free functions so that the calls
814    /// can always be resolved.
815    Force {
816        attr_span: Span,
817        reason: Option<Ustr>,
818    },
819}
820
821/// Possible values for the `#[linkage]` attribute, allowing to specify the
822/// linkage type for a `MonoItem`.
823///
824/// See <https://llvm.org/docs/LangRef.html#linkage-types> for more details about these variants.
825#[derive(Debug, Clone, PartialEq, Eq)]
826#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
827#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcLinkage"))]
828#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("RustcLinkage"))]
829pub enum Linkage {
830    AvailableExternally,
831    Common,
832    ExternalWeak,
833    External,
834    Internal,
835    LinkOnceAny,
836    LinkOnceODR,
837    WeakAny,
838    WeakODR,
839}
840
841#[derive(Debug, Clone, PartialEq, Eq)]
842#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
843#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcOptimizeAttr"))]
844#[cfg_attr(
845    feature = "charon_on_charon",
846    charon::variants_prefix("RustcOptimizeAttr")
847)]
848pub enum OptimizeAttr {
849    /// No `#[optimize(..)]` attribute
850    Default,
851    /// `#[optimize(none)]`
852    DoNotOptimize,
853    /// `#[optimize(speed)]`
854    Speed,
855    /// `#[optimize(size)]`
856    Size,
857}
858
859/// Release in which an API is deprecated.
860#[derive(Debug, Clone, PartialEq, Eq)]
861#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
862#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcDeprecatedSince"))]
863#[cfg_attr(
864    feature = "charon_on_charon",
865    charon::variants_prefix("RustcDeprecatedSince")
866)]
867pub enum DeprecatedSince {
868    RustcVersion(RustcVersion),
869    /// Deprecated in the future ("to be determined").
870    Future,
871    /// `feature(staged_api)` is off. Deprecation versions outside the standard
872    /// library are allowed to be arbitrary strings, for better or worse.
873    NonStandard(Ustr),
874    /// Deprecation version is unspecified but optional.
875    Unspecified,
876    /// Failed to parse a deprecation version, or the deprecation version is
877    /// unspecified and required. An error has already been emitted.
878    Err,
879}
880
881#[derive(Debug, Clone, PartialEq, Eq)]
882#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
883#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcIdent"))]
884pub struct Ident {
885    /// `name` should never be the empty symbol. If you are considering that,
886    /// you are probably conflating "empty identifier with "no identifier" and
887    /// you should use `Option<Ident>` instead.
888    /// Trying to construct an `Ident` with an empty name will trigger debug assertions.
889    pub name: Ustr,
890    pub span: Span,
891}
892
893#[derive(Debug, Clone, PartialEq, Eq)]
894#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
895#[cfg_attr(feature = "charon_on_charon", charon::rename("RustcRustcVersion"))]
896pub struct RustcVersion {
897    pub major: u16,
898    pub minor: u16,
899    pub patch: u16,
900}
charon_lib/ast/from_rustc.rs

charon_lib/ast/
from_rustc.rs
