Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Worst case path computation

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>