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] Jessie plugin

  • Subject: [Frama-c-discuss] Jessie plugin
  • From: devia88 at mail.ru (Viktoriia)
  • Date: Fri, 14 May 2010 02:06:45 +0400
Hello.

I have just begun to use Frama-C. While trying to see the work of Jessie Plugin, I was confronted by such difficulty: when I call Jessie Plugin on standard examples from "Jessie Plugin Tutorial"(Lithium Version as well as Beryllium Version) I see such list of commands with error:

 >Frama-c -jessie -jessie-atp simplify Jessie/max.c
Parsing
[preprocessing] running gcc -C -E -I. -include  C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD Jessie/max.c
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
Producing Jessie files in subdir Jessie/max.jessie
File Jessie/max.jessie/max.jc written.
File Jessie/max.jessie/max.cloc written.
Calling Jessie tool in Jessie/max.jessie
Generating Why function max
Calling VCs generator.
 why -simplify [+.] why/max.why'
"WHYLIB" is neither internal nor external command, not an executable program or not a batch file.
make: *** [simplify/max_why.sx] Error 1
Jessie subprocess failed: make -f max.makefile simplify

Could anybody, please, help me to find the reason that causes this problem?

With best regards,
Viktoriia