[Why3-club] why3IDE Gtk-critical error

Xiao-lei Cui x_cui at hotmail.com
Fri Nov 15 08:15:42 CET 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


 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131115/16bc676d/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/why3-club/attachments/20131115/16bc676d/attachment-0001.png>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: jessie_out.txt
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131115/16bc676d/attachment-0001.txt>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: usrConfig.c
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131115/16bc676d/attachment-0001.c>


More information about the Why3-club mailing list