--- layout: fc_discuss_archives title: Message 58 from Frama-C-discuss on January 2011 ---
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.