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] 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