--- layout: fc_discuss_archives title: Message 64 from Frama-C-discuss on May 2010 ---
Boris Hollas a ?crit : > On Mon, 2010-05-17 at 14:59 +0200, Julien Signoles wrote: > >> It works if you insert a space between .. and BUFF_SIZE like this: >> >> /*@ requires \valid(msg+(0.. BUFF_SIZE)); >> > > Jessie is still unable to verify the postcondition in my example. The > relevant VC is integer_of_int8(select(char_P_char_M_msg_1_1, shift(msg, > 4))) = 0. > I use the Beryllium2 distribution. Which provers do you use? I test Alt-Ergo, Simplify and Z3. The first tool is still unable to verify the postcondition. But the two other tools do the job. Combining several provers is often useful. -- Julien