当我运行 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
似乎什么都没做。所有 VC 都失败了。
我的猜测是有些东西没有正确安装或丢失,但没有更有意义的错误消息,我被卡住了。
最佳答案
关于linux - frama-c:所有 VC 都失败,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/42602273/