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

    i@main==0

  6. Pred(i@main < 10000)

    i@main==0

  7. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    And [,i@main<=1,i@main!=0]

  8. Pred(i@main < 10000)

    And [,i@main<=1,i@main!=0]

  9. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    i@main<=2

  10. Pred(i@main < 10000)

    i@main<=2

  11. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    i@main<=3

  12. Pred(i@main < 10000)

    i@main<=3

  13. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    i@main<=4

  14. Pred(i@main < 10000)

    i@main<=4

  15. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    i@main<=5

  16. Pred(i@main < 10000)

    i@main<=5

  17. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    i@main<=6

  18. Pred(i@main < 10000)

    i@main<=6

  19. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    i@main<=7

  20. Pred(i@main < 10000)

    i@main<=7

  21. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    i@main<=8

  22. Pred(i@main < 10000)

    i@main<=8

  23. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    i@main<=9

  24. Pred(i@main < 10000)

    i@main<=9

  25. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    i@main<=10

  26. Pred(i@main < 10000)

    i@main<=10

  27. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    i@main<=11

  28. Pred(i@main < 10000)

    i@main<=11

  29. Block(a@main[ i@main ] = 0;i@main = i@main + 1;)

    true

  30. Pred(i@main >= 10000)

    And [,i@main>11,i@main>10,i@main>9,i@main>8,i@main>7,i@main>6,i@main>5,i@main>4,i@main>3,i@main>2,i@main>1,i@main!=0]

  31. FunctionCall(FSMLock())

    And [,i@main>11,i@main>10,i@main>9,i@main>8,i@main>7,i@main>6,i@main>5,i@main>4,i@main>3,i@main>2,i@main>1,i@main!=0]

  32. Pred(lockStatus != 0)

    And [,i@main>11,i@main>10,i@main>9,i@main>8,i@main>7,i@main>6,i@main>5,i@main>4,i@main>3,i@main>2,i@main>1,i@main!=0]

  33. FunctionCall(errorFn())

    And [,i@main>11,i@main>10,i@main>9,i@main>8,i@main>7,i@main>6,i@main>5,i@main>4,i@main>3,i@main>2,i@main>1,i@main!=0]