On 10/3/2015 8:43 AM, Timon Gehr wrote:
There are also some other, more minor issues. For example, when the language specification speaks about "memory safety", it is really unclear what this means, as the language designers seem to think it that it is fine to have undefined behaviour in a section of code that is "verified memory safe".
Memory safety means no memory corruption is possible.
