frama-cに欠けている機能のコードを追加する

Question

私の無知を許してください。プロジェクトのバックワードスライスを計算する必要があります。いくつかの検索の後、私はframa-cに出くわしました。私はFrama-cバージョン：Fluorine-20130601を入手した私のubuntuシステムにパッケージをダウンロードしました。私は初めてそれを使用しようとしています。私のプロジェクトで未定義の関数を見つけ出すと、ほとんどすべてのライブラリ関数は未定義です。printf、scanfなど（関数printfのコードも指定もありません）。チュートリアルによれば、未定義の関数すべてにスタブを追加する必要があります。 printfでも使用しているすべてのライブラリ関数用のコードを追加する必要がありますか？ご案内ください。

Answer 1

Variadicの機能に関する多くの改善点をもたらすFrama-C Phosphorusに更新する必要があります。特に、printf/scanfのような関数が定数形式の文字列で呼び出されたときに、自動的に仕様が生成されます。非可変関数の場合、いくつかの基本的な実装がディレクトリ$FRAMA_C_INSTALL/share/libc/*.c（最近のFrama-Cのリリース）で利用できます。