[QUESTION] Initializing large arrays

[elsonkurian1991]

Let us suppose I have a large array and that I need to initialize it with inputs. It seems that the only way to do it is by explicitly initializing every member, e.g.

int x[100];
__CPROVER_INPUT("x[0]", x[0]);
...
__CPROVER_INPUT("x[99]", x[99]);

It would be nicer to do something like:

int x[100];
char name[10];
for (int i = 0; i < 100; ++i) {
    sprintf(name, "x[%d]", i);
    __CPROVER_INPUT(name, x[i]);
}

but this does not work (__CPROVER_INPUT accepts only string constants as names, and there is no model of sprintf anyways). Is there any way to initialize the members of an array in bulk?

[tautschnig]

Would you mind expanding on what you are trying to accomplish with this initialisation? I'd like to add two observations that make me ask this question:

1. The built-in is __CPROVER_input, not __CPROVER_INPUT.
2. If you use just int x[100]; without any further initialisation it will be set to non-deterministic values, and that might be all that you need?

[elsonkurian1991]

1. Yes, it is __CPROVER_input, it was a typo.
2. Just setting the 100 ints to nondeterministic input values is not enough, we need to give each input a distinct name. At the end of the analysis we need CBMC to generate test cases, and CBMC test cases use the name parameter of __CPROVER_input to identify the different values.
3. It is unclear to me one thing: If declaring a variable without assigning any value to it is enough for CBMC to initialize it with a symbolic input value, why do we need a __CPROVER_input call to do that explicitly?

[tautschnig]

Ok, so if you're doing test-input generation and you want to use --show-test-suite then __CPROVER_input is the right way to go (the sole purpose of __CPROVER_input is to report an input value, see https://www.cprover.org/cprover-manual/api/). There are three possible next steps:

• You just use the trace to generate input (perhaps consider building upon https://github.com/tautschnig/fshell-w2t to construct a full harness).
• You auto-generate that large sequence of __CPROVER_input calls.
• Someone propose a patch to make __CPROVER_input deal with arrays, or introduce a new built-in aimed at arrays.

[remi-delmas-3000]

Suggestion: add some primitive to print whole arrays in the test suites:

int main() {
  size_t size;
  char *arr = malloc(size);
  __CPROVER_input("size", size);
  // would result in the whole array being printed in the test vector
  __CPROVER_input_array("arr", arr, size); 
  program_under_test(arr, size);
}

[kroening]

I am so very tempted to add a proper array type, for modeling use only, of course.