linux - frama-c:所有VC都失败

当我运行frama-c -jessie -jessie-atp simplify max-anno.c时，得到以下结果：

[kernel] preprocessing with "gcc -C -E -I.  -dD max-anno.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir max-anno.jessie
[jessie] File max-anno.jessie/max-anno.jc written.
[jessie] File max-anno.jessie/max-anno.cloc written.
[jessie] Calling Jessie tool in subdir max-anno.jessie
Generating Why function max
[jessie] Calling VCs generator.
why -simplify [...] why/max-anno.why
Running Simplify on proof obligations
(. = valid * = invalid ? = unknown # = timeout ! = failure)
simplify/max-anno_why.sx      : !!!!!! (0/0/0/0/6)
total   :   6
valid   :   0 (  0%)
invalid :   0 (  0%)
unknown :   0 (  0%)
timeout :   0 (  0%)
failure :   6 (100%) <=======================================
total wallclock time : 0.01 sec
total CPU time       : 0.00 sec
valid VCs:
    average CPU time : -nan
    max CPU time     : 0.00
invalid VCs:
    average CPU time : -nan
    max CPU time     : 0.00
unknown VCs:
    average CPU time : -nan
    max CPU time     : 0.00

似乎什么都没做。所有风投都失败了。
我的猜测是有些东西没有正确安装或丢失，但是如果没有更有意义的错误消息，我就卡住了。

最佳答案

未安装Simplify。
在二进制形式中可以找到Simplifyhere。我找不到消息来源。
将它移到/usr/bin或您路径中的其他位置。

关于linux - frama-c:所有VC都失败，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/42602273/