Incorrect order when using {:ProgramInitialization} attribute

[garbervetsky]

I expected to use this attribute with a method to initialize my variables with my custom code. However AV instrument the code in a way that a global variables are reinitialized after invoking the method.

Suppose there is a method $initialize_globals() that is meant to initialize some variables. So my file example.bpl (see attached zip file) will include this code:

var global : int;
procedure {:ProgramInitialization} $initialize_globals();
implementation $initialize_globals()
{
   global := 1; 
   return;
}

The problem is that AV adds initialization code for the global variable just after my own initializer. For instance, example_inst.bpl look like this

...
implementation CorralMain()
{

  CorralMainStart:
    assume true;
    call $initialize_globals(); 
    call {:ConcretizeConstantName "global"} global := unknown_int();
    goto L_BAF_0;

  L_BAF_0:
    assume __block_call_Main;
    assume MustReach(true);
    call {:AvhEntryPoint} Main();
    return;
} 
...

I think the correct instrumentation will be adding the default intialization first and then my customized procedure.

example.zip

[shuvendu-lahiri]

@akashlal do you rely on the Initialization to be placed before the unknown initialization of inputs?

[akashlal]

Note that this a harness instrumentation issue (AVH), not an AV issue. AVH in general has been designed specific to the applications we have seen so far. The current usage of this feature was to set up the initial heap, not global variables. I would suggest just adding a flag to AVH to delay the call to this method.