Spurious Invalid memory access
Description
Mopsa raises an invalid memory access error while it shouldn't.
Steps to reproduce
The issue happens on the following program when running mopsa-c with no parameters.
extern int nondet_number(void);
int main ( ) {
int a[100000];
int e = nondet_number();
int i = 0;
int j;
for ( j = 0 ; j < 100000; j++) {
a[j] = nondet_number();
}
while( i < 100000 && a[i] != e ) {
i = i + 1;
}
return 0;
}
This is a slightly simplified version of the SV Comp test standard_find_ground-1.i
What is the bug behavior?
I get the following error:
mopsa-bug.c:12.23-27: warning: Invalid memory access
12: while( i < 100000 && a[i] != e ) {
^^^^
accessing 4 bytes at offsets [4,400000] of variable 'a:./mopsa-bug.c:3.2-15' of size 400000 bytes
Callstack:
from ./mopsa-bug.c:2.4-8: main
What is the expected correct behavior?
No warning.
Possible cause or fix
It seems like Mopsa is not applying and operator laziness correctly.