search

llvm / llvm-project

The LLVM Project is a collection of modular and reusable compiler and toolchain technologies.
http://llvm.org
Other
29.35k stars 12.13k forks source link

clang-format: Support CBMC-style annotations after signatures and loops #115265

Open hanno-becker opened 3 weeks ago

hanno-becker commented 3 weeks ago

Context: The C bounded model checker (CBMC) uses annotations of the following form to specify function contracts:

type function(...)
  REQUIRES(...)
  ASSIGNS(...)
  ENSURES(...)
;

Loop annotations are provided as follows:

for (...)
   ASSIGNS(...)
   LOOP_INVARIANT(...)
{
    ...
}

I looked through the existing clang-format attribute options, but could not find one that would not muddle with those annotations in these unusual places.

Ask: Provide a configuration option to clang-format similar to AttributeMacros which allows to designate macros as expected in the odd position as above, and cause them to not be touched by clang-format.

So far, we have to work around the issue by placing // clang-format on/off annotations everywhere, which is visually rather annoying.

hanno-becker commented 3 weeks ago

See https://github.com/pq-code-package/mlkem-c-aarch64/blob/main/mlkem/poly.c for various practical examples.