--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on May 2009 ---
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