--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on December 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Following execution through function pointer



> If you intend to use a plugin that do not support function
> pointers, I'd suggest that you take advantage of the information
> computed by Value Analysis in order to generate the possible cases,
> instead of an external pre-processor. In the easiest case, where each
> function pointer points to a unique function, you just have to call the
> semantic constant folding plug-in to get rid of them.

This looks like this. Original:

int printf(const char *f, ...);

void func1(void)
{
  printf("boo!");
}

void func2(void)
{
  printf("bah");
}

int main() {

        void (*myFunc)();

        myFunc = &func1;

        if (myFunc == &func1) { func1();} else
        if (myFunc == &func2) { func2();} else
        { printf("unhappiness\n"); exit(0); }


        myFunc = &func2;

        if (myFunc == &func1) { func1();} else
        if (myFunc == &func2) { func2();} else
        { printf("unhappiness\n"); exit(0); }

}

$ frama-c -scf t.c

/* Generated by Frama-C */
/*@ assigns \at(\result,Post) \from *f; */
extern int printf(char const *f , ...);
void func1(void)
{
  printf("boo!");
  return;
}

void func2(void)
{
  printf("bah");
  return;
}

extern int ( /* missing proto */ exit)(int x_0);
int main(void)
{
  int __retres;
  void (*myFunc)();
  myFunc = (void (*)())(& func1);
  if (1) { func1(); }
  else {
    if (myFunc == & func2) { func2(); }
    else {
      printf("unhappiness\n");
      exit(0); }
  }
  myFunc = (void (*)())(& func2);
  if (0) { func1(); }
  else {
    if (1) { func2(); }
    else {
      printf("unhappiness\n");
      exit(0); } }
  __retres = 0;
  return (__retres);
}

The value of variable myFunc has not been replaced inside the if
conditions that were unreachable. Hopefully that won't be an issue.