-consider-volatile-qualifier-on-fields)Примите, что квалифицированные поля структуры volatile могут иметь все возможные значения в любой точке в коде
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Укажите, что верификация должна учесть спецификатор volatile на полях структуры.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Verification Assumptions.
Командная строка: Используйте опцию -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 */
}
} |
В Коде С++ опция также применяется к членам класса.
Параметр: -consider-volatile-qualifier-on-fields |
| Значение по умолчанию: 'off' |
Пример (программа автоматического доказательства кода): |
Пример (сервер программы автоматического доказательства кода): |