--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on October 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Worst case path computation



Hi,

is there already a plugin that is able to perform worst case path
computation, that is able to compute the C instructions that a
function can "at most" execute?

If not, how hard would that be to develop such a plugin in the actual
state of frama-C? Is there possibility to get support for that?

The use case would be to statically verify the bounded execution time
of RT embedded systems.

Thanks,
Sylvain