Этот пример показывает, как запустить динамические тесты на оранжевых проверках. Оранжевая проверка означает, что Polyspace® статическая верификация обнаруживает возможную ошибку, но не может доказать его. Оранжевые проверки могут произойти из-за:
Ошибки времени выполнения.
Приближения, что Polyspace сделан во время статической верификации.
Для получения дополнительной информации смотрите Оранжевые Регистрации Программы автоматического доказательства Кода.
Путем запущения тестов можно определить, какие оранжевые проверки представляют ошибки времени выполнения. При условии, что вы эмулировали среду выполнения точно, если динамический тест перестал работать, оранжевая проверка представляет ошибку времени выполнения. В данном примере сохраните следующий код в файле 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 в свой проект.
В настройке проекта, под Advanced Settings, выбирают Automatic Orange Tester.
После верификации Polyspace генерирует дополнительный исходный код, который тестирует каждую оранжевую проверку на ошибки времени выполнения. Программное обеспечение компилирует этот оснащенный код. Когда вы запускаете автоматический оранжевый тестер позже, программное обеспечение тестирует получившийся двоичный код.
Запустите верификацию и откройте результаты.
Оранжевая ошибка Division by zero появляется на операции 1.0/x.
Выберите Tools> Automatic Orange Tester.
В окне Automatic Orange Tester нажмите Start.
Автоматический Оранжевый Тестер запускает тесты на вашем коде. Если тесты занимают слишком много времени, используйте кнопку Stop All, чтобы остановить тесты. Уменьшайте Number of tests прежде, чем запуститься снова.
После того, как тесты завершаются, под AOT Results, просматривают количество Tests that detected run-time errors.
Оранжевая проверка Division by zero представляет ошибку времени выполнения, таким образом, вы видите отказы теста.
На вкладке Results кликните по строке, описывающей проверку.
Окно Test Case Detail показывает:
Операция, на которой были запущены тесты.
Тесты, которые перестали работать с причиной отказа.
Окно Automatic Orange Tester перечисляет переменные, которые вызывают оранжевые проверки. Поскольку Polyspace не имеет достаточной информации об этих переменных, это делает предположения об их области значений. Если вы знаете переменный диапазон, можно задать его прежде, чем запустить динамические тесты на оранжевых проверках. Для переменных указателя можно задать объем памяти, записанный через указатель. Например, если указатель указывает на массив, можно задать, записан ли первый элемент массива или целого массива через указатель.
В окне Automatic Orange Tester, на строке, описывающей r, нажимают Advanced.
В окне Edit Values, под Variable Values, выбирают Range of values.
Задайте минимальное значение 1 и максимум 9 для r. Автоматический Оранжевый Тестер сохраняет область значений как файл .tgf в папке Polyspace-Instrumented в вашей папке результатов.
Нажмите Start, чтобы перезапустить тесты на оранжевой проверке Division by zero на r в [1,9].
Деление на нуль не может произойти для r в [1,9], таким образом, нет никаких непройденных тестов. Несмотря на то, что непройденный тест указывает на ошибку времени выполнения для заданных входных параметров из-за конечного числа выполняемых тестов, отсутствие непройденных тестов не означает отсутствия ошибки времени выполнения.
Чтобы доказать, что ваша область значений преобразовывает оранжевую проверку в зеленую проверку, необходимо предоставить спектр во время другой статической верификации.
В окне Automatic Orange Tester выберите File> Export Constraints.
Сохраните свои области значений как текстовый файл.
Прежде, чем запустить следующую верификацию, на панели Configuration, под Inputs & Stubbing, предоставляют текстовый файл для Constraint setup.
Запустите верификацию и откройте ваши результаты.
Вместо оранжевого существует зеленый Division by zero, проверяют операцию 1.0/x.