Project

General

Profile

Download (1.12 KB)

Bug #10019 » add_one.c

Denis Efremov, 06/01/2020 09:14 PM

 
#include <stddef.h>
#include <string.h>
#include <assert.h>

/*@
requires \valid(an_array + (0 .. size-1));
requires \forall size_t x; 0 <= x < size ==> -2147483647 <= an_array[x] < 2147483646;
assigns an_array[0 .. size - 1];
ensures \forall size_t x; 0 <= x < size ==> an_array[x] == \old(an_array[x]) + 1;
*/
void add_one(int *an_array, size_t size) {
/*@
loop invariant 0 <= i <= size;
loop invariant \forall size_t j; i <= j < size ==> an_array[j] < 2147483646;
loop invariant \forall size_t j; 0 <= j < i ==> an_array[j] == 1 + \at(an_array[j], LoopCurrent) ;
loop assigns i, an_array[0 .. size - 1];
loop variant size - i;
*/
for (size_t i = 0; i < size; i++) {
an_array[i] = an_array[i] + 1;
}
}


/*
If you name this function 'main' it is not able to prove the
'requires' clause, because this data is provided by the user.
*/
/*@
requires 0 <= v < 5;
*/
void driver(int v) {
int an_array[5] = {0, 1, 2, 3, 4};
int *alias = an_array + v;
int dummy_array[5] = {1, 2, 3, 4, 5};
add_one(an_array, 5);
//@ assert \forall size_t x; 0 <= x < 5 ==> an_array[x] == dummy_array[x];
//@ assert 1 <= *alias <= 5;
}
(2-2/2)