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] Postdominators


  • Subject: [Frama-c-discuss] Postdominators
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Wed, 25 Apr 2012 12:08:20 +0200
  • In-reply-to: <CABbVA-Bfsn48SW5=2xdxTxd3iv4mfiNL-ZvPki91sdP697r-sg@mail.gmail.com>
  • References: <1335251651.2148.204.camel@iti27.informatik.htw-dresden.de> <CABbVA-Bfsn48SW5=2xdxTxd3iv4mfiNL-ZvPki91sdP697r-sg@mail.gmail.com>

Hello,

> 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

ok, agreed...

> 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.

Recently means it's not contained in Nitrogen? Because the
implementation in Nitrogen uses the Dataflow module.

Does the new implementation supersede the Dominators module in cil/ext?
And does it compute immediate (post)dominators (because this is part of
the algorithm described above)? If it compiles with Nitrogen, I'd like
to get it.
-- 
Best regards,
Boris