% 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
                       calling)

  • 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

...

• Vault

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