Элемент массива.

Один из последних элементов массива. Для образца:

int arr[3];
int* res;
res = arr+3; // res points to one beyond arr

ptr + int_exp

int_exp + ptr

ptr - int_exp

ptr + +

++ ptr

-- ptr

ptr--

ptr [int_exp ]

Одиночные объекты, которые не являются частью массива, считаются массивами одного элемента. Например, в этом примере кода arr_one эквивалентно массиву из одного элемента. Polyspace^® не помечает шаг указателя ptr_to_one потому что он указывает на один за последним элементом arr_one.

void f_incr(int* x){
	int* ptr_to_one = x;
    ++ptr_to_one;  // Compliant
}

void func(){
	int arr_one=1; // Equivalent to array of one element
	f_incr(&arr_one);
}

Polyspace не помечает использование параметров указателя в арифметических операциях указателя, когда эти указатели указывают на массивы. Например, в этом фрагменте кода использование &a1[2] в f1 совместим, когда вы передаете массив в f1.

void f1( int* const a1){
       int* b= &a1[2]; // Compliant
}
void f2(){
	int arr[3] {};
	f1(arr);	
}

В структурах с несколькими элементами Polyspace не помечает результат арифметической операции указателя на элемент, который приводит к указателю, который указывает на другой элемент, если указатель указывает в выделенной памяти структуры или на один за последним элементом структуры.

Например, в этом фрагменте кода назначение ptr_to_struct соответствует, потому что остается внутри myStruct, даже если это указывает снаружи myStruct.elem1. Использование индекса, большего, чем размерность элемента, для доступа к содержимому этого элемента не соответствует, даже если полученный адрес находится в выделенной памяти структуры.

void func(){
	struct {
		char elem1[10];
		char elem2[10];
	} myStruct;
	
	char* ptr_to_struct = &myStruct.elem1[11]; //Compliant
      // Address of myStruct.elem1[11] is inside myStruct
      char val_to_struct = myStruct.elem1[11]; // Non-compliant
}

В многомерных массивах Polyspace помечает любое использование индексов, которые больше, чем размерность подрешетки, для доступа к элементу этой подрешетки. Polyspace не помечает назначение адреса того же элемента подрешетки, если адрес находится внутри выделенной памяти массива верхнего уровня.

Для примера в этом фрагменте кода назначение указателю ptr_to_arr совместим, потому что указатель указывает на адрес, который находится в выделенной памяти multi_arr. Назначение переменной arr_val не совместим, поскольку индекс, используемый для доступа к элементу подрешетки (3), больше размерности подрешетки (2).

void func(){
	int multi_arr[5][2];

      // Assigned memory is inside top level array
	int* ptr_to_arr = &multi_arr[2][3]; //Compliant

	// Use of index 3 with subarray of size 2
	int arr_val = multi_arr[2][3]; // Non-compliant
}

Polyspace помечает разыменование указателя, когда этот указатель указывает на один мимо последнего элемента массива. Например, в этом фрагменте кода назначение ptr соответствует, но дереферентство ptr не является. tab+3 один за последним элементом вкладки.

void derefPtr(){
	int tab[3] {};
	int* ptr = tab+3; //Compliant
	int res = *(tab+3); // Non-compliant
}