[WP] Fails to verify loop invariant of type-independent pattern-fill function only when type of array elements is floating point
Steps to reproduce the issue
With Alt-Ergo 2.4.1,
frama-c -wp -wp-rte main.c
/ frama-c-gui -wp -wp-rte main.c
using main.c
(note that all of the function bodies are exactly the same, also the annotations for all of the functions):
#include <stdbool.h>
#include <stddef.h>
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillInt(
int *const buf,
const size_t bufLen,
const int pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillUInt(
unsigned int *const buf,
const size_t bufLen,
const unsigned int pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillBool(
bool *const buf,
const size_t bufLen,
const bool pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillFloat(
float *const buf,
const size_t bufLen,
const float pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillDouble(
double *const buf,
const size_t bufLen,
const double pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillIntPtr(
int* *const buf,
const size_t bufLen,
const int *const pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillFloatPtr(
float* *const buf,
const size_t bufLen,
const float *const pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
Expected behaviour
Since all of the function bodies and all of the function annotations are exactly identical and assigning a value is equivalent for any type (unless?), I would expect either all functions to be verified, or all functions to fail to verify in the same way.
Actual behaviour
The loop invariant \forall size_t j; (0 <= j < i) ==> buf[j] == pattern[j % 4];
fails only for PatternFillFloat
and PatternFillDouble
functions.
$ frama-c -wp -wp-rte main.c
[kernel] Parsing main.c (with preprocessing)
[rte] annotating function PatternFillBool
[rte] annotating function PatternFillDouble
[rte] annotating function PatternFillFloat
[rte] annotating function PatternFillFloatPtr
[rte] annotating function PatternFillInt
[rte] annotating function PatternFillIntPtr
[rte] annotating function PatternFillUInt
[wp] 92 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_PatternFillFloat_loop_invariant_2_preserved : Timeout (Qed:8ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_PatternFillDouble_loop_invariant_2_preserved : Timeout (Qed:10ms) (10s)
[wp] Proved goals: 90 / 92
Qed: 35 (0.33ms-6ms-41ms)
Alt-Ergo 2.4.1: 55 (8ms-37ms-131ms) (1523) (interrupted: 2)
[wp:pedantic-assigns] main.c:133: Warning:
No \from specification for assigned pointer '*(buf + (0 .. bufLen - 1))'.
Callers assumptions might be imprecise.
[wp:pedantic-assigns] main.c:158: Warning:
No \from specification for assigned pointer '*(buf + (0 .. bufLen - 1))'.
Callers assumptions might be imprecise.
Contextual information
- Frama-C installation mode: opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP, RTE
- OS name: Manjaro Linux
- OS version: Qonos 21.2.5
Additional information (optional)
N/A