--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on November 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem using jessie plug in



Hello all,

I am a new user of jessie plug in. I am using Frama-c version Boron and why version 2.24.
I installed the provers.

I started by the first example in the jessie tutorial.
After "frama-c -jessie -jessie-atp simplify max.c" command I get this:
[kernel] preprocessing with "gcc -C -E -I.? -dD max.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir max.jessie
[jessie] File max.jessie/max.jc written.
[jessie] File max.jessie/max.cloc written.
[jessie] Calling Jessie tool in subdir max.jessie
Generating Why function max
[jessie] Calling VCs generator.
why -simplify [...] why/max.why
Running Simplify on proof obligations
(. = valid * = invalid ? = unknown # = timeout ! = failure)
simplify/max_why.sx?????????? : Uncaught exception: Sys_error("simplify/max_why.sx: No such file or directory")
make: *** [simplify] Error 2
[jessie] user error: Jessie subprocess failed: make -f max.makefile simplify


Can anyone help me to know the origin of this error and why I am not getting same thing as in the tutorial .

Best regards,
Intissar 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121120/76182c29/attachment.html>