--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on October 2011 ---
Hello, 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? > There is the start of something to do this. Since you are interested in this question, I do not need to tell you that it is difficult to work only at the source level for worst case execution time verification. What Frama-C currently provides (as an unsupported proof of concept) is complementary of binary execution and measurements. It would be possible to do more at the source level, but let me first tell you about what we have. Please read: http://blog.frama-c.com/index.php?post/2011/10/10/Execution-path-dependencies A blog post that I wrote in a rush because I will refer to the information there more conveniently in the future it is stored there. Using -experimental-path-deps -deps, you can obtain a list of memory locations that influence the execution path of your function. Let us assume that the execution time depends only on the source code execution path (warning: this assumption is wrong for many architectures, not so much because compilation may create different paths where there is only one at source level ?this is possible but probably rare? but because it doesn't account for the various levels of data caches). Then, you only need to test exhaustively for the values that these locations can take. You cannot test the locations independently, of course: you have to test them as a large tuple of values, and the number of combinations can grow correspondingly large. This is probably not going to be satisfactory as such, but I hope it gives an idea of what Frama-C can offer. Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111010/cc336e0f/attachment.htm>