--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on July 2013 ---
Hi You're missing some requires clauses to guarantee that the memory areas pointed by satmin, satmax and error are valid and separated from each other, ie: the memory areas do not overlap. Adding this to the function's contract works for me: requires \valid(satmin); requires \valid(satmax); requires \valid(error); requires \separated(satmin, satmax, error); Proved with Fluorine 2, WP and Alt-ergo 0.95.1 2013/7/11 Tailliar Alice <alice.tailliar at etu.enseeiht.fr> > Hello, > > I contact you because I can't manage to prove all the ensures clauses of > the function in the attached file. > > What is happening is that I can only prove the ensures clauses about the > last affection, even if I change the order of the three instructions. When > I try to prove the others ensures clauses by WP, alt-Ergo fails and detects > a syntax error in a file generated by frama-c. > > So I would like to know if there is a problem in my function that prevents > frama-c from doing its job and how I can fix it, or if the problem comes > from frama-c. > > Thank you for yours answers, > Best regards > > Alice Tailliar > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Cumprimentos, Cristiano Sousa -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130711/8d0f282c/attachment.html>