Loading article…
| 開発者 | バグセン有限責任会社 |
|---|---|
| 安定版リリース | 3.12.0 / 2022年2月28日[1] |
| オペレーティング·システム | クロスプラットフォーム |
| タイプ | 静的コード分析 |
| ライセンス | 独自 |
| Webサイト | 翻訳元 |
ECLAIR は、BUGSENG, LLC がCおよびC++プログラムの自動分析、検証、テスト、変換用に開発した商用の静的コード分析ツールです。
機能
ECLAIRは、パルマ大学の応用形式手法研究所で開発された一連のプロトタイプ[2]を完全に再設計したものです。抽象解釈やモデル検査などの形式手法に基づく静的コード解析技術と制約充足技術を組み合わせて、ソースコード内の特定の実行時エラーが存在しないことを検出または証明し、プログラム解析と検証、プログラムテスト生成、プログラム変換をサポートします。
プログラム分析と検証に関しては、ECLAIR は実行時の異常がないことの静的な検出や証明ができるほか、MISRA C、MISRA C++、CERT C セキュアコーディング標準、CERT C++ セキュアコーディング標準、[3] High-Integrity C++、NASA / JPL C、ESA /BSSC C/C++、JSF C++、EC--、[4] Netrino Embedded C、[5] The Power of Ten (C)、[6] Industrial Strength C++ などのいくつかのコーディング標準への準拠を自動的にチェックできます。[7]
プログラム テストの場合、ECLAIR は、ユーザーが指定したカバレッジ基準に達するユニット テスト入力のセットを自動的に合成し、プログラム内の実行不可能な条件のためにこのカバレッジを達成できない場合にユーザーに警告します。
プログラム変換に関しては、ECLAIR は複雑なプログラム変換を実行するために使用できます。これらは、構文および意味に基づく基準によって指定され、これらの基準に一致するソース内のプログラム領域は、オプションでパラメーター化された置換によって置き換えることができます。
参照
参考文献
- ^ 「ニュース - BUGSENG」。bugseng.com 。 2021年4月4日閲覧。
- ^ R. Bagnara; PM Hill; E. Zaffanella (2007). 「プログラミング言語についての推論のための Prolog ベースの環境」. arXiv : 0711.0345 [cs.PL].
- ^ Seacord, Robert C. (2013). C および C++ でのセキュアコーディング。SEI シリーズ ソフトウェアエンジニアリング (第 2 版)。Addison-Wesley Professional。ISBN 978-0-321-82213-0。
- ^ Hatton, L. (2005). 「EC—組み込みシステム開発に適した、測定に基づいたより安全な ISO C のサブセット」.情報およびソフトウェア技術. 47 (3): 181–695. CiteSeerX 10.1.1.101.7828 . doi :10.1016/j.infsof.2004.08.001.
- ^ Barr, Michael (2008).組み込み C コーディング標準. Barr Group. ISBN 978-1442164826。
- ^ Gerald, J. (2006). 「10 の力: 安全性重視のコードを開発するためのルール」. Computer . 39 (6): 95–97. doi :10.1109/MC.2006.212. S2CID 7334261.
- ^ Henricson, Mats; Nyquist, Erik (1997). Industrial Strength C++ . Prentice-Hall PTR. ISBN 978-0131209657。
外部リンク
- ECLAIR公式サイト