--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on November 2016 ---
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