Я думаю Вы ошиблись ссылкой. Это примеры работы диагностики для 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/

У меня теперь такой вопрос: есть ли у вас в планах реализовать нечто для проверки корректности самих алгоритмов, а не просто выявления неких подозрительных мест и явных ошибок? Или хотя бы сделать такой же способ сведения к единому виду, который используется в компиляторах, чтоб посредством этого можно было бы свести одинаковые но по-разному написанные проверки к одному виду и проверить их на одинаковость

Кроме того, проверки корректности самого кода может быть недостаточно. Например тут описаны баги, обнаруженные в fuzz-тестированием, притом там много wrong code ошибок, а это очень, очень плохо. Лучше пусть компилятор падает, чем делает неправльный код (надо пилить верификатор для ассемблера короче). Кроме того, проблема еще может быть не в компиляторе и не в коде, а в самом процессоре(например недавний баг в интелях)

А если код писали разные люди, один человек написал проверку в одном стиле, потом другой человек дописывал код и написал еще одну проверку, которая проверяет по сути то же самое, но записана в другом виде — разве такого не может быть?
....
Некоторые компиляторы справляются с таким. Ну то есть как справляются — ошибки или предупреждения они не выдадут, но в ассемблерном коде вы увидите всего одну проверку, а не две.

Доказать свою позицию мне сложно. Но после сотен диагностик у меня уже есть чутьё, что стоит делать, а что нет. Мы делали немало экспериментов по диагностикам, которые затем не были взяты на вооружение. Теоретически идея смотрится хорошо, а вот как сделаешь - оказывается, что нет ни одной найденной ошибки, зато сотни ложных срабатываний. Хочешь не хочешь, со временем вырабатывается предвидение. И здесь оно говорит - не надо этого делать.

Вот Вы говорите про две одинаковые проверки, и что компилятор это заметит (с целью оптимизации). Но это ведь не обязательно ошибка. Простая ситуация, для которой у нас существует исключение.

Если написано так:

if (A == 22 || A == 22)

То следует ругаться. Видимо человек опечатался. А если написано так:

#define MAGIC_CONT_X 22
#define MAGIC_CONT_Y 22
if (A == MAGIC_CONT_X || A == MAGIC_CONT_Y)

То требуется молчать. Макрос сделан не просто так. Его идея в том, чтобы его изменить. Возможно в другом режиме сборки он другой, а вот сейчас совпадает. Это практическая ситуация, про которую знает PVS-Studio и молчит. Мы проделываем огромную работу в этом направлении.

У меня теперь такой вопрос: есть ли у вас в планах реализовать нечто для проверки корректности самих алгоритмов?

Нет. Нам это не интересно. Программисты преувеличивают необходимость поиска ошибок в алгоритмах и недооценивают вред, которые приносят опечатки и невнимательность.

Что-бы найти ошибку в алгоритме, требует искусственный интеллект, который понимает алгоритм на высоком уровне. Поэтому обсуждать эту тему смысла нет. О ней любят порассуждать те, кому выделяется грант и т.п. А нам надо ошибки искать и деньги зарабатывать. :)

P.S. Это не значит, что мы не пытаемся искать сложные ошибки. Но я очень не люблю темы, далёкие от практической реализации. Доказывать корректность С++ это нереально. И не нужно. Для этого есть более подходящие языки.

gtk

По поводу статьи о проверке gtk: Скажите, а есть ли возможность полностью проверить и исправить gtk? Можно было бы попросить у гнома грантик на эту работу, было бы полезно, чтобы хотя бы их демо примеры из дистрибутива виндового не падали (treeeview редактирование полей например)

есть ли возможность полностью проверить и исправить gtk?

Я не понял, что имеется в виду. Нет никакого препятствия получить у нас версию и заняться более тщательной проверкой.

Можно было бы попросить у гнома грантик на эту работу

Про грант, тоже непонятно. Если автором GTK хочется полноценную версию и поддержку, они могут приобрести лицензию. Гран тут как-тол перпендикулярен.

Что-бы найти ошибку в алгоритме, требует искусственный интеллект, который понимает алгоритм на высоком уровне. Поэтому обсуждать эту тему смысла нет.

Нет, там через логики первого порядка и всякие кванторы можно много чего доказать автоматически. А если нельзя - можно использовать естественный человеческий интеллект, а машина может проверять корректность доказательства, которое выдал человек. К тому же вот недавно какой-то ИИ уделал человека в Go так что можно этими задачами доказательства корректности понагружать аппаратуру. И не забывайте про https://ru.wikipedia.org/wiki/Тезис_Чёрча_—_Тьюринга_—_Дойча

Поскольку мозг человека это тоже вполне физическая штука (бредни про душу в расчет не берем), ЭВМ вам должна уметь доказывать все то, что человек может доказать своим органическим мозгом. ЧТД.

Доказывать корректность С++ это нереально. И не нужно.

Реально. Си умеют доказывать, значит и плюсы смогут. А вот насчет нужность - доказательства корректности нужны для особых вещей, например чтобы от переполнения буфера где-нибудь что-нибудь не отказало в самолете или ракете, летящей в небе. Или какой-нибудь автоматики на производстве или АЭС, где цена ошибки слишком высока. Или медицинском оборудовании. Не ваша это ниша просто