Switch-case blocks are not considered as branches by LTest

[dlonguet]

LTest does not consider switch-case blocks as branches (for criterion DC for instance), I think because Frama-C does not rewrite these blocks during preprocessing. It seems that while and for loops, as well as the conditional ternary operator are rewritten with if statements by Frama-C, and then annotated by LTest as branches.

Can it be considered using the option -simplify-cfg of Frama-C to normalize the switch-case blocks so that LTest would annotate their branches? Should it be a (yet another) SeaCoral configuration option?

[Stevendeo]

It seems reasonable to me for the -simplify-cfg to be used without adding another configuration option if it was added. I wonder though if it may have a bad effect on the exploration of other tools. The "simpified" CFG of the following example

#include <stdlib.h>
#include <stdio.h>

int f (int i, int j){
  switch(i){
  case 0: return j;
  case 1: j = 1; break;
  case 2: i = j;
  default: j = i; break;
  case 3: return i;
  }
  return 0;
}

has 9 gotos.

[Stevendeo]

I tried it in #69 and it does not change the tests significantly, so I'd be in favor to use this option by default without exposing any new configuration option. I'm a bit concerned about the growing difference between the original program and the tested program. @nberth any thoughts about this?