Struct charon_lib::transform::ullbc_to_llbc::LoopExitCandidateInfo

struct LoopExitCandidateInfo {
    pub occurrences: Vec<usize>,
}

Fields

occurrences: Vec<usize>

The occurrences going to this exit. For every occurrence, we register the distance between the loop entry and the node from which the edge going to the exit starts. If later we have to choose between candidates with the same number of occurrences, we choose the one with the smallest distances.

Note that it may happen that we have several exit candidates referenced more than once for one loop. This comes from the fact that whenever we reach a node from which the loop entry is not reachable (without using a backward edge leading to an outer loop entry), we register this node as well as all its children as exit candidates. Consider the following example:

while i < max {
    if cond {
        break;
    }
    s += i;
    i += 1
}
// All the below nodes are exit candidates (each of them is referenced twice)
s += 1;
return s;

Trait Implementations

impl Clone for LoopExitCandidateInfo

fn clone(&self) -> LoopExitCandidateInfo

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LoopExitCandidateInfo

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.