That would be quite the surprise to me. Quite unfortunate that you can't find a source given what the -fanalyzer docs currently say.

> Any UB exploits not catched by -fanalyzer would need to be disabled.

I'd be curious as to the hypothetical performance impact of this, as well as the amount of work it'd take to make -fanalyzer reliable enough.

> When writing Frama-C what I was thinking of was actually PVS-Studio (https://pvs-studio.com/), as this can also be used by students. It's also more of a standalone linter.

Ah, that's quite different.

> Yes, this is an escape hatch, when the pointer shenanigans can't be fully described.

Ah, that's fair. Bit different than what Rust offers, but what you say makes sense.

> But I heard Rust also has those.

Sort of yes, sort of no. Rust has an escape hatch in `unsafe`, but it technically doesn't disable any checks - for example, the borrow checker will check the validity of references, bounds checks will continue to be inserted, etc. regardless of whether you're in an `unsafe` block or not. What it does instead is to give you the ability to perform `unsafe` operations, which for borrow checker-related shenanigans would typically involve dealing with pointers (to be specific, dereferencing them since some other pointer operations are considered safe) since the borrow checker doesn't check pointers.

> I don't know enough Rust, but from what I read at https://doc.rust-lang.org/book/ch10-03-lifetime-syntax.html, yes it does. Specifying that the 'lifetime' of the return value corresponds to a parameter happens with the `returned` annotation.

That's one of the things named lifetimes let you do, but named lifetimes are flexible enough for more than just that use case, from slightly more complex things like dealing with multiple independent lifetimes at the same time (for example, returning two references instead of just one, or structs/functions using multiple lifetimes), to more obscure stuff like dealing with higher-ranked trait bounds [1].

Kind of a tangent, but the manual is a bit unclear to me as to what `returned` is capable of. It states "The returned annotation denotes a parameter that may be aliased by the return value.", but that's immediately followed by "Splint checks the call assuming the result may be an alias to the returned parameter." And later in the example it states "Because of the `returned` qualifier, Splint assumes the result of `intSet_insert` is the same storage as its first parameter, in this case the storage returned by `intSet_new`."

Does `returned` require that the annotated parameter correspond exactly to the return value, or can a "subset" of the parameter be returned? In more concrete terms, would something like the following be accepted (assuming the access is in bounds, of course)?

    int *get_fifth(/*@returned*/ int *slice) {
        return &slice[4];
    }

    fn max<'a>(a: &'a i32, b: &'a i32) -> &'a i32 {
        if a > b { a } else { b }
    }

    int *max(/*@returned*/ int *a, /*@returned*/ int *b) {
        if (*a > *b) { return a; } else { return b; }
    }

In general, though, it does seem that Splint is able to describe many common patterns the borrow checker is also able to cover. I suspect the differences (in both directions) are probably only going to emerge for more complex use cases.

> You also can combine this with parameters, so you can say that param1.baz[0..param2] is writable and param1.baz[0..param3] is readable and also that readable param1.baz[0..X] and writable param1.baz[0..Y] always means that X > Y.

To be honest I don't quite follow, but I would guess that Rust isn't capable of anything similar since there isn't a way to describe properties for a subset of a slice in signatures.

> How much of these features can be written in Rust? (Honest question)

Assuming I'm understanding these correctly:

- owned: Typically represented via Box<T> or plain non-reference types.

- allocated, initialized, readable, writable: I believe these are generally handled via MaybeUninit [0] because everything is otherwise assumed to be properly initialized. Readable/writable might need &/&mut on top of MaybeUninit.

- Other properties: Might depend on the exact properties, but I think stuff like tainted input would usually be represented directly in the type system - in this example, taintedness would be types and transitions would be functions. There are at least two ways to implement that that I can think of right now. The first is via a simple newtype (might have syntax errors, but the gist should be clear):

    struct SafeUserString(String);
    struct UnsafeUserString(String);
    fn validate(s: UnsafeUserString) -> Result<SafeUserString, ValidationError> {
        if s.0.contains("/") {
            Err(ValidationError::InvalidChar)
        } else {
            Ok(SafeUserString{s.0})
        }
    }

    trait Safety {}
    struct Safe;
    impl Safety for Safe {}
    struct Unsafe;
    impl Safety for Unsafe {}
    struct UserString<S: Safety> { data: String }
    fn validate(input: UserString<Unsafe>) -> Result<UserString<Safe>, ValidationError> {
        // ...
    }
    fn op_that_does_not_care_about_safety<S: Safety>(input: UserString<S>) -> UserString<S> {
        // ...
    }

Basically a struct that contains a reference into data something else owns. Something like:

    struct ByteSlice<'a> {
        slice: &'a [u8]
    }

[0]: https://doc.rust-lang.org/beta/std/mem/union.MaybeUninit.htm...

[1]: https://doc.rust-lang.org/nomicon/hrtb.html