Crate decy_verify 

Safety property verification for transpiled Rust code.

Verifies memory safety, type safety, and other Rust safety guarantees.

Unsafe Code Auditing

This module provides comprehensive auditing of unsafe blocks in generated Rust code:

• Detection and counting of all unsafe blocks
• Confidence scoring for elimination potential
• Suggestions for safer alternatives
• Unsafe density metrics (<5 per 1000 LOC target)

Example

use decy_verify::{UnsafeAuditor, audit_rust_code};

let rust_code = r#"
    fn example() {
        unsafe {
            let ptr = std::ptr::null_mut();
        }
    }
"#;

let report = audit_rust_code(rust_code).expect("Failed to audit");
println!("Unsafe blocks found: {}", report.unsafe_blocks.len());
println!("Unsafe density: {:.2}%", report.unsafe_density_percent);

Modules

diff_test

Differential testing against GCC semantics (S5).

lock_verify

Lock discipline verification (DECY-079).

Structs

CompilationError

A structured compilation error from rustc

CompilationResult

Result of compiling generated Rust code

UnsafeAuditReport

Report summarizing unsafe code in a Rust file

UnsafeAuditor

Main auditor for analyzing unsafe code

UnsafeBlock

Represents a single unsafe block found in Rust code

Enums

UnsafePattern

Categories of unsafe patterns

Functions

audit_rust_code

Convenience function to audit Rust code

verify_compilation

Verify that generated Rust code compiles by invoking rustc.