Spinroot

Hi again!, What im trying to do now is use the test driver to read from a .PRN file and input those values into the state machine. I inserted an array bounds error in the update method to see if spin will pick it up, after running pan.exe spin doesnt seem to find the error. My question is: does it look like my test driver correctly driving my code through its states?
one more thing would it be incorrect to use a large c_code{} statement to do the file input? doing it that way picks up the array bounds error.

c_decl{
\#include "header.h"
\#include <stdio.h>
\#include <stdlib.h>
extern void myFuncInitialize(myStr *inst)
extern void myFunc2Update(myStr *inst, int num)
extern void myFunc3(myStr *inst)
extern myStr structure;
extern myStr1 str
int inputValue;
int ig;
char inputValuesArray [2];
FILE *inputFile;
};
c_track "&structure" "sizeof(myStr)";
c_track "&str" "sizeof(myStr1)";
init
{        //READS IN VALUES FROM A .PRN FILE AND INPUTS THEM TO THE STATE MAHCINE
    c_code
        {               
        inputFile = fopen("input.prn","r");
        myFunc1Initialize(&structure); //INITIALIZES THE STATE MACHINE WITH DEFAULTS           
        };
        if
        :: c_expr { (inputFile != NULL)} -> do::c_expr{(!feof(inputFile))} ->  c_code  {
                                                                                fgets(inputValuesArray,20,inputFile);
                                                                                ig = 0;
                                                                                        };
            do::c_expr{ig <=2} -> c_code {
                inputValue = inputValuesArray[ig];                   
                    switch (ig)
                {                   
                    break;                                   
                    case 1:   
                    structure.amount = (int)inputValue;
                    break;
                    case 2:    
                    structure.value = (int)inputValue;
                    break;               
                }   
                    ig++;
                myFunc2Update(structure,120);// UPDATES THE STATE MACHINE
                };
                :: else -> break
                od;
       
            c_code {
                    fclose(inputFile);
                   };   
        :: else ->  break
        od;
        ::else printf("cannot open file")
        fi;   
}