--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on May 2009 ---
Hi, I wrote a short program in order to find out whether Jessie understands the limits of the builti-in integer types (see Section 5.2.4.2.1 Sizes of integer types <limits.h> in http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1256.pdf). ----- char char_range(char i) { //@ assert i >= CHAR_MIN; //@ assert i <= CHAR_MAX; return i; } signed char schar_range(signed char i) { //@ assert i >= SCHAR_MIN; //@ assert i <= SCHAR_MAX; return i; } unsigned char uchar_range(unsigned char i) { //@ assert i >= UCHAR_MIN; //@ assert i <= UCHAR_MAX; return i; } short short_range(short i) { //@ assert i >= SHRT_MIN; //@ assert i <= SHRT_MAX; return i; } --------------- I compiled with "frama-c -jessie-analysis -jessie-int-model modulo - jessie-gui ranges.c" and noticed the following: 1.) I did not need to include limits.h So Jessie nows about these limits? 2.) All three provers (alt-ergo, yices, CVC3) that I used under Mac OS X cannot prove the line //@ assert i >= CHAR_MIN; Is this an oversight? 3.) The line //@ assert i >= UCHAR_MIN; is not recognised at all. Regards Jens, Berlin -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090524/465cbf4d/attachment.htm