The OpenNET Project / Index page

[ новости /+++ | форум | wiki | теги | ]

В рамках проекта SMACK развивается новая система статической проверки кода C/C++

04.02.2013 21:32

В списке рассылки разработчиков LLVM представлен новый проект SMACK, в рамках которого создан инструмент для статической проверки свойств программ, написанных на языках C/C++. На основании анализа исходных текстов программы, без непосредственного выполнения приложения, SMACK позволяет выявить нарушение заданных пользователем утверждений корректности (assertions).

Код инструмента поставляется под лицензией MIT и интегрируется с инфраструктурой компиляции LLVM. При желании SMACK может быть выведен за рамки C/C++ и после небольшой доработки использован для проверки кода на любом другом языке программирования, поддерживаемом в LLVM. Также возможно создание расширений, работающих поверх SMACK.

  1. Главная ссылка к новости (http://lists.cs.uiuc.edu/piper...)
Лицензия: CC BY 3.0
Короткая ссылка: https://opennet.ru/36023-assert
Ключевые слова: assert, code, llvm, static, debug
При перепечатке указание ссылки на opennet.ru обязательно


Обсуждение (51) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.1, x0r (??), 21:42, 04/02/2013 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    побыстрей бы clang checker допилили до C++...
     
  • 1.2, Аноним (-), 23:12, 04/02/2013 [ответить] [﹢﹢﹢] [ · · · ]  
  • –7 +/
    Что только не сделают, лишь бы хаскелл не учить.:)
     
     
  • 2.3, Аноним (-), 23:28, 04/02/2013 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Так где ваши ядра операционок на хаскелле, сэр?
     
     
  • 3.5, BratSinot (ok), 01:20, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    http://web.archive.org/web/20041117045537/http://www.macs.hw.ac.uk/~sebc/hOp/
     
     
  • 4.8, Аноним (-), 03:04, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +5 +/
    > http://web.archive.org/web/20041117045537/http://www.macs.hw.ac.uk/~sebc/hOp/

    Оно настолько живет и процветает что даже пришлось использовать веб-архив? А что, вы не хотите пользоваться этим? Надо же, какая незадача. Круто придумано - пытаться впаривать ДРУГИМ то что не хочешь жрать САМ.


     
     
  • 5.17, scor (ok), 09:35, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +1 +/
    >> http://web.archive.org/web/20041117045537/http://www.macs.hw.ac.uk/~sebc/hOp/
    > Оно настолько живет и процветает что даже пришлось использовать веб-архив? А что,
    > вы не хотите пользоваться этим? Надо же, какая незадача. Круто придумано
    > - пытаться впаривать ДРУГИМ то что не хочешь жрать САМ.

    Не нравится hOp из веб-архива? Ну вот вам House http://programatica.cs.pdx.edu/House/. Вполне себе из "интернета".:)
    А вообще, в чём претензия? Вы задали вопрос: "есть ли ядра на хаскеле?" Вам доказательно ответили, что есть. Или вы имели ввиду: "есть ли <ядро моей любимой ОС> на хаскеле?":)

     
     
  • 6.28, Crazy Alex (ok), 19:18, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Обычно в таких случаях подразумевается "есть ли актуальное, развивающееся, где-то реально применяемое"...
     
     
  • 7.33, scor (ok), 23:09, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Обычно в таких случаях подразумевается "есть ли актуальное, развивающееся, где-то реально
    > применяемое"...

    Тогда нужно определиться в терминологии и контексте. Если имелись ввиду _именно_ ядра, то утвердительный ответ был дан. Если же имелось ввиду "низкоуровневое" программирование, как таковое, то и тут есть эволюция hOp -> House -> HaLVM (https://github.com/GaloisInc/HaLVM). Правда не знаю, послужили ли два предыдущих проекта основой для последнего, но толчком уж точно явились. Так что даже в этой области у функциональщиков не всё так плохо.:)

    PS. Собственно были даже попытки писать модули для Linux на хаскеле (http://www.haskell.org/haskellwiki/Kernel_Modules). Но это скорее proof-of-concept, т.е. можно, но зачем, если есть C?

     
  • 3.23, AnonymousSL (?), 16:14, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • –1 +/
    А где ядра операционок на C++, мэм?
     
     
  • 4.26, Crazy Alex (ok), 18:55, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    навскидку вспоминается ядро NT. Но если не нравится - полуось. Мргучая вещь была, кстати.
     
     
  • 5.32, scor (ok), 23:01, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > навскидку вспоминается ядро NT. Но если не нравится - полуось. Мргучая вещь
    > была, кстати.

    Немного противоречит вашему же #28.:) Они может где-то и применяются, но вот развивающимися и актуальными я бы их не назвал.:)

     
     
  • 6.40, Crazy Alex (ok), 04:30, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    NT вполне себе актуально. Просто здесь его некоторые активно не любят по понятным причинам, но ядро, насколько я знаю, неплохое.
     
     
  • 7.46, Vkni (ok), 15:48, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > NT вполне себе актуально. Просто здесь его некоторые активно не любят по
    > понятным причинам, но ядро, насколько я знаю, неплохое.

    Очень хорошее ядро. Позволяет, в частности, построить поверх себя POSIX, OS/2, Win32 и т.д.

     
  • 4.34, Aesthetus Animus (ok), 00:13, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > А где ядра операционок на C++

    L4

     
  • 2.6, Crazy Alex (ok), 02:39, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +4 +/
    Угу, язык равно чужеродный как для человека, который должен на нём писать, так и для машины, которая должна его исполнять. Зато красивые математические абстракции, угу.
     
     
  • 3.7, Crazy Alex (ok), 02:53, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Да, реплика у меня холиворная получилась, но это случайность - я не против хаскеля или функциональщины. Я всего лишь против её применения в продакшне в чистом виде. А вот как отдельные элементы она живёт отлчино - вон, всякие map уже давно норма. Внутри императивщины.
     
     
  • 4.9, Аноним (-), 03:06, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > Да, реплика у меня холиворная получилась,

    ...но суть дела отражает неплохо. Поэтому чего стесняться то?

     
  • 4.12, Аноним (-), 07:38, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • –8 +/
    > Я всего лишь...

    ...ламо. Мы уже поняли.

     
  • 3.15, Vkni (ok), 09:25, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > Угу, язык равно чужеродный как для человека, который должен на нём писать,
    > так и для машины, которая должна его исполнять. Зато красивые математические
    > абстракции, угу.

    C++ не менее чужероден.

     
     
  • 4.21, Аноним (-), 16:06, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • –1 +/
    >C++ не менее чужероден.

    По каким критериям, мальчик?

     
     
  • 5.27, Crazy Alex (ok), 18:58, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Вы б хоть погуглили прежде чем хамить...
     
  • 4.24, Crazy Alex (ok), 18:53, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Плюсы странны, но ровно по двум причинам. Во-первых, совместимость с С. Благодаря ей плюсы вообще взлетели, но красоты им она не добавляет. Во-вторых, ориентация на системщину, из-за которой, скажем, GC жестко прибивать нежелательно, а без него некоторые удобства не сделать.

    Но в принципе императивный подход - он же естественен до безобразия, люди от века составляли разные инструкции, в которых и ветвления были, и циклы... Например, представьте, как будете объяснять кому-то как взвесить килограмм сахара - всё будет.

     
     
  • 5.29, тоже Аноним (ok), 20:02, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > императивный подход - он же естественен до безобразия

    Причем как для человека, так и для компьютера. Все более высокоуровневые завихрения все равно выстраиваются в очередь перед процессором. Плюсы, в отличие от языков со всеми удобствами, позволяют этой очередью хоть как-то управлять.

     
     
  • 6.37, Vkni (ok), 04:02, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > Плюсы, в отличие от  языков со всеми удобствами, позволяют этой очередью хоть как-то управлять.

    Чаще всего это низкоуровневое управление не только нежелательно, а прямо таки вредно.

     
     
  • 7.39, Crazy Alex (ok), 04:23, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Дык там, где вредно - не берите плюсы, какие проблемы? Вон, в том же D или питоне или C# на худой конец всё это низкоуровневое скрыто.
     
  • 5.31, scor (ok), 22:57, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > ...люди от века составляли разные инструкции, в которых и ветвления были, и циклы...

    Только, как правило, все эти алгоритмы преследуют своей целью не выполнить некоторые действия ради выполнения этих действий, а получить некий результат от их выполнения. В этом и есть фундаментальная разница подходов и мышления: можно описывать алгоритм получения результата, а можно описывать сам результат. Всё сводится к поставленной задаче.

    > Например, представьте, как будете объяснять кому-то как взвесить килограмм сахара - всё будет.

    Вопрос подходов.:) Например, можно так: на одной чаше весов лежит эталонный киллограмм, а на другой сахар. Показания стрелки весов и есть ответ на вопрос: "сахар весит больше, меньше или ровно киллограм".

    data Indicator = Center
                   | ReferenceSide
                   | SugarSide

    type Result = String

    is1Kg :: Indicator -> Result
    is1Kg Center          = "exact 1Kg!"
    is1Kg ReferenceSide   = "less than. add more sugar"
    is1Kg SugarSide      = "too mutch. remove some sugar"

    *Main> is1Kg ReferenceSide
    "less than. add more sugar"
    *Main> is1Kg SugarSide
    "too mutch. remove some sugar"
    *Main> is1Kg Center
    "exact 1Kg!"
    *Main>

    Ваш императивный вариант будет проще в понимании?:)

     
     
  • 6.36, Crazy Alex (ok), 04:02, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Конечно проще. Здесь же натуральное изменение переменной, никакой иммутабельности.


    empty(scales.right_cup);
    scales.left_cup - WEIGHT_1_KG;
    add_some(SUGAR, scales.right_cup);
    do {
       ;
       if (scales.arrow.is_at_left())
         add_some(SUGAR, scales.right_cup);
       else if (scales.arrow.is_at_right)
         remove_some(SUGAR, scales.right_cup);
       else
        exit(0);
    } while(1);

    описывает ровно то, что делает человек. Читабельно даже если вообще ЯП не знать (для таких специально exit а не break поставил).

     
  • 5.35, Vkni (ok), 04:01, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > Плюсы странны, но ровно по двум причинам.

    Не только этим. Слишком сложный подход к шаблонам, к примеру. Груда костылей, связанных с историей.

    > Но в принципе императивный подход - он же естественен до безобразия, люди
    > от века составляли разные инструкции, в которых и ветвления были, и
    > циклы...

    Так императивный подход - это в С. С++ - объектно-ориентированный (это неестественная вещь) и "обобщённый" (сделан несколько костыльно и неудобно).

    > Например, представьте, как будете объяснять кому-то как взвесить килограмм сахара
    > - всё будет.

    Мне формулы писать тоже естественно. Опять-таки, после некоторой практики ловлю себя на том, что писать

    let iter factorial x =
        if x > 0 then
             x*(factorial (x - 1))
        else
            1;;

    мне "приятнее" чем через цикл.

     
     
  • 6.38, Crazy Alex (ok), 04:14, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    ООП тоже абсолютно естественно :-) Мы всю свою жизнь проводим, как-то взаимодействуя с чем-то, что мы выделили в среде как объекты, затем либо активно запрашиваем их состояние (глазками смотрим, ушками слушаем и т.п.) либо ждём,когда они нам как-то просигналят.

    ООП на примере. Есть у нас автомобиль. В нём - место для магнитофона.

    Магнитофон,понятное дело, реализует стандартные интерфейсы (форм-фактор, питание, колонки, интерфейс пользователя - те самые кнопочки - перемотка вперед-назад, старт/стоп, пауза). Он инкапсулирован - мы можем заменить его, скажем, на CD-плеер или mp3-проигрыватель (вот вам полиморфизм) и всё подключится точно также и кнопочки будут такими же, и машину нам для этого модифицировать не надо. Он может реализовывать дополнительный интерфейс - быть радиолой. Тогда его потребитель может этот интерфейс использовать, может - не использовать, но ничего другого это не коснётся.

    Наследования здесь нет, и это тоже важно - наследование, вообще говоря, является деталью реализации и отнюдь не обязательно (что в плюсах и дают дженерики, сделанные, согласен, криво).

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

     
     
  • 7.42, Vkni (ok), 05:23, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > ООП тоже абсолютно естественно :-) Мы всю свою жизнь проводим, как-то взаимодействуя
    > с чем-то, что мы выделили в среде как объекты, затем либо
    > активно запрашиваем их состояние (глазками смотрим, ушками слушаем и т.п.) либо
    > ждём,когда они нам как-то просигналят.

    Хорошо, неестественно наследование. Неестественны виртуальные функции. Так что тут мы с вами соглашаемся.

     
     
  • 8.47, Crazy Alex (ok), 17:01, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    ну да, это трудно понимаемый кусок, помню с каким трудом въезжал - ещё на паскал... текст свёрнут, показать
     
     
  • 9.49, Vkni (ok), 17:50, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Алекс, по моему опыту, переход на по-настоящему новые приёмы всегда приводит к м... текст свёрнут, показать
     
  • 7.45, scor (ok), 09:57, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > Хотя нет - эта не развернется, это ж не хвостовая рекурсия... будет стек создавать зачем-то...

    Тут вы правы. Гораздо читабельней и эффективней будет так:
    let fac n = product [1..n]

    Понять, что тут произойдёт и чему равен результат сможет почти кто угодно.:)

     
  • 6.41, Crazy Alex (ok), 04:35, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Да, насчет шаблонов. Они в плюсах редкая гадость (кстати,  в основном из-за того, что их попытались сделать функциональными - в D вон императивщина - удобная и понятная). Но сложная писанина на них, в общем-то, простым смертным особо и не требуется, это для разных авторов бустов и подобного.

    А простой template class MyClass<class T> :public T {...} наваять - ничего сложного, в общем-то. Простейшую шаблонную функцию - аналогично. Вон каноничный простейший пример:
    template <typename Type> Type max(Type a, Type b) {
        return a > b ? a : b;
    }

    ничего ж сложного. А дебри сможно оставить тем, кому они нужны. Авторы буста, вон, справляются.

     
     
  • 7.43, Vkni (ok), 05:27, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > А простой template class MyClass<class T> :public T {...} наваять - ничего
    > сложного, в общем-то.

    Алекс, наваять и метапрограммную фигню на них несложно. Сложно это читать. :-)

    Там, в шаблонах масса всяких косяков. Например, в С++98 целое число может быть параметром шаблона, а вещественное - нет.

     
  • 7.44, scor (ok), 09:31, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    сложного ничего конечно, но работает не так, как, очевидно, ожидается.:)
    чему равна в этом случае:
    max(1, 2.3);
    очевидно, что должно быть:
    max(1, 2.3) == 2.3
    но компилятор не согласен:)
    error: no matching function for call to 'max(int, double)'
    note: candidate is:
    note: template<class Type> Type max(Type, Type)
    note: template argument deduction/substitution failed
    note: deduced conflicting types for parameter 'Type' ('int' and 'double')

    в отличии от:
    Prelude> :t max
    max :: Ord a => a -> a -> a
    Prelude> max 1 2
    2
    Prelude> max 1.0 2
    2.0
    Prelude> max 1 2.0
    2.0
    Prelude> max 1 (2/3)
    1.0
    Prelude> :t 1
    1 :: Num a => a
    Prelude> :t 2.0
    2.0 :: Fractional a => a
    Prelude> :t (2/3)
    (2/3) :: Fractional a => a
    можно и явно указать, что мы хотим получить в результате:
    Prelude> max 1 (2.0 :: Double)
    2.0
    Prelude> :t max 1 (2.0 :: Double)
    max 1 (2.0 :: Double) :: Double

    Ну это я уже придираюсь видимо.:)

     
     
  • 8.48, Crazy Alex (ok), 17:04, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    ох, наверное, да В вашем примере же правила приведения какие-то отрабатывают, я... текст свёрнут, показать
     
     
  • 9.50, scor (ok), 18:01, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    http www ibm com developerworks ru library l-haskell2 index html ca drs- Типы ... текст свёрнут, показать
     
     
  • 10.51, Vkni (ok), 21:08, 06/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Хаскелл появился через год после введения шаблонов в С ... текст свёрнут, показать
     
  • 3.16, scor (ok), 09:29, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > Угу, язык равно чужеродный как для человека, который должен на нём писать, так и для машины, которая должна его исполнять. Зато красивые математические абстракции, угу.

    http://code.google.com/p/hedgewars/source/browse/#hg/gameServer
    Вроде и люди пишут, но и машины понимают. И это даже работает.:)

    ЗЫ. А абстракции действительно годные.:)

     
     
  • 4.25, Crazy Alex (ok), 18:54, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Дык, всегда найдётся кто-то со странно завернутыми мозгами :-) А уж о безумии математиков легенды ходят.
     

  • 1.4, Аноним (-), 00:30, 05/02/2013 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    AddressSanitizer: a fast memory error detector

    http://code.google.com/p/address-sanitizer/

     
     
  • 2.10, Путин В.В. (?), 03:48, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Адресной дизинфектор уже давно включен в состав clang. Просто компиляете проект с нужными опциями. Но адресной_сатана нужен только тогда когда ваша программа падает. Это не утилита для проверки кода.
     
     
  • 3.11, Аноним (-), 04:31, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Спасибо за описание, но какие флаги нужны для его вкомпиляции ?
     
     
  • 4.14, arka (?), 07:52, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    Там же в вики - http://code.google.com/p/address-sanitizer/wiki/Flags
     
  • 3.13, Аноним (-), 07:39, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    > Адресной дизинфектор уже давно включен в состав clang

    И с какой же версии?

    > Просто компиляете проект с нужными опциями

    И с какими же?

     
     
  • 4.19, Клыкастый (ok), 09:57, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +/
    http://clang.llvm.org/docs/AddressSanitizer.html
     

  • 1.18, Аноним (-), 09:57, 05/02/2013 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    boost уже проходит валидацию этим SMACK-ом?
     
     
  • 2.22, const86 (ok), 16:07, 05/02/2013 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Сначала SMACK должен пройти боевое крещение бустом :)
     

  • 1.20, anonymous (??), 13:58, 05/02/2013 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Static analysis of C/C++ code. Checks for: memory leaks, mismatching allocation-deallocation, buffer overrun, and many more.
    http://sourceforge.net/projects/cppcheck/
     
  • 1.30, EuPhobos (ok), 20:17, 05/02/2013 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/
    А Макаревич будет?
     
     Добавить комментарий
    Имя:
    E-Mail:
    Текст:



    Партнёры:
    PostgresPro
    Inferno Solutions
    Hosting by Hoster.ru
    Хостинг:

    Закладки на сайте
    Проследить за страницей
    Created 1996-2024 by Maxim Chirkov
    Добавить, Поддержать, Вебмастеру