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: Claude.Marche at inria.fr (Claude Marché)
  • Date: Wed Nov 12 12:43:54 2008
  • In-reply-to: <011101c944b2$e37123c0$aa536b40$@com>
  • References: <011101c944b2$e37123c0$aa536b40$@com>
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                    |