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

[Frama-c-discuss] HELP FRAMA-C



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