ISO C++ forbids flexible array member ‘literals’

[Geremia]

I get tons of ISO C++ forbids flexible array member ‘literals’ warnings when building 1.9.5 or 2.0.0-rc.6.
For example:

In file included from /tmp/SBo/cbmc-cbmc-5.95.1/build/cadical-src/src/internal.hpp:55,
                 from /tmp/SBo/cbmc-cbmc-5.95.1/build/cadical-src/src/clause.cpp:1:
/tmp/SBo/cbmc-cbmc-5.95.1/build/cadical-src/src/clause.hpp:114:7: warning: ISO C++ forbids flexible array member ‘literals’ [-Wpedantic]
  114 |   int literals[];
      |       ^~~~~~~~

My GCC version:

$ g++ -v
Lecture des spécifications à partir de /usr/lib64/gcc/x86_64-slackware-linux/13.2.0/specs
COLLECT_GCC=g++
COLLECT_LTO_WRAPPER=/usr/libexec/gcc/x86_64-slackware-linux/13.2.0/lto-wrapper
Cible : x86_64-slackware-linux
Configuré avec: ../gcc-13.2.0/configure --prefix=/usr --libdir=/usr/lib64 --mandir=/usr/man --infodir=/usr/info --enable-shared --enable-bootstrap --enable-languages=ada,c,c++,d,fortran,go,lto,m2,objc,obj-c++ --enable-threads=posix --enable-checking=release --enable-objc-gc --with-system-zlib --enable-libstdcxx-dual-abi --with-default-libstdcxx-abi=new --disable-libstdcxx-pch --disable-libunwind-exceptions --enable-__cxa_atexit --disable-libssp --enable-gnu-unique-object --enable-plugin --enable-lto --disable-install-libiberty --enable-gnu-indirect-function --with-linker-hash-style=gnu --with-gnu-ld --with-isl --verbose --with-arch-directory=amd64 --disable-gtktest --disable-werror --enable-clocale=gnu --enable-multilib --target=x86_64-slackware-linux --build=x86_64-slackware-linux --host=x86_64-slackware-linux
Modèle de thread: posix
Algorithmes de compression LTO supportés: zlib zstd
gcc version 13.2.0 (GCC)

[a1880]

Have you seen the comment in lines 105..111 of clause.hpp?

  // However, it turns out that even though flexible array members are in
  // C99 they are not in C11++, and therefore pedantic compilation with
  // '--pedantic' fails completely. Therefore we still support as
  // alternative faked flexible array members, which unfortunately need
  // then again more care when accessing the literals outside the faked
  // virtual sizes and the compiler can somehow figure that out, because
  // that would in turn produce a warning.

I am building Cadical using g++ 13.2 without any complaints.
g++ 11.4 under Ubuntu/WSL2 also works well.
It might help to update the development packages or to resort to

CXXFLAGS=-Wall -Wextra -O3 -DNDEBUG -DNUNLOCKED -DNFLEXIBLE

in your makefile.

[Geremia]

@a1880 I was able to get it to compile by removing -Werror, but I was wondering why these warnings are cropping up.

[m-fleury]

I am building Cadical using g++ 13.2 without any complaints.

Same here (gcc 12 and gcc 14). Can you share what you are compiling and how?

[Geremia]

@m-fleury In my OP, I give one example that throws this warning: compiling src/internal.hpp:55.

My CMAKE_CXX_FLAGS are: -O2 -fPIC -Wall -Wpedantic -Wno-deprecated-declarations -Wswitch-enum

[m-fleury]

We do not support cmake. I tried

$ ./configure CXX="g++ -O2 -fPIC -Wall -Wpedantic  -Wno-deprecated-declarations -Wswitch-enum"

and besides warning in mobical, I did not get any warning.

[Geremia]

@m-fleury Not in my case.

Doing this:

$ ./configure CXX="g++ -O2 -fPIC -Wall -Wpedantic -Wno-deprecated-declarations -Wswitch-enum"

and then make generates many of those warnings. Here's the full log: make.log

[arminbiere]

Can you try first with '-DNFLEXIBLE'? BTW, the idea is to split this into CXX and CXXFLAGS

