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

Одно прошлое последний элемент массива. Например:

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
}