I read the Cyclone papers when I designed the original Rust borrow checker, and we spoke to Dan Grossman.
Cyclone only works because it uses garbage collection for the heap. There is a uniqueness extension, but it is limited compared to what Rust can do. (See Grossman's "Existential Types for Imperative Languages" presentation for details.) The uniqueness extension was not designed to (and is not flexible enough to) supplant the garbage collector in most real-world projects.
This theoretical static checker for C code would not be compatible with virtually any existing C code in the wild, and so it would be effectively a new language.
Cyclone only works because it uses garbage collection for the heap. There is a uniqueness extension, but it is limited compared to what Rust can do. (See Grossman's "Existential Types for Imperative Languages" presentation for details.) The uniqueness extension was not designed to (and is not flexible enough to) supplant the garbage collector in most real-world projects.
This theoretical static checker for C code would not be compatible with virtually any existing C code in the wild, and so it would be effectively a new language.