| Issue |
115265
|
| Summary |
clang-format: Support CBMC-style annotations between after signature and loop
|
| Labels |
clang-format
|
| Assignees |
|
| Reporter |
hanno-becker
|
**Context:** The [C bounded model checker (CBMC)](https://github.com/diffblue/cbmc) uses annotations of the following form to specify function contracts:
```c
type function(...)
REQUIRES(...)
ASSIGNS(...)
ENSURES(...)
;
```
Loop annotations are provided as follows:
```c
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.
![]()
_______________________________________________
llvm-bugs mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-bugs
