[WP] Correction of loop-based copy function not prooved if using 32-bit integer sizes
Steps to reproduce the issue
Save the following code into a file called "copy.c"
#include <stdint.h>
typedef uint32_t size_t;
typedef enum {
OK, NOK
} error_t;
typedef struct {
size_t size;
unsigned int *values;
} buffer_t ;
/*@
requires
\valid(destination) && \valid(source) &&
\valid(destination->values+(0..destination->size-1)) &&
\valid(source->values+(0..source->size-1)) &&
\separated(source->values+(0..source->size-1), destination->values+(0..destination->size-1));
assigns
*(destination->values+(0..source->size-1));
ensures
(destination->size >= source->size) ==> ((\forall integer i; 0 <= i < source->size
==> (destination->values[i] == source->values[i])) && \result == OK);
ensures
(destination->size < source->size) ==> (\forall integer i; 0 <= i < destination->size
==> (destination->values[i] == \old(destination->values[i])) && \result == NOK);
*/
error_t copy(buffer_t* source, buffer_t* destination) {
error_t ret = NOK;
if (destination->size >= source->size) {
/*@
loop invariant 0 <= i <= source->size <= destination->size;
loop invariant \forall integer j ; 0 <= j < i ==> destination->values[j] == source->values[j];
loop assigns i, destination->values[0..source->size-1];
loop variant source->size-i;
*/
for(size_t i=0; i<source->size; i++) {
destination->values[i] = source->values[i];
}
ret = OK;
}
return ret;
}
Then analyse this code using the WP plugin with the command
frama-c copy.c -wp -wp-rte -wp-prover alt-ergo,z3,cvc4 -wp-cache none
Expected behaviour
The annotations should be proved. Indeed, if the type of our local "size_t" type is changed to uint8_t, uint16_t or uint64_t, then all assertions are proved.
Actual behaviour
Only 12 out of the 20 assertions are proved. Notably, none of the loop annotations can be proved.
Contextual information
- Frama-C installation mode: docker
- Frama-C version: 23.1
- Plug-in used: Eva, WP
- OS name: Ubuntu
- OS version: 20.04