--- layout: fc_discuss_archives title: Message 104 from Frama-C-discuss on March 2009 ---
Hi, I'm trying to use the tool FRAMA-C and plugin Jessie. I have problems with installation of FRAMA-C. I read some hints in [Frama-c-discuss] list but it didn?t work. I will describe the steps that I did : 1. I have been downloaded the Windows installer frama-c-Lithium-20081201.exe. 2. I installed the FRAMA-C in the Windows XP in C:\Frama-C. 3. I installed the tool MinGW because of compiler gcc.exe. (C:\MinGW) 4. I set the environment variable WHYLIB in the Windows: C:\> set WHYLIB=C:/Frama-C/share/frama-c/why (Barbara?hint) 5. I tested the variable: C:\>echo %WHYLIB% C:/Frama-C/share/frama-c/why/ 6. The installation of FRAMA-C created the environment variable FRAMAC_SHARE (C:\Frama-C\share\frama-c). When I run the frama-c, this error message below 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; } It doesn't work. What am I doing wrong? And I have other problem. 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' ----------------------------------------------------------------------------------- What is the problem? Can you help me, please? Best regards, Rovedy