use antigen::{antigen, presents};
#[antigen(
name = "get-unchecked-without-proof",
category = AntigenCategory::FunctionalCorrectness,
fingerprint = r#"any_of([body_calls("get_unchecked"), body_calls("get_unchecked_mut")])"#,
family = "panic-on-index",
summary = "A call to get_unchecked / get_unchecked_mut — the unchecked-indexing escape hatch whose out-of-bounds case is Undefined Behavior.",
references = ["https://doc.rust-lang.org/std/primitive.slice.html#method.get_unchecked"],
)]
pub struct GetUncheckedWithoutProof;
struct ToyBuf {
data: Vec<u8>,
}
impl ToyBuf {
fn get_unchecked(&self, i: usize) -> u8 {
self.data[i % self.data.len().max(1)]
}
}
#[presents(GetUncheckedWithoutProof)]
fn first_unchecked(buf: &ToyBuf, i: usize) -> u8 {
buf.get_unchecked(i)
}
#[presents(GetUncheckedWithoutProof)]
fn first_checked(v: &[u8], i: usize) -> Option<u8> {
v.get(i).copied()
}
fn main() {
println!("antigen panic-on-index example: see source for the affinity-pair.");
println!(
"Both siblings are #[presents]-marked, so audit lists both; the checked .get path is spared by the FINGERPRINT (it doesn't bind). To read the bind/spare side by side, see antigen/tests/stdlib_family_fingerprints.rs."
);
let buf = ToyBuf {
data: vec![1u8, 2, 3],
};
let _ = first_unchecked(&buf, 1);
let _ = first_checked(&buf.data, 1);
}