// time cbmc --trace --function check -DLEN=4 kmp_eel2.c

#include <stdio.h>

unsigned search_eel_brute (char *s, unsigned len)
{
        if (len<3)
                return len; // not found
        for (unsigned i=0; i<len-2; i++)
        {
                if (s[i]=='e' && s[i+1]=='e' && s[i+2]=='l')
                        return i;
        };
        return len; // not found
};

unsigned search_eel_naive (char *s, unsigned len)
{
        if (len<3)
                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=='e')
                        seen=1;
                else if (seen==1 && ch=='e')
                        seen=2;
                else if (seen==2 && ch=='l')
                        return i-2;  // found
                else
                        seen=0;    // reset
        }
        return len;                // not found
};

unsigned search_eel_fixed (char *s, unsigned len)
{
        if (len<3)
                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=='e')
                        seen=1;
                else if (seen==1 && ch=='e')
                        seen=2;
                else if (seen==2 && ch=='l')
                        return i-2;  // found
                else if (seen==2 && ch=='e')  // fix
                        seen=2;               // fix
                else
                        seen=0;    // reset
        }
        return len;                // not found
};

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

#if 0
int main()
{
#define S "e1d"
#define S_LEN 3
        printf ("%d\n", search_eel_brute(S, S_LEN));
        printf ("%d\n", search_eel_naive(S, S_LEN));
};
#endif