--- layout: fc_discuss_archives title: Message 55 from Frama-C-discuss on December 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] FW: Windows Frama-C Release



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