Функции к тупику (-functions-to-stub)

Задайте функции к тупику во время анализа

Описание

Эта опция применяется, в основном, к анализу Программы автоматического доказательства Кода.

Задайте функции к тупику во время анализа.

Для заданных функций, Polyspace®:

  • Игнорирует функциональное определение, даже если оно существует.

  • Принимает, что входным параметрам функции и выходным параметрам позволил полный спектр значений их тип.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Inputs & Stubbing.

Командная строка: Используйте опцию -functions-to-stub. Смотрите информацию о Командной строке.

Почему использование эта опция

Если вы хотите, чтобы анализ проигнорировал код в теле функции, можно заблокировать функцию.

Например:

  • Предположим, что вы не завершили запись функции и не хотите, чтобы анализ рассмотрел тело функции. Можно использовать эту опцию, чтобы заблокировать функцию и затем задать ограничения на ее возвращаемое значение и модифицируемые аргументы.

  • Предположим, что анализ тела функции неточен. Анализ принимает, что функция возвращает все возможные значения, которые позволяет функциональный тип возврата. Можно использовать эту опцию, чтобы заблокировать функцию и затем задать ограничения на ее возвращаемое значение.

Настройки

Никакое значение по умолчанию

Введите имена функций или выберите из списка.

  • Щелкните, чтобы добавить поле и ввести имя функции.

  • Щелкните, чтобы перечислить функции в вашем коде. Выберите функции из списка.

При вводе имен функций используйте или базовый синтаксис или, чтобы дифференцировать перегруженные функции, синтаксис аргумента. Для синтаксиса аргумента, аргументов отдельной функции с точками с запятой. См. следующий код и таблицу для примеров.

//simple function

void test(int a, int b);

//C++ template function

Template <class myType>
myType test(myType a, myType b);

//C++ class method

class A {
	public:
	int test(int var1, int var2);
};


//C++ template class method

template <class myType> class A
{
	public:
	myType test(myType var1, myType var2);
};

Функциональный типБазовый синтаксисСинтаксис аргумента
Простая функцияtesttest(int; int)
Функция шаблона C++testtest(myType; myType)
Метод класса C++A::testA::test(int;int)
Метод шаблонного класса C++A<myType>::testA<myType>::test(myType;myType)

Советы

Опция более важна для анализа Программы автоматического доказательства Кода.

  • Программа автоматического доказательства кода делает предположения об аргументах и возвращаемых значениях заблокированных функций. Например, Polyspace принимает, что возвращаемые значения заблокированных функций являются полным спектром. Эти предположения могут влиять на регистрации других разделов кода. Смотрите Заблокированные Функции (Polyspace Code Prover).

  • Если вы блокируете функцию, можно ограничить аргументы множества значений функции и возвращаемое значение. Чтобы задать ограничения, используйте аналитическую опцию Constraint setup (-data-range-specifications).

  • Для функций C эти специальные символы являются allowed:( ) < > ; _

    Для функций C++ позволены эти специальные символы: ( ) < > ; _ * & [ ]

    Пробелы позволены для C++, но не допускаются функции C.

Информация о командной строке

Параметр: -functions-to-stub
Никакое значение по умолчанию
Значение: function1[,function2[,...]]
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -functions-to-stub function_1,function_2
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -functions-to-stub function_1,function_2