--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on November 2012 ---
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>