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];
    }

   
}