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] RE: [Why-discuss] New Frama-C release
- Subject: [Frama-c-discuss] RE: [Why-discuss] New Frama-C release
- From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
- Date: Fri Nov 14 13:15:07 2008
- In-reply-to: <491AC17B.7090207@inria.fr>
- References: <011101c944b2$e37123c0$aa536b40$@com> <491AC17B.7090207@inria.fr>
First, sorry for sent the questions related to FRAMA-C to WHY list, and second, sorry for took so long to give you an answer. Well, I'm sending to you the code of a short example of what I'm trying to do. This code compiled with the following command: frama-c -jessie-analysis -jc-opt -separation short_file.c Gives the following output: Parsing [preprocessing] running gcc -C -E -I. -include C:/Frama-C/share/frama-c\jessie\jessie_prolog.h -dD short_file.c Cleaning unused parts Symbolic link Starting semantical analysis Starting Jessie translation Producing Jessie files in subdir short_file.jessie. File short_file.jessie/short_file.jc written. File short_file.jessie/short_file.cloc written. Calling Jessie tool. Uncaught exception: Failure("Unexpected internal region in logic") Failed to run: jessie -why-opt -split-user-conj -v -separation -locs short_file.cloc short_file.jc I already solved the problem of .whyrc file. I put it on my HOME=C:\Users\Barbara, and it works very well. -----Original Message----- From: Claude March? [mailto:Claude.Marche@inria.fr] Sent: quarta-feira, 12 de Novembro de 2008 11:44 To: B?rbara Vieira Cc: why-discuss@lists.gforge.inria.fr; frama-c-discuss@lists.gforge.inria.fr Subject: Re: [Why-discuss] New Frama-C release First thing: please send questions related to Frama-C to the Frama-C discuss list. B?rbara Vieira wrote: > I have a predicate very similar to the one that is on page 46 in the new > manual ? predicate permute. The fact is that when the code is compiled, and > why file is generated, the following error is presented: > ************************************ERROR IS PRESENTED > HERE*************************** File "why/ni_short.why", line 1765, > characters 28-524: > > This function does not have the right number of arguments > > make: *** [simplify/ni_short_why.sx] Error 1 > > Failed to run: make -f ni_short.makefile simplify > I think we already know about this problem, but to be sure, could you please send me the ni_short.c file ? > > But I think I solved the problem separating the two last axioms from the > ?axiomatic? definition and it works! Well, I don?t know if the problem is > solved or not, because after this I tried again to run the command and the > following output was presented: > > > > Parsing > > [preprocessing] running gcc -C -E -I. -include > C:/Frama-C/share/frama-c\jessie\jessie_prolog.h -dD ni_short.c > > File "ni_short.c", line 14, characters 4-9: syntax error while parsing > annotation Could you send the problematic annotations too, please ? > Well, I run why-config file and it generates a file .whyrc. And then I tried > to run the command again and the same error ?Why config file not found, > please run why-config first? was presented again. > I?m using Cygwin under Windows Vista. The oldest version worked very well > until know, but I installed the new one, because I want to see if some > features, that I need, are implemented in this new version. My guess is that .whyrc is searched in the current directory, whereas it should look in your "home" directory. Under unix, this is achieved by looking at the HOME environment variable. If you don't have it set under your environment, then you might sent it, e.g if .whyrc is in dir C:\PATH then set HOME=C:\PATH Any advice on alternative ways to access .whyrc in home dir under Windows is welcome... -- 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 | -------------- next part -------------- // Compilation: frama-c -jessie-analysis -jc-opt -separation file.c /*@ axiomatic Sumone { @ predicate sumone{L1,L2}(int k1,int a1[],int b1[], int k2,int a2[],int b2[], int n); @ axiom sumone_start{L} : @ \forall int k1, int k2,int a[],int b[], @ int n, int i; @ k1==k2 ==> sumone{L,L}(k1,a,b,k2,a,b,n); @ axiom sumone_inv{L1,L2,L3} : @ \forall int k1,int a1[],int b1[], @ int k2,int a2[],int b2[], @ int k3,int a3[],int b3[], @ int n; @ sumone{L1,L2}(k1,a1,b1,k2,a2,b2,n) @ ==> k3 == k2 + 1 @ ==> \at(b3[k2],L3) == \at(a3[k2],L3) + 1 @ ==> (\forall int l; 0<=l<n ==> \at(a3[l],L3)== \at(a2[l],L2)) @ ==> (\forall int l; 0<=l<n && k2!=l ==> \at(b3[l],L3)== \at(b2[l],L2)) @ ==> sumone{L1,L3}(k1,a1,b1,k3,b3,b3,n); @ axiom sumone_end{L1,L2} : @ \forall int a1[],int b1[],int k2,int a2[],int b2[],int n; @ sumone{L1,L2}((int)0,a1,b1,k2,a2,b2,n) @ ==> k2 == n @ ==> (\forall int l; 0<=l<n ==> \at(b2[l],L2) == \at(a2[l],L2) + 1) @ && (\forall int l; 0<=l<n ==> \at(a2[l],L2)== \at(a1[l],L1)); @ } @*/ /*int a[10]; int b[10]; int n = 10; */ /*@ requires @ \valid_range(a,0,n) && \valid_range(b,0,n) && @ n>0 && 0<=i<n; @ ensures b[i] == a[i]+ 1; @*/ void func(int i,int a[], int b[],int n){ int k; /*@ loop invariant @ sumone{Pre,Here}((int)0,a,b,k,a,b,n) && 0<=k<=n; @ loop variant @ (n-k); @*/ for(k=0;k<n;k++) { b[k] = a[k] + 1; } /*@ ghost goto L; @*/ /*@ ghost L: @*/ /*@ loop invariant @ (\forall int l; 0<=l<n ==> \at(b[l],L) == \at(b[l],Here)) && @ 0<=k<=n; @*/ for(k=0;k<n;k++) { a[k] = a[k]; } }
- Follow-Ups:
- [Frama-c-discuss] RE: [Why-discuss] New Frama-C release
- From: yannick.moy at gmail.com (Yannick Moy)
- [Frama-c-discuss] RE: [Why-discuss] New Frama-C release
- References:
- [Frama-c-discuss] Re: [Why-discuss] New Frama-C release
- From: Claude.Marche at inria.fr (Claude Marché)
- [Frama-c-discuss] Re: [Why-discuss] New Frama-C release
- Prev by Date: [Frama-c-discuss] Re: [Why-discuss] New Frama-C release
- Next by Date: [Frama-c-discuss] Value analysis plug-in algorithms
- Previous by thread: [Frama-c-discuss] Re: [Why-discuss] New Frama-C release
- Next by thread: [Frama-c-discuss] RE: [Why-discuss] New Frama-C release
- Index(es):