search

rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
49 stars 25 forks source link

CN: ANSI escape codes in html output #235

Open peterohanley opened 4 months ago

peterohanley commented 4 months ago

...{Block&lt;unsigned int&gt;(member_shift&lt;instrumentation_state&gt;(state, reading) + i * 4u64)}(i.reading)</td><td>ESC[1munsupported quantified permissionESC[0m:...

Renders as: Screenshot 2024-04-25 at 4 13 26 PM

Looks like bad prettyprinter settings here? https://github.com/rems-project/cerberus/blob/c10d117797558ddb666462ac3811e76da261d87d/backend/cn/spans.ml#L162

peterohanley commented 4 months ago

And here's the opposite, HTML escape codes in terminal output:

void f(char *mode)
/*@ requires take state_in = each(u64 k; k < 1u64) {Owned< char>(array_shift(mode, k))};
    ensures true;
@*/
{
  for (char i = 0; i < 1; ++i)
  /*@ inv i <= 1u8;
          take mode_i = each(u64 j; (0u64 <= j) && (j < 3u64)) {Owned<int>(array_shift(mode, j))};
  @*/
  {
    char mod = mode[i];
  }
}

result:

guso@000492-guso src % cn escaped_html_in_output.c
[1/1]: f
other location (Dune__exe__Spans.model_res_spans)  warning: q-resource step disagrees with ctype size:
each(u64 j; (0u64 &lt;= j) && (j &lt; 3u64))
{Owned&lt;signed int&gt;(mode + j * 1u64)}

other location (Dune__exe__Spans.model_res_spans)  warning: q-resource step disagrees with ctype size:
each(u64 j; (0u64 &lt;= j) && (j &lt; 3u64))
{Owned&lt;signed int&gt;(mode + j * 1u64)}

escaped_html_in_output.c:6:3: error: Missing resource for entering loop pre-body
  for (char i = 0; i < 1; ++i)
  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
Resource needed: each(u64 j; (0u64 <= j) && (j < 3u64))
{Owned<signed int>(mode + j * 1u64)}
      escaped_html_in_output.c:8:16: (arg mode_i)
Consider the state in /var/folders/tz/g0kxkm2915xdtm6qgv8rff000000gp/T/state_9489d4.html

The error is about Owned vs Owned and is correct, it's just been escaped incorrectly.