--- layout: fc_discuss_archives title: Message 109 from Frama-C-discuss on October 2008 ---
Something I forgot to mention: Your [assumes] clauses mention variable \result. A warning is now issued that says: Error during analysis of annotation: \result meaningless Indeed, [assumes] clauses are interpreted in the pre-state of the function, where \result is indeed meaningless. The correct way to go is to write an implication in the postcondition, as I did in my answer. Cheers, Yannick On Fri, Oct 24, 2008 at 1:38 AM, Yannick Moy <yannick.moy@gmail.com> wrote: > Hi, > > The current CVS (henceforth the next release) correctly treats the > following valid annotated program. Please note I use only math integers in > logic, it is usually easier because it removes the need for casts from C > ints to math integers. > > /*@ > @logic integer min(integer a, integer b) = > @ (a < b) ? a : b; > @ > */ > > /*@ > requires last1 > first1; > requires \valid_range (first1, 0, last1-first1-1); > requires \valid_range (first2, 0, last2-first2-1); > behavior is_less: > ensures \result == \true ==> \exists integer k2; \forall integer k1; > 0 <= k1 <= k2 < min(last1-first1, last2-first2) > ==> ((first1[k2] < first2[k2]) ^^ (last1-first1 < last2-first2)) && > first1[k1] <= first2[k1]; > > behavior is_not_less: > ensures \result == \false ==> \forall integer k2; \forall integer k1; > 0 <= k1 <= k2 < min(last1-first1, last2-first2) > ==> first1[k2] >= first2[k2] || first1[k1] >= first2[k1]; > > */ > int lexicographical_compare_int_array (int* first1, int* last1, int* > first2, int* last2 ) > { > //@ ghost int* a = first1; > //@ ghost int* b = first2; > //@ ghost int length1 = last1-first1; > //@ ghost int length2 = last2-first2; > > /*@ > loop invariant a <= first1 <= last1; > loop invariant first2 - b == first1 - a; > loop invariant b <= first2 <= last2; > > loop invariant \forall integer k; 0 <= k < first1-a ==> a[k] == b[k]; > > */ > for ( ; first1 != last1 && first2 != last2; ++first1, ++first2) > { > if (*first1 < *first2) > return 1; > if (*first2 < *first1) > return 0; > } > return first1 == last1 && first2 != last2; > } > > At first glance, your annotations seem ok, but you should try it yourself > with Frama-C next release. Guessing annotations is not very successful in > general, much better to run them. > > HTH > Yannick > > PS: I had problems just to have the code compile, could you make sure you > do not have any errors besides an error that you want to report? Thanks. > > > On Thu, Oct 23, 2008 at 8:25 AM, Christoph Weber < > Christoph.Weber@first.fraunhofer.de> wrote: > >> Hello, >> today I have something more complex. >> >> I tried to specify a function lexicogrphical_compare. This function shall >> compare two arrays, and return true if the first array is smaller than the >> other. >> >> First I need a conditional assignment. I did not find any other condition >> and even this one is not recognized. >> /*@ >> logic integer min(int a, int b) = >> (a < b) ? a : b; >> >> */ >> >> /*@ >> requires last > first; >> requires \valid_range (first1, 0, last1-first1-1); >> requires \valid_range (first2, 0, last2-first2-1); >> behavior is_less: >> assumes \result == true; >> ensures \exists integer k2; \forall integer k1; >> 0 <= k1 <= k2 < min(last1-first1, last2-first2) >> ==> ((first1[k2] < first2[k2]) ^^ (last1-first1 < last2-first2)) && >> first1[k1] <= first2[k1]; >> >> behavior is_not_less: >> assumes \result == false; >> 0 <= k1 <= k2 < min(last1-first1, last2-first2) >> ==> first1[k2] >= first2[k2] || first1[k1] >= first2[k1]; >> >> */ >> bool lexicographical_compare_int_array (int* first1, int* last1, int* >> first2, int* last2 ) >> { >> //@ ghost int* a = first1; >> //@ ghost int* b = first2; >> //@ ghost int length1 = last1-first1; >> //@ ghost int length2 = last2-first2; >> >> /*@ >> loop invariant a <= first1 <= last1; >> loop invariant first2 - b == first1 - a; >> loop invariant b <= first2 <= last2; >> >> loop invariant \forall integer k; 0 <= k < first1-a ==> a[k] == >> b[k]; >> */ >> for ( ; first1 != last1 && first2 != last2; ++first1, ++first2) >> { >> if (*first1 < *first2) >> return true; >> if (*first2 < *first1) >> return false; >> } >> return first1 == last1 && first2 != last2; >> } >> >> The Question is, what has to be done, that Jessie understands what I want >> to describe? And is my loop invariant strong/specific enough. >> >> Merci d'avance. >> >> Christoph >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss@lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss >> >> > > > -- > Yannick > -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081024/93f33210/attachment.html