frama-c: all VCs fail

Question

When I run frama-c -jessie -jessie-atp simplify max-anno.c I get the following:

[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

Nothing seems to be done. All VCs fail.

My guess is that something is not installed properly or is missing, but without more meaningful error messages, I'm stuck.

Answer 1

Simplify is not installed.

Simplify can be found here in binary form. I was unable to find the sources.

Move it to /usr/bin or somewhere else in your path.