--- layout: fc_discuss_archives title: Message 66 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



Thanks for your help. In fact, I just had to uninstall the Why old version
and reinstall Frama-C and everything worked very well. 

Best regards,
B?rbara 

-----Original Message-----
From: Claude March? [mailto:Claude.Marche at inria.fr] 
Sent: quinta-feira, 18 de Dezembro de 2008 08:31
To: B?rbara Vieira
Cc: frama-c-discuss at lists.gforge.inria.fr
Subject: Re: [Frama-c-discuss] FW: Windows Frama-C Release



B?rbara Vieira wrote:
> 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  
> 

Thanks !

> 
> I installed the new release in windows, and I?m getting problems with it.
> 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.


My guess is that the new jessie version of the jessie tool itself has 
not been installed, or more probable: that in your path an older version 
of jessie is found prior to the new one

try to remove a prior installation of Why, or indeed try to install the 
new Why release 2.17 which is the one synchronized with Lithium.

>  
> 
> 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;
> 
>    @ }
> 
>    @*/
> 
> 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? 

This is a new consistency check for axioms. It is not possible anymore 
to give axioms without declaring a new function symbol. In such a case 
you must use a lemma :

/*@ lemma valid_range_ax1a:
   @        \forall unsigned long k; k>=0 ==> 0<=(k >> 3L)<=k;
   @*/

such a lemma will generate a VC, that will probably not proved by auto 
provers since they do not now anything about the ">>" operator. You have 
just to ignore that VC.

side remark: I recomment to write this lemma as

/*@ lemma valid_range_ax1a:
   @        \forall integer k; k>=0 ==> 0<=(k >> 3L)<=k;
   @*/



-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |