Frama-C安装过程
堵存
第一步：安装opam
opam的安装依赖make、m4和cc。
cc其实包含在gcc中。
sudo add-apt-repository ppa:avsm/ppa
sudo apt update
sudo apt install make m4 gcc opam第二步：opam初始化
sudo opam init完成初始化后运行下面指令
eval $(opam env)第三步：安装frama-C
sudo opam install depext
eval $(opam env)
sudo opam depext frama-c
sudo opam install frama-c第三条指令需要下载frama-c相关包，并进行编译安装，时间比较久，要耐心等待。
第四步：启动frama-c
eval $(opam env)每次在新的terminal上要寻找opam安装的库，需要先执行上面指令才可以找到frama-c。
第五步：更换wp插件的版本
目前wp插件需要依赖why3和alt-ergo这两个验证工具，
当我们执行下面的命令时：
frama-c -wp Armst.c #Armst.c代码在下文Armst.c代码如下：
#include <stdio.h>
void main()
{
long int n1, n2; /* intervals */
long int i, temp, num, rem;
printf("%d", 6/0);
printf("Enter two intervals: ");
scanf("%ld %ld", &n1, &n2);
printf("Armstrong numbers between %ld and %ld are: \n", n1, n2);
/*@ ensures n1 > 0;
ensures n2 > 0;
*/
/*@ loop invariant n1 <= i <= n2;
*/
for(i=n1; i<=n2; ++i)
{
/*@ assigns temp, num;
*/
temp=i;
num=0;
while(temp!=0)
{
/*@ assigns rem, num, temp;
*/
rem=(temp%10);
num+=rem*rem*rem;
temp/=10;
}
if(i==num)
printf("%ld\t ",i);
}
printf("\n");
}会出现如下错误：
[kernel] Parsing Armst.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] adpcm.c:288: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] adpcm.c:277: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] User Error: Prover 'alt-ergo' not found in why3.conf
[wp] Goal typed_encode_ensures : not tried
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.这个产生的主要原因是frama-c使用的why3有特定的版本，原因是版本不对导致无法识别。
why3 --version #1.2.1是ok的
alt-ergo -version #2.3.0是ok的
### 如果上面查看的版本不对，则通过opam进行重新安装编译即可
### opam重新安装编译指令如下
sudo opam install why3.1.2.1 #会同步把why3-ide等软件的版本
eval $(opam env) #刷新保存
sudo opam install altgr-ergo.2.3.0 #同理
eval $(opam env) #刷新保存
why3 config --detect #使用why3进行更新why3.conf文件
### 再执行frama-c 的 wp插件验证就ok了这样就可以愉快的使用wp插件了。
再次执行一下frama-c验证Armst.c
frama-c -wp Armst.c #Armst.c代码在下文其验证结果如下：
[kernel] Parsing Armst.c (with preprocessing)
[wp] [CFG] Goal main_ensures : Valid (Unreachable)
[wp] [CFG] Goal main_ensures_2 : Valid (Unreachable)
[wp] Warning: Missing RTE guards
[wp] Armst.c:39: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] Armst.c:27: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] Armst.c:15: Warning:
Allocation, initialization and danglingness not yet implemented
(\initialized(param0))
[wp] Armst.c:15: Warning:
Allocation, initialization and danglingness not yet implemented
(\initialized(param1))
[wp] 12 goals scheduled
[wp] [Alt-Ergo 2.3.0] Goal typed_main_call_printf_va_2_requires : Timeout (Qed:2ms) (3s)
[wp] [Alt-Ergo 2.3.0] Goal typed_main_call_printf_va_1_requires : Timeout (Qed:1ms) (3s)
[wp] [Alt-Ergo 2.3.0] Goal typed_main_loop_invariant_established : Timeout (Qed:8ms) (3s) (Stronger, 2 warnings)
[wp] [Alt-Ergo 2.3.0] Goal typed_main_loop_invariant_preserved : Timeout (Qed:14ms) (3s) (Stronger, 2 warnings)
[wp] [Alt-Ergo 2.3.0] Goal typed_main_call_printf_va_4_requires : Timeout (Qed:10ms) (4s) (Stronger, 2 warnings)
[wp] [Alt-Ergo 2.3.0] Goal typed_main_call_printf_va_3_requires : Timeout (Qed:4ms) (4s) (Stronger, 2 warnings)
[wp] [Alt-Ergo 2.3.0] Goal typed_main_call_scanf_va_1_requires_3 : Timeout (Qed:4ms) (4s)
[wp] Proved goals: 5 / 12
Qed: 5 (1ms-2ms)
Alt-Ergo 2.3.0: 0 (interrupted: 7)第六步：添加其他验证工具
安装CVC4
wget https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
sudo cp cvc4-1.7-x86_64-linux-opt /usr/local/bin/cvc4
sudo chmod +x /usr/local/bin/cvc4
cvc4 --version安装Z3
wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.6/z3-4.8.6-x64-ubuntu-16.04.zip
unzip z3-4.8.6-x64-ubuntu-16.04.zip
sudo cp z3-4.8.6-x64-ubuntu-16.04/bin/z3 /usr/local/bin
sudo chmod +x /usr/local/bin/z3
z3 -versionwhy3检测验证工具
why3检测验证工具，并更新why3.config文件
why3 config --detect
why3 --list-provers如果显示ok，即说明安装的验证工具被检测识别出来。
Found prover Alt-Ergo version 2.3.0, Ok.
Found prover CVC4 version 1.7, Ok.
Found prover Z3 version 4.8.6, Ok安装Coq
opam install coq #安装coq
eval $(opam env) #刷新opam配置
coqc -version
why3 config --detect #why3检测coq
类似资料：