Error with _SYM and array indexing (worked in 4.1.6)

[MichalDobes2]

Verification of the following code could be launched in 4.1.6 but in 4.1.20 and 4.2.0, verification fails with error.

ticket19.c:
#include <assert.h>
#include <rst/domains.h>
int main() {

int array[2];
_SYM int x;
array[1] = 42;
if ( x == 1 )

assert( array[x] == 42 );

return 0;

}

Alternatively:
#include <assert.h>
int VERIFIER_nondet_int();
int main() {

int array[2];
int x = VERIFIER_nondet_int();
array[1] = 42;
if ( x == 1 )

assert( array[x] == 42 );

return 0;

}

DIVINE 4.2.0 and 4.1.20+f2ee2f2c0505:
$ ~/tools/divine-4.2.0/_build.release/tools/divine verify --symbolic ticket19.c
compiling ticket19.c
loading bitcode … LART … E: Propagating through unsupported operation in sym domain:

%arrayidx1 = getelementptr inbounds [2 x i32], [2 x i32]* %array, i64 0, i64 %idxprom, !dbg !34610

Aborted (core dumped)

DIVINE 4, version 4.1.6+43d9a505081f:
$divine verify --symbolic ticket19.c
compiling ticket19.c
loading bitcode … LART … RR … constants … done
...
error found: yes
error trace: |

FAULT: conditional jump depends on an undefined value
[0] FATAL: control error in userspace

...

[mornfall]

This did not work ever -- making this fail explicitly, however, was part of the fix for #19. The problem here is that we do not support symbolic pointer offsets yet, but the code used to fail silently. Making this work is a fairly major feature, but it is on the TODO. (You can probably see that the error you get from 4.1.6 is spurious.)

[MichalDobes2]

Thank you for the explanation, I did not realize that.

Replying to mornfall:

This did not work ever -- making this fail explicitly, however, was part of the fix for #19. The problem here is that we do not support symbolic pointer offsets yet, but the code used to fail silently. Making this work is a fairly major feature, but it is on the TODO. (You can probably see that the error you get from 4.1.6 is spurious.)

[mornfall]

Milestone renamed