IKOS should tolerate snprintf(NULL, 0, ...)

[szhorvat]

ikos claims that the following C program is unsafe because of the null pointer passed to snprintf():

#include <stdio.h>

int main(void) {
    snprintf(NULL, 0, "%d", 123);
    return 0;
}

However, according to cppreference, when the second argument is 0, the first argument is allowed to be NULL.

https://en.cppreference.com/w/c/io/fprintf

If bufsz is zero, nothing is written and buffer may be a null pointer, however the return value (number of bytes that would be written not including the null terminator) is still calculated and returned.

We use this feature to determine the number of characters that would be written before actually writing them.

[ivanperez-keera]

I could be wrong, but at first glance I think we'd need to change:

ikos/analyzer/src/checker/null_dereference.cpp

Lines 335 to 338 in ae8200b

	case ar::Intrinsic::LibcSnprintf: {
	return {this->check_null(call, call->argument(0), inv),
	this->check_null(call, call->argument(2), inv)};
	}

so that this->check_null(call, call->argument(0), inv) is only included when this->_lit_factory.get_scalar(call->argument(1)); is not zero. There may be several cases that we'd have to consider, such as it not being zero but being a variable (which may contain the value zero) and so on.

[arthaud]

Maybe handling the special case of argument 1 being the 0 constant would be fine for now since that seems like a common use case.