--- layout: fc_discuss_archives title: Message 70 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



Hello,

On Sun, May 24, 2009 at 20:49, Jens Gerlach
<jens.gerlach at first.fraunhofer.de> wrote:
> 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?

Yes, see FRAMAC_INSTALLATION_PATH/share/frama-c/jessie/limits.h

> 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?

I don't know.

The proof obligation for this property is:
""""
char_range_ensures_default_po_1

i_1: int8
H1: true = true


integer_of_int8(i_1) >= 0
"""

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.


unsigned char uchar_range(unsigned char i)
{
    //@ assert i >= 0;
    //@ assert i <= UCHAR_MAX;
    return i;
}


Sincerely yours,
david