printf inside non-executed conditional branch is printed anyway

[noresistence]

This makes debugging even harder than it is already:

A printf inside an if condition is printed anyway, no matter if the condition is true or false.

Example

inputs

1

example.c

struct In { int in; }; // This should be 1
struct Out { int out; };

void compute(struct In *input, struct Out *output) {
    if(input->in > 42) {
        printf("This should not be printed.");
        output->out = 40;
    }
    output->out = input->in;
}

console output during proof

NUMBER OF CONSTRAINTS:  2
PRINTF in computation_p 0:
"This should not be printed."
reading proving key from file...
[...]

output after execution of proof

0
1

[maxhowald]

Thanks for reporting this! Unfortunately, Pepper's printf implementation is a bit primitive, so this is expected behavior. I've added a bit of documentation on the limits in printf.txt.

Of course, it would be nice to improve the implementation, but I don't have much time to take this on myself at the moment. If you (or anyone else) is interested, we're always happy to accept pull requests though! Probably, this would require re-writing the way the frontend of the compiler emits PRINTF statements in the prover worksheet files, and the way the prover interprets these statements, to keep track of the conditionals at runtime.

[noresistence]

Thank you very much for adding the documentation, and also for the note on how to print numbers; I didn't stumble upon that bit yet. That will be helpful for debugging actual calculations :)