Removed definitions of memcmp function

[zvonimir]

This is a standard library function and hence it should not be defined in benchmarks.

[dbeyer]

Is this a stub function that is there by purpose? Then we could rename it perhaps? @tautschnig What do you think?

[zvonimir]

Good question. I'll test it once the other pull request a created gets merged. To me this looks like a standard implementation of memcmp, and there is nothing special about it except these two lines:

    assume_abort_if_not((((n) == 0) || (s1)));
    assume_abort_if_not((((n) == 0) || (s2)));

I guess removing them would potentially lead to more behaviors being explored, and maybe to false bugs. I think maybe one thing that would make this benchmark more realistic would be to add these assumptions before calls to memcmp, and then still remove this memcmp body.

Now, if you read for example this: https://stackoverflow.com/questions/16362925/can-i-pass-a-null-pointer-to-memcmp I would say that these assumptions are not totally right since memcmp seems to be undefined if s1 or s2 are not valid pointers.

Anyhow, I am totally open to suggestions here.

[PhilippWendler]

So it seems these tasks depend on a non-standard assumption about memcmp, right? So one solution would be to wrap memcmp into something like a safe_memcmp that includes the above two assumptions and then calls the stdlib memcmp?

[zvonimir]

I like that suggestion! I'll update my pull request later today. Thx!

[zvonimir]

I am sorry, but I somehow messed up by branch here. I moved this to #1187 , and so please review that one instead. I am closing this one now.