bashrs 6.66.0

Rust-to-Shell transpiler for deterministic bootstrap scripts
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

//! Formal verification module for the rash emitter
//!
//! This module implements formal verification of the emitter's correctness
//! for a tiny subset of the rash AST, proving semantic equivalence between
//! rash AST nodes and their emitted POSIX shell commands.
//!
//! ## Safety Note
//! Formal verification uses unwrap() on validated proofs and checked invariants.
#![allow(clippy::unwrap_used)]
#![allow(clippy::indexing_slicing)]

pub mod abstract_state;
pub mod emitter;
pub mod enhanced_state;
pub mod inspector;
pub mod semantics;
pub mod tiny_ast;

#[cfg(test)]
pub mod proofs;

#[cfg(kani)]
pub mod kani_harnesses;

#[cfg(test)]
#[path = "inspector_coverage_tests.rs"]
mod inspector_coverage_tests;

pub use abstract_state::*;
pub use emitter::*;
pub use enhanced_state::*;
pub use inspector::*;
pub use semantics::*;
pub use tiny_ast::*;