Frama-C:
Plug-ins:
Libraries:

Frama-C API - LoopAnalysis

Loop Analysis plugin.

module Loop_analysis : sig ... end

Loop exports functions related to the estimation of loop iteration bounds.