Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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