This article is an unpublished draft.

% Language Annotation

Validators (lint only)

  • ACSL; see Frama-C.
  • Linux Kernel's sparse; enables annotation of C to enforce certain rules at
                         compile time (e.g. tagging of address spaces on
                         pointers, tagging of functions to enforce rules for
    • Casting, Pointers & Integers
      • bitwise GCC-attribute. Warn about explicit or implicit casting to different types. Details
      • address_space(x) GCC-attribute, x is an integer designating an address space. Pointers are considered different types.
      • force GCC-attribute for forcing bad casts.
      • noderef GCC-attribute.
    • Functions & Function Calls
      • context(expr,in_c,out_c) GCC-attribute. expr must have value in_c when called and have value out_c when returning.
    • Fields of structs can be marked as requiring designated initializers using a GCC attribute designated_init.
    • More information


See also Language Research; some tools there are sufficiently powerful as to enable language annotation as a side effect.