--- layout: fc_discuss_archives title: Message 95 from Frama-C-discuss on November 2013 ---
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>