Implicit array initialisation

[Novak756]

Hi, I was trying to run a program like

extern void __VERIFIER_error(void);

int main(){
    int arr[256];
    if(((arr)[((unsigned int) 149)]) == ((unsigned char) 249)){
	__VERIFIER_error();
    }
    return 0;
}

using default configuration. However symbiotic it did not find manage to find the error. Is there a flag that allows for arrays to be initialised implicitly, or do I have to run something like

for(int i = 0; i < ARRAY_SIZE; i++){
    array[i] = __VERIFIER_nondet_int();
}

and explicitly initialize arrays to random values?

Version is

version: 8.0.0-pre
LLVM version: 10.0.0
symbiotic            -> 7134bcf2c0688a1301f0bb71f3d768db5914afd7 (Release)
dg                   -> fec223486f67a51915c64775ac8e0c226c9f703d (Release)
sbt-slicer           -> 85c8cb482fecdd065329a55551bae93af2408c7b (Release)
sbt-instrumentation  -> d0251925f23cb0b0faff204ba3f3662b94bef440 (Release)
klee                 -> a549d22eff3df86710a2b618e8cee889ddc01e6e (Release)

[mchalupa]

What command did you use to run Symbiotic? If you used the --sv-comp flag, then the automatic initialization of uninitialized memory was turned off (https://github.com/staticafi/symbiotic/blob/main/lib/symbioticpy/symbiotic/options.py#L122). The relevant command-line option is --explicit-symbolic, but it turns off this feature. I do not think there is currently a way to use --sv-comp and turn off --explicit-symbolic. To get the desired behavior, you must modify the line I referenced above. If you didn't use --sv-comp, then it is probably a bug.

[Novak756]

I ran it with the default settings, so without --sv-comp or --explicit-symbolic. It only found the bug when I explicitly initialized the array with nondet values.