% 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. Detailsaddress_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 valuein_c
when called and have valueout_c
when returning.
- Fields of structs can be marked as requiring designated initializers
using a GCC attribute
designated_init
. - More information
- Casting, Pointers & Integers
...
See also Language Research; some tools there are sufficiently powerful as to enable language annotation as a side effect.