#[cfg_attr(coverage_nightly, coverage(off))]
#[cfg(test)]
mod tests {
use super::*;
use tempfile::TempDir;
#[tokio::test]
async fn test_rust_borrow_checker_creation() {
let checker = RustBorrowChecker::new();
assert!(checker.is_ok());
}
#[tokio::test]
async fn test_rust_borrow_checker_collect() {
let temp_dir = TempDir::new().unwrap();
let rust_file = temp_dir.path().join("test.rs");
std::fs::write(
&rust_file,
r#"
fn safe_function() {
let x = 42;
println!("{}", x);
}
"#,
)
.unwrap();
let checker = RustBorrowChecker::default();
let cache = Arc::new(RwLock::new(ProofCache::new()));
let symbol_table = Arc::new(SymbolTable::new());
let result = checker
.collect(temp_dir.path(), &cache, &symbol_table)
.await;
assert!(result.is_ok());
let collection_result = result.unwrap();
assert_eq!(collection_result.metrics.files_processed, 1);
assert!(!collection_result.annotations.is_empty());
}
#[test]
fn test_memory_safety_annotation() {
let checker = RustBorrowChecker::default();
let annotation = checker.memory_safety_annotation();
assert_eq!(annotation.property_proven, PropertyType::MemorySafety);
assert_eq!(annotation.method, VerificationMethod::BorrowChecker);
assert_eq!(annotation.confidence_level, ConfidenceLevel::High);
assert_eq!(annotation.tool_name, "rustc-stable");
}
#[test]
fn test_thread_safety_annotation() {
let checker = RustBorrowChecker::default();
let annotation = checker.create_thread_safety_annotation();
assert_eq!(annotation.property_proven, PropertyType::ThreadSafety);
assert_eq!(annotation.method, VerificationMethod::BorrowChecker);
assert_eq!(annotation.confidence_level, ConfidenceLevel::High);
}
}
#[cfg_attr(coverage_nightly, coverage(off))]
#[cfg(test)]
mod property_tests {
use proptest::prelude::*;
proptest! {
#[test]
fn basic_property_stability(_input in ".*") {
prop_assert!(true);
}
#[test]
fn module_consistency_check(_x in 0u32..1000) {
prop_assert!(_x < 1001);
}
}
}