Comments 44
Заранее прошу прощения за оффтоп, но: PVS-Studio, довольно серьезный продукт, имеет большое комьюнити, много кастомеров с громкими именами, и соответственно (думаю не ошибусь) — большую команду разработчиков.
«Хочешь сделать хорошо — сделай сам» тут не пройдет, а вот «сколько людей — столько мнений» (а формальнее «стилей программирования/уровней подготовки» и тд) как раз уместно.
В связи с этим возникла небольшая, но мне кажется интересная мысль, а не пробовали ли вы проверить PVS-Studio с помощью PVS-Studio?
«Хочешь сделать хорошо — сделай сам» тут не пройдет, а вот «сколько людей — столько мнений» (а формальнее «стилей программирования/уровней подготовки» и тд) как раз уместно.
В связи с этим возникла небольшая, но мне кажется интересная мысль, а не пробовали ли вы проверить PVS-Studio с помощью PVS-Studio?
очень трудно представить, что такой проверки не было
Они же и так в комментариях к каждой статье отвечают на этот вопрос
Нет, мы пока не большая команда. О нас: CppCat — тульский анализатор кода C++ с большими амбициями.
Там есть ответ и о проверке самих себя. И вообще, это вечный вопрос. Он есть к почти каждой нашей статье. См. также: Ответы на вопросы, которые часто задают после прочтения наших статей.
Там есть ответ и о проверке самих себя. И вообще, это вечный вопрос. Он есть к почти каждой нашей статье. См. также: Ответы на вопросы, которые часто задают после прочтения наших статей.
Спасибо за ответ, кратко и емко. В принципе как раз о ночных запусках и было интересно узнать.
P.S. Привет тем кто продолжает сливать карму. Не совсем понятно почему, но все же хотя бы аргументируйте.
P.S. Привет тем кто продолжает сливать карму. Не совсем понятно почему, но все же хотя бы аргументируйте.
CppCat — то, что нужно! Вам бы сделать отдельный пост про него. Буду выпрашивать у руководства, чай недорого :)
Спасибо. Как всегда, есть над чем задуматься.
И это не документировано? Жуть.
Мне кажется, оператор 'break' между <...> отсутствует специально.
И это не документировано? Жуть.
Нет. Сейчас ещё раз посмотрел. А может и забыты тут break;… ХЗ.
case isc_sdl_add: sdl_operator = op_add; case isc_sdl_subtract: if (!sdl_operator) sdl_operator = op_subtract; case isc_sdl_multiply: if (!sdl_operator) sdl_operator = op_multiply; case isc_sdl_divide: if (!sdl_operator) sdl_operator = op_divide; COMPILE(p, arg); COMPILE(p, arg); STUFF(sdl_operator, arg); return p;
неплохо бы в самом начале статьи указать, код какой именно версии Firebird проверялся. Например, если 3.0, то она пока в alpha-состоянии.
Последняя, которая была месяц назад.
Собственно, решается задача сравнения анализаторов на наборе проектов, а не проверка самой последней версии проекта. Всё равно, авторам надо самим проверять проект, так как я вполне могу пропустить ошибки. Или могу не описать очень плохой, но работающий код, так как он не подходит для сравнения. Но этот код явно стоит изучить и отрефакторить.
Статья хорошо показано, что анализатор находит ошибки в этом проекте, а значит может быть полезен разработчикам. Может что-то из ошибок поправлено, но зато добавлено новое. Плюс не забываем, что анализ надо выполнять регулярно, а не раз в год.
Собственно, решается задача сравнения анализаторов на наборе проектов, а не проверка самой последней версии проекта. Всё равно, авторам надо самим проверять проект, так как я вполне могу пропустить ошибки. Или могу не описать очень плохой, но работающий код, так как он не подходит для сравнения. Но этот код явно стоит изучить и отрефакторить.
Статья хорошо показано, что анализатор находит ошибки в этом проекте, а значит может быть полезен разработчикам. Может что-то из ошибок поправлено, но зато добавлено новое. Плюс не забываем, что анализ надо выполнять регулярно, а не раз в год.
что значит «последняя»? В коде Firebird параллельно идут обновления версий 2.1, 2.5, 3.0.
sourceforge.net/p/firebird/code/HEAD/tree/firebird/
см. tags. Если trunk, то это альфа ФБ 3.0.
sourceforge.net/p/firebird/code/HEAD/tree/firebird/
см. tags. Если trunk, то это альфа ФБ 3.0.
Ну и что?
Скачкой занимался коллега. С вероятность 99% это был trunk. Могу попросить его вспомнить, но в этом нет смысла.
Самое плохое, что можно сделать, это начать править ошибки, основываясь на этой статье.
Вот переведём статью, покажем её разработчикам. Они увидят, что можно найти ошибки. Они спокойно проверят код и поправят ошибки. Profit.
Скачкой занимался коллега. С вероятность 99% это был trunk. Могу попросить его вспомнить, но в этом нет смысла.
Самое плохое, что можно сделать, это начать править ошибки, основываясь на этой статье.
- Я могу ошибаться и ошибки нет.
- Я могу пропустить другие ошибки.
- Особенно забавно, когда сразу двое доброходов правят один и тот-же код, прочитав статью. Уже были такие случаи. :) В статье написано, что перепутан 2 и 3 аргумент функции memset(). Первый меняет эти аргументы. Всё правильно. А потом второй человек, ещё раз меняет аргументы. В результате, получается то, что и было. :)
Вот переведём статью, покажем её разработчикам. Они увидят, что можно найти ошибки. Они спокойно проверят код и поправят ошибки. Profit.
Статью можно не переводить — разработчики вполне себе местные :)
не подумайте, что я прикопался, но подобные
— ошибки в коде альфа-версии вполне допустимы. конечно, их нужно вычищать, и спасибо вам и инструменту за это
— ошибки в коде релиза недопустимы, и если исследовался код релиза, то эти ошибки нужно срочно исправлять
в этом и был смысл моих вопросов. Либо «ахтунг!», либо «ничего страшного» :-)
— ошибки в коде альфа-версии вполне допустимы. конечно, их нужно вычищать, и спасибо вам и инструменту за это
— ошибки в коде релиза недопустимы, и если исследовался код релиза, то эти ошибки нужно срочно исправлять
в этом и был смысл моих вопросов. Либо «ахтунг!», либо «ничего страшного» :-)
Не, «ахтунг!» однозначно. Если Вы используете инкрементальный анализ на машинах всех разработчиков (т.е. автоматическую проверку только что перекомпилированных файлов), то ошибка даже в систему контроля версий не попадет.
А так сколько времени пройдет, пока вы ее найдете. Да еще если и на этапе тестирования только выявлять… Помните, сколько стоит исправление ошибки на каждом этапе разработки ПО?
А так сколько времени пройдет, пока вы ее найдете. Да еще если и на этапе тестирования только выявлять… Помните, сколько стоит исправление ошибки на каждом этапе разработки ПО?
тут я особых проблем не вижу, cvs все стерпит :-), но Windows только у двух разработчиков, так что если PVS и использовать, то только на билд-сервере.
Билд-серверный вариант у нас в PVS-Studio отлично проработан, можете пробовать.
Правда нельзя забывать, что «cvs стерпит», но с табличкой не поспоришь:
Средняя стоимость исправления дефектов в зависимости от времени их внесения и обнаружения (данные для таблицы взяты из книги С. Макконнелла 'Совершенный Код')
Правда нельзя забывать, что «cvs стерпит», но с табличкой не поспоришь:
Средняя стоимость исправления дефектов в зависимости от времени их внесения и обнаружения (данные для таблицы взяты из книги С. Макконнелла 'Совершенный Код')
кстати, передаю спасибо от разработчиков Firebird.
p.s. в статье есть «Что это за подозрительный 'braeak'?», при этом слова braeak я больше нигде не вижу.
p.s. в статье есть «Что это за подозрительный 'braeak'?», при этом слова braeak я больше нигде не вижу.
Есть ли новости о портировании cppcat под *nix? Планируете ли этим заниматься?
Кстати, интересно — а ядро Линукса вы проверяли?
На данный момент мы проверили и написали про: "Open-source проекты, которые мы проверили с помощью PVS-Studio".
Ядро Линукс не проверяли, но когда ни будь проверим. Но не думаю, что из этого что-то интересное получится. Его чем только не проверяли.
Я уверен, можно было бы найти много забавного, если ежедневно выкачивать исходники Linux, проверять и смотреть сообщения, относящиеся к свежему коду. Думаю, за пару месяцев было бы немало интересного насобирать. Но это достаточно сложная в реализации задача, которая нам не интересна.
Ядро Линукс не проверяли, но когда ни будь проверим. Но не думаю, что из этого что-то интересное получится. Его чем только не проверяли.
Я уверен, можно было бы найти много забавного, если ежедневно выкачивать исходники Linux, проверять и смотреть сообщения, относящиеся к свежему коду. Думаю, за пару месяцев было бы немало интересного насобирать. Но это достаточно сложная в реализации задача, которая нам не интересна.
Андрей, спасибо за статью. Ждем новых проверок — PostgreSQL и других :)
А разве сдвиг влево знакового числа не определен? Мне казалось, что это только про сдвиг вправо.
Знакового — определён. Отрицательного — нет. (~0) — имеет тип int и равно -1.
The shift operators <> group left-to-right.
shift-expression << additive-expression
shift-expression >> additive-expression
The operands shall be of integral or unscoped enumeration type and integral promotions are performed.
1. The type of the result is that of the promoted left operand. The behavior is undefined if the right operand is negative, or greater than or equal to the length in bits of the promoted left operand.
2. The value of E1 << E2 is E1 left-shifted E2 bit positions; vacated bits are zero-filled. If E1 has an unsigned type, the value of the result is E1 * 2^E2, reduced modulo one more than the maximum value representable in the result type. Otherwise, if E1 has a signed type and non-negative value, and E1*2^E2 is representable in the result type, then that is the resulting value; otherwise, the behavior is undefined.
3. The value of E1 >> E2 is E1 right-shifted E2 bit positions. If E1 has an unsigned type or if E1 has a signed type and a non-negative value, the value of the result is the integral part of the quotient of E1/2^E2. If E1 has a signed type and a negative value, the resulting value is implementation-defined.
The shift operators <> group left-to-right.
shift-expression << additive-expression
shift-expression >> additive-expression
The operands shall be of integral or unscoped enumeration type and integral promotions are performed.
1. The type of the result is that of the promoted left operand. The behavior is undefined if the right operand is negative, or greater than or equal to the length in bits of the promoted left operand.
2. The value of E1 << E2 is E1 left-shifted E2 bit positions; vacated bits are zero-filled. If E1 has an unsigned type, the value of the result is E1 * 2^E2, reduced modulo one more than the maximum value representable in the result type. Otherwise, if E1 has a signed type and non-negative value, and E1*2^E2 is representable in the result type, then that is the resulting value; otherwise, the behavior is undefined.
3. The value of E1 >> E2 is E1 right-shifted E2 bit positions. If E1 has an unsigned type or if E1 has a signed type and a non-negative value, the value of the result is the integral part of the quotient of E1/2^E2. If E1 has a signed type and a negative value, the resulting value is implementation-defined.
Есть мнение, что вектор движения на логотипе предпочтительнее направлять направо-вверх. Так конверсия будет ещё больше. :)
А assert не пробывали+логика Хоара. Я понимаю, отрасль перегрета, полно идиотов, которые считают себя программистам,.но на них делать, деньги.
Стыдно товарищи! + агрессивная реклама. Еще раз стыдно.
Стыдно товарищи! + агрессивная реклама. Еще раз стыдно.
Стыдно? Неужели?
Мы гордимся тем, что делаем. Не понятно, почему нам должно быть стыдно. Это Ваши фантазии (зависть) и не более того.
Мы делаем самую замечательную и полезную рекламу, которая может быть. Мы существенно помогаем миру open-source программ. Многие разработчики этих проектов благодарны нам.
И мир это ценит. Наши клиенты не «идиоты», а как раз наоборот компании, которые понимают всю важность качества кода, и сколько стоят ошибки: наши клиенты. Мы прилучаем от них много благодарственных слов. Многие компании продлевают лицензию уже не один год.
Недавно мы пошли навстречу и небольшим компаниям, выпустив лёгкий вариант анализатора за $250 — CppCat. Теперь со временем нас полюбят и маленькие команды и индивидуальные разработчики.
Продолжать дискуссию с Вами считаю нецелесообразным.
Мы делаем самую замечательную и полезную рекламу, которая может быть. Мы существенно помогаем миру open-source программ. Многие разработчики этих проектов благодарны нам.
И мир это ценит. Наши клиенты не «идиоты», а как раз наоборот компании, которые понимают всю важность качества кода, и сколько стоят ошибки: наши клиенты. Мы прилучаем от них много благодарственных слов. Многие компании продлевают лицензию уже не один год.
Недавно мы пошли навстречу и небольшим компаниям, выпустив лёгкий вариант анализатора за $250 — CppCat. Теперь со временем нас полюбят и маленькие команды и индивидуальные разработчики.
Продолжать дискуссию с Вами считаю нецелесообразным.
«Мы делаем самую замечательную и полезную рекламу, которая может быть.»
Вы уже думаете на английском языке. И она рассчитана на идиотов.
Основная идея Хоара дать для каждой конструкции императивного языка пред и постусловие записанное в виде логической формулы. Поэтому и возникает в названии тройка — предусловие, конструкция языка, постусловие.
Ясно, что для пустого оператора пред и постусловия совпадают.
Для оператора присваивания в постусловие кроме предусловия должно учитывать факт, что значение переменной стало другим.
Для составного оператора (в Python это отступы, в C это {}) имеем цепочку пред и постусловий. В результате для составного оператора можно оставить первое предусловие и последнее постусловие.
Правило вывода говорит, что можно усилить пред и ослабить постусловие если нам это понадобиться. Нет смысла волочь через всю программу какое-то утверждение, которое не помогает решить поставленную задачу.
Оператор ветвления или просто if. Его условно можно разбить на две ветки then и else. Если к предусловию добавить истинность логического условия (то, что стоит под if), то после выполнения ветки then должно следовать постусловие. Аналогично, если к предусловию добавить отрицание логического условия (то, что стоит под if), то после выполнения ветки else должно следовать постусловие
Оператор цикла. Это самое нетривиальное и сложное, поскольку цикл может выполняется много раз и даже не окончится. Чтобы решить проблему возможно многократного повтора тела цикла вводят инвариант цикла. Инвариант цикла это то, что истинно перед его выполнением, истинно после каждого выполнения тела цикла и следовательно истинно и после его окончания. Предусловие для оператора цикла это просто его инвариант цикла. Если истинно условие продолжения цикла (то, что стоит под while), то после выполнения тела цикла должна следовать истинность инвариант цикла. В результате после окончания цикла имеем в качестве постусловия истинность инвариант цикла и отрицание условия продолжения цикла.
Оператора цикла с полной корректностью. Для этого к предыдущему пункту добавляют ограничивающую функцию, с помощью которой легко доказать, что цикл будет выполнятся ограниченное число раз. На нее накладывают условия, что она всегда >=0, строго убывает после каждого выполнения тела цикла и в точности =0, когда цикл заканчивается.
Хоар фактически предложил:
Давайте воспользуемся произволом при написании программ и будем их писать так, чтобы легче было доказать их корректность. В результате и программу легче написать, и доказательство корректности сразу получим.
Это мои слова.
По поводу доказательства правильности алгоритма. Есть в математике набор инструментов позволяющий доказывать теоремы. Я назову общеизвестные: метод математической индукции, от противного. Так вот логика Хоара это инструмент доказательства корректности программ (правильнее частичной корректности, но это уже нюансы), который в принципе может быть использован и для доказательства корректности алгоритма, если он записан в основных конструкциях императивного программирования, для которых есть Тройки Хоара.
Это мое и взято отсюда freehabr.ru/blog/programming/1934.html
Мне за державу обидно, потому и на Вас наехал. И по Вашим комментариям, похоже правильно.
Вы уже думаете на английском языке. И она рассчитана на идиотов.
Основная идея Хоара дать для каждой конструкции императивного языка пред и постусловие записанное в виде логической формулы. Поэтому и возникает в названии тройка — предусловие, конструкция языка, постусловие.
Ясно, что для пустого оператора пред и постусловия совпадают.
Для оператора присваивания в постусловие кроме предусловия должно учитывать факт, что значение переменной стало другим.
Для составного оператора (в Python это отступы, в C это {}) имеем цепочку пред и постусловий. В результате для составного оператора можно оставить первое предусловие и последнее постусловие.
Правило вывода говорит, что можно усилить пред и ослабить постусловие если нам это понадобиться. Нет смысла волочь через всю программу какое-то утверждение, которое не помогает решить поставленную задачу.
Оператор ветвления или просто if. Его условно можно разбить на две ветки then и else. Если к предусловию добавить истинность логического условия (то, что стоит под if), то после выполнения ветки then должно следовать постусловие. Аналогично, если к предусловию добавить отрицание логического условия (то, что стоит под if), то после выполнения ветки else должно следовать постусловие
Оператор цикла. Это самое нетривиальное и сложное, поскольку цикл может выполняется много раз и даже не окончится. Чтобы решить проблему возможно многократного повтора тела цикла вводят инвариант цикла. Инвариант цикла это то, что истинно перед его выполнением, истинно после каждого выполнения тела цикла и следовательно истинно и после его окончания. Предусловие для оператора цикла это просто его инвариант цикла. Если истинно условие продолжения цикла (то, что стоит под while), то после выполнения тела цикла должна следовать истинность инвариант цикла. В результате после окончания цикла имеем в качестве постусловия истинность инвариант цикла и отрицание условия продолжения цикла.
Оператора цикла с полной корректностью. Для этого к предыдущему пункту добавляют ограничивающую функцию, с помощью которой легко доказать, что цикл будет выполнятся ограниченное число раз. На нее накладывают условия, что она всегда >=0, строго убывает после каждого выполнения тела цикла и в точности =0, когда цикл заканчивается.
Хоар фактически предложил:
Давайте воспользуемся произволом при написании программ и будем их писать так, чтобы легче было доказать их корректность. В результате и программу легче написать, и доказательство корректности сразу получим.
Это мои слова.
По поводу доказательства правильности алгоритма. Есть в математике набор инструментов позволяющий доказывать теоремы. Я назову общеизвестные: метод математической индукции, от противного. Так вот логика Хоара это инструмент доказательства корректности программ (правильнее частичной корректности, но это уже нюансы), который в принципе может быть использован и для доказательства корректности алгоритма, если он записан в основных конструкциях императивного программирования, для которых есть Тройки Хоара.
Это мое и взято отсюда freehabr.ru/blog/programming/1934.html
Мне за державу обидно, потому и на Вас наехал. И по Вашим комментариям, похоже правильно.
А SQLite не планируете проверить? Очень интересно, помогает ли полное покрытие тестами избавиться от различных ошибок :)
Sign up to leave a comment.
Побочный результат: проверяем Firebird с помощью PVS-Studio