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

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

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
}

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

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