#include <stdio.h>

unsigned search_cocos_brute (char *s, unsigned len)
{
        if (len<5)
                return len;       // not found
        for (unsigned i=0; i<len-4; i++)
        {
                if (s[i]=='c' &&
                                s[i+1]=='o' &&
                                s[i+2]=='c' &&
                                s[i+3]=='o' &&
                                s[i+4]=='s')
                        return i; // found
        };
        return len;               // not found
};

unsigned search_cocos_naive (char *s, unsigned len)
{
        if (len<5)
                return len;          // not found
        unsigned seen=0;
        for (unsigned i=0; i<len; i++)
        {
                char ch=s[i];        // this is single read operation
                if (seen==0 && ch=='c')
                        seen=1;
                else if (seen==1 && ch=='o')
                        seen=2;
                else if (seen==2 && ch=='c')
                        seen=3;
                else if (seen==3 && ch=='o')
                        seen=4;
                else if (seen==4 && ch=='s')
                        return i-4;  // found
                else
                        seen=0;      // reset
        }
        return len;                  // not found
};

unsigned search_cocos_fixed (char *s, unsigned len)
{
        if (len<5)
                return len;          // not found
        unsigned seen=0;
        for (unsigned i=0; i<len; i++)
        {
                char ch=s[i];        // this is single read operation
                if (seen==0 && ch=='c')
                        seen=1;
                else if (seen==1 && ch=='o')
                        seen=2;
                else if (seen==1 && ch!='o')
                {
                                     // we can be here if the input is 'ccocos'
                        if (ch=='c')
                                seen=1;
                        else
                                seen=0;
                }
                else if (seen==2 && ch=='c')
                        seen=3;
                else if (seen==3 && ch=='o')
                        seen=4;
                else if (seen==3 && ch!='o')
                {
                        // if input='coccocos'
                        if (ch=='c')
                                seen=1;
                        else
                                seen=0; // reset
                }
                else if (seen==4 && ch=='s')
                        return i-4;  // found
                else if (seen==4 && ch!='s')
                {
                        // the input string is 'cocoX' where X is not 's'
                        // (current state of ch='X')
                        // but 'X' could be 'c' if the input string is 'cococos'
                        if (ch=='c')
                        {
                                // if the string is 'cococos',
                                // we can say that we have already seen the 'coc' part of it:
                                seen=3;
                        }
                        else
                        {
                                // 'X' is not 'c', so reset
                                seen=0;
                        };
                }
                else
                        seen=0;      // reset
        }
        return len;                  // not found
};

#if 1
void check()
{
        unsigned len=LEN;
        char s[len];
        //__CPROVER_assert (search_cocos_brute(s, len)==search_cocos_naive(s, len), "assert");
        __CPROVER_assert (search_cocos_brute(s, len)==search_cocos_fixed(s, len), "assert");
};
#endif