-consider-external-array-access-unsafe
Remove the default assumption that external arrays of unspecified size can be safely accessed at any index
Syntax
-consider-external-array-access-unsafe
Description
-consider-external-array-access-unsafe
removes the default Code Prover assumption that external arrays of unspecified size can be safely accessed at any index. By default, because of this assumption, Code Prover shows green Out of bounds array index checks on external array accesses code despite their size being unknown. If you use this option, the same check is orange indicating that the access is not proven safe and requires manual
inspection.
If you are running an analysis from the user interface
(Polyspace® desktop products only), on the Configuration pane, you can
enter this option in the Other field. See Other
.
Examples
Run Code Prover on this example with and without the option.
extern int arr[]; int getFifthElement(void) { return arr[5]; }
The array access shows a green Out of bounds array index check without the option but an orange check with the option.