How to avoid the error of dead code in the default branch of the switch statement

In C, some compilers require the default branch to be included in the switch statement. For polyspace, if the case already covers all switch conditions, it will throw a dead code error. How do I avoid dead code errors without using suppressed annotations

eg:

typedef enum

{

aaa,

bbb,

}value;

switch(value)

{

case aaa:

xxx;

case bbb:

xxx;

defualt:

xxxx; // this line will throw a Dead Code error

}

Answer 1

[Anirban]

The situation you show here is dead code, so Bug Finder will flag the issue.

If you turn off the checker for dead code, all dead code detection will be removed. You probably do not want that. You probably do not even want dead branches of switch statements to go undetected for all switch statements. So, you are really looking at a very specific situation here.

If you want to turn off the dead code checker only for specific cases, then you must mark/justify those cases in the code itself (or in the Polyspace results and have your justifications carry over to future analyses). You can add an annotation next to the dead code justifying the issue. For more information on the annotation syntax, see Annotate Code and Hide Known or Acceptable Results.

You also said that you had to enter the default branch to satisfy your compiler. Maybe you can indicate that in the code like this:

typedef enum
{
  aaa,
  bbb,
}value;
switch(value)
{
   case aaa:
           xxx;
   case bbb:
           xxx;
   #ifdef COMPILER_STRICT_MODE        
   default:
           xxxx;     
   #endif
}

When compiling your code, you can define the macro COMPILER_STRICT_MODE using a compiler option. But when analyzing the code with Polyspace, you can leave the macro undefined (that is, do not add any analysis option that defines this macro). Then, Polyspace will skip the code in between the #ifdef ... #endif directives.