AstraVer Toolset » Deductive Verification Tools for Linux Kernel

Changed integral type selection for constants when in GCC compatibility mode (-machdep gcc_x86_*) (commit c0d393e8). Now Frama-C tries all available integral types to represent the constant, disregarding the specified LL postfix (as does GCC). The problem is that according to ISO (C11 / ISO/IEC 9899:201x), there are no negative integer constants and expressions such as -1 apply the unary minus operator to the value represented by the positive constant. Thus the constant 9223372036854775808LL cannot be represented as long long. Yet it can be represented as unsigned long long and later can be converted to long long, though in general the result in this case is implementation-defined.