5 ms·
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
by boxfire 6y ago
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.
- mlyle 6y agoNote that the use of CMBC here was not thorough enough to spot that his reference implementation reads past the end of the string.
- shric 6y agoI don't think it does, assuming the passed len is correct.
- mlyle 6y agofor (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.
- shric 6y agoA string in C is, by definition, null terminated.
- mlyle 6y agoThen 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".
- shric 6y agoBecause 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.
- mlyle 6y agoThe 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
- makapuf 6y agoThats why strncpy is deprecated for strlcpy.
- billsnow 6y agoOh I have some bad news for you, buddy.