AstraVer Toolset » Deductive Verification Tools for Linux Kernel

For instance, for such the examples:

typedef short unsigned int wchar_t;
wchar_t *abc, *empty;
abc = L"ABC";
empty = L"";

it outputs something like

typedef short unsigned int wchar_t;
wchar_t *abc, *empty;
abc = L"A" "B" "C";
empty = L;

(if the former is acceptable, the latter is an obvious bug).

I did not investigate if the issue exists with different options, but at least it exists for "-machdep gcc_x86_64 -c11 -short-wchar" (other options are not likely relevant).