--- layout: fc_discuss_archives title: Message 100 from Frama-C-discuss on March 2009 ---
Hi Rovedy! I'm normal user of Frama-C tool, but I think I can help you in this situation, because I had the same problem. What I have is WHYLIB = C:/Frama-C/share/frama-c/why Try to do this. I don't know if it will work with you, but with me, worked. Best regards, B?rbara Vieira -----Original Message----- From: Rovedy Aparecida Busquim e Silva [mailto:rovedy at ig.com.br] Sent: sexta-feira, 27 de Mar?o de 2009 20:33 To: barbaraisabelvieira at gmail.com Subject: HELP FRAMA-C HI Barbara, I?m a brazilian student and I'm trying to use the tool FRAMA-C and plugin Jessie. I read yours hints in [Frama-c-discuss] list and I decided to write. Could you help me, please? I installed the FRAMA-C in the Windows (Windows Vista - C:\Frama-C). I installed the tool MinGW because of compiler gcc.exe. (C:\MinGW) I set the environment variable WHYLIB in the Windows: C:\> set WHYLIB=C:\Frama-C\share\frama-c\why When I run the frama-c, this error message is showed: ---------------------------------------------------------------------------- ------ C:\>frama-c -jessie-analysis max.c Parsing [preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\j essie_prolog.h -dD max.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir max.jessie File max.jessie/max.jc written. File max.jessie/max.cloc written. Calling Jessie tool in subdir max.jessie Generating Why function max Calling VCs generator. 'why -simplify [...] why/max.why' 'WHYLIB' is not recognized as an internal or external command, operable program or batch file. C:\mingw\bin\mingw32-make.exe: *** [simplify/max_why.sx] Error 1 ---------------------------------------------------------------------------- --- I used the simple source (max.x), available in the manual (Jessie Plugin Tutorial Lithium Version December 9,2008): int max(int i, int j) { return (i < j) ? j : i; } After the execution, I saw that the file max.why was created (C:\max.jessie\why). I tried to run the tool WHY alone, this error message is showed: ---------------------------------------------------------------------------- ------ C:\>why --coq c:\max.jessie\why\max.why File "c:\max.jessie\why\max.why", line 21, characters 45-54: Unbound type 'bitvector' ---------------------------------------------------------------------------- ------- I attached the file max.why. What is the problem? Can you help me, please? Sorry for my english. Thank you!! Rovedy