Re:Checked C
by ptspts on Tuesday June 14, 2016 @03:06PM
(#11904469)
Indeed, checkedc also introduces these 3 new pointer types (ptr, array-ptr and span). It also introduces invariants on variables, arguments and return values:
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.
Quoting from the paper (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.