verif_stlib has a spec for strcmp and there's a verified implementation of strcmp in strlib.c. But the code is wrong relative to the Posix-etc specs which say unsigned char comparison should be used. The code can be fixed by adding a casts to unsigned char. The current spec is too weak, the postcondition requires only equality/disequality which explains the bug slipping through.
This issue was found by Frederico Ramos, a student of José Santos at Instituto Superior Técnico, Lisbon, using symbolic execution.
verif_stlib has a spec for strcmp and there's a verified implementation of strcmp in strlib.c. But the code is wrong relative to the Posix-etc specs which say unsigned char comparison should be used. The code can be fixed by adding a casts to unsigned char. The current spec is too weak, the postcondition requires only equality/disequality which explains the bug slipping through.
This issue was found by Frederico Ramos, a student of José Santos at Instituto Superior Técnico, Lisbon, using symbolic execution.