frama-c: alle VCs scheitern

Question

Wenn ich frama-c -jessie -jessie-atp simplify max-anno.c laufen bekomme ich die folgende:

[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 

nichts getan zu sein scheint. Alle VCs schlagen fehl.

Meine Vermutung ist, dass etwas nicht richtig installiert ist oder fehlt, aber ohne aussagekräftige Fehlermeldungen, stecke ich fest.

Answer 1

Simplify ist nicht installiert.

Simplify kann here in binärer Form gefunden werden. Ich konnte die Quellen nicht finden.

Verschieben Sie es nach/usr/bin oder woanders in Ihrem Pfad.