在frama-c中添加缺少函數的代碼

請原諒我的無知。我需要爲一個項目計算後向切片。經過一番搜索後，我碰到了frama-c。我在我的ubuntu系統上下載了這個軟件包，這個軟件包得到了Frama-c版本：Fluorine-20130601。我正在嘗試第一次使用它。在我的項目中找到未定義的函數時，幾乎所有的庫函數都是未定義的，甚至printf，scanf等（函數printf都不是代碼或規範）。根據教程，我必須爲所有未定義的函數添加存根。我真的必須爲我使用的每個庫函數甚至printf添加代碼嗎？請指導。在frama-c中添加缺少函數的代碼

來源

2017-06-02 Jina Lee

首先，這個版本很舊！你應該使用最新版本的Frama-C 15磷。看看http://frama-c.com/download.html。 – Anne

您應該更新到Frama-C磷，這將帶來關於Variadic功能的大量改進。特別是，當printf/scanf-like函數在恆定格式字符串上被調用時，會自動生成規範。對於非可變參數函數，目錄$FRAMA_C_INSTALL/share/libc/*.c（在Frama-C的最新發行版中）提供了一些基本實現。

來源

2017-06-02 12:55:30 byako

由於設法安裝了frama-c鋁合金版本。未定義函數的數量急劇減少。（對不起，我沒有足夠的學分來接受答案） –

其實，作爲問問題的人，你總是可以接受答案：https://stackoverflow.com/help/someone-answers。此外，請注意鋁的缺失支持功能缺失。全面支持只能在磷中找到。 – byako

是的，但之前我不允許這麼做...因爲我的聲譽太低了！ –

在frama-c中添加缺少函數的代碼

回答

相關問題