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

[Frama-c-discuss] Installation Problem



Hi,

Sorry for the inconvenience.
Could you try to set FRAMAC_SHARE to a windows like path with forward
slahes like
C:/Frama-C/share/frama-c ?

Cheers,
Benjamin
2008/12/22 Juan Soto <juan.soto at first.fraunhofer.de>:
> Greetings,
>
>
>
> (1) Here are the results from the call to the Jessie plugin via setting the FRAMAC_SHARE environment variable.
>
>
>
> $ FRAMAC_SHARE=/usr/local/Frama-C/bin/frama-c frama-c -jessie-analysis -jessie-gui a.c
>
> Parsing
>
> [preprocessing] running gcc -C -E -I. -include /usr/local/Frama-C/bin/frama-c\jessie\jessie_prolog.h -dD a.c
>
> cc1: /usr/local/Frama-C/bin/frama-c\jessie\jessie_prolog.h: No such file or directory
>
> Failed to run: gcc -C -E -I. -include /usr/local/Frama-C/bin/frama-c\jessie\jessie_prolog.h -dD -o "C:\Users\jua\AppData\Local\Temp\a.c3bc755.i" "a.c"
>
>
>
>           You may set the CPP environment variable to select the proper preprocessor command ...
>
>        or use the -cpp-command program argument.
>
> Fatal error: exception Sys_error("C:\Users\sotjua\AppData\Local\Temp\a.c3bc755.i: No such file or directory")
>
>
>
> From the looks of things there appears to be a problem with respect to forward slashes and backward slashes.
>
>
>
> (2) Also, on a slightly related problem, I experienced an odd problem on my home laptop. I downloaded and installed Z3 without any problems, i.e., I am able to invoke it from a DOS command shell).
>
> However, when I ran the why-config utility, there was a problem with respect to the detection of the Z3 prover. Has anyone else encountered this? I was able to confirm that there was a problem when
>
> I tried to invoke Z3 directly from within a Cygwin shell.
>
>
>
> The output from the why-config call is below:
>
>
>
> $ why-config
>
> starting autodetection...
>
> 'alt-ergo' is not recognized as an internal or external command, operable program or batch file.
>
> command alt-ergo failed
>
> Found prover Alt-Ergo version 0.8
>
> Found prover Simplify version 1.5.4
>
> The system cannot execute the specified program.
>
> command z3 failed
>
> The system cannot execute the specified program.
>
> command z3 failed
>
> detection of prover Z3 failed
>
> Found prover Yices version 1.0.15
>
> Found prover CVC3 version 1.5
>
> Found prover Coq version 8.1pl4
>
> detection done.
>
> writing rc file...
>
>
>
> Any thoughts on what can be done to resolve these problems?
>
>
>
> Thanks,
>
> 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
>