Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Problem using jessie plug in
  • From: intissar_mzalouat at yahoo.fr (intissar mzalouat)
  • Date: Tue, 20 Nov 2012 08:38:36 +0000 (GMT)
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>