Support for literal operator in C++ frontend

[vedadux]

Here is the toy example I wanted to parse:

#include <assert.h>
#include <stdint.h>

uint64_t operator"" _test(unsigned long long num) { return (uint64_t)num; }

int main(int argc, char* argv[])
{
    uint64_t x = 12345_test;
    assert(0);
    return 0;
}

CBMC version: 5.10
Operating system: Ubuntu 20.4
Exact command line resulting in the issue: cbmc --cpp11 main.cpp
What behaviour did you expect: success
What happened instead:

CBMC version 5.10 (cbmc-5.10) 64-bit x86_64 linux
Parsing main.cpp
file main.cpp line 4: parse error before ` _test ( unsigned'
file main.cpp line 4: parse error before `} int main ('
file main.cpp line 9: parse error before `( static_cast < bool'
file main.cpp line 10: parse error before `return 0 ; }'
file main.cpp line 11: parse error before `}'
PARSING ERROR
Numeric exception : 0

After looking into the cbmc C++ parser, It appears that the literal operator operator"" is not implemented, although it is part of the C++11 standard. As far as I know, there are two variants of how this is implemented in code. The first one, where a const char* or unsigned long long is converted, and the second one with templates going through each character of the literal recursively. It would be cool to support at least the first variant.

[tautschnig]

Thank you for calling this out. Our C++ front-end (even in versions much more recent than 5.10) has very incomplete C++-11 support, but it does help to have a better idea of which those missing aspects are.