--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on March 2009 ---
and offset_max [are used] to express the minimal/maximal offset at which a pointer can be indexed". However, "stdin" is a global (integer?) variable in the standard library. I don't understand why "stdin" would index a memory location and which one exactly. Could somebody explain to me what is exactly requested by Jessie? Do I need to prove "stdin == 0"? I'm calling Jessie with "-jessie-std-stubs" option. Thanks a lot, Yours, david [1] http://lists.gforge.inria.fr/pipermail/why-discuss/2008-March/000033.html