-consider-volatile-qualifier-on-fields)Предположим, что volatile квалифицированные поля структуры могут иметь все возможные значения в любой точке кода
Этот параметр влияет только на анализ программы проверки кода.
Укажите, что проверка должна учитывать volatile квалификатор для полей структуры.
Пользовательский интерфейс (только для настольных ПК): в конфигурации проекта эта опция доступна в узле Проверочные допущения.
файл командной строки и параметров: Использовать параметр -consider-volatile-qualifier-on-fields. См. раздел Сведения о командной строке.
volatile квалификатор переменной указывает, что значение переменной может изменяться между последовательными операциями, даже если оно не было явно изменено в коде. Например, если var является volatile переменная, последовательные операции res = var; res =var; может привести к двум различным значениям var считывается в res.
Используйте эту опцию, чтобы проверка эмулировала volatile квалификатор для полей структуры. При выборе этого параметра программа предполагает, что volatile поле структуры имеет полный диапазон значений в любой точке кода. Диапазон определяется только типом данных поля структуры.
НаПроверка рассматривает volatile квалификатор для полей структуры.
В следующем примере проверка считает, что поле val1 могут иметь все значения, допустимые для int введите в любой точке кода.
struct myStruct {
volatile int val1;
int val2;
};Даже при записи определенного значения в val1 и считывают переменную в следующей операции, считывание переменной приводит к любому возможному значению.
struct myStruct myStructInstance;
myStructInstance.val1 = 1;
assert (myStructInstance.val1 == 1); // Assertion can fail
Выкл. (по умолчанию)Проверка игнорирует volatile квалификатор для полей структуры.
В следующем примере проверка игнорирует квалификатор в поле val1.
struct myStruct {
volatile int val1;
int val2;
};При записи определенного значения в val1 и считывают переменную в следующей операции, считывание переменной приводит к этому конкретному значению.
struct myStruct myStructInstance;
myStructInstance.val1 = 1;
assert (myStructInstance.val1 == 1); // Assertion passesЕсли изменчивые поля не представляют значения, считанные с оборудования, и их значения не изменяются между последовательными операциями, отключите этот параметр. Вы используете volatile квалификатор по какой-либо другой причине, и при проверке не требуется учитывать полный диапазон значений поля.
Если этот параметр включен, количество красных, серых и зеленых чеков в коде может уменьшиться. Количество оранжевых чеков может увеличиться.
В следующем примере красный или зеленый чек изменяется на оранжевый или серый, когда используется опция. Учитывая volatile квалификатор изменяет цвет проверки. В этих примерах используется следующее определение структуры:
struct myStruct {
volatile int field1;
int field2;
};
| Цвет без опции | Результат без опции | Результат с опцией |
|---|---|---|
| Зеленый | void main(){
struct myStruct structVal;
structVal.field1 = 1;
assert(structVal.field1 == 1);
} | void main(){
struct myStruct structVal;
structVal.field1 = 1;
assert(structVal.field1 ==1);
} |
| Красный | void main(){
struct myStruct structVal;
structVal.field1 = 1;
assert(structVal.field1 != 1);
} | void main(){
struct myStruct structVal;
structVal.field1 = 1;
assert(structVal.field1 !=1);
} |
| Серый | void main(){
struct myStruct structVal;
structVal.field1 = 1;
if (structVal.field1 != 1)
{
/* Perform operation */
}
} | void main(){
struct myStruct structVal;
structVal.field1 = 1;
if (structVal.field1 != 1)
{
/* Perform operation */
}
} |
В коде C++ опция также применяется к членам класса.
Параметр: -consider-volatile-qualifier-on-fields |
| По умолчанию: Откл. |
Пример (проверка кода): polyspace-code-prover -sources |
Пример (сервер проверки кода): polyspace-code-prover-server -sources |