On 6/15/2014 3:45 PM, Timon Gehr wrote:
I don't know why the documentation says that. D's @safe is about memory
safety, not undefined behavior.
...
Note that this is frustratingly unhelpful for deciphering your point about
"memory safe" <=> "verifiably @safe" by definition. Are you defining "memory
safe" or "verifiably @safe"?
I don't understand your question. I don't know what is unhelpful about saying
that @safe refers to memory safety.
Note that the list of eschewed behaviors are possibly memory corrupting.
It is an incomplete list.
I ask that you enumerate the missing items, put the list in bugzilla, and tag
them with the 'safe' keyword.
In any case, I
don't see how any list of (syntactic) verifiable properties of the code is
supposed to be equivalent to the (non-trivial semantic) memory safety property.
The list is not restricted to syntactic issues.
Are you assuming @trusted as an oracle for memory safety and saying @trusted
code is 'verifiably @safe' code? (That's not the intended reading.)
Not at all. Where does the spec suggest that?
Signed integer overflow, for example, is not listed.
Are you trying to say that signed integer overflow is undefined behaviour in D?
(This would again contradict the documentation.)
I know the spec says it follows 2's complement arithmetic. I'm not 100%
confident we can rely on that for all 2's complement CPUs, and furthermore we
have a bit of a problem in relying on optimizers built for C/C++ which rely on
it being undefined behavior.
In any case, it is still not an issue for @safe.
