--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Postdominators



Hi,

On Tue, Apr 24, 2012 at 9:14 AM, Boris Hollas
<hollas at informatik.htw-dresden.de> wrote:
> Also, there's an undocumented Postdominators plugin in
> src/postdominators/. Is this meant to be used by plugin developers?

Well, undocumented is quite an exaggeration in this case. It's hard to
write something really different from what is printed by frama-c
-postdominators-help: the sole goal of the plugin is to compute
postdominators! Also, a programmatic and commented interface is given
in the module Db.Postdominators. A second API, PostdominatorsValue,
use Value to take into account statements that are proved unreachable.

Also, notice that we recently replaced our basic, dataflow-based
implementation of dominators by an optimized one (see
www.cs.rice.edu/~keith/Embed/dom.pdf). The performances of the
original one were really too bad on big functions.

Hope this helps,

-- 
Boris