A small typo, there's a sentence after the Frama-C code block that ends "[...] and that a subsequent memcpy() of the two regions will return zero" which should have a s/memcpy/memcmp/. Quite obvious, but in an article such as this it's best to be precise of course.
A small typo, there's a sentence after the Frama-C code block that ends "[...] and that a subsequent memcpy() of the two regions will return zero" which should have a s/memcpy/memcmp/. Quite obvious, but in an article such as this it's best to be precise of course.