Version 1.0 of the Checked C specification

Create Version 1.0 of the Checked C specification now that the design of the Checked C extension is complete.

• Make sure the specification matches what is in the compiler. An exception is flow-sensitive bounds declarations, which are still under development in the compiler. The specification clearly marks all other future work.
• Reorganize the specification so that it is easier to read.
  -- Put all the chapters that describe the language extension first and move the fairly technical chapters on checking bounds declarations to the end of the specification.
  -- Move the related work chapter and the rejected design choices chapter to the appendix. These are informational in nature, not normative, and do not need to be included in the body of the specification.

Version 0.9 of the Checked C specification

This is a minor update to the Checked C specification released on September 14th, 2021.

• Clarification in the Checked C specification about the policy for bounds checking when checked and unchecked pointers are mixed in assignment expressions.
• Documentation of the semantics of realloc.
• Documentation about the shift from mailing lists to GitHub Discussions.

Version 0.9 of the Checked C specification

This is a minor update to the Checked C specification that brings it into agreement with the compiler implementation.

• Update documentation for Where clauses.
• Update documentation for using function pointers.
• Update description of checking conditional expressions.
• Introduce read/write sets for bounds declaration checking.
• Include missing cases for bounds-safe interface assignments.
• Remove holds/suspends annotations for structures.
• Revamp bounds declaration checking rules for expressions with control-flow.
• Fix various typographical errors.

Version 0.7.1 of the Checked C specification

This is a minor update to the Checked C specification that brings it into agreement with the compiler implementation.

• Rename BOUNDS_CHECKED TO CHECKED_SCOPE.
• Update the syntax for bounds_cast expressions. Remove the old syntax where the kind of bounds expression was inferred based on the number of arguments. Now the target bounds expression is an additional argument.
• Allow an interop type and a bounds expressions as part of a bounds-safe interface.
• Make it clear that bounds-safe interfaces can be applied to unchecked arrays too.

Version 0.7 of the Checked C specification

The main improvement in Version 0.7 is adding support for checked strings and checked pointers to null-terminated arrays.

The improvements and changes include:

• Add types for checked null-terminated arrays (nt_checked) and checked pointers to null-terminated arrays (nt_array_ptr)
• Extend typing rules to allow string and array literals to be used where expressions with checked pointer types are expected.
• Require initializers for variables with checked pointer types or struct or array types that contain checked pointers.
• Describe handling of initializer expressions involving checked pointers.
• Revise rules for implicit conversions between checked pointer types. Allow conversions to/from void pointers for now.
• Change syntax for bounds cast operators.
• Remove span type.
• Rename bounds(none) to bounds(unknown).
• Describe static checking rules for return statements.
• Disallow array_ptrs of function types.
• Various wording clean ups.

Caveats:
A non-null value at the upper bound an nt_array_ptr allows the bounds of the nt_array_ptr to be widened. The flow analysis for widening bounds still needs to be described in detail.

Version 0.6 of the Checked C Specification

The improvements in Version 0.6 include:

• Better interoperation support. Bounds-safe interface types have been added to support nested levels of pointers at interoperation boundaries.
• Function pointer types with bounds information are now supported.
• Keywords are now backwards-compatible with existing C programs.
• The restriction on lexical hiding of variables have been removed.
• Restrictions on the use of functions without prototypes with checked code have been added.
• Definitions of type compatibility have been added.

Chapter 3 (bounds for variables) has been revised to be easier to follow. Sections have been reordered to follow more logically and advanced material that can be skipped has been moved to the end of the chapter.

Version 0.5 of the Checked C Specification

Version 0.5 of the Checked C Specification