Initialization of a flexible array member leads to cbmc crash or verification failure.

[andreast271]

CBMC version: cbmc-5.11, cbmc-5.11-1479-ga86978840
Operating system: Linux 4.15.0-45-generic x86_64 GNU/Linux
Exact command line resulting in the issue: cbmc ccb.c , cbmc ccb.c --smt2
What behaviour did you expect: all 4 assertions should pass
What happened instead: 2 assertions fail (SAT backend), CBMC crash (smt2 backend)

In the following code all assertions should be true:

#include <assert.h>
struct St {
  char c;
  int d[];
};
struct St s = {'a', {11, 5}};

int main () {
  unsigned char c;
  c = c && 1;
  assert(c==0 || c==1);
  assert(s.d[1]==5);
  s.d[1] += c;
  assert(s.d[1]<8);
  assert(s.d[0]==11);
}

With cbmc, the behavior depends on the solver backend. With the default SAT solver backend, assertions 3 and 4 are failing for both cbmc-5.11 and cbmc-5.11-1479-ga86978840:

** Results:
ccb.c function main
[main.assertion.1] line 11 assertion c==0 || c==1: SUCCESS
[main.assertion.2] line 12 assertion s.d[1]==5: SUCCESS
[main.assertion.3] line 14 assertion s.d[1]<8: FAILURE
[main.assertion.4] line 15 assertion s.d[0]==11: FAILURE

With the smt2 backend, cbmc crashes. With cbmc-5.11 the error message is:

converting SSA
cannot unpack struct with non-byte aligned components

With cbmc-5.11-1479-ga86978840 from the develop branch (rev a869788), the error message is:

converting SSA
map::at

[tautschnig]

Just adding that with --no-simplify the assertion s.d[1]==5 also fails. We need to make sure we work with the actual size in the back-end, not the one we infer from the type.

[Smattr]

Is there a work around for this? I hit something that looks like the latter failure (converting SSA map::at) when using the SMT2 back end on cbmc-5.12-d8598f8-1368-g5e956891d. My example does not use flexible array members and I have not attempted to minimise it, but can do so if you think it's a different issue.

[jackhumphries]

@Smattr Did you discover a workaround?

[Smattr]

No, I don't think so. IIRC at the time I was trying to do something involving a suite of verification tools, so I simply lent more heavily on one of the others to get the job done instead of CBMC.

[martin-cs]

Work arounds at the bottom of this comment:

#5297 (comment)

[tautschnig]

We probably have more than one bug around flexible array members. Likely we should consider introducing a dedicated type (or at least some annotation to the containing struct) to handle these.

[SaswatPadhi]

I think the crash with SMT backend might be fixed by #5904 (the PR is waiting for Z3 integration in CI).

[TGWDB]

Can confirm there is no crash with --smt2 and Z3.