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

[Frama-c-discuss] Installation Problem



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