--- layout: fc_discuss_archives title: Message 3 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



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>