-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.