Overview

Checked scopes provide a way for programmers to opt-in to bounds checking or memory-safety for a region of a program or an entire program. A program is memory-safe if pointers are only used to access memory within the bounds of objects.

In the Checked C extension, bounds checking and null pointer checking are tied to the type of a pointer or an array. _Array_ptr types have bounds checking and null checking, _Ptr types have null checking, and checked array types have bounds checking. We want a way to ensure that only checked pointers are used in a region of a program. Unchecked pointers are dangerous because they can corrupt memory, including memory that contains checked pointers. Type casts involving pointers are also dangerous because they can lead to memory corruption.

There are two kinds of checked scopes:

Memory-safe checked scopes are the default: they are designated by _Checked. They enforce bounds-checking and null checking by restricting the use of unchecked pointer and array types. They also restrict type casts that could lead to memory corruption.
A programmer may choose a lower level of checking by using bounds-checked checked scopes, designated by _Checked _Bounds_only. They only enforce bounds checking and null-pointer checking.

A checked scope can be declared:

Using a checked compound statement: _Checked { ... } or _Checked _Bounds_only { ... }.
Using a pragma: #pragma CHECKED_SCOPE on or #pragma CHECKED_SCOPE _Bounds_only. This can be used at the top-level of a file to make the rest of the file be in a checked scope. It can also be used within a compound statement, in which case it is in effect for the remainder of the scope.
As a declaration specifier on a function: extern _Checked int f(void) { ... } or extern _Checked _Bounds_only int f(void) { ... }. In this case, the declaration of the function's parameters, return type, and body are within a checked scope.

Examples

A function can be declared in a checked scope in the following ways. The checked scope enforces that the parameters and return types must be checked types or have bounds-safe interfaces:

#pragma CHECKED_SCOPE on
void f(_Array_ptr<int> p : count(len), int len);

_Checked void f(_Array_ptr<int>> p : count(len), int len);

A bounds-safe interface is OK:

_Checked void g(int *p : count(len), int len);

An unchecked pointer without a bounds-safe interface is not OK:

_Checked void g(int *p, int len);  // error.

A function can be defined in a checked scope in similar ways:

#pragma CHECKED_SCOPE on
void f(_Array_ptr<int> p : count(len), int len) { ... }

_Checked void f(_Array_ptr<int>> p: count(len), int len) { ... }

Checking

All checked scopes

In all checked scopes, unchecked pointer and array types are only allowed when used in a bound declaration with a bounds-safe interface.

The following is not allowed:

Declarations or uses of function without prototypes. A function prototype declares the expected types for arguments. In C, the function int f() is a function that has no prototype declared. For functions where no prototype is declared, arguments are passed at call sites based on their types. There could be a mismatch between the actual definition of a function and the arguments that are passed.
Declarations or uses of functions with variable numbers of arguments. Again, there is no way to guarantee that arguments are used at their correct type.
Not returning a value when is expected for a function.
Returning a value when none is expected for a function.
The _Assume_bounds_cast operator.

Memory-safe checked scopes

For memory-safe checked scopes, casts involving pointer types are restricted:

Implicit casts between void pointers and other pointer types are not allowed.
Casts between void pointer types and other pointer types are only allowed when the other pointer types do not point to data containing checked pointers. In other words, the pointer types must point to integers, floating-point numbers, or structs containing only integers and floating-point numbers.
Casts between different types are only allowed when those types are structurally identical with respect to checked pointers and bounds declarations on struct members.
Member of union types must meet the same structural identical requirements as casts between different types.

Saving and restoring checked scope state.

The checked scope state at a point in a program can be saved using #pragma CHECKED_SCOPE push. It can be restored using #pragma CHECKED_SCOPE pop. This is useful when writing header files that make declarations within a checked scope to enforce the presence of bounds-safe interfaces. The header files may be included in checked or unchecked scopes and should not alter the enclosing checked scope state.

Unchecked scopes

By default, the top-level scope of a file is an unchecked scope. In an unchecked scope, none of the restrictions of checked scopes apply. Any functions declared in an unchecked scope are by default unchecked as well

If code in a checked scope, needs to do an operation only allowed in a unchecked scope, an unchecked scope can be declared in the following ways:

As an unchecked compound statement: _Unchecked { ... }
Using a program: #pragma CHECKED_SCOPE OFF
As a declaration specifier on a function extern _Unchecked int f(void) { ...}

Examples

A function can be defined in a checked scope, yet the body of the function can remain unchecked for later conversion:

#pragma CHECKED_SCOPE off
void f(_Array_ptr<int> p : count(len), int len) _Unchecked { ... }

Syntax and static checking subtleties

The keywords _Checked and _Unchecked are treated as declaration specifiers unless they are followed by the [ or { tokens. They are only allowed as declaration specifiers on functions.

Limitations

Memory-safe checked scopes assume that memory management is done correctly, that is, there are no use-after-free errors. They also assume that concurrency is done correctly: data races when updating struct members could result in an update being torn: two members being updated by different threads, causing bounds information to become inconsistent.

Checked C Wiki