[Why3-club] why3IDE Gtk-critical error

Claude Marche Claude.Marche at inria.fr
Sat Nov 16 09:32:04 CET 2013


As you guessed, there is a small issue when source files contain 
non-UTF8 characters.

This is now fix in the dev version of Why3. In the meantime, you can try 
to remove such characters in your source.

- Claude

On 11/15/2013 08:15 AM, Xiao-lei Cui 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
>
>
>
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>



More information about the Why3-club mailing list