このリリースは C のフロント エンドと価値分析の改善をもたらします (自動状況依存のデータ フロー分析） WP (ホーア論理を用いた機能性の検証)、(世代) の簡略化、コンパイル可能な C プログラムのスライシングとプラグイン。
This release brings improvements in the C front-end and in the value analysis (automatic context-sensitive data flow analysis), WP (verification of functional properties using Hoare logic), slicing (generation of simplified, compilable C programs), and plug-ins.
この新しいメジャー バージョンには、多くのバグ修正と改善が含まれています。パフォーマンス値の解析、スライシング プラグイン、プラグイン C プログラムに対する線形時相論理式の確認のための Aoraï、GUI、およびカーネル プロパティの状態をプラグインのコラボレーションを向上します。
This new major version includes many bugfixes and improvements. Performance improvements benefit the Value Analysis and Slicing plug-ins, the Aoraï plug-in for verification of C programs against Linear Temporal Logic formulas, the GUI, and kernel property statuses for plug-in collaboration.
This release fixes bugs identified in beta version 20101202 and makes the API stable for external plug-in developers. Value analysis users, consider applying this patch before compiling: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-February/002527.html . Jessie users: this release is compatible with Why 2.29, available from http://why.lri.fr/ . WP users: the WP plug-in will be made available separately later.
Many bugfixes. Small usability improvements to the GUI.
A few API changes. Value analysis: improved speed and memory consumption; handle single-precision type float as such (instead of lumping it with double as previously); better handling of structs passed as arguments to functions. A new deductive verification plug-in: WP.
The support for the ACSL specification language was improved framework-wide. The value analysis benefits from numerous new options to improve precision and scale to larger codebases.
