--- layout: fc_discuss_archives title: Message 104 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Installation problem



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