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

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>
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]
> [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
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss




-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20161107/5702af5d/attachment.html>