[WP] Preservation of "is_finite" property
Steps to reproduce the issue
Run the following example with the command
frama-c -wp-model typed+int+float -wp-rte -wp-timeout 5 -wp test.c
#include <__fc_builtin.h>
/*@
@requires \valid(vec + (0 .. (size - 1)));
@requires \forall unsigned i; i < size ==> \is_finite(vec[i]);
@requires \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@terminates \true;
@ensures \forall unsigned i; i < size ==> \is_finite(vec[i]);
@ensures \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@ensures \forall unsigned i; i < size ==> vec[i] == \old(vec)[i];
@assigns vec[0 .. (size - 1)];
@*/
extern void vec_nop(double * const vec, unsigned const size);
void vec_nop(double * const vec, unsigned const size) {
/*@
@loop invariant i <= size;
@loop invariant \forall unsigned x; x < i ==> \is_finite(vec[x]);
@loop invariant \forall unsigned x; x < i ==> !\is_NaN(vec[x]);
@loop invariant \forall unsigned x; x < i ==> vec[x] == \at(vec, LoopEntry)[x];
@loop assigns i;
@loop variant (size - i);
@*/
for (unsigned i = 0; i < size; ++i) {
}
}
/*@
@requires \valid(vec + (0 .. (size - 1)));
@requires \forall unsigned i; i < size ==> \is_finite(vec[i]);
@requires \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@terminates \true;
@ensures \forall unsigned i; i < size ==> \is_finite(vec[i]);
@ensures \forall unsigned i; i < size ==> !\is_NaN(vec[i]);
@ensures \forall unsigned i; i < size ==> vec[i] == \old(vec)[i];
@assigns vec[0 .. (size - 1)];
@*/
extern void vec_ident(double * const vec, unsigned const size);
void vec_ident(double * const vec, unsigned const size) {
/*@
@loop invariant i <= size;
@loop invariant \forall unsigned x; x < i ==> \is_finite(vec[x]);
@loop invariant \forall unsigned x; x < i ==> !\is_NaN(vec[x]);
@loop invariant \forall unsigned x; x < i ==> vec[x] == \at(vec, LoopEntry)[x];
@loop assigns i;
@loop assigns vec[0 .. (size - 1)];
@loop variant (size - i);
@*/
for (unsigned i = 0; i < size; ++i) {
vec[i] = vec[i];
}
}
Expected behaviour
All properties should be validated.
Actual behaviour
In the given example, all properties of the vec_nop
are correctly verified with WP. However, in the vec_ident
function below where the only difference with the vec_nop
function is the addition of the statement vec[i] = vec[i];
in the loop, the loop invariant \is_finite(vec[x])
is not verified anymore.
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 27.1 (Cobalt)
- Plug-in used: WP
- OS name: Linux
Additional information (optional)
When using model typed+int+real
all properties are validated...