Как-то там неаккуратно. В одном абзаце "one would naively expect" и "the program in fact prints “4 8”, which does not correspond to the expected results of any of the evaluation orders". Ну так просто не надо быть такими наивными чудаками и считать, что наивно ожидаемые порядки выполнения покрывают все возможные порядки выполнения; тривиальный анализ SSA-графа сказал бы, что наблюдаемый результат очень даже ожидаем. (Аббревиатура SSA в тексте не встречается.)
И вот это C’s expression semantics, which have been ignored by most existing verification tools, в то время как слово Coverity не встречается в тексте нигде, заставляет задуматься, а не высосали ли авторы это своё "ignored by most existing verification tools" из какого-нибудь bodily appendage.
no subject
not correspond to the expected results of any of the evaluation orders". Ну так просто не надо быть такими наивными чудаками и считать, что наивно ожидаемые порядки выполнения покрывают все возможные порядки выполнения; тривиальный анализ SSA-графа сказал бы, что наблюдаемый результат очень даже ожидаем. (Аббревиатура SSA в тексте не встречается.)
И вот это C’s expression semantics, which have been ignored by most existing verification tools, в то время как слово Coverity не встречается в тексте нигде, заставляет задуматься, а не высосали ли авторы это своё "ignored by most existing verification tools" из какого-нибудь bodily appendage.
no subject