Instructions for the case loops_bad.c of CVE-2006-6876 of Verisec

• read README file
• try a commandline that includes the right directory for header and files:

frama-c-gui 
  -cpp-command "gcc -C -E -Ilib" lib/stubs.c
  programs/apps/OpenSER/CVE-2006-6876/fetchsms/loops_bad.c 
  -slevel 100 -val

• Find a problem:

…/loops_bad.c:31:… 
accessing uninitialized l-value answer[end]:…

• Notice that the benchmark uses “uninitialized” for “unknown” which is not compatible with value analysis:

  /* Input magically appears */
  answer[ANSWERSIZE-1] = EOS;

Change to:

  /* Input magically appears */

  /* In Frama-C you have to make it appear.
     uninitialized is not allowed */
  for (int i=0; i<ANSWERSIZE-1; i++)
    answer[i]=Frama_C_interval(0, 255);

  answer[ANSWERSIZE-1] = EOS;

• Do not forget to add ”…/share/builtin.c” to commandline since we are using Frama_C_interval() now.