Hacker News Reader

Comment by boxfire | Hacker News Reader

For Part I, though I get the point to demonstrate proofs with CBMC, this is a pretty contrived example. E.g. using state machines for the cocos search makes an on-line very lazily written implementation human-verifiable at a read. I would like to see an example that doesn't have such a contrived nature.

Edit: Now I see in part II/III where the title actually comes to fruition and there is a state machine oriented generator is made and used. That still doesn't satisfy me about part I, honestly I would have just skipped it in retrospect.

View on HN

Note that the use of CMBC here was not thorough enough to spot that his reference implementation reads past the end of the string.

I don't think it does, assuming the passed len is correct.

        for (unsigned i=0; i<len; i++)
        {
                if (s[i]=='o' && s[i+1]=='k')
                        return i; // found
        };

The last iteration of this loop, it accesses s[len-1] and s[len]. If the string is null terminated, that's OK. If it's really just a length qualified string, that's not OK.

The later implementations treat len differently.

EDIT: It's worse than I said. The later version won't detect "ok" at the end of the string, because they are off by one in the OPPOSITE direction.

A string in C is, by definition, null terminated.

Then why are we providing a length? Plenty of string-handling functions in the c standard library result in no terminating null if max length -- e.g. strncpy.

Note the second function is off by one in the opposite direction-- it doesn't find "ok" in "ok".

Because the writer of the function doesn't want to bother to check the null terminator. I'm not saying it's a good function, it just doesn't have an issue as long as the input is a valid string with a correct length.

strncpy, despite what its name implies, does indeed not necessarily produce strings.

Regardless, a C string is defined to have a null terminator. All bets are off if you don't provide a string.

The issue is: the two functions that we're comparing for correctness treat lengths very differently: one scans len-1 bytes, the other scans len+1 bytes.

Even with a null terminator, there isn't a length that would work for both without overrunning the buffer.

        printf("%d %d\n", search_ok_1("mok", 2), search_ok_2("mok", 2));
        printf("%d %d\n", search_ok_1("mok", 3), search_ok_2("mok", 3));   /* Overruns without null term */
        printf("%d %d\n", search_ok_1("mok", 4), search_ok_2("mok", 4));   /* Overruns even WITH null term */

Prints out:

    1 2
    1 3
    1 1

Thats why strncpy is deprecated for strlcpy.

Oh I have some bad news for you, buddy.

Reply on news.ycombinator.com