История изменений
Исправление SZT, (текущая версия) :
Я думаю Вы ошиблись ссылкой. Это примеры работы диагностики для C#. Если речь идёт про C++, то правильнее будет смотреть сюда: http://www.viva64.com/ru/examples/V501/
Не принципиально. Все равно они об одном и том же.
Пример который привели Вы, анализатор PVS-Studio не найдёт. И моё экспертное мнение - не должен находить. Это неестественная ошибка. Никто не будет делать однотипные проверки разными способами в рамках одного выражения. Ну не пишут просто люди так.
А если код писали разные люди, один человек написал проверку в одном стиле, потом другой человек дописывал код и написал еще одну проверку, которая проверяет по сути то же самое, но записана в другом виде — разве такого не может быть? Например, человек, дописавший новую проверку, мог не понять смысл того, что делает старая проверка, и написать свою, аналогичную.
Насчет «не должен находить» — а по-моему вполне должен. Некоторые компиляторы справляются с таким. Ну то есть как справляются — ошибки или предупреждения они не выдадут, но в ассемблерном коде вы увидите всего одну проверку, а не две. http://goo.gl/poYCSm
И там между прочим не используются все эти средства формальной верификации. Взгляните например на эту функцию simplify_binary_operation_1 которая черт знает сколько строк кода занимает, и в ней просто вшиты определенные правила преобразований (упрощений) https://gcc.gnu.org/viewcvs/gcc/trunk/gcc/simplify-rtx.c?view=markup&path...
. Там они делают некие операции над RTL в целях оптимизации, и оно «съедает» эти одинаковые проверки https://gcc.gnu.org/onlinedocs/gccint/RTL-Objects.html . Но RTL представление это уже ближе к машинному представлению, там есть еще GIMPLE, GENERIC и может быть эти лишние проверки были убраны еще на более ранней стадии в другом представлении. Clang тоже может эту лишнюю проверку выкинуть из моего примера, а вот ICC уже нет. Вы тоже могли бы добавить такой способ обнаружения identical sub-expressions, введя некий набор операций над тем абстрактным представлением, которым вы у себя там оперируете и попробовав привести условия к некоему единому виду(конечно тут не всегда сработает, проблема эквивалентности алгоритмов как и проблема останова алгоритмически неразрешима).
Про Frama-C мы слушали. Но это немного другое. Бесплатных обедов не бывает. Что-бы добиться от него какого-то интересного результата (причем только для С), нужно потратить очень много времени на разметку кода. Это просто не работает, на больших проектах: нельзя просто взять и начать использовать Frama-C. А вот PVS-Studio можно.
Насчет Frama-C, SMT солверов и прочего — естественно там надо больше тратить времени, но результат получается совсем другим: если весь код «замостить» этими контрактами и доказать корректность каждой функции/метода, то можно и доказать корректность всего кода в целом т.е. доказать отсутствие ошибок. PVS-Studio же может только показывать на подозрительные и некоторые явно ошибочные участки кода, корректность алгоритмов он гарантировать не может. Да, кстати. Была выявлена ошибка в одном алгоритме сортировки, когда его корректность пытались математически доказать https://habrahabr.ru/post/251751/
У меня теперь такой вопрос: есть ли у вас в планах реализовать нечто для проверки корректности самих алгоритмов, а не просто выявления неких подозрительных мест и явных ошибок? Или хотя бы сделать такой же способ сведения к единому виду, который используется в компиляторах, чтоб посредством этого можно было бы свести одинаковые но по-разному написанные проверки к одному виду и проверить их на одинаковость
Исправление SZT, :
Я думаю Вы ошиблись ссылкой. Это примеры работы диагностики для C#. Если речь идёт про C++, то правильнее будет смотреть сюда: http://www.viva64.com/ru/examples/V501/
Не принципиально. Все равно они об одном и том же.
Пример который привели Вы, анализатор PVS-Studio не найдёт. И моё экспертное мнение - не должен находить. Это неестественная ошибка. Никто не будет делать однотипные проверки разными способами в рамках одного выражения. Ну не пишут просто люди так.
А если код писали разные люди, один человек написал проверку в одном стиле, потом другой человек дописывал код и написал еще одну проверку, которая проверяет по сути то же самое, но записана в другом виде — разве такого не может быть? Например, человек, дописавший новую проверку, мог не понять смысл того, что делает старая проверка, и написать свою, аналогичную.
Насчет «не должен находить» — а по-моему вполне должен. Некоторые компиляторы справляются с таким. Ну то есть как справляются — ошибки или предупреждения они не выдадут, но в ассемблерном коде вы увидите всего одну проверку, а не две. http://goo.gl/poYCSm
И там между прочим не используются все эти средства формальной верификации. Взгляните например на эту функцию simplify_binary_operation_1 которая черт знает сколько строк кода занимает, и в ней просто вшиты определенные правила преобразований (упрощений) https://gcc.gnu.org/viewcvs/gcc/trunk/gcc/simplify-rtx.c?view=markup&path...
. Там они делают некие операции над RTL в целях оптимизации, и оно «съедает» эти одинаковые проверки https://gcc.gnu.org/onlinedocs/gccint/RTL-Objects.html . Но RTL представление это уже ближе к машинному представлению, там есть еще GIMPLE, GENERIC и может быть эти лишние проверки были убраны еще на более ранней стадии в другом представлении. Clang тоже может эту лишнюю проверку выкинуть из моего примера, а вот ICC уже нет. Вы тоже могли бы добавить такой способ обнаружения identical sub-expressions, введя некий набор операций над тем абстрактным представлением, которым вы у себя там оперируете и попробовав привести условия к некоему единому виду(конечно тут не всегда сработает, проблема эквивалентности алгоритмов как и проблема останова алгоритмически неразрешима).
Про Frama-C мы слушали. Но это немного другое. Бесплатных обедов не бывает. Что-бы добиться от него какого-то интересного результата (причем только для С), нужно потратить очень много времени на разметку кода. Это просто не работает, на больших проектах: нельзя просто взять и начать использовать Frama-C. А вот PVS-Studio можно.
Насчет Frama-C, SMT солверов и прочего — естественно там надо больше тратить времени, но результат получается совсем другим: если весь код «замостить» этими контрактами и доказать корректность каждой функции/метода, то можно и доказать корректность всего кода в целом т.е. доказать отсутствие ошибок. PVS-Studio же может только показывать на подозрительные и некоторые явно ошибочные участки кода, корректность алгоритмов он гарантировать не может. Да, кстати. Была выявлена ошибка в одном алгоритме сортировки, когда его корректность пытались математически доказать https://habrahabr.ru/post/251751/
У меня теперь такой вопрос: есть ли у вас в планах реализовать нечто для проверки корректности самих алгоритмов, а не просто выявления неких «подозрительных мест»?
Исходная версия SZT, :
Я думаю Вы ошиблись ссылкой. Это примеры работы диагностики для C#. Если речь идёт про C++, то правильнее будет смотреть сюда: http://www.viva64.com/ru/examples/V501/
Не принципиально. Все равно они об одном и том же.
Пример который привели Вы, анализатор PVS-Studio не найдёт. И моё экспертное мнение - не должен находить. Это неестественная ошибка. Никто не будет делать однотипные проверки разными способами в рамках одного выражения. Ну не пишут просто люди так.
А если код писали разные люди, один человек написал проверку в одном стиле, потом другой человек дописывал код и написал еще одну проверку, которая проверяет по сути то же самое, но записана в другом виде — разве такого не может быть? Например, человек, дописавший новую проверку, мог не понять смысл того, что делает старая проверка, и написать свою, аналогичную.
Насчет «не должен находить» — а по-моему вполне должен. Некоторые компиляторы справляются с таким. Ну то есть как справляются — ошибки или предупреждения они не выдадут, но в ассемблерном коде вы увидите всего одну проверку, а не две. http://goo.gl/poYCSm
И там между прочим не используются все эти средства формальной верификации. Взгляните например на эту функцию simplify_binary_operation_1 которая черт знает сколько строк кода занимает, и в ней просто вшиты определенные правила преобразований (упрощений) https://gcc.gnu.org/viewcvs/gcc/trunk/gcc/simplify-rtx.c?view=markup&path...
. Там они делают некие операции над RTL в целях оптимизации, и оно «съедает» эти одинаковые проверки https://gcc.gnu.org/onlinedocs/gccint/RTL-Objects.html . Но RTL представление это уже ближе к машинному представлению, там есть еще GIMPLE, GENERIC и может быть эти лишние проверки были убраны еще на более ранней стадии в другом представлении. Clang тоже может эту лишнюю проверку выкинуть из моего примера, а вот ICC уже нет. Вы тоже могли бы добавить такой способ обнаружения identical sub-expressions, введя некий набор операций над тем абстрактным представлением, которым вы у себя там оперируете и попробовав привести условия к некоему единому виду(конечно тут не всегда сработает, проблема эквивалентности алгоритмов как и проблема останова алгоритмически неразрешима).
Про Frama-C мы слушали. Но это немного другое. Бесплатных обедов не бывает. Что-бы добиться от него какого-то интересного результата (причем только для С), нужно потратить очень много времени на разметку кода. Это просто не работает, на больших проектах: нельзя просто взять и начать использовать Frama-C. А вот PVS-Studio можно.
Насчет Frama-C, SMT солверов и прочего — естественно там надо больше тратить времени, но результат получается совсем другим: если весь код «замостить» этими контрактами и доказать корректность каждой функции/метода, то можно и доказать корректность всего кода в целом т.е. доказать отсутствие ошибок. PVS-Studio же может только показывать на подозрительные и некоторые явно ошибочные участки кода, корректность алгоритмов он гарантировать не может. Да, кстати. Была выявлена ошибка в одном алгоритме сортировки, когда его корректность пытались математически доказать https://habrahabr.ru/post/251751/ .