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] Set global variables uninitialized at Value analysis start

  • Subject: [Frama-c-discuss] Set global variables uninitialized at Value analysis start
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Mon, 27 May 2013 16:39:55 +0200
  • In-reply-to: <CAC3Lx=ZT5n1iZ-oJZHGr2emVsNRd2HgoSaC+Tghn69Cj=UR0eA@mail.gmail.com>
  • References: <CAC3Lx=Zzm7DFwU_XEtn+u_p=18kgn-qFRQMp5VOpBqRs8PDZAw@mail.gmail.com> <E50756B2-BF80-4A38-AE62-AD3F4A70A264@cea.fr> <CAC3Lx=ZT5n1iZ-oJZHGr2emVsNRd2HgoSaC+Tghn69Cj=UR0eA@mail.gmail.com>
Hello,

2013/5/15 David MENTRE <dmentre at linux-france.org>:
>> As for changing the initial state of Value, this is possible but only programmatically.
>
> You mean, by modifying Frama-C source code or through a plugin.
> Probably more complicated but probably doable if really needed.

Well, I will apparently need this.

> I'll ask back at the original code's developer about his exotic
> developing environment and check the real needs.

I checked. In his development environment, some global variables are
indeed uninitialized at program start. So I need to mark them
"UNITIALIZED" (uninitialized) and not "[--..--]" (initialized to an
unknown value, done with -lib-entry).


I started to look at src/value/initial_state.ml in Fluorine 2 source
code but I am a bit lost in that code. I tried to change the code in
function "initialize_var_using_type" in the following way:
"""
      match typ with
      | TInt _ | TEnum (_, _)->
          bind_entire_loc Cvalue.V_Or_Uninitialized.uninitialized
"""

Above code does not compile because a value of type Cvalue.V.t is
expected and "uninitialized" is of type
"Cvalue.V_Or_Uninitialized.un_t".

I then used value "CValue.V.bottom". This time, the code compiles, but
when I launch value analysis on a simple program[1] I get:
"""
[value] Values of globals at initialization
        NOT ACCESSIBLE
[value] Value analysis not started because globals initialization is
not computable.
"""

So it is clear that I'm not doing the correct modification. :-)

Would somebody have a hint on kind of modification I should do into
order to get global variables uninitialized at program start?

Best regards,
david

[1]
int a = 0;
int g;

void main(void)
{
  int l;

  l = g;
  return;
}