-consider-volatile-qualifier-on-fields)Предположим, что volatile поля квалифицированной структуры могут иметь все возможные значения в любой точке кода
Эта опция влияет только на анализ Code Prover.
Укажите, что верификация должна учитывать volatile квалификатор в полях структуры.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция доступна на узле Verification Assumptions.
Командная строка и файл опций: Используйте опцию -consider-volatile-qualifier-on-fields. См. «Информация о командной строке».
The volatile квалификатор переменной указывает, что значение переменных может меняться между последовательными операциями, даже если вы явным образом не изменяете его в коде. Для образца, если var является volatile переменная, последовательные операции res = var; res =var; может привести к двум различным значениям var считывание в res.
Используйте эту опцию, чтобы верификация эмулировала volatile квалификатор для полей структуры. Если вы выбираете эту опцию, программное обеспечение принимает, что volatile поле structure имеет полную область значений значений в любой точке кода. Область значений определяется только типом данных поля структуры.
НаВ верификацию рассматривается volatile квалификатор в полях структуры.
В следующем примере верификация считает, что поле val1 могут иметь все значения, разрешенные для int введите в любой точке кода.
struct myStruct {
volatile int val1;
int val2;
};Даже если вы записываете определенное значение в val1 и считайте переменную в следующей операции, переменная read приводит к любому возможному значению.
struct myStruct myStructInstance;
myStructInstance.val1 = 1;
assert (myStructInstance.val1 == 1); // Assertion can fail
Off (по умолчанию)Верификация игнорирует 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 */
}
} |
В коде С++ опция также применяется к членам класса.
Параметр: -consider-volatile-qualifier-on-fields |
| По умолчанию: Off |
Пример (Code Prover): Polyspace Code Prover -sources |
Пример (Код Prover Server): Полипространство -code-prover-server -sources |