Indeed, checkedc also introduces these 3 new pointer types (ptr, array-ptr and span). It also introduces invariants on variables, arguments and return values:

Indeed, checkedc also introduces these 3 new pointer types (ptr, array-ptr and span). It also introduces invariants on variables, arguments and return values: Quoting from the paper (https://github.com/Microsoft/checkedc/releases/download/v0.5-final/checkedc-v0.5.pdf https://github.com/Microsoft/checkedc/releases/download/v0.5...): Reasoning about the correctness of programs with declared bounds sometimes requires reasoning about simple aspects of program behavior. To support this, lightweight invariants are added to Checked C. A lightweight invariant declares a relation between a variable and a simple expression using a relational operator. An example would be the statement x < y + 5. Lightweight invariants can be declared at variable declarations, at assignment statements, for parameters, and for return values. Checked C is extended with rules for checking these lightweight invariants. Just as type checking rules are defined by the programming language, so are rules for checking lightweight invariants. The checking of the correctness of programmer-declared bounds is integrated with the checking of invariants.