Frama-C-discuss mailing list archives

yannick.moy at gmail.com (Yannick Moy) · Fri Nov 14 17:21:18 2008

Hi,

The bug you found is the same as the one reported recently by Christoph
Weber. I sent an email on Nov 7 to explain in which cases this message
"Unexpected internal region in logic" is issued, and why it is a bug in his
and your examples. It is on top of our list, so we will notify the list when
it is corrected.

Regards,
Yannick

On Fri, Nov 14, 2008 at 1:15 PM, B?rbara Vieira <
barbaraisabelvieira@gmail.com> wrote:

> 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 <http://www.lri.fr/%7Emarche/F-91893> ORSAY Cedex
>    |
>
>
>
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>

-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081114/b60cb469/attachment.html

Frama-C-discuss mailing list archives

[Frama-c-discuss] RE: [Why-discuss] New Frama-C release