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: Thu, 18 Dec 2008 11:37:52 -0000
  • In-reply-to: <494A0A59.3010909@inria.fr>
  • References: <00c401c96064$f97ee990$ec7cbcb0$@com> <494A0A59.3010909@inria.fr>
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                    |