They’re deterministically detected at runtime. Any use of a pointer to an object that got freed will trap with a filc safety error, which terminates program execution and prints a backtrace.
I don’t think it’s possible to catch all use after frees at compile time precisely. Like, you could have a checker that catches all errors but also rejects valid programs or you can have a checker that accepts all valid programs but doesn’t find all the bugs. To be precise it has to be at runtime, and that’s what Fil-C does.
Memory safe languages aren’t about proving everything at compile time. Some version of a panic is going to be there, at a minimum for array bounds checking.
In Fil-C, if you don’t like the use after free panic, then just don’t call free and let the GC free your objects.
And if you’re doing safety critical stuff (I’m assuming that’s what you’re getting at) then the game is to prove that the system will be safe in the sense of not hurting people, not in the sense of memory safety. And that proof burden is much higher than the proof burden for memory safety.
I don’t think it’s possible to catch all use after frees at compile time precisely. Like, you could have a checker that catches all errors but also rejects valid programs or you can have a checker that accepts all valid programs but doesn’t find all the bugs. To be precise it has to be at runtime, and that’s what Fil-C does.