--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on November 2016 ---
Dear all, I'm using Frama-C value analysis on some library code using function pointers. A simplified version looks like this: File "fctptr.c": 1 2 int f1(void) { return 1; } 3 int f2(void) { return 2; } 4 5 typedef int fct_t(void); 6 7 static fct_t *fct = f1; 8 int a = 1; 9 10 void setFct(int i) { 11 switch (i) { 12 case 1: fct = f1; return; 13 case 2: fct = f2; return; 14 default: return; 15 } 16 } 17 18 void foo(void) { 19 a += (*fct)(); 20 } I ran the command "frama-c -val -main foo -lib-entry fctptr.c" on that file, and got an output like this: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing fctptr.c (with preprocessing) [value] Analyzing an incomplete application starting at foo [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization a â [--..--] fct â {0} fctptr.c:19:[kernel] warning: pointer to function with incompatible type. assert \valid_function(fct); [value] Recording results for foo [value] done for function foo fctptr.c:19:[value] assertion 'Value,function_pointer' got final status invalid. [value] ====== VALUES COMPUTED ====== [value] Values at end of function foo: NON TERMINATING FUNCTION 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, although it is obvious that it contains &f1 or &f2 at any time (note that "fct" is declared "static"). I wonder if this may be considered a bug of value analysis, or if I missed some other command-line option enabling the "-lib-entry" behavior also on function pointers. If I omit option "-lib-entry", I get "fct â {{ &f1 }}", as expected. However, using "-lib-entry" should have resulted in a superset of values, shouldn't it? Best regards Jochen -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161103/e850124c/attachment.html>