CXX=g++ CXXFLAGS="-O2 -fPIC -Wall -Wpedantic -Wno-deprecated-declarations -Wswitch-enum -DNFLEXIBLE" ./configure

In 'configure' there is code to check for that. And that should avoid this issue and if the above worked I wonder, why it apparently did not in your case.

[Geremia]

@arminbiere Yes, that gets rid of the warning: ISO C++ forbids flexible array member ‘literals’ [-Wpedantic]. Now I just get these:

warnings: enumeration value ‘…’ not handled in switch [-Wswitch-enum]

/tmp/cadical/src/mobical.cpp: In function ‘bool CaDiCaL::is_basic(Call*)’:
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘INIT’ not handled in switch [-Wswitch-enum]
 2928 |   switch (c->type) {
      |          ^
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘SET’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘CONFIGURE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘PHASE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘ADD’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘DUMP’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘STATS’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘RESET’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘CONSTRAIN’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘CONNECT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘LEMMA’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘DISCONNECT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘TRACEPROOF’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘FLUSHPROOFTRACE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘CLOSEPROOFTRACE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘ALWAYS’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘CONFIG’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘BEFORE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘PROCESS’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘DURING’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:2928:10: warning: enumeration value ‘AFTER’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp: In function ‘bool CaDiCaL::has_lit_arg_type(Call*)’:
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘INIT’ not handled in switch [-Wswitch-enum]
 3182 |   switch (c->type) {
      |          ^
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘SET’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘CONFIGURE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘VARS’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘ACTIVE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘REDUNDANT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘IRREDUNDANT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘PHASE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘SOLVE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘SIMPLIFY’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘LOOKAHEAD’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘CUBING’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘VAL’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘LIMIT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘OPTIMIZE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘DUMP’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘STATS’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘RESET’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘CONNECT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘CONCLUDE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘DISCONNECT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘TRACEPROOF’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘FLUSHPROOFTRACE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘CLOSEPROOFTRACE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘ALWAYS’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘CONFIG’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘BEFORE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘PROCESS’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3182:10: warning: enumeration value ‘AFTER’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp: In member function ‘void CaDiCaL::Reader::parse()’:
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘VARS’ not handled in switch [-Wswitch-enum]
 3800 |       switch (c->type) {
      |              ^
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘ACTIVE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘REDUNDANT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘IRREDUNDANT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘RESERVE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘PHASE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘FIXED’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘FREEZE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘FROZEN’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘MELT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘LIMIT’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘OPTIMIZE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘DUMP’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘STATS’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘CONSTRAIN’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘TRACEPROOF’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘FLUSHPROOFTRACE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘CLOSEPROOFTRACE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘ALWAYS’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘CONFIG’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘BEFORE’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘PROCESS’ not handled in switch [-Wswitch-enum]
/tmp/cadical/src/mobical.cpp:3800:14: warning: enumeration value ‘AFTER’ not handled in switch [-Wswitch-enum]

[arminbiere]

What about no doing '-Wswitch-enum'?

[arminbiere]

The warnings are really spurious (as there is an explicit 'default'):

static bool is_basic (Call *c) {
  switch ((uint64_t)c->type) {
  case Call::ASSUME:
  case Call::SOLVE:
  case Call::SIMPLIFY:
  case Call::LOOKAHEAD:
  case Call::CUBING:
  case Call::VARS:
  case Call::ACTIVE:
  case Call::REDUNDANT:
  case Call::IRREDUNDANT:
  case Call::RESERVE:
  case Call::VAL:
  case Call::FLIP:
  case Call::FLIPPABLE:
  case Call::FIXED:
  case Call::FAILED:
  case Call::FROZEN:
  case Call::CONCLUDE:
  case Call::FREEZE:
  case Call::MELT:
  case Call::LIMIT:
  case Call::OPTIMIZE:
  case Call::OBSERVE:
    return true;
  default:
    return false;
  }
}

There is an easy way to squelch them by casting as (uint64_t)c->type though, but it looks to me that -Wswitch-enum gives spurious warnings.