[CN] Adjust output/printing for multiple errors

[dc-mak]

https://github.com/rems-project/cerberus/pull/474 and https://github.com/rems-project/cerberus/commit/e5a5131fbbe4ef8621a58993a9619d72fe93b163 added the ability to report multiple errors, which is very useful. However, the output is a little less structured as a result. Perhaps this won't matter so much because the primary way of interacting will be an LSP client, but fwiw here's a couple of small suggestions:

• use different colours for passing/failing function (or for --fail /--pass)
• interleave errors per function.

The function also serves as a progress bar through, so some care will need to be taken (perhaps rewriting/overwriting stdout mutably like dune does?)

Current:

16:40 ➜  cerberus git:(cn-vip-null) ✗ cn verify tests/cn/ptr_eq.c
[1/2]: f -- fail
[2/2]: main -- fail
tests/cn/ptr_eq.c:11:7: error: Unprovable constraint
  /*@ assert (ptr_eq(p, q)); @*/
      ^~~~~~~~~~~~~~~~~~~~~~
Constraint from tests/cn/ptr_eq.c:11:7:
  /*@ assert (ptr_eq(p, q)); @*/
      ^~~~~~~~~~~~~~~~~~~~~~
State file: file:///tmp/state__ptr_eq.c__f.html
tests/cn/ptr_eq.c:17:3: error: Unprovable constraint
  f(p);
  ^~~~
Constraint from tests/cn/ptr_eq.c:4:5:
    has_alloc_id(p);
    ^~~~~~~~~~~~~~~~
State file: file:///tmp/state__ptr_eq.c__main.html

Proposed:

16:40 ➜  cerberus git:(cn-vip-null) ✗ cn verify tests/cn/ptr_eq.c
[1/2]: f -- fail
tests/cn/ptr_eq.c:11:7: error: Unprovable constraint
  /*@ assert (ptr_eq(p, q)); @*/
      ^~~~~~~~~~~~~~~~~~~~~~
Constraint from tests/cn/ptr_eq.c:11:7:
  /*@ assert (ptr_eq(p, q)); @*/
      ^~~~~~~~~~~~~~~~~~~~~~
State file: file:///tmp/state__ptr_eq.c__f.html
[2/2]: main -- fail
tests/cn/ptr_eq.c:17:3: error: Unprovable constraint
  f(p);
  ^~~~
Constraint from tests/cn/ptr_eq.c:4:5:
    has_alloc_id(p);
    ^~~~~~~~~~~~~~~~
State file: file:///tmp/state__ptr_eq.c__main.html

Alternatively: One File to Rule Them All

[septract]

@samcowger

[samcowger]

Anyone with permission to do so can go ahead and assign this to me.

The function also serves as a progress bar through, so some care will need to be taken (perhaps rewriting/overwriting stdout mutably like dune does?)

If I understand this correctly, you're worried about interleaved errors polluting CN output such that users are unable to recognize progress indicators in the midst of error reporting. This is a valid concern, and exactly what --quiet attends to, which was implemented in #474 - it would silence rich error reporting and only report single-line pass/fail information per function.

[dc-mak]

No it was more that I don't know if it's possible/easy to report errors as they arise per function (i.e. it would be bad if users had to wait for the whole thing to finish before seeing any output when --quiet is not passed).