--- layout: fc_discuss_archives title: Message 60 from Frama-C-discuss on December 2008 ---
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 |