The size of the first dimension is omitted when the array is defined.

[Elowen-jjw]

Example 1:

struct {
  char a3c;
  char a3p[];
} a3 = {'o', "wx"};

int main() {

  if (a3.a3p[0] != 'w') {
    abort();
  }
  if (a3.a3p[1] != 'x') {
    abort();
  }

  return 0;
}

Example 2:

#include<assert.h>

int a[][2][4] = {[2 ... 4][0 ... 1][2 ... 3] = 1, [2] = 2, [2][0][2] = 3};

int main(void) {
    assert( sizeof(a)/(sizeof(int)*2*4) == 5);
}

In the Example 1, run cbmc example1.c --bounds-check generate following output results:

[main.array_bounds.1] line 10 array 'a3'.a3p upper bound in a3.a3p[(signed long int)0]: FAILURE
[main.array_bounds.2] line 13 array 'a3'.a3p upper bound in a3.a3p[(signed long int)1]: FAILURE

In the Example 2, the assert() function is true, which is confirmed by compiling with gcc and clang, while cbmc gives the FAILURE result by running cbmc example2.c.

Is it related that the size of the first dimension is omitted when the array is defined?

CBMC version: 5.88.0 Operating system: Ubuntu 22.04, MacOS

[esteffin]

Hi, I think there is a bit of confusion here. gcc and clang are compilers and not program verifiers, so a program like the following:

#include <assert.h>
int main() {
  assert(0);
  return 0;
}

compiles successfully irregardless of assert(0).

CBMC instead is a bounded model checker that can be used for software verification. It tries to find if there is a configuration that fails one or more of the assertions in the analyzed software. In the example above running CBMC returns a FAILURE as any run of the compiled program WILL result in an assertion violation.

Again a slightly more complex program as the following:

#include <assert.h>

int main() {
  int x;
  assert(x != 0);
  return 0;
}

Can be successfully compiled with gcc or clang, and also some runs of it will succeed as the value of x is nondeterministically chosen, so it can be different than 0 (as it often is).

CBMC instead will still return FAILURE as there exist a value for x that fails the assertion (0 in this case).

In this case if you want CBMC to show the counterexample (the value of x that fails the assertion) add --trace to CBMC and you will see why and when the assertion failed.

In the second example above (say main.c) if you run cbmc --trace main.c it will show something as:

Runtime decision procedure: 0.000216876s
Building error trace

** Results:
main.c function main
[main.assertion.1] line 5 assertion x != 0: FAILURE

Trace for main.assertion.1:

State 11 file main.c function main line 4 thread 0
----------------------------------------------------
  x=0 (00000000 00000000 00000000 00000000)

Violated property:
  file main.c function main line 5 thread 0
  assertion x != 0
  !((signed long int)(signed long int)!(x != 0) != 0l)

** 1 of 1 failed (2 iterations)
VERIFICATION FAILED

Although this comment does not address the issue here, I will strongly suggest to run the program you posted with --trace first to see if the unexpected failure is a bug of CBMC or if it is indeed a valid FAILURE.

Also when you have the trace, you can plug the values of the trace in the code and see if the assertion is violated at runtime.

[Elowen-jjw]

Thanks for your advice, I will use this method to check my program carefully.