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