#![cfg_attr(coverage_nightly, coverage(off))]
use super::{PropertyTypeFilter, VerificationMethodFilter};
use crate::models::unified_ast::{
ConfidenceLevel, Location, ProofAnnotation, PropertyType, VerificationMethod,
};
use crate::services::proof_annotator::ProofAnnotator;
use anyhow::Result;
use std::path::Path;
pub struct ProofAnnotationFilter {
pub high_confidence_only: bool,
pub property_type: Option<PropertyTypeFilter>,
pub verification_method: Option<VerificationMethodFilter>,
}
include!("proof_annotation_helpers_filter.rs");
include!("proof_annotation_helpers_format.rs");
include!("proof_annotation_helpers_report.rs");
#[cfg_attr(coverage_nightly, coverage(off))]
#[cfg(test)]
mod tests {
#[test]
fn test_proof_annotation_helpers_basic() {
assert_eq!(1 + 1, 2);
}
}
#[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);
}
}
}