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]

[no subject]

Best regards
Jochen
________________________________________
From: Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] on behalf of Boris Yakobowski [boris at yakobowski.org]
Sent: Monday, November 7, 2016 6:40 PM
To: Frama-C public discussion
Subject: Re: [Frama-c-discuss] Value analysis with "-lib-entry" on function     pointers

Hi,

Thanks Jochen and David for the interesting bug report and subsequent investigations. The behavior for such an analysis has changed in Magnesium, the relevant Changelog being:

-! Value      [2015/04/13] In -lib-entry mode, functions pointers no longer
              force the generation of dummy functions. Instead, they are
              initialized to NULL. Fixes bug #!2104.

Previously, we used to generate a fresh function, and assign the pointer to the address of this new function. However, this was very limited, and problematic:
- there was no way to add a specification to the new functions, making the analysis quite imprecise afterwards
- the new functions were not really "in" the AST, leading to all sort of crashes in the other plugins (as those were unaware of Value's subtleties)

In particular, the initial contents of the pointer has never been used by Value. We could theoretically use the Value Top (⊤) to represent the contents of the pointer, but the analyzer would stop at the first call. Plus, we have tried very hard to avoid using Top (for various technical reasons).

I'm actually not sure of what should be done on this example, and I'm open to suggestions. At the very least, we will update the Changelog and possibly emit a warning. But no "natural" and general semantics come to mind.


On Sat, Nov 5, 2016 at 3:52 PM, David MENTRÉ <dmentre at linux-france.org<mailto:dmentre at linux-france.org>> wrote:
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<tel: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<tel:%5B1..2147483647>]
  fct ∈ {‌{ &f1 ; &f2 }‌}
"""

Best regards,
david

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gforge.inria.fr>
http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss



--
Boris