ВСПЫШКА
 | Эта статья нуждается в дополнительных цитатах для проверки . ( декабрь 2012 г. ) |
| Разработчик(и) | БУГСЕНГ, ООО |
|---|---|
| Стабильная версия | 3.12.0 / 28 февраля 2022 г [1] |
| Операционная система | Кросс-платформенный |
| Тип | Статический анализ кода |
| Лицензия | Собственный |
| Веб-сайт | www |
ECLAIR — это коммерческий инструмент статического анализа кода, разработанный BUGSENG, LLC для автоматического анализа, проверки, тестирования и преобразования программ на C и C++ .
Возможности
[ редактировать ]ECLAIR — это полная модернизация серии прототипов. [2] разработан в Лаборатории прикладных формальных методов Пармского университета . Он использует методы статического анализа кода на основе формальных методов, такие как абстрактная интерпретация и проверка модели, в сочетании с методами удовлетворения ограничений для обнаружения или доказательства отсутствия определенных ошибок во время выполнения в исходном коде , а также обеспечивает поддержку анализа и проверки программ, создания тестов программы и трансформация программы.
Что касается анализа и проверки программ, ECLAIR может статически обнаруживать или доказывать отсутствие аномалий во время выполнения, а также автоматически проверять соответствие нескольким стандартам кодирования, таким как MISRA C , MISRA C++, CERT C Secure Coding Standard, CERT C++ Secure. Стандарт кодирования, [3] C++ с высокой степенью интеграции, NASA / JPL C, ESA /BSSC C/C++, JSF C++, EC--, [4] Нетрино Встроенный C, [5] Сила десяти (С), [6] Промышленная мощь C++. [7]
Для тестирования программы ECLAIR может автоматически синтезировать наборы входных данных модульного теста, которые достигают заданного пользователем критерия покрытия, предупреждая пользователя, когда из-за невыполнимых условий в программе это покрытие не может быть достигнуто.
Что касается преобразования программ, ECLAIR можно использовать для выполнения сложных преобразований программ: они определяются синтаксическими и семантическими критериями; программные области в источнике, соответствующие этим критериям, могут быть опционально заменены параметризованной заменой.
См. также
[ редактировать ]- Абстрактная интерпретация
- Проверка модели
- Статический анализ кода
- Список инструментов для статического анализа кода
Ссылки
[ редактировать ]- ^ «Новости – БУГСЕНГ» . bugseng.com . Проверено 4 апреля 2021 г.
- ^ Р. Баньяра; П.М. Хилл; Э. Заффанелла (2007). «Среда для рассуждений о языках программирования на основе Пролога». arXiv : 0711.0345 [ cs.PL ].
- ^ Сикорд, Роберт С. (2013). Безопасное программирование на C и C++ . Серия SEI по разработке программного обеспечения (2-е изд.). Аддисон-Уэсли Профессионал. ISBN 978-0-321-82213-0 .
- ^ Хаттон, Л. (2005). «EC - более безопасное подмножество ISO C, основанное на измерениях, подходящее для разработки встроенных систем». Информационные и программные технологии . 47 (3): 181–695. CiteSeerX 10.1.1.101.7828 . дои : 10.1016/j.infsof.2004.08.001 .
- ^ Барр, Майкл (2008). Встроенный стандарт кодирования C. Группа Барр. ISBN 978-1442164826 .
- ^ Джеральд, Дж. (2006). «Сила 10: правила разработки кода, критического для безопасности». Компьютер . 39 (6): 95–97. дои : 10.1109/MC.2006.212 . S2CID 7334261 .
- ^ Хенриксон, Матс; Найквист, Эрик (1997). Промышленная мощь C++ . ПТР Прентис-Холл. ISBN 978-0131209657 .