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] Source loop identification

  • Subject: [Frama-c-discuss] Source loop identification
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Mon, 24 Jun 2013 13:22:52 +0200
  • In-reply-to: <CAOT7Vm0=VJ4soZirFuHvLnQZ_+1TTCU2gG-11wJzuxyCht=jYQ@mail.gmail.com>
  • References: <CAOT7Vm0=VJ4soZirFuHvLnQZ_+1TTCU2gG-11wJzuxyCht=jYQ@mail.gmail.com>
Hello,

You should also look at the function Stmt_graphs.get_stmt_stmts, which
will return all the statements that constitue a given block of code.
By calling it on the block corresponding to a 'for' or 'while' loop,
it will be very easy to derive the location information you seek.

HTH,

On Tue, Jun 11, 2013 at 9:46 AM, Daniel Garcia <dhekir at gmail.com> wrote:
> Hi,
>
> Some time ago someone told me about loop instrumentation using a source code
> analysis tool, and I think it was Frama-C he mentioned, but I don't remember
> it clearly. What I'd like to do is to identify, on the source code, which
> lines correspond to a loop body and which are outside the loop (only
> considering structured loops here). I've been looking for something like
> this on the Frama-C GUI and manual, but couldn't find it. Is there such a
> thing on Frama-C, or am I mistaken about this feature?
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss



-- 
Boris