1. FunctionCall(__BLAST_initialize_driver1.c())

    true

  2. Block(STATUS_SUCCESS = 0;STATUS_UNSUCCESSFUL = -1;lockStatus = 0;)

    true

  3. Block(Return(0);)

    true

  4. Skip

    true

  5. Block(IO_NO_INCREMENT@main = 3;devExt@main = &(devE);i@main = 0;)

    true

  6. Pred(i@main >= 10000)

    true

  7. FunctionCall(FSMLock())

    true

  8. Pred(lockStatus != 0)

    true

  9. FunctionCall(errorFn())

    true