Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] YASE lexicogrphical_compare

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