--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on April 2012 ---
Hi, > 3) as Boris Hollas pointed out, an 'Unknown' status does not > intrinsically indicate a deficiency in the analyzer. For the record, I didn't suspected a deficiency in the analyzer but rather in my understanding of how V.A. works. I was right with that. > If you want to avoid those warnings, position your disjunction _before_ your > ? ? ? ?/*@ assert ( in_int8 < 0 ) || ( in_int8 >= 0 ); */ > ? ? ? ?uint8 out_uint8 = abs8(in_int8); So a "requires" in a contract hasn't the same effect? > Hope this helps, Yes, definitively. Thank you very much. Sylvain