Логические переменные заданы через _Bool ключевое слово в C (или bool макрос задан в stdbool.h) и bool ключевое слово на C++. Стандарт C (C99, Раздел 6.3.1.2) утверждает это, когда скалярное значение преобразовано в _Bool, результат 0, если значение равно 0; в противном случае результат равняется 1.
Code Prover придерживается технических требований стандарта C относительно Логических переменных. Например, анализ принимает, что, следуя за явными записями к Логической переменной из неизвестных источников, переменная может иметь значение 0 или 1.
Например, в этом примере, определении getFlag() неизвестно. После явного присвоения на переменную flag от getFlag() функция, переменная принята, чтобы иметь значение 0 или 1.
_Bool getFlag();
void main() {
_Bool flag = getFlag(); //flag is 0 or 1
//...
}В некоторых случаях Code Prover не принимает значение 0 или 1 для Логической переменной. Вместо этого анализ принимает, что переменная может иметь полный спектр значений, позволенных базовым типом (в большинстве случаев, unsigned char).
Например:
Если Логической переменной является volatile, это может быть изменено, например, с помощью периферийных устройств с отображенной памятью. Code Prover не принимает значение 0 или 1 для volatile Логические переменные.
_Bool func() {
volatile _Bool flag;
//...
return flag; //flag is in 0 .. 255
}Если Логическая переменная является частью объединения, это может быть изменено, например, путем изменения других членов объединения. Code Prover не принимает значение 0 или 1 для булевых членов объединения.
typedef union U {
int x;
_Bool flag;
} U;
_Bool func() {
U u;
u.x = 11;
return u.flag; //u.flag is in 0 .. 255
}