--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on December 2008 ---
Hello, Le vendredi 19 d?cembre 2008 ? 18:58 +0100, Benjamin Monate a ?crit : > Thanks for your report, > > As I do not have any access to a Windows Vista installation, I cannot > reproduce the problem you describe. > Could you try to run > > $ FRAMAC_SHARE=C:/Frama-C/share/frama-c frama-c -jessie-analysis -jessie-gui a.c > > and report what happens? I've recently seen that the jessie plug-in does not work when FRAMAC_SHARE is set because the file prelude.why is not found (it is searched in an unexisting directory). I've already reported this bug (internal bts#418). Best regards, Julien > > Thanks for your interest in Frama-C! > Cheers, > Benjamin > > 2008/12/19 Juan Soto <juan.soto at first.fraunhofer.de>: > > *Folks,* > > > > *Thanks for the updated Frama-C release. Fortunately, I was able to get > > the Frama-C tools up and running on my personal laptop (Windows XP) > > using the binary installer.* > > > > *However, I have some installation problems on my office laptop (Windows > > Vista). In particular, the problem lies when I attempt to execute the > > Jessie plugin.* > > > > $ frama-c -jessie-analysis -jessie-gui a.c > > > > Parsing > > > > [preprocessing] running gcc -C -E -I. -include > > */usr/local/share/frama-c\jessie\jessie_prolog.h* -dD a.c > > > > Cleaning unused parts > > > > Symbolic link > > > > Starting semantical analysis > > > > Starting Jessie translation > > > > Producing Jessie files in subdir a.jessie > > > > File a.jessie/a.jc written. > > > > File a.jessie/a.cloc written. > > > > Calling Jessie tool in subdir a.jessie > > > > Generating Why function max > > > > Calling VCs generator. > > > > gwhy-bin [...] why/a.why > > > > *cannot find prelude file* */usr/local/share/frama-c/why\why\prelude.why* > > > > make: *** [a.stat] Error 1 > > > > Jessie subprocess failed: make -f a.makefile gui > > > > *To help track down the problem, I uninstalled all previous versions of > > Frama-C, Why and Cygwin, then reinstalled both Cygwin and the > > binary-installer for Lithium (under the Cygwin folder in an attempt to > > see if this would rectify the problem). I verified that I have both the > > latest version for Why 2.17 and the correct Frama-C Lithium version > > running. I also tried it under the default folder, "C:\Frama-C", but > > alas this did not help. Unfortunately, the [*forward slash, backslash*] > > problem still lingers. I realize there was a similar post some time ago, > > see: > > **http://lists.gforge.inria.fr/pipermail/why-discuss/2008-February/000025.html.*** > > > > *Perhaps, additional guidelines need to be included in the installation > > instructions, e.g., are there any other Cygwin specific options that > > need to be pre-configured other than /gcc/? * > > > > *Your help would be greatly appreciated.* > > > > Regards, > > > > Juan > > > > _______________________________________________ > > Frama-c-discuss mailing list > > Frama-c-discuss at lists.gforge.inria.fr > > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss