Skip to content
GitLab
Closed
Issue created by Costava@Costava

[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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information