Frama-C API - Partitioning_index

A partitioning index is a collection of states optimized to determine if a new state is included in one of the states it contains — in a more efficient way than to test the inclusion with all stored states. Such an index is used to keep track of all the states already propagated through a control point, and to rule out new incoming states included in previous ones.

Partitioning index relies on an heuristics on the cvalue domain, and is very inefficient without it.