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

  • Subject: [Frama-c-discuss] Value analysis with "-lib-entry" on function pointers
  • From: jochen.burghardt at fokus.fraunhofer.de (Jochen Burghardt)
  • Date: Thu, 3 Nov 2016 16:20:06 +0100
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>