--- layout: fc_discuss_archives title: Message 67 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie and CHAR_MIN



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