GitLab

Steps to reproduce the issue

With Alt-Ergo 2.4.1 installed:
frama-c -wp -wp-rte poc.c / frama-c-gui -wp -wp-rte poc.c

using poc.c :

/*@
  requires \valid_read(arr + (0 .. 3));
  assigns \nothing;
*/
int foo(const int arr[const static 4]) {
	const unsigned int h = 7 & 0b11;
	//@ assert 0 <= h < 4;
	const int hvalue = arr[h];

	const unsigned int i = 7 % 4;
	//@ assert 0 <= i < 4;
	const int ivalue = arr[i];

	/*@
	  loop invariant 0 <= s <= 8;
	  loop assigns s;
	  loop variant 8 - s;
	*/
	for (unsigned int s = 0; s < 8; s += 1) {
		const unsigned int j = s & 0b11;
		//@ assert 0 <= j < 4;
		const int jvalue = arr[j];

		const unsigned int k = s % 4;
		//@ assert 0 <= k < 4;
		const int kvalue = arr[k];
	}

	return 0;
}

/*@
  assigns \nothing;
*/
int main(void) {
	const int arr[4] = {0, 1, 2, 3};

	const unsigned int h = 7 & 0b11;
	//@ assert 0 <= h < 4;
	const int hvalue = arr[h];

	const unsigned int i = 7 % 4;
	//@ assert 0 <= i < 4;
	const int ivalue = arr[i];

	/*@
	  loop invariant 0 <= s <= 8;
	  loop assigns s;
	  loop variant 8 - s;
	*/
	for (unsigned int s = 0; s < 8; s += 1) {
		const unsigned int j = s & 0b11;
		//@ assert 0 <= j < 4;
		const int jvalue = arr[j];

		const unsigned int k = s % 4;
		//@ assert 0 <= k < 4;
		const int kvalue = arr[k];
	}

	foo(arr);

	return 0;
}

Expected behaviour

All goals proved.

Actual behaviour

$ frama-c -wp -wp-rte poc.c
[kernel] Parsing poc.c (with preprocessing)
[rte] annotating function foo
[rte] annotating function main
[wp] 34 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_foo_assert_rte_mem_access_3 : Timeout (Qed:9ms) (10s)
[wp] Proved goals:   33 / 34
  Qed:              23  (2ms-5ms-14ms)
  Alt-Ergo 2.4.1:   10  (7ms-17ms-30ms) (556) (interrupted: 1)

33/34 goals proved.
The verification of /*@ assert rte: mem_access: \valid_read(arr + j); */ for code const int jvalue = arr[j]; in function foo is not successful.
From a naive perspective, the arr[j] accesses in main and foo are equivalent, so the assert in foo should be verifiable if the assert in main is.
(I am aware that a different assert is generated in main: /*@ assert rte: index_bound: j < 4; */)
Also, the //@ assert 0 <= j < 4; immediately before the access can be verified, both in main and foo, so it seems the rte assert should be able to be verified also.

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.4

Additional information (optional)

The poc.c is a simplified proof of concept, but I did hit this situation when working on a real program.

To be explicit about the provers involved:

$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
1 prover(s) added
Save config to /home/user/.why3.conf

I was uncertain whether to submit this here or at the alt-ergo issues.
Apologies if this is the wrong place. Let me know if I should post there instead.