--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie subprocess failed



Hi everyone,

I try to get Jessie running on Windows XP and cygwin. I've installed Frama-C, Z3, and Simplify. When I run Jessie on a test program, I get an error message:

~/progs/fc/swap> frama-c -jessie-analysis swap.c
Parsing
[preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD swap.c
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
Producing Jessie files in subdir swap.jessie
File swap.jessie/swap.jc written.
File swap.jessie/swap.cloc written.
Calling Jessie tool in subdir swap.jessie
Generating Why function Swap
Generating Why function main
Calling VCs generator.
why -simplify [...] why/swap.why
Fatal error: exception Sys_error("File exists")
make: *** [simplify/swap_why.sx] Error 2
Jessie subprocess failed: make -f swap.makefile simplify


Juan Soto reported a similar problem on this list and it was suggested to set some environment variables. If I add

export WHYLIB=/cygdrive/c/Frama-C/share/frama-c/why
export FRAMAC_SHARE=/cygdrive/c/Frama-C/share/frama-c

to my .bashrc, why doesn't find prelude.why:

~/progs/fc/swap> frama-c -jessie-analysis swap.c
[...]
make: Warning: File `swap.makefile' has modification time 0.09 s in the future
why -simplify [...] why/swap.why
cannot find prelude file /cygdrive/c/Frama-C/share/frama-c/why\why\prelude.why
make: *** [simplify/swap_why.sx] Error 1
Jessie subprocess failed: make -f swap.makefile simplify


Setting WHYLIB to C:/Frama-C/share/frama-c/why

export WHYLIB=C:/Frama-C/share/frama-c/why

as B?rbara Vieira suggested also doesn't work.


Any ideas?

- Boris