# Frama-C 心得筆記 Frama-c C 語言驗證工具組 > 自己的期許希望可以減少自己犯傻的錯誤 ## 安裝 https://frama-c.com/html/installations/manganese.html#installing-frama-c-on-windows-via-wsl WSL 需要額外安裝 ```bash sudo apt install yaru-theme-icon ``` ## WSL執行 https://frama-c.com/html/installations/manganese.html#installing-custom-versions-of-frama-c ```bash export LIBGL_ALWAYS_INDIRECT=1 export DISPLAY=$(cat /etc/resolv.conf | grep nameserver | awk '{print $2; exit;}'):0.0 frama-c-gui ``` ## Ubnubtu 執行 Ubuntu 需要在~/.bashrc 最後一行放這一段 就可以執行opam 的Code 了 ```bash eval `opam config env ``` ## 官方教學 https://frama-c.com/html/teaching.html > 好多法文看不懂 ## 範例A https://frama-c.com/fc-plugins/eva.html ![](https://i.imgur.com/Bk6oxDZ.png) 1. 設定EVA 的Main 為fact 2. 按下Run 3. 點選中間畫面的變數，x、y、z 下方就可以看到順序 ## 範例B 分析Arduino Code 當作Real Code 好了 ### 目標計算出#define 的變數結果 https://frama-c.com/2018/07/06/Parsing-realistic-code-bases-with-Frama-C.pdf ## 閱讀清單 - [ ] https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf - [ ] frama-c-eva-manual.pdf - [ ] Apreenix A. - [ ] https://arxiv.org/pdf/2111.08208.pdf - [ ] http://julien.signoles.free.fr/publis/2016_rv.pdf - [ ] https://julien-signoles.fr/publis/2013_rv.pdf - [ ] https://nikolai-kosmatov.eu/publications/blanchard_kl_hpcs_2018.pdf