The bounds widening for pointers to null-terminated arrays relies on flow-sensitive bounds declarations for widening bounds using strlen. Currently the bounds widening is unsound because the flow-sensitive bounds declarations are not checked or used. We should implement flow-sensitive bounds checking. The implementation can be done in 4 stages:
The bounds widening for pointers to null-terminated arrays relies on flow-sensitive bounds declarations for widening bounds using
strlen. Currently the bounds widening is unsound because the flow-sensitive bounds declarations are not checked or used. We should implement flow-sensitive bounds checking. The implementation can be done in 4 stages:_Whereclauses: Check bounds declarations in where clauses #1209