Disable OOB checks during reachability calculations

[karoliineh]

Reachability computation in Base.reachable_from_addr uses the normal value read path via get_addr -> get_mval -> VD.eval_offset. For array-backed addresses, this goes through CArrays.get, which performs array OOB checks.

That is the wrong behavior for reachability: the analysis is only trying to inspect the immediate contents of a cell to discover embedded pointers, not to report an actual dereference. On zero-length VLAs this triggered array_oob_check during function-entry reachability handling. This was found using the dashboard comparison between Goblint and Mopsa and was exposed by the SV-COMP task ldv-memsafety/ArraysOfVariableLength2.c

Changes:

• Added a regression extracted from ldv-memsafety/ArraysOfVariableLength2.c
• Added an optional checkBounds flag to VD.eval_offset, threads it through get_mval and get_addr, and uses checkBounds=false specifically in reachable_from_addr. Normal semantic reads still keep bounds checks enabled.
• Unrelated to the discovered bug, also added ~checkBounds:false to all ValueDomain.CArrays.get calls within the functions that calculate reachability.

[sim642]

I wonder if the whole reachability calculation should just be under executing_speculative_computations and the OOB warnings suppressed when speculating, similarly to the overflow ones.

[michael-schwarz]

I wonder if the whole reachability calculation should just be under executing_speculative_computations and the OOB warnings suppressed when speculating, similarly to the overflow ones.

That sounds like a good idea!