私は、Why2、Why3、および Coq と共に Frama-C Neon (Ubuntu) を正常にコンパイルしました。
以前のバージョン (Nitrogen) では、次のようなシンボルを定義することで、特定のヒープ モデルを選択することができました。
#define FRAMA_C_MALLOC_HEAP
等々。
Frama-C Neonのユーザー マニュアルでは、ファイルを含めるように提案されていますshare/malloc.cが、見つかりません。
- Frama-C Nitrogen には
share/malloc.cとの両方が含まれていますshare/libc/stdlib.c(後者は正常に機能しました)。 - Frama-C Fluorine 3 には次の成分
share/stdlib.cのみが含まれています。 - Frama-C Fluorine 2 にはどちらも含まれていません。
- Frama-C Neon にはどちらも含まれていません。
さらに、Fluorine 3 の変更ログには、「欠落している C ライブラリ ファイルを追加する」と記載されています。
シンボルは非推奨ですかFRAMA_C_MALLOC_*、それとも Neon ソース配布はやや不完全ですか?