Undefined behavior in src/main.c: passing off_t expression to printf("%ld",

[pascal-cuoq]

The file src/main.c defines variable a offset of type off_t and prints it with %ld:

#include <sys/types.h>
…
#include <unistd.h>
…
    off_t pos, offset = 0;
…
#ifdef ERROR_TRACE_ENABLE
        printf("%05d %ld %d %s\n", -ret, offset, eaten, path);
#endif
        if (ret == 1) {
            eaten = 1;
            printf("not a sequence %ld %d\n", offset, num_certs);

While it's a good idea to use the POSIX type off_t to represent the result of a call to lseek, the function printf only accepts long arguments for the %ld format. If printf was not variadic, an implicit conversion would take place as per C11 6.5.2.2:7 (this is why cos(0) works despite 0 having type int, as long as the prototype for cos has been provided). But printf is variadic and the compiler does no conversion for the arguments after its first one. Instead, the behavior is undefined if the expression passed for %ld is not of type long.

Frama-C's value analysis should warn for type mismatches in printf, but of course you need to apply it to the file for it to warn about this UB.

[pascal-cuoq]

The header inttypes.h provides macros such as, for instance, PRIi32 to print a value of type int32_t which may be aliased to int, long, or something else. However POSIX provides no such facility for off_t. Instead I would recommend:

            printf("not a sequence %ld %d\n", (long)offset, num_certs);

This works at least as well as the original line. In general, the following works in more cases but requires including stdint.h:

            printf("not a sequence %jd %d\n", (intmax_t)offset, num_certs);