В этом примере показано, как Polyspace флаги do операторы вне макроса. Этот код использует указатель в do-while цикл. Завершающим условием является то, что указатель не является указателем на значение NULL.

#include<cstdint>
struct P
{
	int val;
	struct P* next;
};

void psKO(P*p)
{
	do              // Noncompliant
	{
		p = p->next;
	} while(p!=nullptr);
}

Этот код может аннулировать пустой указатель, потому что завершающее условие проверяется после выполнения do блок. Код также трудно считать, потому что условие завершения помещено в конец блока. Polyspace помечает do оператор.

Этот пример показывает, как Polyspace лечит do операторы в макросе. Рассмотрим этот код, где два макроса, SWAP и SWAP2 реализованы. SWAP использует do оператор в то время как SWAP2 не делает.

#include <cstdint>
//Compliant by exception 
#define SWAP(a, b) \
        do                         \
        {                          \
            decltype(a) tmp = (a); \
           (a) = (b);             \
           (b) = tmp;             \
       } while (0)

#define SWAP2(a, b)        \
       decltype(a) tmp = (a); \
       (a) = (b);             \
       (b) = tmp;

int main(void)
{
  uint8_t a = 24;
  uint8_t b = 12;

  if (a > 12)
//  SWAP2(a, b);  // Compilation Error
  SWAP(a, b);
return 0;
}

Эти два макроса предназначены для вызова как функции. Вы не можете использовать SWAP2 как функциональный макрос в if блок, потому что после расширения, только первый оператор выражения SWAP2 остается в пределах if блок. Это распад макроса меняет его смысл, и в этом случае вызывает ошибку компиляции. Решение этой проблемы состоит в том, чтобы заключить макрос в do-while заблокировать и поместить условие завершения как ложное. Такие вложенные макросы не могут быть разбиты и могут быть вызваны как функции. Polyspace не помечает do операторы в макросах.