We do not support closures that do a recursive call.

[Lysxia]

extern crate creusot_contracts;
use creusot_contracts::*;

#[variant(i)]
pub fn count_paths(i: usize) {
    (0..i).map(|j| count_paths(j));
}

thread 'rustc' panicked at creusot/src/backend/clone_map.rs:383:17:
assertion `left == right` failed
  left: 2
 right: 1

The mentioned line:

creusot/creusot/src/backend/clone_map.rs

Lines 381 to 386 in 739b2d0

	for scc in petgraph::algo::tarjan_scc(&graph).into_iter() {
	if scc.iter().any(|node| node == &self_node) {
	assert_eq!(scc.len(), 1);
	bodies.remove(&scc[0]);
	continue;
	}

[jhjourdan]

Ok, the error message is not nice. But the problem here is that this is essentially mutually recursive functions (closure / function), which we do not support.

[arnaudgolfouse]

Ok, the error message is not nice. But the problem here is that this is essentially mutually recursive functions (closure / function), which we do not support.

But we do (in programs)? E.g.

pub fn count_paths(i: usize) {
    (0..i).map(|j| closure(j));
}

fn closure(j: usize) { count_paths(j) }

Works. The error is caused by the closure calling the enclosing function directly.

[jhjourdan]

Right. We do not support it in the case the mutual recursion is between a closure and the function which contains it. That's clearly a limitation we need to work on.

One issue is that Coma would not support (yet?) spec inference in this case.