# 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] adjacent_find problem

*Subject*: [Frama-c-discuss] adjacent_find problem*From*: jens.gerlach at first.fraunhofer.de (Jens Gerlach)*Date*: Sat, 16 Jan 2010 11:59:43 +0100

Hi, here is a specification and implementation of the function adjacent_find that returns the smallest index i of of an array a where a[i] == a[i+1] holds. If no such index exists it returns the length of the array. (It's a simplified version of the C++ standard algorithms http://www.sgi.com/tech/stl/adjacent_find.html) /*@ predicate have_equal_neighbours{Label}(int* a, int n) = \exists int i; 0 <= i < n-1 && a[i] == a[i+1]; */ /*@ requires 0 <= n; requires \valid_range(a, 0, n); assigns \nothing; behavior some: assumes have_equal_neighbours(a, n); ensures 0 <= \result < n-1; ensures a[\result] == a[\result+1]; ensures !have_equal_neighbours(a, \result); behavior none: assumes !have_equal_neighbours(a, n); ensures \result == n; complete behaviors some, none; disjoint behaviors some, none; */ int adjacent_find(int* a, int n) { if (0 == n) return n; /*@ loop invariant 0 <= i < n; loop variant n-i; loop invariant !have_equal_neighbours(a, i+1); //loop invariant !have_equal_neighbours(a, i); //loop invariant 0 < i ==> a[i-1] != a[i]; */ for (int i = 0; i < n-1; i++) if (a[i] == a[i+1]) return i; return n; } When I compile it with frama-c -jessie -jessie-no-regions -jessie-why-opt="-exp goal" adjacent_find.c then I obtain the error message adjacent_find.c:34:[kernel] user error: Error during annotations analysis: invalid implicit conversion from integer to int which refers to the third loop invariant. I am not sure whether it's a bug or a feature, but when I replace this loop invariant by the following (in my opinion equivalent) loop invariants then most atp can proof all verification conditions. loop invariant !have_equal_neighbours(a, i); loop invariant 0 < i ==> a[i-1] != a[i]; Regards Jens -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100116/476d3b2a/attachment.htm

**Follow-Ups**:**[Frama-c-discuss] adjacent_find problem***From:*guillaume.melquiond at inria.fr (Guillaume Melquiond)

- Prev by Date:
**[Frama-c-discuss] Licensing clarification re: Q Modified License** - Next by Date:
**[Frama-c-discuss] adjacent_find problem** - Previous by thread:
**[Frama-c-discuss] Licensing clarification re: Q Modified License** - Next by thread:
**[Frama-c-discuss] adjacent_find problem** - Index(es):