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