diffblue/cbmc

Usage of string format specifier in `__CPROVER_printf`?

Closed this issue · 0 comments

CBMC version: 5.91.0
Operating system: Linux, 22.04.1-Ubuntu
Exact command line resulting in the issue: cbmc --trace test.c where test.c is

int main(void) {
    __CPROVER_printf("results: %s, %d", "five", 5);
    assert(0);
}

What behaviour did you expect: I would have thought that this would print both "five" and "5" in the trace, something like:

** Results:
test.c function main
[main.assertion.1] line 3 assertion 0: FAILURE

Trace for main.assertion.1:
results: five, 5

Violated property:
  file test.c function main line 3 thread 0
  assertion 0
  (__CPROVER_bool)0



** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

What happened instead: Only "5" is printed.

** Results:
test.c function main
[main.assertion.1] line 3 assertion 0: FAILURE

Trace for main.assertion.1:
results: , 5

Violated property:
  file test.c function main line 3 thread 0
  assertion 0
  (__CPROVER_bool)0



** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

This is a minimal reproduction, extracted from a larger case. I expect that I'm missing some background on using __CPROVER_printf properly, but I wasn't able to figure it out from the documentation, and I didn't see any similar issues (this seems different) so I thought perhaps it was worth asking for clarification on what's going on here. Thanks for your help!