--- layout: fc_discuss_archives title: Message 72 from Frama-C-discuss on December 2008 ---
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 >