Daniel Dietsch
Daniel Dietsch
I am with most of the people here: * I am again in the situation where I need to change the URL * Redirect is not an option anymore (no...
Regarding the standard: an overview over the different places in the different versions of the standard can be found at http://en.cppreference.com/w/c/string/byte/strncpy. It also seems that regardless of the version of...
A possible solution would be an implementation for this particular ``strncpy`` function (at least if we do not want to assume the semantics of the standard variant). Btw, a quick...
We supplied these benchmarks. You are right that in C11/C99 division by zero is undefined behaviour for all types, but only without Annex F. Annex F specifies the behaviour for...
Note: this is a sideeffect from the conversion of ``r_strncpy`` from an undefined function to the actual function.
I will try to confirm the issues for all items with Ultimate Automizer and then see about fixing them.
Our tool does not help with a lot of the examples from the list (either resource problems or unsupported C features). We can confirm a division by zero for *...
I can check the benchmarks our tool supports (see above), but I think there are way more ``ldv-*`` benchmarks (85 of the 120).
I second that; we already had a lot of discussions about the difference between ``if(y==0) abort()`` and ``__VERIFIER_assume(y!=0)``
I think ``abort()`` would be a problem; ``__VERIFIER_assume()`` is fine.