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

  • Subject: [Frama-c-discuss] why3IDE Gtk-critical error
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Wed, 13 Nov 2013 05:03:57 -0500
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>