FunctionCall(__BLAST_initialize_driver2.c())
true
Block(STATUS_SUCCESS = 0;STATUS_UNSUCCESSFUL = -1;lockStatus = 0;)
lockStatus==0
Block(Return(0);)
lockStatus==0
Skip
lockStatus==0
Block(IO_NO_INCREMENT@main = 3;devExt@main = &(devE);i@main = 0;)
And [,i@main==0,lockStatus==0]
Pred(i@main < 10000)
And [,i@main==0,lockStatus==0]
Block(a@main[ i@main ] = 0;i@main = i@main + 1;)
And [,lockStatus!=1,i@main<=1,i@main!=0,lockStatus==0]
Pred(i@main < 10000)
And [,lockStatus!=1,i@main<=1,i@main!=0,lockStatus==0]
Block(a@main[ i@main ] = 0;i@main = i@main + 1;)
And [,i@main<=2,lockStatus!=1,lockStatus==0]
Pred(i@main < 10000)
And [,i@main<=2,lockStatus!=1,lockStatus==0]
Block(a@main[ i@main ] = 0;i@main = i@main + 1;)
And [,i@main<=3,lockStatus!=1,lockStatus==0]
Pred(i@main < 10000)
And [,i@main<=3,lockStatus!=1,lockStatus==0]
Block(a@main[ i@main ] = 0;i@main = i@main + 1;)
And [,lockStatus!=1,lockStatus==0]
Pred(i@main >= 10000)
And [,i@main>3,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
FunctionCall(FSMLock())
And [,i@main>3,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Pred(lockStatus == 0)
And [,i@main>3,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Block(lockStatus = 1;)
And [,i@main>3,i@main>2,lockStatus==1,i@main>1,i@main!=0,lockStatus!=0]
Block(Return(0);)
And [,i@main>3,i@main>2,lockStatus==1,i@main>1,i@main!=0,lockStatus!=0]
Skip
And [,i@main>3,i@main>2,lockStatus==1,i@main>1,i@main!=0,lockStatus!=0]
Block(nPacketsOld@main = nPackets@main;request@main = * (devExt@main ).WriteListHeadVa;)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus==1,i@main>1,i@main!=0,lockStatus!=0]
Pred(request@main != 0)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus==1,i@main>1,i@main!=0,lockStatus!=0]
Pred(* (request@main ).Status != 0)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus==1,i@main>1,i@main!=0,lockStatus!=0]
Block(* (devExt@main ).WriteListHeadVa = * (request@main ).Next;)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus==1,i@main>1,i@main!=0,lockStatus!=0]
FunctionCall(FSMUnlock())
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus==1,i@main>1,i@main!=0,lockStatus!=0]
Pred(lockStatus == 1)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus==1,i@main>1,i@main!=0,lockStatus!=0]
Block(lockStatus = 0;)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Block(Return(0);)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Skip
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Block(irp@main = * (request@main ).irp;)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Pred(* (request@main ).Status > 0)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Block(* (irp@main ).Status = STATUS_SUCCESS;* (irp@main ).Information = * (request@main ).Status;)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
FunctionCall(SmartDevFreeBlock(r@SmartDevFreeBlock = request@main,))
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Block(Return(0);)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Skip
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Block(IO_NO_INCREMENT@main = 3;)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Pred(nPackets@main == nPacketsOld@main)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
FunctionCall(FSMUnlock())
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
Pred(lockStatus != 1)
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]
FunctionCall(errorFn())
And [,i@main>3,nPackets@main==nPacketsOld@main,i@main>2,lockStatus!=1,i@main>1,i@main!=0,lockStatus==0]