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] HELP FRAMA-C

  • Subject: [Frama-c-discuss] HELP FRAMA-C
  • From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
  • Date: Fri, 27 Mar 2009 23:44:21 +0100
  • In-reply-to: <df25346e0903271232s774b196aw9a09428f8bee0276@mail.gmail.com>
  • References: <df25346e0903271232s774b196aw9a09428f8bee0276@mail.gmail.com>
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