--- layout: fc_discuss_archives title: Message 95 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why3IDE Gtk-critical error



Hello, xiaolei,

This seems not an issue of frama-c. I suggest you also post this question
to the why3 discussion mailing list.

-david
On Nov 13, 2013 10:04 AM, "Xiao-lei Cui" <x_cui at hotmail.com> wrote:

> Hi,
>    I had some trouble with tracing the source code from proof obligations
> in why3ide. This happens under some scenario. For instance,  there is only
> one file in src/bsp/ folder: usrcofig.c (code is attached).
> When why3ide pops up, two proof obligation are generated, but I can not
> trace them to the locations in C code. As in the screen capture, the
> lower-right area is empty. What Claude suggests was to check standard
> error, so I looked into the error output. The following line produced at
> scene looks suspicious:
>
> (why3ide:2825): Gtk-CRITICAL **: gtk_text_buffer_emit_insert: assertion
> `g_utf8_validate (text, len, NULL)' failed
>
> The relevant output message is also attached.
>
> Another thing that confuses me is, why the IDE generate 2 proof
> obligation, given that I did not put any ACSL specification in that c file?
> One of the proof-obligation is to check overflow for this bit-wise
> operation,
> //where the type of  Sys_health is unsigned int:
> #define TRAP_DEBUG_ENABLE        ((unsigned int)(0X80000000))
>
> if (Sys_health==(Sys_health & TRAP_DEBUG_ENABLE))
> {//}
>
> Many thanks!
>
> cheers,
>
> xiaolei
>
>
> > Date: Tue, 12 Nov 2013 01:24:21 +0100
> > From: Claude.Marche at inria.fr
> > To: frama-c-discuss at lists.gforge.inria.fr
> > Subject: Re: [Frama-c-discuss] adding new provers to why3
> >
> >
> >
> > On 11/08/2013 08:11 AM, Xiao-lei Cui wrote:
> > >    Another question arises when I use why3 is that there seems no source
> > > code(ACSL and C) tracing from given proof obligations.
> >
> > You should see the positions of the PO in the lower right part of
> > Why3ide window. If you don't, then there is a problem: look at the
> > standard error if there are some problems reported.
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131113/02870efd/attachment.html>