Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Installation problem

  • Subject: [Frama-c-discuss] Installation problem
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Mon, 30 Mar 2009 17:36:18 -0300
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