--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on May 2013 ---
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; }