by aw1621107 | 2025-09-24 18:31:40+00:00
> I was saying it just can be transferred, with a large "just".

I'm not really convinced it can be transferred at all, but I'm not convinced it can't be either. The "just" feels so large as effectively

> There is however a commitment from GCC, that every UB the compiler exploits must be reported by -fanalyzer, otherwise it's a compiler bug.

Huh, don't think I've heard that commitment before. Do you mean that the GCC devs intend for -fanalyzer to (eventually?) guarantee catching all exploitable UB (which would be... ambitious, to say the least), or that -fanalyzer is a best-effort analysis? The docs currently state the latter more or less ("It is neither sound nor complete: it can have false positives and false negatives.") but that doesn't necessarily rule out attempts to make it so later (though that feels like it should run into Rice's theorem and/or false positive rate issues and/or require code alterations).

The closest thing I heard of is something about Clang/LLVM aiming to catch all the UB it exploits using sanitizers, but that's done at runtime so it's a lot easier to be precise about what you catch.

> I think Frama-C is a modern program: https://frama-c.com/.

Ah. I suppose that counts, though I would probably describe Frama-C as more than just an ownership tracking program given its other capabilities. I guess it technically could fill the same niche as the borrow checker, though given its capabilities and what's needed to use it I think there's probably not a lot of practical overlap in use cases.

> Where I got to know the concept is SPlint: http://splint.org/

Haven't heard of that one before. It does look like it can provide (some?) similar capabilities, though perhaps not to the same level of soundness as what the borrow checker provides. From one of the papers linked on the website [0]:

> In real programs it is sometimes necessary to use weaker assumptions about memory use. The `owned` annotation denotes a reference with an obligation to release storage. Unlike `only`, however, other external references (marked with `dependent` annotations) may share this object. It is up to the programmer to ensure that the lifetime of a `dependent `reference is contained within the lifetime of the corresponding `owned` reference.

It's also not quite clear to me whether Splint can cover more "interesting" borrow checker cases like those involving named lifetimes or view structs, but given this is the first time I've heard of it I definitely don't have the experience or knowledge to say for sure.

> There are C APIs out there without the necessary documentation, but you can't actually use them, without either introducing leaks, use-after-free bugs or reading the source code.

Sure, and that's what makes analysis so practically difficult. Whole program analysis doesn't scale well, standard C doesn't have enough information for cheap inference, etc., etc.

> "it" means ownership tracking implementation intended for Rust in the frontend.

In that case I'm not sure if gccrs would provide the implementation you hope for since they currently plan on integrating rustc's borrow checker implementation as-is. I'm not aware of a desire to write an independent borrow checker implementation at the moment as well.

[0]: https://www.cs.virginia.edu/~evans/pubs/pldi96.pdf