Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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