--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on May 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Set global variables uninitialized at Value analysis start



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;
}