--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on January 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Regression in Jessie with Frama-C Boron and Carbon beta 2



Hello Calude,

2011/1/25 Claude Marche <Claude.Marche at inria.fr>:
> Quick guess: avoid including the stdio.h in your code
>
> The stdio.h distributed with Frama-C is not fully supported by Jessie.

That helps! After specifying my own stdlib.h, I am able to generate
Jessie verification conditions and start Jessie GUI. I only needed to
add "#pragma SeparationPolicy(none)", after seeing following error
message:
"""
[jessie] Calling Jessie tool in subdir wholeprogram.jessie
File "wholeprogram.jc", line 255, characters 14-48: Unable to complete
region analysis, aborting. Consider using #pragma
SeparationPolicy(none)
[jessie] user error: Jessie subprocess failed:   jessie  -why-opt
-split-user-conj  -v       -locs wholeprogram.cloc wholeprogram.jc
"""

I need to look back at the manual to understand the implication of this pragma.

Thanks a lot!
Regards,
d.