--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on November 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value analysis with "-lib-entry" on function pointers



Hello,

Le 2016-11-03 à 16:20, Jochen Burghardt a écrit :
> While option "-lib-entry" behaves on the int variable "a" as described
> in the value analysis manual (sect.5.2.3, p.58), it seems to have no
> effect on the function pointer variable "fct".  Moreover, the latter is
> analyzed to contain a null pointer initially,

Well, the manual states that "Global variables of pointer type contain
the non-deterministic superposition of NULL and of the addresses of
locations allocated by the analyzer." (p. 58) So NULL is expected, but
there should also be a second possible value for this pointer.

And what is puzzling me is that this second value never occurs. Even if
I modify foo() as follow and use command line :
  frama-c-gui -val -lib-entry -context-valid-pointers -main foo
function-pointer.c
"""
void foo(fct_t *fct) {
  a += (*fct)();
}
"""

Apparently, -context-valid-pointers as no effect in this case. In my
current understanding it should.

> although it is obvious
> that it contains &f1 or &f2 at any time (note that "fct" is declared
> "static").

It is obvious for you but not for the analyzer, at least with current
Value assumptions. ;-)

As a work-around for your issue and also to take into account your
assumption, I would use a driver calling in a non-deterministic way your
functions. Something like:
"""
#include "__fc_builtin.h"

int f1(void) { return 1; }
int f2(void) { return 2; }

typedef int fct_t(void);

static fct_t *fct = f1;
int a = 1;

void setFct(int i) {
  switch (i) {
  case 1: fct = f1;       return;
  case 2: fct = f2;       return;
  default:                return;
  }
}

void foo(void) {
  a += (*fct)();
}

void driver(int i) {
  while(Frama_C_interval(0,1)) {
    switch (Frama_C_interval(0,1)) {
    case 0:
      setFct(i);
      break;

    case 1:
      foo();
      break;

    default:
      //@ assert \false;
    }
  }
}
"""

Command line:
  frama-c -val -main driver function-pointer.c
gives:
"""
[value] ====== VALUES COMPUTED ======
[value] Values at end of function f1:
  __retres ∈ {1}
[value] Values at end of function f2:
  __retres ∈ {2}
[value] Values at end of function foo:
  a ∈ [2..2147483647]
[value] Values at end of function setFct:
  fct ∈ {‌{ &f1 ; &f2 }‌}
[value] Values at end of function driver:
  Frama_C_entropy_source ∈ [--..--]
  a ∈ [1..2147483647]
  fct ∈ {‌{ &f1 ; &f2 }‌}
"""

Best regards,
david