On switch statements Pascal Cuoq on 28 February 2011
In Carbon 20110201 and earlier versions of Frama-C, if you do not use precautions when analyzing a program with switch statements, you get imprecise results. Consider the example program below. main(int argc, char **argv){ switch(argc){ case 1: Frama_C_show_each_no_args(argc); break; case 2: Frama_C_show_each_exactly_2(argc); /* fall through */ case 3: Frama_C_show_each_2_or_3(argc); break;...
Read More