symbiotic
symbiotic copied to clipboard
A bug in checking undefined behavior
Symbiotic reports false(def-behavior)
for this program
int main() {
int array1[1];
int count;
for(count=0;count<1;count++) {
array1[count] = 0;
}
}
The command: symbiotic/bin/symbiotic --sv-comp --prp undefined --save-files --no-slice program.c
Symbiotic version: SV-COMP 2022 (the official archive)
This program probably triggers the same bug - undefined
behavior is reported.
int main() {
int c = 0;
int arr[1];
arr[c] = 42;
return 0;
}