search

diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
853 stars 265 forks source link

Allow loop annotations at the top of loop body #8481

Open hanno-becker opened 1 month ago

hanno-becker commented 1 month ago

Issue: CBMC currently requires loop annotations to be placed between for(...) and {...}. This is inconvenient for code that's subject to automatic formatting. For example, there is no option (I know of) for clang-format that would lead to a reasonable formatting of annotations. One can work around it by adding // clang-format: on/off annotations, but that adds to the visual load of the annotation themselves, and makes the code overall harder to read.

Ask: For CBMC to additionally support loop annotations be placed at the top of the loop body.

Continuing the example of clang-format, one could then mark the CBMC macros as statements, and they would be formatted in-line with the rest of the loop body.

hanno-becker commented 1 month ago

Ask 2: To additionally support function contracts be placed atop or below (either will be OK) function declarations in .h files.

(Reason is the same)

tautschnig commented 1 month ago

Ask 2: To additionally support function contracts be placed atop or below (either will be OK) function declarations in .h files.

(Reason is the same)

I must be misunderstanding as placing them below is exactly what we do right now? Could you please clarify?

hanno-becker commented 1 month ago

Here's an example of what we do at the moment: https://github.com/pq-code-package/mlkem-c-aarch64/blob/main/mlkem/reduce.h#L12

Are you saying we could move everything past the ; and it would be fine?