Задайте функции завершения процесса
-termination-functions function1[,function2[,...]]
-termination-functions задает функции, которые ведут себя как выходная функция и прекращают работу вашей программы.function1[,function2[,...]]
Используйте эту опцию, чтобы задать функции завершения программы, которые объявлены, но не определены в вашем коде.
Если вы запускаете анализ из пользовательского интерфейса (Polyspace® только для продуктов), на панели Configuration, можно ввести эту опцию в поле Other. См. Other.
Polyspace обнаруживает дефект Integer division by zero в следующем коде, потому что он не распознает это my_exit завершает программу.
void my_exit();
double reciprocal(int val) {
if(val==0)
my_exit();
return (1/val);
}
-termination-functions опция:polyspace-bug-finder -termination-functions my_exit