Skip to content

Fix out-of-bounds bug in popl20-prod-cons-eq-wvr

Hernan Ponce de Leon requested to merge weaver-memsafety into main

The update array contains non-det values and is never overwritten. The array is read, and the obtained value is used to access the done array. Without checking that the index is smaller than the array size, this leads to an out-of-bound access.

Last year, ESBMC was the only tool detecting this bug.

Note about the milestone: this fix comes after the deadline, which means that this task needs to be excluded from SVCOMP 2025.

Merge request reports