I was thinking for implementing borrow-checker like rules for C but after I have seen what SMT solver can do I think it is not necessary to constrain the language in this way.