<table border="1" cellspacing="0" cellpadding="8">
    <tr>
        <th>Issue</th>
        <td>
            <a href=https://github.com/llvm/llvm-project/issues/115265>115265</a>
        </td>
    </tr>

    <tr>
        <th>Summary</th>
        <td>
            clang-format: Support CBMC-style annotations between after signature and loop
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            clang-format
      </td>
    </tr>

    <tr>
      <th>Assignees</th>
      <td>
      </td>
    </tr>

    <tr>
      <th>Reporter</th>
      <td>
          hanno-becker
      </td>
    </tr>
</table>

<pre>
    **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.
</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJyEVFmPGjkQ_jXmpQRqDM3x0A_AhBVSMskOyb6ufFTT3jGulg8Y_v3KhkyGSTYrIVq26_iOskUI5uAQG1avWf0wECl25JtOOEdDieoZ_UCSvjSMrxhfbchFfIlssrqu4WuHwOr1BiQlp1HDkTRaUF1JBcYXm_WnDeNLVj8wvuhi7EPJ3jK-PZjYJTlSdGR8q03bSpuQ8a2SR8X4ElLAABlJFNGQC0AtxA6hJWvpbNwBWvJHiAShR2XaC7TJqRwKilz0QsXSrHpg1ff_WXX9qes6Xnp8zWJ8MRqNMthyBvD04c9vu6cP-_cHq_1-98fjT9vw4XH_7edwNlm_a_4W0Uei_o6k8Ai9p5PJcopwY_t_RFoqat_j-S-gHz9__vL37vGv1dNu9fj1Pdz5-jUf8sFt9-E3JHZgiZ5RQ-w8pUNXbMIXE2J2KaO0wh2G2S4R2awCEaM3MkUE6gttxjcgUwRFyWpwFKE1TgM5hNiJCOfX_WPS2iKcTcxtKOCdesbl3gEhuRSSsNBboTCM7rQrs7sKzz_m-MtVcBB5clpzSL7Uu6HLI_YLEsEcjRX-drr6TumTUJ5CDjh3RnUgin85SmO-bSIiHEtMthdfelQR9Q05kNbQUzClrwggJJ0wqyOcBiVSyIJgmfqshkSIlFSHGuTlFyDviO8JWuFzsTNCJ045F87kn0H4fH8LABNCwlwsK3ez73pf4W1tyPdlS21b7HzjAJ7QX84d-oL6KoEJcDLZDnsBL2KHvqRcjDuMBrqZ6OVkKQbYjOeTallPZws-6Jp2NpkpXXO-lBLnotJtu5jMqnFdq3aBWA9Mwys-HY-reTWdTqd8JHEsF6KaLUUtp0sxZ9MKj8LYkbWn44j8YVDINeNxzWf1wAqJNpSnj_M73TjPj6Fvct5QpkNg08qaEMOPStFEi81d1mQF-9T35CPkV28Y4sXeT6fEeEZ0INqIHq7DkDwWby1RP0jeNr95JHP322fYe_oHVWR8W0gFxrc3XqeG_xsAAP__D7DVeg">