Frama-C Analyser revealed undefined behaviours in examples/api/main.c

[RadioPotin]

Undefined behaviours: possible NULL pointer dereference and non-standard declaration of VLA of size 0.

Hello,

I ran electionguard-c under Frama-C today and the analyser has revealed two possible undefined behaviours and/or non-standard practices in examples/api/main.c that I would like to report to you.

Null pointer dereferenced

https://github.com/microsoft/electionguard-c/blob/cc2b1be05a38673e523e427e0326eff9678812cb/examples/api/main.c#L102-L109

Here you can see that localtime() function may return a NULL pointer that gets dereferenced in the next call to snprintf()

Possible patch

Adding a ternary operator for each dereferencing of variable local_time in the call to snprintf checking the validity of that pointer and, if it isn't, passing a default value to snprintf() instead of invalid local_time:

sprintf(encrypted_output_prefix, "%s_%d_%d_%d", "encrypted-ballots", 
        (local_time ? local_time->tm_year + 1900 : -1), 
             (local_time ? local_time->tm_mon + 1 : -1),
                   (local_time ? local_time->tm_mday : -1));

VLA of size 0 is non-standard

https://github.com/microsoft/electionguard-c/blob/cc2b1be05a38673e523e427e0326eff9678812cb/examples/api/main.c#L255

The analyser has revealed that there exist execution traces where variable current_cast_index is equal to 0 when this statement is reached while ISO 9899:2011 6.7.6.2 states:

If the expression is a constant expression, it shall have a value greater than zero.

As I'm not very familiar with the code it would take me to much time to offer a decent possible fix, i felt you should know about it nevertheless.