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 subprocess failed

  • Subject: [Frama-c-discuss] Jessie subprocess failed
  • From: Boris.Hollas at de.bosch.com (Hollas Boris (CR/AEY1))
  • Date: Tue, 24 Mar 2009 16:47:22 +0100
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