Frama-C API - Make
This functor provides the partitioning algorithm constructing a WTO.
Parameters
module Node : sig ... end
Signature
Partial order of preference for the choice of the head of a loop. pref current_head new_candidate
must return < 0 if new_candidate
is preferred to current_head
. Use "(fun _ _ -> 0)" for no specific preference.
Implements Bourdoncle "Efficient chaotic iteration strategies with widenings" algorithm to compute a WTO.