Usage of string format specifier in `__CPROVER_printf`?
Closed this issue · 0 comments
gleachkr commented
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!