polyspace: best practice for stubbing functions that exit?

I'm not sure what the best practice is with respect to stubbing functions that exit/terminate the program. Consider a reboot() function rebooting the system. I can stub it as

void reboot(void)
{
   for (;;) {
      ;
   }
}

But that makes "for" a red NTC which I can't seem to make go away with "-known-NTC reboot". So I went with

#include <stdlib.h>
void reboot(void)
{
    exit(0);
}

This makes "exit" a dashed red underline, with a bubble comment saying "A problem occurs during the execution of call to function __polyspace__stdstubs.exit.".

How do I stub such a function without getting a red or other problematic statement?

Answer 1

[Alexandre De Barros]

Hi Tommy!

If a function exits the program, then by definition the call to this function will never return, and the program will not continue after this call. This is why Polyspace will flag an NTC check, indicating that if you call this function, your program will stop.

It is important to use this red check to understand for example why some code is unreachable:

 reboot(); // your function that exits the application. We have a red NTC here
 restart(); // problem: this function is not called !

If you stub your function without an NTC or NTL, then Polyspace will consider that, in the example above, the function restart() can be called, which is not true. So the results will not reflect the reality.

Please note also that Polyspace will propagate this check through the call tree and it is also very important to keep this NTC check.

Let's take another example with this function:

 int check(int status_code) {
  if (status_code > 10)
    reboot();
  else
    return 1;
 }

and later this code where we will suppose that my_status is set to an incorrect value:

 my_status = 11;  // oops, wrong value here!
 if (check(my_status)) {  
    ...
    // do something very important
 }

In the function check(), there will be an NTC on reboot(), but there will be another NTC on the call to check() because Polyspace knows that the function reboot() is going to be called since the parameter status_code is 11.

If reboot() was stubbed without an NTC, the call to check() with status_code equal to 11 would appear as ok. But in reality, this code will cause an unexpected reboot.

More information on this NTC check here.

Alex

[Tommy]

Thanks Alex for taking the time to answer. I understand that Polyspace needs to know about NTCs to spot unreachable code. The problem I face is that there is code that is perfectly ok to not terminate, like reboot(); I annotated it with a polyspace comment

void reboot(void)
{
    /* polyspace<RTE:NTL:Not a defect:Never returns.> */
    for (;;)
    {
        ;
    }
}

and this still causes the statistics in the Report.pdf Chapter "Polyspace Code Verification Summary" to contain a "red" error. I can filter all "Not a defect" in the Results Explorer. Is there a way to justify a red error in a way so it does not appear in the Report.pdf? I have a hard time explaining the customer why there is a red error.

[Alexandre De Barros]

Hi!

There is no way to justifiy a red check so it does not appear as a check. Using the annotation is indeed a solution, but if you want this red check not to appear in the report, then I suggest you to replace the forever loop by a call to exit in reboot(). A call to exit will indeed not give an NTC check but a red "indication" (dashed red).

Best regards,

Alex