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] FW: Windows Frama-C Release

  • Subject: [Frama-c-discuss] FW: Windows Frama-C Release
  • From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
  • Date: Wed, 17 Dec 2008 16:31:54 -0000
Dear all,

 

Congratulations for new frama-c release and thanks a lot for your support
and improvement of the tool. 

The new Jessie manual is very cool J  

 

I installed the new release in windows, and I?m getting problems with it.
For example, for this simple program:

#pragma JessieIntegerModel(exact)

 

 

//@ ensures *p >= 0;

void abs1(int *p) {

  if (*p < 0) *p = -*p;

}

 

/*@ requires \valid(p);

  @ ensures *p >= 0 

  @ ;

  @*/

void abs2(int *p) {

  if (*p < 0) *p = -*p;

}

 

 

 

That I took from Frama-C distribution, running the command: 

frama-c ?jessie-analysis sample.c

 it gives the following output :

 

Parsing

[preprocessing] running gcc -C -E -I. -include
C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD little_sample.c

Cleaning unused parts

Symbolic link

Starting semantical analysis

Starting Jessie translation

Producing Jessie files in subdir little_sample.jessie

File little_sample.jessie/little_sample.jc written.

File little_sample.jessie/little_sample.cloc written.

Calling Jessie tool in subdir little_sample.jessie

File "little_sample.jc", line 6, characters 18-19: syntax error

Jessie subprocess failed:    jessie  -why-opt -split-user-conj  -v
-locs little_sample.cloc little_sample.jc

 

This error is presented for every file. I tried examples that I had created
to the beta release that are not working here.

Is there something that I?m doing wrong ?!

 

 

I also installed the new release in Linux (Ubuntu), and the same example
worked very well.  So I think that the problem is in Windows version.

 

But I have another example with axiomatic definitions, that was working in
the beta version, that is not working any more( in Linux  and in Windows).
For this axiomatic definition:

 

/*@ axiomatic valid_range{

   @ axiom valid_range_ax1a:

   @        \forall unsigned long k; k>=0 ==> 0<=(k >> 3L)<=k;

   @ }

   @*/

 

 It presents the following output:

 

Parsing

[preprocessing] running gcc -C -E -I. -include
/usr/local/share/frama-c/jessie/jessie_prolog.h -dD rc4_acsl_1.4.c

Cleaning unused parts

Symbolic link

Starting semantical analysis

Starting Jessie translation

Producing Jessie files in subdir rc4_acsl_1.4.jessie

File rc4_acsl_1.4.jessie/rc4_acsl_1.4.jc written.

File rc4_acsl_1.4.jessie/rc4_acsl_1.4.cloc written.

Calling Jessie tool in subdir rc4_acsl_1.4.jessie

File "rc4_acsl_1.4.jc", line 370, characters 2-102: typing error: axiom
valid_range_ax1a should contain at least one occurrence of a symbol declared
in axiomatic valid_range

Jessie subprocess failed:    jessie  -why-opt -split-user-conj  -v
-locs rc4_acsl_1.4.cloc rc4_acsl_1.4.jc

 

How I can define now an axiom? 

 

 

Best regards,

B?rbara 

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081217/ba067200/attachment.htm