--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plugin



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