--- layout: fc_discuss_archives title: Message 94 from Frama-C-discuss on November 2013 ---
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. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131113/7ba10240/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: Screenshot from 2013-11-13 171134.png Type: image/png Size: 231997 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131113/7ba10240/attachment-0001.png> -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: jessie_out.txt URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131113/7ba10240/attachment-0001.txt> -------------- next part -------------- An embedded and charset-unspecified text was scrubbed... Name: usrConfig.c URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131113/7ba10240/attachment-0001.c>