In Polyspace, the source code has to be adapted to allow asynchronous tasks and interruptions to be taken into account. Without such adaptations, interrupt service routines will appear as grey (dead code) in the Viewer. The standard execution model is such that the main is executed initially. Only if the main terminates and returns control (i.e. if it is not an infinite loop and has no red errors) will the entry points be started, with all potential starting sequences being modeled automatically. There are several different approaches which may be adopted to implement the required adaptations.
As an example you can modify your main from:
void main (void)
{
int J = 0;
Init_globals(J);
while (1)
management();
}
to
void main (void)
{
int J = 0;
Init_globals(J);
}
void main_task (void)
{
while (1)
management();
}
So the main() function will terminate. Additionally you need to specify the new entry point like -entry-points "main_task"
