Примечание
Автоматический оранжевый тестер будет удален в следующем выпуске.
В этом примере показано, как выполнять динамические тесты при проверке оранжевого цвета. Оранжевая проверка означает, что статическая проверка Polyspace ® обнаруживает возможную ошибку, но не может ее доказать. Проверка оранжевого цвета может происходить по следующим причинам:
Ошибки времени выполнения.
Аппроксимации, сделанные Polyspace во время статической проверки.
Дополнительные сведения см. в разделе Orange Checks in Code Prover.
При выполнении тестов можно определить, какие оранжевые проверки представляют ошибки времени выполнения. При условии точной эмуляции среды выполнения, если динамический тест завершается неуспешно, оранжевая проверка представляет ошибку времени выполнения. Для этого примера сохраните следующий код в файле test_orange.c:
volatile int r;
#include <stdio.h>
int input() {
int k;
k = r%21 - 10;
// k has value in [-10,10]
return k;
}
void main() {
int x=input();
printf("%.2f",1.0/x);
}
Примечание
Автоматический оранжевый тестер не поддерживается в Mac.
Создайте проект Polyspace. Добавить test_orange.c в ваш проект.
В конфигурации проекта в разделе «Дополнительные параметры» выберите «Автоматический оранжевый тестер».
После проверки Polyspace генерирует дополнительный исходный код, который проверяет каждую оранжевую проверку на наличие ошибок во время выполнения. Программное обеспечение компилирует этот инструментальный код. При последующем запуске автоматического оранжевого тестера программа проверяет полученный двоичный код.
Выполните проверку и откройте результаты.
В операции появляется оранжевая ошибка деления по нулю 1.0/x.
Выберите «Сервис» > «Автоматический оранжевый тестер».
В окне Automatic Orange Tester нажмите кнопку Start.
Автоматический оранжевый тестер запускает тесты для вашего кода. Если тесты занимают слишком много времени, нажмите кнопку Stop All (Остановить все), чтобы остановить тесты. Перед повторным запуском сократите число тестов.
После завершения тестов в разделе Результаты AOT просмотрите количество тестов, обнаруживших ошибки во время выполнения.
Orange Division by zero check представляет ошибку времени выполнения, поэтому вы видите сбои в тестовом примере.
На вкладке Результаты (Results) щелкните строку, описывающую проверку.
В окне «Test Case Detail» отображаются следующие данные:
Операция, в которой выполнялись тесты.
Провал тестовых случаев с причиной сбоя.
В окне Automatic Orange Tester перечислены переменные, вызывающие проверку оранжевого цвета. Поскольку Polyspace не имеет достаточной информации об этих переменных, он делает предположения об их диапазоне. Если диапазон переменных известен, его можно указать перед выполнением динамических тестов при проверке оранжевого цвета. Для переменных указателя можно указать объем памяти, записанной через указатель. Например, если указатель указывает на массив, можно указать, будет ли первый элемент массива или весь массив записан через указатель.
В окне Automatic Orange Tester в строке с описанием rнажмите кнопку «Дополнительно».
В окне Править значения в разделе Переменные значения выберите Диапазон значений.
Укажите минимальное значение 1 и максимальное значение 9 для r. Автоматический оранжевый тестер сохраняет диапазон как .tgf в файле Polyspace-Instrumented в папке результатов.
Нажмите кнопку Start (Пуск), чтобы перезапустить тесты оранжевой секции путем нулевой проверки для r в [1,9].
Деление на ноль не может произойти для r в [1,9], так что провалов тестов нет. Несмотря на то, что сбой теста указывает на ошибку времени выполнения для указанных входов, из-за ограниченного числа выполненных тестов отсутствие сбоев теста не означает отсутствие ошибки времени выполнения.
Чтобы доказать, что диапазон преобразует оранжевый чек в зеленый чек, необходимо указать диапазон во время другой статической проверки.
В окне Automatic Orange Tester выберите File > Export Constraints.
Сохраните диапазоны в текстовом файле.
Перед выполнением следующей проверки на панели Конфигурация (Configuration) в разделе Входы и заглушки (Inputs & Stubbing) укажите текстовый файл для настройки ограничения.
Выполните проверку и откройте результаты.
Вместо оранжевого существует зеленая проверка Division by zero на операции 1.0/x.