charon_lib/
lib.rs

1//! This library contains utilities to extract the MIR from a Rust project,
2//! by compiling it to an easy-to-use AST called LLBC (Low-Level Borrow Calculus).
3//! This AST is serialized into JSON files.
4//!
5//! A good entry point to explore the project is [`driver`](../charon_driver/index.html),
6//! and in particular [`driver::CharonCallbacks`](../charon_driver/driver/struct.CharonCallbacks.html),
7//! which implements the callback which we provide to Rustc.
8//!
9//! The ASTs are in [`ullbc_ast`] (Unstructured LLBC - basically
10//! a cleaned-up version of MIR) and [`llbc_ast`] (same as ULLBC, but
11//! we reconstructed the control-flow to have `if ... then ... else ...`,
12//! loops, etc. instead of `GOTO`s).
13
14// For rustdoc: prevents overflows
15#![recursion_limit = "256"]
16#![allow(clippy::borrowed_box)]
17#![allow(clippy::derivable_impls)]
18#![allow(clippy::field_reassign_with_default)]
19#![allow(clippy::manual_map)]
20#![allow(clippy::mem_replace_with_default)]
21#![allow(clippy::new_without_default)]
22#![allow(clippy::useless_format)]
23#![expect(incomplete_features)]
24#![feature(assert_matches)]
25#![feature(box_patterns)]
26#![feature(deref_patterns)]
27#![feature(deref_pure_trait)]
28#![feature(if_let_guard)]
29#![feature(impl_trait_in_assoc_type)]
30#![feature(iterator_try_collect)]
31#![feature(register_tool)]
32#![feature(trait_alias)]
33#![feature(trivial_bounds)]
34// For when we use charon on itself :3
35#![register_tool(charon)]
36
37#[macro_use]
38pub mod ids;
39#[macro_use]
40pub mod logger;
41pub mod ast;
42pub mod common;
43pub mod errors;
44pub mod export;
45pub mod name_matcher;
46pub mod options;
47pub mod pretty;
48pub mod transform;
49
50// Re-export all the ast modules so we can keep the old import structure.
51pub use ast::{builtins, expressions, gast, llbc_ast, meta, names, types, ullbc_ast, values};
52pub use pretty::formatter;
53
54/// The version of the crate, as defined in `Cargo.toml`.
55pub const VERSION: &str = env!("CARGO_PKG_VERSION");
56
57/// Read a `.llbc` file.
58pub fn deserialize_llbc(path: &std::path::Path) -> anyhow::Result<ast::TranslatedCrate> {
59    use crate::export::CrateData;
60    Ok(CrateData::deserialize_from_file(path)?.translated)
61}
charon_lib/lib.rs

charon_lib/
lib.rs
