--- layout: fc_discuss_archives title: Message 72 from Frama-C-discuss on May 2009 ---
> > So a C "char" is mapped to a Why "int8". However I could not find > where this int8 is defined. > >> 3.) The line //@ assert i >= UCHAR_MIN; is not recognised at all. > > Notice that I you just put "//@ assert i >= 0;" it also fails. > You are right. However, for unsigned short and unsigned int the assertion "//@ assert i >= 0;" is proven. Looks like a problem with char. Jens -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090525/d9b8a335/attachment.htm -------------- next part -------------- A non-text attachment was scrubbed... Name: ranges.c Type: application/octet-stream Size: 775 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090525/d9b8a335/attachment.obj -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090525/d9b8a335/attachment-0001.htm