|
/* Generated by Frama-C */
|
|
typedef int value_type;
|
|
typedef unsigned int size_type;
|
|
struct size_type_pair {
|
|
size_type first ;
|
|
size_type second ;
|
|
};
|
|
typedef struct size_type_pair size_type_pair;
|
|
/*@ ensures \result.first == \old(first);
|
|
ensures \result.second == \old(second);
|
|
assigns \nothing;
|
|
*/
|
|
__inline static size_type_pair make_pair(size_type first, size_type second)
|
|
{
|
|
size_type_pair pair;
|
|
pair.first = first;
|
|
pair.second = second;
|
|
return pair;
|
|
}
|
|
|
|
/*@
|
|
predicate Sorted{L}(value_type *a, integer m, integer n) =
|
|
\forall integer i, integer j; m <= i < j < n ==> *(a + i) <= *(a + j);
|
|
*/
|
|
/*@ predicate Sorted{L}(value_type *a, integer n) = Sorted(a, 0, n);
|
|
*/
|
|
/*@
|
|
predicate ConstantRange{L}
|
|
(value_type *a, integer first, integer last, value_type v) =
|
|
\at(\forall integer i; first <= i < last ==> *(a + i) == v,L);
|
|
*/
|
|
/*@
|
|
predicate ConstantRange{L}(value_type *a, integer first, integer last) =
|
|
\at(ConstantRange(a, first, last, *(a + first)),L);
|
|
*/
|
|
/*@
|
|
predicate ConstantRange{L}(value_type *a, integer n, value_type v) =
|
|
\at(ConstantRange(a, 0, n, v),L);
|
|
*/
|
|
/*@
|
|
predicate StrictUpperBound{L}
|
|
(value_type *a, integer m, integer n, value_type v) =
|
|
\forall integer i; m <= i < n ==> *(a + i) < v;
|
|
*/
|
|
/*@
|
|
predicate StrictUpperBound{L}(value_type *a, integer n, value_type v) =
|
|
StrictUpperBound(a, 0, n, v);
|
|
*/
|
|
/*@
|
|
predicate StrictLowerBound{L}
|
|
(value_type *a, integer m, integer n, value_type v) =
|
|
\forall integer i; m <= i < n ==> v < *(a + i);
|
|
*/
|
|
/*@
|
|
predicate StrictLowerBound{L}(value_type *a, integer n, value_type v) =
|
|
StrictLowerBound(a, 0, n, v);
|
|
|
|
*/
|
|
size_type_pair equal_range2(value_type const *a, size_type n, value_type val);
|
|
|
|
/*@
|
|
predicate LowerBound{L}(value_type *a, integer m, integer n, value_type v) =
|
|
\forall integer i; m <= i < n ==> v <= *(a + i);
|
|
*/
|
|
/*@
|
|
predicate LowerBound{L}(value_type *a, integer n, value_type v) =
|
|
LowerBound(a, 0, n, v);
|
|
|
|
*/
|
|
/*@ requires valid: \valid_read(a + (0 .. n - 1));
|
|
requires sorted: Sorted(a, n);
|
|
ensures result: 0 <= \result <= \old(n);
|
|
ensures left: StrictUpperBound(\old(a), 0, \result, \old(val));
|
|
ensures right: LowerBound(\old(a), \result, \old(n), \old(val));
|
|
assigns \nothing;
|
|
*/
|
|
size_type lower_bound(value_type const *a, size_type n, value_type val);
|
|
|
|
/*@
|
|
predicate UpperBound{L}(value_type *a, integer m, integer n, value_type v) =
|
|
\forall integer i; m <= i < n ==> *(a + i) <= v;
|
|
*/
|
|
/*@
|
|
predicate UpperBound{L}(value_type *a, integer n, value_type v) =
|
|
UpperBound(a, 0, n, v);
|
|
|
|
*/
|
|
/*@ requires valid: \valid_read(a + (0 .. n - 1));
|
|
requires sorted: Sorted(a, n);
|
|
ensures result: 0 <= \result <= \old(n);
|
|
ensures left: UpperBound(\old(a), 0, \result, \old(val));
|
|
ensures right: StrictLowerBound(\old(a), \result, \old(n), \old(val));
|
|
assigns \nothing;
|
|
*/
|
|
size_type upper_bound(value_type const *a, size_type n, value_type val);
|
|
|
|
/*@
|
|
lemma SortedShift{L}:
|
|
\forall value_type *a, integer l, integer r;
|
|
0 <= l <= r ==> Sorted(a, l, r) ==> Sorted(a + l, r - l);
|
|
*/
|
|
/*@
|
|
lemma LowerBoundShift{L}:
|
|
\forall value_type *a, int val, integer b, integer c, integer d;
|
|
LowerBound(a + b, c, d, val) ==> LowerBound(a, c + b, d + b, val);
|
|
*/
|
|
/*@
|
|
lemma StrictLowerBoundShift{L}:
|
|
\forall value_type *a, int val, integer b, integer c, integer d;
|
|
StrictLowerBound(a + b, c, d, val) ==>
|
|
StrictLowerBound(a, c + b, d + b, val);
|
|
*/
|
|
/*@
|
|
lemma UpperBoundShift{L}:
|
|
\forall value_type *a, int val, integer b, integer c;
|
|
UpperBound(a + b, 0, c - b, val) ==> UpperBound(a, b, c, val);
|
|
*/
|
|
/*@
|
|
lemma StrictUpperBoundShift{L}:
|
|
\forall value_type *a, int val, integer b, integer c;
|
|
StrictUpperBound(a + b, 0, c - b, val) ==> StrictUpperBound(a, b, c, val);
|
|
|
|
*/
|
|
/*@ requires valid: \valid_read(a + (0 .. n - 1));
|
|
requires sorted: Sorted(a, n);
|
|
ensures result: 0 <= \result.first <= \result.second <= \old(n);
|
|
ensures left: StrictUpperBound(\old(a), 0, \result.first, \old(val));
|
|
ensures
|
|
middle: ConstantRange(\old(a), \result.first, \result.second, \old(val));
|
|
ensures
|
|
right: StrictLowerBound(\old(a), \result.second, \old(n), \old(val));
|
|
assigns \nothing;
|
|
*/
|
|
size_type_pair equal_range2(value_type const *a, size_type n, value_type val)
|
|
{
|
|
size_type_pair __retres;
|
|
size_type first = 0u;
|
|
size_type middle = 0u;
|
|
size_type last = n;
|
|
/*@ loop invariant bounds: 0 <= first <= last <= n;
|
|
loop invariant left: StrictUpperBound(a, 0, first, val);
|
|
loop invariant right: StrictLowerBound(a, last, n, val);
|
|
loop assigns first, last, middle;
|
|
loop variant last - first;
|
|
*/
|
|
while (last > first) {
|
|
middle = first + (last - first) / 2u;
|
|
if (*(a + middle) < val) first = middle + 1u;
|
|
else
|
|
if (val < *(a + middle)) last = middle; else break;
|
|
}
|
|
if (first < last) {
|
|
size_type tmp;
|
|
size_type tmp_0;
|
|
size_type_pair tmp_1;
|
|
/*@ assert sorted: Sorted(a, first, middle); */ ;
|
|
tmp = lower_bound(a + first,middle - first,val);
|
|
size_type left = first + tmp;
|
|
/*@ assert constant: LowerBound(a, left, middle, val); */ ;
|
|
/*@ assert strict: StrictUpperBound(a, first, left, val); */ ;
|
|
middle ++;
|
|
/*@ assert sorted: Sorted(a, middle, last); */ ;
|
|
tmp_0 = upper_bound(a + middle,last - middle,val);
|
|
size_type right = middle + tmp_0;
|
|
/*@ assert constant: UpperBound(a, middle, right, val); */ ;
|
|
/*@ assert strict: StrictLowerBound(a, right, last, val); */ ;
|
|
tmp_1 = make_pair(left,right);
|
|
__retres = tmp_1;
|
|
goto return_label;
|
|
}
|
|
else {
|
|
size_type_pair tmp_2;
|
|
tmp_2 = make_pair(first,first);
|
|
__retres = tmp_2;
|
|
goto return_label;
|
|
}
|
|
return_label: return __retres;
|
|
}
|
|
|
|
|